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 2N 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