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".

My work-in-progress software generated the following axiomatic proofs:

If you have an interesting/challenging theorem, please send it to me. I will feed it to my program, maybe it will output some unusual result.