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 < {a}, I0 >, 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