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

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

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

Ⅰ NDEPENDENCE Logic in Computer Science- p 2/19

Independence Logic in Computer Science – p.2/19

Interpretation over a singleton Let i be s lap ,10>,anda∈∑ 1.T(A()=(xA)() 2.T(+)()=a 3.(Snn)(0)=(4)() 4. Io(P),a (P)E(T(n, un) for every n-an predicate constant(variable), where ( n(,,an)=t and u(n) n)=f Ifh a then v occurs in a Ifh a. then a occurs in a Logic in Computer Science -p 3/19

Interpretation over a singleton Let I be , and σ ∈ ΣI. 1. I(A)(σ) = I(∀xA)(σ). 2. I(t)(σ) = a. 3. I(Sx1,···,xn t1,···,tn A)(σ) = I(A)(σ). 4. I0(P), σ(P) ∈ {I(n), Ψ(n)} for every n-ary predicate constant (variable), where I(n)(a1, · · · , an) = T and Ψ(n)(a1, · · · , an) = F If ` A, then ∨ occurs in A. If ` A, then ∼ occurs in A. Logic in Computer Science – p.3/19

Independence Theorem The rules of inference and axiom schemata of f are independent Proof sketch Step 1 MP is independent Step 2 Gen is independent Step 3 Asl, AS2 and A S3 are independent Step 4 A 4 IS Independent etneⅤas Step 5 ASs is independent Do a transformation In a proof from hypothesis ab rule is independent Logic in Computer Science -p 4/19

Independence Theorem The rules of inference and axiom schemata of F are independent. Proof Sketch: Step 1 MP is independent. Step 2 Gen is independent. Step 3 AS1, AS2 and AS3 are independent. Step 4 AS4 is independent. “Define”∀ as ∃. Step 5 AS5 is independent. Do a transformation. In a proof from hypothesis, αβ rule is independent. Logic in Computer Science – p.4/19

CONSISTENCY Logic in Computer Science-p.5/19

Consistency Logic in Computer Science – p.5/19

Consistency absolutely consistency there is a wff which is not a theorem consistency w.r.t negation there is no wff A such that both a and n a are theorems consistency there is a wff a such that Ty a f is absolutely consistent and consistent with respect to negation Logic in Computer Science -p6/19

Consistency absolutely consistency there is a wff which is not a theorem. consistency w.r.t negation there is no wff A such that both A and ∼ A are theorems. consistency there is a wff A such that Γ 6` A. F is absolutely consistent and consistent with respect to negation. Logic in Computer Science – p.6/19

t is consistent The following parts are equivalent fA∈C(F),then A Th(r)or N Th(T There is A E L()such that A∈Th()o~A∈Th() T is consistent Logic in Computer Science-p. 7/19

Γ is consistent The following parts are equivalent. • If A ∈ L(F), then A 6∈ Th(Γ) or ∼ A 6∈ Th(Γ) • There is A ∈ L(F) such that A 6∈ Th(Γ) or ∼ A 6∈ Th(Γ) • Γ is consistent. Logic in Computer Science – p.7/19

t is consistent with t/ T is consistent with d iffturl is consistent A1,…, A is consistent with r iff r∪{A1,…,An} Is consistent An is inconsistent with r iff F~A1V…~An 2 A is inconsistent with r ifft a 3. fr is consistent andr a then a is consistent with r Logic in Computer Science -p8/19

Γ is consistent with Γ0 Γ is consistent with Γ0 iff Γ ∪ Γ0 is consistent. A1, · · · , An is consistent with Γ iff Γ ∪ {A1, · · · , An} is consistent. 1. A1, · · · , An is inconsistent with Γ iff Γ `∼ A1 ∨ · · · ∼ An. 2. A is inconsistent with Γ iff Γ `∼ A. 3. If Γ is consistent and Γ ` A, then A is consistent with Γ. Logic in Computer Science – p.8/19

Maximal consistent set 1.t is complete iff for any wff a A∈Tor~A∈ 2. fr satisfies (a)r is consistent, and (b) For any wff a r, a is inconsistent with I, then we say that i is consistent and maximal Logic in Computer Science-p.9/19

Maximal Consistent Set 1. Γ is complete iff for any wff A A ∈ Γ or ∼ A ∈ Γ 2. If Γ satisfies (a) Γ is consistent, and (b) For any wff A 6∈ Γ, A is inconsistent with Γ, then we say that Γ is consistent and maximal. Logic in Computer Science – p.9/19

Maximal consistent set Let i be a consistent and maximal set 1.A∈rif卜A 2.A∈rif~A∈T Let r be a set of wffs. the following parts are equivalent I is consistent and maximal T is consistent and complete Logic in Computer Science- p10/19

Maximal Consistent Set Let Γ be a consistent and maximal set. 1. A ∈ Γ iff Γ ` A 2. A ∈ Γ iff ∼ A 6∈ Γ Let Γ be a set of wffs. The following parts are equivalent. • Γ is consistent and maximal. • Γ is consistent and complete. Logic in Computer Science – p.10/19