The Axiomatization of Propositional Logic

Mariusz Giero. "The Axiomatization of Propositional Logic." Formalized Mathematics 24.4 (2016): 281-290. <http://eudml.org/doc/288030>.

@article{MariuszGiero2016,
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.},
author = {Mariusz Giero},
journal = {Formalized Mathematics},
keywords = {completeness; formal system; Lindenbaum’s lemma; Lindenbaum's lemma},
language = {eng},
number = {4},
pages = {281-290},
title = {The Axiomatization of Propositional Logic},
url = {http://eudml.org/doc/288030},
volume = {24},
year = {2016},
}

TY - JOUR
AU - Mariusz Giero
TI - The Axiomatization of Propositional Logic
JO - Formalized Mathematics
PY - 2016
VL - 24
IS - 4
SP - 281
EP - 290
AB - 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.
LA - eng
KW - completeness; formal system; Lindenbaum’s lemma; Lindenbaum's lemma
UR - http://eudml.org/doc/288030
ER -