# Propositional Calculus

One simple version of propositional logic starts off with statements of the form p → q and !p More complicated formulas can be formed by replacing variables with formulas, for example (p → r) → !(q → p). If you assign values true and false to the variables you can calculate the truth of any statement with a very simple “arithmetic.”

true → true = true

true →false = false

false → true = true

false → false = false

!true = false

!false = true

Of particular interest are statements, called theorems, that are always true, no matter what the values of the variables, for example, (p → p). To decide if a statement with N variables is a theorem, one can evaluate it for all 2^{N} possible combination of variable values, and there is probably no general shortcut.

Here are three theorems which are easily shown to be always true, just by calculation.

Axiom1: p → (q → p)

Axiom 2: [p → (q → r)] → [(p → q) → (p → r)]

Axiom 3: (~p → ~q) → (q → p)

These axioms can be used to generate new theorems from proved theorems by using two inference rules.

*Implication Elimination*: If p → q and p are true, then so is q.

*Substitution*: You can substitute any statements for the variables in a theorem as long as you substitute the same statement for a particular variable.

* *

Here is a proof of the obvious theorem (F → F).

T1: (A→(A→A)) by substituting A for p and q in Axiom 1.

T2: {F → [T1 → F]} →{[F → T1] → [F → F]}, by substituting F for both

p and r, and T1 for q in Axiom 2

T3: {[F → [T1→ F]} by substituting F for p and T1 for q in Axiom 1

T4: {[F → T1] → [F → F]}by implication elimination applied to 2 and 3

T5: T1 → [F → T1] by substituting T1 for p and F for q in Axiom 1

T6: [F → T1] by implication elimination applied to T1 and T5

T7: [F → F] by implication elimination applied to T4 and T6