axiom system for propositional logic

The language of (classical) propositional logic PL${}_c$ consists of a set of propositional letters or variables, the symbol $⟂$ (for falsity), together with two symbols for logical connectives $\mathrm{\neg }$ and $\to$. The well-formed formulas (wff’s) of PL${}_c$ are inductively defined as follows:

• each propositional letter is a wff

• $⟂$ is a wff

• if $A$ and $B$ are wff’s, then $A\to B$ is a wff

We also use parentheses $($ and $)$ to remove ambiguities. The other familiar logical connectives may be defined in terms of $\to$: $\mathrm{\neg }A$ is $A\to ⟂$, $A\vee B$ is the abbreviation for $\mathrm{\neg }A\to B$, $A\wedge B$ is the abbreviation for $\mathrm{\neg }(A\to \mathrm{\neg }B)$, and $A\leftrightarrow B$ is the abbreviation for $(A\to B)\wedge (B\to A)$.

The axiom system for PL${}_c$ consists of sets of wffs called axiom schemas together with a rule of inference. The axiom schemas are:

1. $A\to (B\to A)$,

2. $(A\to (B\to C))\to ((A\to B)\to (A\to C))$,

3. $(\mathrm{\neg }A\to \mathrm{\neg }B)\to (B\to A)$,

and the rule of inference is modus ponens (MP): from $A\to B$ and $A$, we may infer $B$.

A deduction is a finite sequence of wff’s $A_1,\mathrm{\dots },A_n$ such that each $A_i$ 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 such that $A_k$ is the wff $A_j\to A_i$. The last wff $A_n$ in the deduction is called a theorem of PL${}_c$. When $A$ is a theorem of PL${}_c$, we write

$${⊢}_{c}A\mathit{\hspace{1em}\hspace{1em}\hspace{1em}\hspace{1em}}\text{or simply}\mathit{\hspace{1em}\hspace{1em}\hspace{1em}\hspace{1em}}⊢A.$$

For example, $⊢A\to A$, whose deduction is

1. $(A\to ((B\to A)\to A))\to ((A\to (B\to A))\to (A\to A))$ by Axiom II,

2. $A\to ((B\to A)\to A)$ by Axiom I,

3. $(A\to (B\to A))\to (A\to A)$ by modus ponens on $2$ to $1$,

4. $A\to (B\to A)$ by Axiom I,

5. $A\to A$ by modus ponens on $4$ to $3$.

More generally, given a set $\mathrm{\Sigma }$ of wff’s, we write

$$\mathrm{\Sigma }⊢A$$

if there is a finite sequence of wff’s such that each wff is either an axiom, a member of $\mathrm{\Sigma }$, or as a result of applying MP to earlier wff’s in the sequence. An important (meta-)theorem called the deduction theorem, states: if $\mathrm{\Sigma },A⊢B$, then $\mathrm{\Sigma }⊢A\to B$. The deduction theorem holds for PL${}_c$ (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 PL${}_c$ 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 $\mathrm{\neg }\mathrm{\neg }A\to A$, with MP its sole inference rule.