axiom system for propositional logic (original) (raw)
The language of (classical) propositional logic
PLc consists of a set of propositional letters or variables
, the symbol ⟂ (for falsity), together with two symbols for logical connectives ¬ and →. The well-formed formulas (wff’s) of PLc are inductively defined as follows:
- •
each propositional letter is a wff - •
⟂ is a wff - •
if A and B are wff’s, then A→B is a wff
We also use parentheses ( and ) to remove ambiguities. The other familiar logical connectives may be defined in terms of →: ¬A is A→⟂, A∨B is the abbreviation for ¬A→B, A∧B is the abbreviation for ¬(A→¬B), and A↔B is the abbreviation for (A→B)∧(B→A).
A deduction
is a finite sequence
of wff’s A1,…,An such that each Ai is either an instance of one of the axiom schemas above, or as a result of applying rule MP to earlier wff’s in the sequence. In other words, there are j,k<i such that Ak is the wff Aj→Ai. The last wff An in the deduction is called a theorem
of PLc. When A is a theorem of PLc, we write
For example, ⊢A→A, whose deduction is
- (A→((B→A)→A))→((A→(B→A))→(A→A)) by Axiom II,
- A→((B→A)→A) by Axiom I,
- (A→(B→A))→(A→A) by modus ponens on 2 to 1,
- A→(B→A) by Axiom I,
- A→A by modus ponens on 4 to 3.
More generally, given a set Σ of wff’s, we write
if there is a finite sequence of wff’s such that each wff is either an axiom, a member of Σ, or as a result of applying MP to earlier wff’s in the sequence. An important (meta-)theorem called the deduction theorem, states: if Σ,A⊢B, then Σ⊢A→B. The deduction theorem holds for PLc (proof here (http://planetmath.org/deductiontheoremholdsforclassicalpropositionallogic))
Remark. The axiom system above was first introduced by Polish logician Jan Łukasiewicz. Two axiom systems are said to be deductively equivalent if every theorem in one system is also a theorem in the other system. There are many axiom systems for PLc that are deductively equivalent to Łukasiewicz’s system. One such system consists of the first two axiom schemas above, but the third axiom schema is ¬¬A→A, with MP its sole inference rule.