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

Logic in Computer Science An Introductory Course for Master Students Wang j iwang@nudt.edu.cn ecture One Preliminaries Logic in Computer Science- p 1/16

Logic in Computer Science An Introductory Course for Master Students Wang Ji jiwang@nudt.edu.cn Lecture One Preliminaries Logic in Computer Science – p.1/16

Theory of equivalence relations (A,R) (E1) For all r: ra (E2 )For all y: If a Ry then y ro (E3)For all 9, z If a Ry and g Rx then Rz Logic in Computer Science- p 2/16

Theory of Equivalence Relations (A, R) (E1) For all x : xRx. (E2) For all x, y : If xRy then yRx. (E3) For all x, y, z : If xRy and yRz then xRz. Logic in Computer Science – p.2/16

Theory of equivalence relations (A,R) (E1) For all r: ra (E2 )For all y: If a Ry then y ro (E3)For all 3, 3, 2: If x Ry and y rx then c Re For all and y, if there is a u such that Ru and Ru, then for all z, o rx if and only if y rx Logic in Computer Science- p 2/16

Theory of Equivalence Relations (A, R) (E1) For all x : xRx. (E2) For all x, y : If xRy then yRx. (E3) For all x, y, z : If xRy and yRz then xRz. For all x and y, if there is a u such that xRu and yRu, then for all z, xRz if and only if yRz. Logic in Computer Science – p.2/16

A Primary Analysis The concept“ Proposition” A formal language formulas The concept“ Follow from” Consequence relation The concept t“ Proof a sequence of formulas, Axioms, rules Logic in Computer Science -p 3/16

A Primary Analysis The concept “Proposition” A formal language, formulas The concept “Follow from” Consequence relation The concept “Proof” A sequence of formulas, Axioms, Rules Logic in Computer Science – p.3/16

Induction Consider an initial set b Cu and a class f of functions containing just two members f and g Where f:U×U→ U and g:U→U Let b=a, b. How to define the set c which contains b,f(b,b),9(a),f((a),f(b,b), Logic in Computer Science- p 4/16

Induction Consider an initial set B ⊆ U and a class F of functions containing just two members f and g, where f : U × U → U and g : U → U Let B = {a, b}. How to define the set C which contains b, f(b, b), g(a), f(g(a), f(b, b)), · · · Logic in Computer Science – p.4/16

Induction: from the top down A subset of s of u is closed under f and g iff whenever elements and y belong to s, then so do f(,g) and g(a S is inductive iff b c s and s is closed under f and Let c be the intersection of all the inductive subsets of u. then C is inductive Logic in Computer Science-p.5/16

Induction: from the top down A subset of S of U is closed under f and g iff whenever elements x and y belong to S, then so do f(x, y) and g(x). S is inductive iff B ⊆ S and S is closed under f and g. Let C∗ be the intersection of all the inductive subsets of U. Then C∗ is inductive. Logic in Computer Science – p.5/16

Induction: from the bottom up Let Cx be the set of things which can be reached from b by applying f and g a finite number of times. Define a constructive sequence to be a finite sequence of elements of U such that for each i< m we have at least one of c;∈B f(;, Ik)for some i<i, k< i i=g(ai) for some j < i Then Ck is the set of all points such that some construction sequence ends with Logic in Computer Science -p6/16

Induction: from the bottom up Let C∗ be the set of things which can be reached from B by applying f and g a finite number of times. Define a constructive sequence to be a finite sequence of elements of U such that for each i ≤ n we have at least one of xi ∈ B xi = f(xj , xk) for some j < i, k < i xi = g(xj ) for some j < i Then C∗ is the set of all points x such that some construction sequence ends with x. Logic in Computer Science – p.6/16

Let ∩{S: S is inductive} where Cm is the set of points such that some construction sequence of length m ends with a We have So, we call the set simply C and refer to it as the set generated from b by the functions in F Logic in Computer Science-p. 7/16

C∗ = C∗ Let C∗ = T{S : S is inductive } C∗ = Sn Cn where Cn is the set of points x such that some construction sequence of length n ends with x. We have C∗ = C∗ So, we call the set simply C and refer to it as the set generated from B by the functions in F. Logic in Computer Science – p.7/16

Induction Principle Assume that C is the set generated from b by the functions in f if s is a subset of c which includes b and is closed under the functions of f then Logic in Computer Science -p8/16

Induction Principle Assume that C is the set generated from B by the functions in F. If S is a subset of C which includes B and is closed under the functions of F, then S = C Logic in Computer Science – p.8/16

Ro excursion There is a set u a subset b of u and two functions f and g, where f:U×U→ U and g:U→U C is the set generated from b by f and g The problem is how to define a function on c recur sively Logic in Computer Science-p.9/16

Recursion There is a set U, a subset B of U, and two functions f and g, where f : U × U → U and g : U → U C is the set generated from B by f and g. The problem is how to define a function on C recur￾sively. Logic in Computer Science – p.9/16