CS205: Building with Artificial Intelligence

It is possible to define another version of propositional calculus, which defines most of the syntax of the logical operators by means of axioms, and which uses only one inference rule.

Axioms

Let φ, χ, and ψ stand for well-formed formulas. (The well-formed formulas themselves would not contain any Greek letters, but only capital Roman letters, connective operators, and parentheses.) Then the axioms are as follows:

• Axiom THEN-2 may be considered to be a "distributive property of implication with respect to implication".
• Axioms AND-1 and AND-2 correspond to "conjunction elimination". The relation between AND-1 and AND-2 reflects the commutativity of the conjunction operator.
• Axiom AND-3 corresponds to "conjunction introduction".
• Axioms OR-1 and OR-2 correspond to "disjunction introduction". The relation between OR-1 and OR-2 reflects the commutativity of the disjunction operator.
• Axiom NOT-1 corresponds to "reductio ad absurdum".
• Axiom NOT-2 says that "anything can be deduced from a contradiction".
• Axiom NOT-3 is called "tertium non-datur" (Latin: "a third is not given") and reflects the semantic valuation of propositional formulas: a formula can have a truth-value of either true or false. There is no third truth-value, at least not in classical logic. Intuitionistic logicians do not accept the axiom NOT-3.

Inference rule

The inference rule is modus ponens:

${\frac {\phi ,\ \phi \to \chi }{\chi }}$.

Meta-inference rule

Let a demonstration be represented by a sequence, with hypotheses to the left of the turnstile and the conclusion to the right of the turnstile. Then the deduction theorem can be stated as follows:

This deduction theorem (DT) is not itself formulated with propositional calculus: it is not a theorem of propositional calculus, but a theorem about propositional calculus. In this sense, it is a meta-theorem, comparable to theorems about the soundness or completeness of propositional calculus.

On the other hand, DT is so useful for simplifying the syntactical proof process that it can be considered and used as another inference rule, accompanying modus ponens. In this sense, DT corresponds to the natural conditional proof inference rule which is part of the first version of propositional calculus introduced in this article.

The converse of DT is also valid:

in fact, the validity of the converse of DT is almost trivial compared to that of DT:

1. $\phi _{1},\ ...,\ \phi _{n},\ \chi \vdash \chi \to \psi$
2. $\phi _{1},\ ...,\ \phi _{n},\ \chi \vdash \chi$
   

3. $\phi _{1},\ ...,\ \phi _{n},\ \chi \vdash \psi$

The converse of DT has powerful implications: it can be used to convert an axiom into an inference rule. For example, by axiom AND-1 we have,

$\vdash \phi \wedge \chi \to \phi$,

which can be transformed by means of the converse of the deduction theorem into

$\phi \wedge \chi \vdash \phi$,

which tells us that the inference rule

${\frac {\phi \wedge \chi }{\phi }}$

is admissible. This inference rule is conjunction elimination, one of the ten inference rules used in the first version (in this article) of the propositional calculus.

Example of a proof

The following is an example of a (syntactical) demonstration, involving only axioms THEN-1 and THEN-2:

Prove: $A\to A$ (Reflexivity of implication).

Proof:

1. $(A\to ((B\to A)\to A))\to ((A\to (B\to A))\to (A\to A))$
   Axiom THEN-2 with $\phi =A,\chi =B\to A,\psi =A$
   
   
2. $A\to ((B\to A)\to A)$
   Axiom THEN-1 with $\phi =A,\chi =B\to A$
   
   
3. $(A\to (B\to A))\to (A\to A)$
   From (1) and (2) by modus ponens.
   
   
4. $A\to (B\to A)$
   Axiom THEN-1 with $\phi =A,\chi =B$
   
   
5. $A\to A$
   From (3) and (4) by modus ponens.