国防科学技术大学：《数理逻辑》（英文版）Lecture 2 Propositional Calculus

Logic in Computer Science An Introductory Course for Master Students Wang j iwang@nudt.edu.cn Lecture 2 Propositional calculus Logic in Computer Science- p 1/39

Logic in Computer Science An Introductory Course for Master Students Wang Ji jiwang@nudt.edu.cn Lecture 2 Propositional Calculus Logic in Computer Science – p.1/39

Syntax Formation Rules for p The The Axiomatic Structure of p Theorems and derived rules Logic in Computer Science- p 2/39

Syntax • Formation Rules for P • The The Axiomatic Structure of P • Theorems and Derived Rules Logic in Computer Science – p.2/39

Primitive Symbols The primitive symbols of p are the following Improper symbols: ( Proper symbols: denumerably many propositional variable, p,g, r, p1, 91, r1, 2: The set of Primitive Symbols Logic in Computer Science - p 3/39

Primitive Symbols The primitive symbols of P are the following: • Improper symbols: (,), ∼,∨ • Proper symbols: denumerably many propositional variable, p, q, r, p1, q1, r1, · · · Σ :The set of Primitive Symbols Logic in Computer Science – p.3/39

Well-formed formulas The set of wffs is the intersection of all sets s of formulas such that 1. pE S for each propositional variable p 2. For each formula a,fA∈S,then(~A)∈S 3. For all formulas a and B,ifA∈ s and e∈S, then(A∨B)∈S a wff is a member of the set of wffs Logic in Computer Science- p 4/39

Well-Formed Formulas The set of wffs is the intersection of all sets S of formulas such that: 1. p ∈ S for each propositional variable p 2. For each formula A, if A ∈ S, then (∼ A) ∈ S 3. For all formulas A and B, if A ∈ S and B ∈ S, then (A ∨ B) ∈ S A wff is a member of the set of wffs. Logic in Computer Science – p.4/39

Principle of Induction on Wif Let be a property of formulas, and let r( A)mean that a has property Suppose r(a) for each propositional variable q 2. Whenever R(A), then e(o a 3. Whenever (A) and Se(B), then R ((AV B) Then every wff has property i Logic in Computer Science - p 5/39

Principle of Induction on Wff Let < be a property of formulas, and let <(A) mean that A has property <. Suppose 1. <(q) for each propositional variable q. 2. Whenever <(A), then <(∼ A). 3. Whenever <(A) and <(B), then <((A ∨ B)). Then every wff has property <. Logic in Computer Science – p.5/39

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