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

•
each propositional letter is a wff

•
$\u27c2$ 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 \u27c2$, $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
$${\u22a2}_{c}A\mathit{\hspace{1em}\hspace{1em}\hspace{1em}\hspace{1em}}\text{or simply}\mathit{\hspace{1em}\hspace{1em}\hspace{1em}\hspace{1em}}\u22a2A.$$ 
For example, $\u22a2A\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}\u22a2A$$ 
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\u22a2B$, then $\mathrm{\Sigma}\u22a2A\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.
Title  axiom system for propositional logic 

Canonical name  AxiomSystemForPropositionalLogic 
Date of creation  20130322 19:31:50 
Last modified on  20130322 19:31:50 
Owner  CWoo (3771) 
Last modified by  CWoo (3771) 
Numerical id  13 
Author  CWoo (3771) 
Entry type  Definition 
Classification  msc 03B05 
Synonym  axiom system for classical propositional logic 
Related topic  DeductionTheoremHoldsForClassicalPropositionalLogic 
Related topic  SubstitutionTheoremForPropositionalLogic 