<abstract xmlns="http://www.w3.org/1999/xhtml">This article introduces propositional logic as a formal system ([<xref ref-type="bibr" rid="j_forma-2016-0024_ref_014_w2aab2b8b9b1b7b1ab1ac14Aa">14</xref>], [<xref ref-type="bibr" rid="j_forma-2016-0024_ref_010_w2aab2b8b9b1b7b1ab1ac10Aa">10</xref>], [<xref ref-type="bibr" rid="j_forma-2016-0024_ref_011_w2aab2b8b9b1b7b1ab1ac11Aa">11</xref>]). The formulae of the language are as follows <italic>φ</italic> ::= ⊥ | <italic>p</italic> | <italic>φ</italic> → <italic>φ</italic>. Other connectives are introduced as abbrevations. The notions of model and satisfaction in model are defined. The axioms are all the formulae of the following schemes
<list list-type="bullet"><list-item><italic>α</italic> ⇒ (<italic>β</italic> ⇒ <italic>α</italic>),</list-item><list-item>(<italic>α</italic> ⇒ (<italic>β</italic> ⇒ <italic>γ</italic>)) ⇒ ((<italic>α</italic> ⇒ <italic>β</italic>) ⇒ (<italic>α</italic> ⇒ <italic>γ</italic>)),</list-item><list-item>(¬<italic>β</italic> ⇒ ¬<italic>α</italic>) ⇒ ((¬<italic>β</italic> ⇒ <italic>α</italic>) ⇒ <italic>β</italic>).</list-item></list>
Modus ponens is the only derivation rule. The soundness theorem and the strong completeness theorem are proved. The proof of the completeness theorem is carried out by a counter-model existence method. In order to prove the completeness theorem, Lindenbaum’s Lemma is proved. Some most widely used tautologies are presented.</abstract>

This article introduces propositional logic as a formal system ([14], [10], [11]). The formulae of the language are as follows φ ::= ⊥ | p | φ → φ. Other connectives are introduced as abbrevations. The notions of model and satisfaction in model are defined. The axioms are all the formulae of the following schemes
α ⇒ (β ⇒ α),(α ⇒ (β ⇒ γ)) ⇒ ((α ⇒ β) ⇒ (α ⇒ γ)),(¬β ⇒ ¬α) ⇒ ((¬β ⇒ α) ⇒ β).
Modus ponens is the only derivation rule. The soundness theorem and the strong completeness theorem are proved. The proof of the completeness theorem is carried out by a counter-model existence method. In order to prove the completeness theorem, Lindenbaum’s Lemma is proved. Some most widely used tautologies are presented.

The Axiomatization of Propositional Logic

Faculty of Economics and Informatics, University of Białystok, Kalvariju 135, LT-08221 Vilnius,

Formalized Mathematics

This work is licensed under version 3.0 of the Creative Commons Attribution–ShareAlike License.

{"article-title":"The Axiomatization of Propositional Logic"}

This article introduces propositional logic as a formal system ([14], [10], [11]). The formulae of the language are as follows φ ::= ⊥ | p | φ → φ. Other...

The Axiomatization of Propositional Logic

Publié en ligne: 23 févr. 2017

Pages: 281 - 290

Reçu: 18 oct. 2016

DOI: https://doi.org/10.1515/forma-2016-0024

Mots clés
completeness, formal system, Lindenbaum’s lemma

© 2016 Mariusz Giero, published by De Gruyter Open

This work is licensed under version 3.0 of the Creative Commons Attribution–ShareAlike License.

The Axiomatization of Propositional Logic

Publié en ligne: 23 févr. 2017

Pages: 281 - 290

Reçu: 18 oct. 2016

DOI: https://doi.org/10.1515/forma-2016-0024

Mots cléscompleteness, formal system, Lindenbaum’s lemma

© 2016 Mariusz Giero, published by De Gruyter Open

This work is licensed under version 3.0 of the Creative Commons Attribution–ShareAlike License.

Mots clés
completeness, formal system, Lindenbaum’s lemma