http://hdl.handle.net/11320/21351 2026-10-30T08:30:03Z 2026-10-30T08:30:03Z Braselmann, Patrick Koepke, Peter http://hdl.handle.net/11320/21374 2026-10-29T14:18:01Z 2005-01-01T00:00:00Z

Tytuł: Equivalences of Inconsistency and Henkin Models Autorzy: Braselmann, Patrick; Koepke, Peter Abstrakt: 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 mathematics 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 present article establishes some equivalences of inconsistency. It is proved that a countable union of consistent sets is consistent. Then the concept of a Henkin model is introduced. The contents of this article correspond to Chapter IV, par. 7 and Chapter V, par. 1 of Ebbinghaus, Flum, Thomas.

2005-01-01T00:00:00Z Braselmann, Patrick Koepke, Peter http://hdl.handle.net/11320/21373 2026-10-29T13:30:13Z 2005-01-01T00:00:00Z

Tytuł: Consequences of the Sequent Calculus Autorzy: Braselmann, Patrick; Koepke, Peter Abstrakt: 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 mathematics 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 article 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.

2005-01-01T00:00:00Z Braselmann, Patrick Koepke, Peter http://hdl.handle.net/11320/21372 2026-10-29T12:27:08Z 2005-01-01T00:00:00Z

Tytuł: A Sequent Calculus for First-Order Logic Autorzy: Braselmann, Patrick; Koepke, Peter Abstrakt: 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 mathematics 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 present article introduces a sequent calculus for first-order logic. The correctness of this calculus is shown and some important inferences are derived. The contents of this article correspond to Chapter IV of Ebbinghaus, Flum, Thomas.

2005-01-01T00:00:00Z Braselmann, Patrick Koepke, Peter http://hdl.handle.net/11320/21369 2026-10-29T11:48:02Z 2005-01-01T00:00:00Z

Tytuł: Substitution in First-Order Formulas. Part II. The Construction of First-Order Formulas Autorzy: Braselmann, Patrick; Koepke, Peter Abstrakt: 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 mathematics 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 present article establishes that every substitution can be applied to every formula as in Chapter III par. 8, Definition 8.1, 8.2 of Ebbinghaus, Flum, Thomas. After that, it is observed that substitution doesn’t change the number of quantifiers of a formula. Then further details about substitution and some results about the construction of formulas are proven.

2005-01-01T00:00:00Z