Axiomatic Approach In Propositional Logic: Axioms, Inference Rules And Theorems

Axiomatic Approach In Propositional Logic

In Axiomatic approach we try to build new, more complex formulas that are true — called theorems, tautologies, or semantically valid formulas, from existing simple formulas that are assumed true by convention — called axioms.

All formulas consist of: atoms, operations, and parentheses, and are built like algebraic expressions. Atom is a lowercase Latin letter and represent an abstract entity that is either true or false, but we don't know it at the moment. Operation is one of: implication → ("if-then", "follows"), conjunction ∧ ("and"), disjunction ∨ ("or"), negation ¬ ("not").

Axioms

Propositional Logic can be axiomatized in many ways. On this website I use axioms listed below that we were taught at Mathematical Logic course in University of Latvia by Karlis Podnieks:

[A1] p→(q→p)
[A2] (p→(q→r))→((p→q)→(p→r))
[A3] p∧q→p
[A4] p∧q→q
[A5] p→(q→p∧q)
[A6] p→p∨q
[A7] q→p∨q
[A8] (p→r)→((q→r)→(p∨q→r))
[A9] (p→q)→((p→¬q)→¬p)
[A10] ¬p→(p→q)
[A11] p∨¬p

Inference Rules

I use 2 rules of inference: substitution and detachment.

Substitution allows to replace all occurences of an atom in a tautology (axiom or theorem), with an arbitrary atom or formula. It can be applied to multiple atoms in a tautology at the same time.

Detachment rule has Latin name "Modus Ponens". It allows, given 2 formulas of form p→q and p, derive formula of form q. If we have "q follows from p" and "it is known that p", then we derive "q is also true".

See axiomatic proofs of theorems in Propositional Logic: