PMATH 330 - Much of these notes is based on the material provided by Barbara Csima for the PDF

Preview

Summary

Much of these notes is based on the material provided by Barbara Csima for the online version of this course....

Description

¬B

= {¬((P → Q) → R), ((P → Q) → R))} ∪ sub((P → Q)) ∪ sub(R) = {¬((P → Q) → R), ((P → Q) → R)), (P → Q), R} ∪ sub(P ) ∪ sub(Q) = {¬((P → Q) → R), ((P → Q) → R)), (P → Q), R, P, Q} ◭

   

.

T F

T T T T F F F F

T F T F T F T F

F T T F F T T F

F T

T F T F T T T T

ϕ T T F F

ψ T F T F

F T F T F F F F

(ϕ → ψ) T F T T

T T T F T F F T

T T F F

T F T F

T F T T

F T F T

F F T T

ϕ=P = ˆ ψ = ϕ[ψ/ˆ

ψ]

ψˆ = ϕ[ψ/ˆ ˆ ] → χ[ψ/ ˆ ψ ] = (θ[ψ/ψ

ψ]

→ ξ[ψ/ˆ

= ϕ[ψ/ˆ

T T F F

T F T F

T F F F

F T F T

T F F F

T T T T F F F F

T F T F T F T F

T T F F T T F F

ϕ T T T T F F F F

ψ T F T F T F T F

θ T T F F T T F F

T F T F F F F F

T F F F F F F F

(ϕ ∨ ψ) ((ϕ ∨ ψ) ∨ θ) T T T T T T T T T T F T T T F F

T F F F F F F F

T F F F F F F F

(ψ ∨ θ) (ϕ ∨ (ψ ∨ θ)) T T T T T T F T T T T T T T F F

T T F F

T F T F

T F T T

eˆ(R) = e(¬R).

T F T T

m(k)

k

∨ · · · ∨ lk

)

m(k)

k

∧ · · · ∧ lk

)

{a1 , . . . , an } ∪ {b1 , . . . , bm }

{Q, R} {P, ¬R} {¬P, R } {¬R, R}

{P, Q, R} {¬P, Q, ¬S } {Q, R, ¬S } {P, ¬R} {¬P, Q, ¬S} {¬R, Q, ¬S }

◭

Γ

Res1 (Γ) = {{¬P }, {R, S}, {¬R, P }, {¬R}, {S, P }} Res2 (Γ) = Res1 (Γ) ∪ {{S}} Res3 (Γ) = Res2 (Γ) ◭

∅

∅

◭

ψ

(¬P → (P → Q)) ((Q → (P → Q)) → ((¬P ∨ Q) → (P → Q))) (Q → (P → Q))

(ψ → χ) ((ψ → χ) → (ϕ → (ψ → χ))) (ϕ → (ψ → χ)) ((ϕ → (ψ → χ)) → ((ϕ → ψ) → (ϕ → χ))) ((ϕ → ψ) → (ϕ → χ))

ϕ

(ψ → (ϕ → ψ))

Γ ⊢ (ϕ → χ)

Γ ⊢ (¬ϕ → ϕ) ((¬ϕ → ϕ) → ((¬ϕ → ¬ϕ) → ¬¬ϕ)) ((¬ϕ → ¬ϕ) → ¬¬ϕ) (¬ϕ → ¬ϕ) ¬¬ϕ (¬¬ϕ → ϕ) ϕ

F

¬P ∈ Θ

x = y +1 ∃y x = y + 1 (x = 0 ∨ ∃y x = y + 1)

∪ sub((S(x3 ) ∨ ¬S(x1 ))) ={ϕ, ∀x1 (¬∀x2 R(x2 , c, x1 ) → x3 = g(x1 ))), (S (x3 ) ∨ ¬S(x1 ))}∪ sub(S(x3 )) ∪ sub(¬S(x1 )) ∪ sub((¬∀x2 R(x2 , c, x1 ) → x3 = g(x1 ))) ={ϕ, ∀x1 (¬∀x2 R(x2 , c, x1 ) → x3 = g(x1 ))), (S (x3 ) ∨ ¬S(x1 )), S (x3 ), ¬S(x1 ), S(x1 ), (¬∀x2 R(x2 , c, x1 ) → x3 = g(x1 ))} ∪ sub(¬∀x2 R(x2 , c, x1 )) ∪ sub(x3 = g(x1 )) ={ϕ, ∀x1 (¬∀x2 R(x2 , c, x1 ) → x3 = g(x1 ))), (S (x3 ) ∨ ¬S(x1 )), S (x3 ), ¬S(x1 ), S(x1 ), (¬∀x2 R(x2 , c, x1 ) → x3 = g(x1 )), ¬∀x2 R(x2 , c, x1 )), x3 = g(x1 )} ∪ sub(∀x2 R(x2 , c, x1 )) ={ϕ, ∀x1 (¬∀x2 R(x2 , c, x1 ) → x3 = g(x1 ))), (S (x3 ) ∨ ¬S(x1 )), S (x3 ) , ¬S(x1 ), S(x1 ), (¬∀x2 R(x2 , c, x1 ) → x3 = g(x1 )), ¬∀x2 R(x2 , c, x1 )), x3 = g(x1 ), ∀x2 R(x2 , c, x1 ), R(x2 , c, x1 )} ◭

f

b

f

f

b

x1 , x2 ) → x1 = d) → ¬f (x2 ) = x3 ) → ∀x3 R(x3 , c))

◭

a

y=x

.

β

β

β

A (t) = f A (val A β (t1 ), . . . , val

A (x ·(1 + 1)) = val A β (x) · val β (1 + 1) A = β(x) · (val A β (1) + val β (1)) = 5 · (1 + 1) = 10

◭

β

(t1 ) = val A β

(t1 ), . . . , valA

β[x/tom] (x)

∈ MA

γ

[y/3](y + 1), valγA[y/3](x)) ∈≤N

β

(t) = val A ˆ

β

(t) = val Aβ (c) = cA = valˆβA(c) = valˆβA (t)

β

(t) = valβA(x) = β(x) = ˆβ(x) = valˆβA(t)

(ti ) βˆ β

= val A

A (t) = f A (val A β (t1 ), . . . , valβ (tn ))

= f A (valˆβA (t1 ), . . . , valˆβA(tn )) = val ˆβA (t).

β

A (t1 ) = val A (t ) = val A ˆ β (t2 ) = val ˆ β 1

β |= ϕ.

β

(t1 ), . . . , valAβ (tn )) ∈ RA

ˆ β

(t1 ), . . . , valAˆ

β |= ϕ.

ˆ β |= ϕ. β |= ψ

β |= ϕ.

ˆ β[x/a] |= ψ.

1

F

→ γ ∗2 ).

A, β 6|= ϕi

1

→ γ ∗2 ) = (γ1 → γ2 )∗

β

A (sx/t) = valβ[ x/valA

β β

(sx/t) = cA = val A β[x/valA

A (sx/t) = val A β (t) = val β[x/valA β

(sx/t) = βy = val Aβ[x/valA β

β

(ti x/t) = val A β[x/valA (t)] (ti ) β

x x (f (t1 , . . . , tn )x/t) = val A β (f (t1 /t, . . . , tn /t)) A x x = f A (val A β (t1 /t), valβ (tn /t)) A = f A (val A β[x/valβA(t)] (t1 ), . . . , valβ[x/valβA(t)] (tn ))

= val A β[x/valA

β

x (t1 x/t1 ) = val A β (t2 /t2 )

(t1 ) β[x/valA β (t)] β (t)]

β

A = valβ[ x/valA (t)] (t2 ) β

|= t1 = t2

(t1 x/t), . . . , val βA (tn x/t)) ∈ RA

A (tn )) β[x/valβA(t)] (t1 ), . . . , valβ[x/valA β (t)] β

β

β

(t)]

(t)]

(t)]

|= R(t1 , . . . , tn )

|= ¬ψ

|= (ψ ∧ θ )

∈ RA

β β

β

(t)]

(t)]

|= ∀xψ

|= ∀yψ.

(t)][x/a]

|= ψ

⇒|= (ϕ ↔ ψ)∗ ⇒|= (ϕ∗ ↔ ψ ∗ ) ⇒ ϕ∗ ≡ ψ ∗

β[y/a]

(y )]

|= ϕ

≡∃u(¬∀x(u = z → x = z) → R(y, z)) ≡∃u(∃x¬(u = z → x = z) → R(y, z)) ≡∃u∀x(¬(u = z → x = z) → R(y, z))

Qx¬ψ0

Qx¬ψ0 ≡ ¯

Qxψ1

¯ ¬ψ0 ≡ ¬Qxψ0 ≡ ¬ψ = ϕ, Qxψ1 ≡ Qx ¯ 1 ) = qn(ψ1 ) +1 = qn(ψ0 ) +1 = qn(Qxψ 0 ) = qn(ψ) = qn(ϕ), qn(Qxψ ¯ 1 ) = free(ψ1 )\{x} = f ree(¬ψ0 )\{x} = f ree(ψ0 )\{x} = free(Qxψ0 ) = f ree(ψ) = free(ϕ) free(Qxψ

free(∀xψ ) = f ree(ψ) \ {x} = f ree(ψ0 ) \ {x} = free(∀xψ0 )

ψ

(∀x(H (x) → M (x)) → (H(s) → M (s))) (H (s) → M (s)) H(s)

ψ → ϕ)) ˆ

ψ → ϕ)) ˆ ∗ = (ϕ ˆ ∗ → (ψˆ∗ → ϕˆ∗ )) = (ϕ → (ψ → ϕ)).

β

(t) = valβA(ˆ...