Axiom Schemata for F Axiom schema1A∨A2A Axiom schema2A(B∨A) Axiom Schema 3 AOBD(CVAD(BVC) Axiom Schema 4 V xAD Si a where t is a term free for the individual variable in a Axiom Schema 5 Vr(AVB)(AvVcB) provided that a is not free in A Logic in Computer Science- p 2/27Axiom Schemata for F Axiom Schema 1 A ∨ A ⊃ A Axiom Schema 2 A ⊃ (B ∨ A) Axiom Schema 3 A ⊃ B ⊃ (C ∨ A ⊃ (B ∨ C)) Axiom Schema 4 ∀xA ⊃ Sxt A where t is a term free for the individual variable x in A Axiom Schema 5 ∀x(A ∨ B) ⊃ (A ∨ ∀xB) provided that x is not free in A Logic in Computer Science – p.2/27