TUCS Technical Report No. 169, March 1998
ISBN 952-12-0183-5
ISSN 1239-1891
We prove in HOL that three proof systems for classical first-order predicate logic, the Hilbertian axiomatization, the system of natural deduction, and a variant of sequent calculus, are isomorphic. The isomorphism is in the sense that provability of a conclusion from hypotheses in one of these proof systems is equivalent to provability of this conclusion from the same hypotheses in the others. Proving isomorphism of these three proof systems allows us to guarantee that meta-logical provability properties about one of them would also hold in relation to the others. We prove the deduction, monotonicity, and compactness theorems for Hilbertian axiomatization, and the substitution theorem for the system of natural deduction. Then we show how these properties can be translated between the proof systems. Besides, by proving a theorem which states that provability in flattened sequent calculus implies provability in standard sequent calculus, we show how some meta-logical results about Hilbertian axiomatization and natural deduction can be translated to sequent calculus.
Keywords: Formalised mathematics, theorem-proving in higher-order logic, first-order proof theories, meta-logical reasoning, Hilbertian axiomatization, natural deduction, sequent calculus.
Full paper in PostScript format (742 Kb) and in compressed PostScript format (128 Kb).