Consequences of the Sequent Calculus 1
Patrick Braselmann, Peter Koepke · 2005
Summary. This article is part of a series of Mizar articles which constitute a formal proof (of a basic version) of Kurt Godel's famous completeness theorem (K. Godel, Die Vollstandigkeit der Axiome des logischen Funktionenkalkuls, Monatshefte fur Mathematik und Physik 37 (1930), 349-360). The completeness theorem provides the theoretical basis for a uniform formalization of mathemat- ics as in the Mizar project. We formalize first-order logic up to the completeness theorem as in H. D. Ebbinghaus, J. Flum, and W. Thomas, Mathematical Logic, 1984, Springer Verlag New York Inc. The first main result of the present arti- cle is that the derivablility of a sequent doesn't depend on the ordering of the antecedent. The second main result says: if a sequent is derivable, then the formulas in the antecendent only need to occur once.