The Axiomatization of Propositional Logic

• Autorzy: Mariusz Giero
• Języki publikacji: EN

Abstrakty

EN

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.

Słowa kluczowe

EN

completeness; formal system; Lindenbaum’s lemma

Kategorie tematyczne

• 03B05: Classical propositional logic
• 03B35: Mechanization of proofs and logical operations

• Wydawca: De Gruyter Open
• Czasopismo: Formalized Mathematics
• Rocznik: 2016
• Tom: 24
• Numer: 4
• Strony: 281-290

Daty

wydano

2016-12-01

otrzymano

2016-10-18

online

2017-02-23

Twórcy

autor

Mariusz Giero

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

Identyfikatory

DOI

10.1515/forma-2016-0024