abbreviations (A∧B) stands for~(~A∨~B (A→B) stands for(~AVB A≡B) stands for(AB)∧(BA) Logic in Computer Science - p 6/39
Abbreviations • ( A ∧ B ) stands fo r ∼ ( ∼ A ∨ ∼ B ) • ( A ⊃ B ) stands fo r ( ∼ A ∨ B ) • ( A ≡ B ) stands fo r (( A ⊃ B ) ∧ ( B ⊃ A)) Logic in Computer Science – p.6/39
Substitution A function:∑*→∑* is a substitution iff 1.f∈∑.,then(x)≠6 2.fx,y∈∑*,then(xy)=(x)(y) If B1 and B2 are substitutions such that B1(a)=B2() for every primitive symbol then Logic in Computer Science - p 7/39
Substitution A function θ : Σ∗ → Σ∗is a substitution iff 1. If x ∈ Σ, then θ(x) 6= 2. If x, y ∈ Σ∗, then θ(xy) = θ(x)θ(y) If θ1 and θ2 are substitutions such that θ1(x) = θ2(x) for every primitive symbol x, then θ1 = θ2 Logic in Computer Science – p.7/39
Substitution( Continued A substitution e is finite iff{∈∑(x)≠x}is finite a substitution o is a substitution for variables iff the only primitive symbols such that 0(a)* are variables Let I1,...,In be distinct primitive symbols and let Y1, ... Yn be formulas. Sy, ym is a substitution e such that Y if x C if c E{x1,…,m Logic in Computer Science -p 8/39
Substitution(Continued) • A substitution θ is finite iff { x ∈ Σ|θ ( x ) 6= x } is finite. • A substitution θ is a substitution fo r variables iff the only primitive symbols x such that θ ( x ) 6= x are variables. • Let x 1, · · · , x n b e distinct primitive symbols and let Y1, · · · , Yn b e formulas. S x 1,···,x n Y1,···,Yn is a substitution θ such that θ ( x ) = Yi if x = x i, 1 ≤ i ≤ n x if x 6∈ { x 1, · · · , x n } Logic in Computer Science – p.8/39
The Axiomatic Structure of p 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 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