The Axiomatic Structure of p Axiom schema1A∨A2A Axiom schema2A(B∨A) ience-p. 9 /39
The Axiomatic Structure of P Axiom Schema 1 A ∨ A ⊃ A Axiom Schema 2 A ⊃ (B ∨ A) Axiom Schema 3 A ⊃ B ⊃ (C ∨ A ⊃ (B ∨ C)) Modus Ponens (MP) A, A ⊃ B B Logic in Computer Science – p.9/39
The Axiomatic Structure of p Axiom schema1A∨A2A Axiom schema2A(B∨A) Axiom Schema 3 A)BD(CVAD(BVC) ience-p. 9 /39
The Axiomatic Structure of P Axiom Schema 1 A ∨ A ⊃ A Axiom Schema 2 A ⊃ (B ∨ A) Axiom Schema 3 A ⊃ B ⊃ (C ∨ A ⊃ (B ∨ C)) Modus Ponens (MP) A, A ⊃ B B Logic in Computer Science – p.9/39
The Axiomatic Structure of p Axiom schema1A∨A2A Axiom schema2A(B∨A) Axiom Schema 3 A)BD(CVAD(BVC) Modus Ponens(MP、A,AB B Logic in Computer Science - p 9/39
The Axiomatic Structure of P Axiom Schema 1 A ∨ A ⊃ A Axiom Schema 2 A ⊃ (B ∨ A) Axiom Schema 3 A ⊃ B ⊃ (C ∨ A ⊃ (B ∨ C)) Modus Ponens (MP) A, A ⊃ B B Logic in Computer Science – p.9/39
What is a proof A proof of a wff b from the set r of hypotheses is a finite sequence Bl, B2, .. Bm of wffs such that Bm is b. and for each j(1≤j≤m) at least one the following conditions is satisfied Bi is an axiom 2.B;∈; 3. Bi is inferred by mp from wffs Bi and bk where i< j and k 3 Logic in Computer Science-p.10/ 39
What is a Proof A proof of a wff B from the set Γ of hypotheses is a finite sequence B1, B2, · · · , Bm of wffs such that • Bm is B, and • for each j(1 ≤ j ≤ m) at least one the following conditions is satisfied. 1. Bj is an axiom; 2. Bj ∈ Γ; 3. Bj is inferred by MP from wffs Bi and Bk, where i < j and k < j. Logic in Computer Science – p.10/39
THB There is a proof of b from r B A proof of a wff b is a proof of b from the empty set of hypotheses. a theorem is a wff which has a proof Logic in Computer Science- p.11/39
` Γ ` B There is a proof of B from Γ. ` B A proof of a wff B is a proof of B from the empty set of hypotheses. A theorem is a wff which has a proof. Logic in Computer Science – p.11/39