Philosophy Now Forum

Arising_uk wrote:One thing egg3000, could you point me towards or name this type of axiomatic proof as I've never encountered this kind before and would like to read-up. From what I see its using what I presume are tautologies(haven't checked yet) and one of the ND rules plus substitution to make deductive proofs?

Yes, I think that's about it: the axioms are just tautologies, the modus ponens inference rule is really just the ND elimination rule for the conditional connective, and the rest is just uniform substitution. As far as I know, they're just called Axiomatic proofs, or Hilbert-Frege style proofs. Though it is a notoriously difficult method of proof, it's relatively easy to demonstrate the soundness and completeness of these systems, which is the trade off.

Many thanks egg3000.