<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

Data publikacji: 23 lut 2017

Zakres stron: 281 - 290

Otrzymano: 18 paź 2016

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

Słowa kluczowe
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

Data publikacji: 23 lut 2017

Zakres stron: 281 - 290

Otrzymano: 18 paź 2016

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

Słowa kluczowecompleteness, 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.

Słowa kluczowe
completeness, formal system, Lindenbaum’s lemma