Propositional Calculus

(Formal Post Canonical System at end)

Meaning:

¬ means "not".

∨ means "or".

⊃ means "implies".

∧ means "and".

Variables:

P, Q, R, and S are variables. (Rule 1)

A variable followed by ' is a variable. (Rule 2)

Examples:

P, Q', S''''', P''

Well-formed formulas (Wffs).

All variables are wffs. (Rule 3)

If x and y are wffs, than so are the following:

¬x (Rule 4)

(x⊃y) (Rule 5)

(x∨y) (Rule 6)

(x∧y) (Rule 7)

Examples:

P, R', ¬P, ¬¬R, (R∧¬¬(P⊃R))

Theorems:

If x,y, and z are well-formed, than the following are theorems:

((x∨x)⊃x) (Rule 8)

(x⊃(y∨x)) (Rule 9)

((x∨y)⊃(y∨x)) (Rule 10)

((x∨(y∨z))⊃(y∨(x∨z))) (Rule 11)

((y⊃z)⊃((x∨y)⊃(x∨z))) (Rule 12)

If x is a wff and y and (y⊃x) are theorems,

then x is a theorem. (Rule 13)

If x and y are wffs than the following are interchangable anywhere in a theorem:

(x⊃y) and (¬x∨y) (Rule 14)

(x∧y) and ¬(¬x∨¬y) (Rule 15)

Example proof (P isn't true, or it is):

By rule 1:

P is a variable. (1)

By rule 3, applying (1):

P is a wff. (2)

By rule 9, applying (2) twice:

(P⊃(P∨P)) is a theorem. (3)

By rule 8, applying (2):

((P∨P)⊃P) is a theorem. (4)

By rule 6, applying (2) twice:

(P∨P) is a wff, (5)

By rule 4, applying (2):

¬P is a wff. (6)

By rule 12, applying (6), (5), and (2):

(((P∨P)⊃P)⊃((¬P∨(P∨P))⊃(¬P∨P))) is a theorem. (7)

By rule 14, applying (2), (5), and (7):

(((P∨P)⊃P)⊃((P⊃(P∨P))⊃(¬P∨P))) is a theorem. (8)

By rule 6, applying (6) and (2):

(¬P∨P) is a wff. (9)

By rule 5, applying (2) and (5):

(P⊃(P∨P)) is a wff. (10)

By rule 5, applying (10) and (9):

((P⊃(P∨P))⊃(¬P∨P)) is a wff. (11)

By rule 13, applying (11), (4), and (8):

((P⊃(P∨P))⊃(¬P∨P)) is a theorem. (12)

By rule 13, applying (9), (3), and (12):

(¬P∨P) is a theorem. (12)

Which translates to "Either P isn't true, or it is."

Here is the formal Post Canonical System:

-> var.p

-> var.q

-> var.r

-> var.s

var.$₁ -> var.$₁'

var.$₁ -> wff.$₁

wff.$₁ -> wff.~$₁

wff.$₁, wff.$₂ -> wff.($₁⊃$₂)

wff.$₁, wff.$₂ -> wff.($₁∨$₂)

wff.$₁, wff.$₂ -> wff.($₁∧$₂)

wff.$₁, wff.$₂, thm.$₃($₁⊃$₂)$₄ -> thm.$₃(~$₁∨$₂)$₄

wff.$₁, wff.$₂, thm.$₃(~$₁∨$₂)$₄ -> thm.$₃($₁⊃$₂)$₄

wff.$₁, wff.$₂, thm.$₃($₁∧$₂)$₄ -> thm.$₃~(~$₁∨~$₂)$₄

wff.$₁, wff.$₂, thm.$₃~(~$₁∨~$₂)$₄ -> thm.$₃($₁∧$₂)$₄

wff.$₁, thm.$₂, thm.($₂⊃$₁) -> thm.$₁

wff.$₁ -> thm.(($₁∨$₁)⊃$₁)

wff.$₁, wff.$₂ -> thm.($₁⊃($₂∨$₁))

wff.$₁, wff.$₂ -> thm.(($₁∨$₂)⊃($₂∨$₁))

wff.$₁, wff.$₂, wff.$₃ -> thm.(($₁∨($₂∨$₃))⊃($₂∨($₁∨$₃)))

wff.$₁, wff.$₂, wff.$₃ -> thm.(($₂⊃$₃)⊃(($₁∨$₂)⊃($₁∨$₃)))