# axiom system for propositional logic

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

• each propositional letter is a wff

• $\perp$ 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$: $\neg A$ is $A\to\perp$, $A\lor B$ is the abbreviation for $\neg A\to B$, $A\land B$ is the abbreviation for $\neg(A\to\neg B)$, and $A\leftrightarrow B$ is the abbreviation for $(A\to B)\land(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. 1.

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

2. 2.

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

3. 3.

$(\neg A\to\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},\ldots,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 $j,k 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

 $\vdash_{c}A\qquad\qquad\mbox{or simply}\qquad\qquad\vdash A.$

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

1. 1.

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

2. 2.

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

3. 3.

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

4. 4.

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

5. 5.

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

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

 $\Sigma\vdash A$

if there is a finite sequence of wff’s such that each wff is either an axiom, a member of $\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 $\Sigma,A\vdash B$, then $\Sigma\vdash 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 $\neg\neg A\to A$, with MP its sole inference rule.

Title axiom system for propositional logic AxiomSystemForPropositionalLogic 2013-03-22 19:31:50 2013-03-22 19:31:50 CWoo (3771) CWoo (3771) 13 CWoo (3771) Definition msc 03B05 axiom system for classical propositional logic DeductionTheoremHoldsForClassicalPropositionalLogic SubstitutionTheoremForPropositionalLogic