You are here
Homeaxiom system for propositional logic
Primary tabs
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 wellformed 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. $A\to(B\to A)$,
2. $(A\to(B\to C))\to((A\to B)\to(A\to C))$,
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<i$ 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. $(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 $\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)
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.
Mathematics Subject Classification
03B05 no label found Forums
 Planetary Bugs
 HS/Secondary
 University/Tertiary
 Graduate/Advanced
 Industry/Practice
 Research Topics
 LaTeX help
 Math Comptetitions
 Math History
 Math Humor
 PlanetMath Comments
 PlanetMath System Updates and News
 PlanetMath help
 PlanetMath.ORG
 Strategic Communications Development
 The Math Pub
 Testing messages (ignore)
 Other useful stuff
 Corrections