MATH 1090 Study Guide - Final Guide: Surface Integral, Null Hypothesis, Standard Normal Deviate
Introduction to Logic 1090 c
Richard Robinson
The deduction theorem 2.6.3 states
⊢Γ→ϕ⇐⇒ Γ⊢ϕ(1)
An occurrence of a variable is bound iff it is within
the scope of a quantifier in a formula.
A formula ϕis satisfiable iff there exists a set of states
for all p∈ϕsuch that ϕ=⊤.
The precedence of operators is given by
¬ ∀ ∧ ∨ → ≡ (2)
A set of formulas Γ is consistent iff there does not
exist a formula ϕsuch that
(Γ ⊢ϕ)∧(Γ ⊢ ¬ϕ) (3)
The rule of inference reductio ad absurdum is
ϕ→ ⊥ ⊢ ¬ϕ(4)
of which by A25 and 2.5.7 follow:
(ϕ→ψ)∧(ϕ→ ¬ψ)⊢ ¬ϕ(5)
The Leibniz rule of inference is where C:γ◦p,
ϕ≡ψ⊢γ[p:= ϕ]≡γ[p:= ψ] (6)
ϕ≡ψ⊢γ◦ϕ≡γ◦ψ(7)
The ping-pong theorem states
A≡B⇐⇒ (A→B)∧(B→A) (8)
The split/merge hypothesis states
Γ∪∆⊢ϕ⇐⇒ Γ∪(V∆i)⊢ϕ(9)
The cut rule states
(ϕ∨ψ)∧(¬ϕ∨γ)⊢ψ∨γ(10)
Metatheorem 2.6.6 states
Γ⊢ ⊥ ⇐⇒ Γ⊢ ∀ϕ⇐⇒ Γ⊢ϕ∧ ¬ϕ(11)
Soundness and completeness state respectively
Γ⊢ϕ⇐⇒ Γ|=ϕ(12)
Substitution of terms into variables is defined as
s[x:= t]≡
s s ≡ {c, y}
t s ≡x
f(si[x:= t]) s≡f(si)
(13)
The quantifiers are related or dualed in that
(∃x)ϕ≡ ¬(∀x)¬ϕ(14)
Substitution of terms into formulas is defined as
ϕ[x:= t]≡
φ(si[x:= t]) ϕ≡φ(si)
s1[x:= t] = s2[x=t]ϕ≡s1=s2
¬ψ[x:= t]ϕ≡ ¬ψ
ψ[x:= t]◦γ[x:= t]ϕ≡ψ◦γ
ϕ ϕ ∈AF
(∀y)ψ[x:= t]y6∈ t∨xbnd
undefined y∈t∧xfree
(15)
Substitution of variables into formula is defined as
ϕ[p:= ψ]≡
ψ ϕ ≡p
ϕ ϕ ∈AF 6=p
¬γ[p:= ψ]ϕ≡ ¬γ
γ[p:= ψ]◦β[p:= ψ]ϕ≡γ◦β
(∀x)γ[p:= ψ]ϕ≡xbnd(ψ)
undefined else
(16)
The set of logical axioms of first-order logic consists
of Ax1 −Ax6.
The metatheorem Weak Generalization states
(Γ ⊢ϕ)∧xbnd =⇒Γ⊢(∀x)ϕ(17)
Simultaneous substitution states for all i= 1,2, ...,
ϕ[xi:= ti]≡ϕ[xi:= zi][zi:= ti] (18)
The substitution theorem states
A∧ti→A[xi:= ti] (19)
The interchange of dummies theorem states
(∀x)ϕ(∀y)ψγ≡(∀y)ψ(∀x)ϕγ(20)
where (∀z)ϕψ⇐⇒ (∀z)(ϕ→ψ).
Single-Formula Leibniz is defined as
t=s→(ϕ[z:= t]≡ϕ[z:= s]) (21)
find more resources at oneclass.com
find more resources at oneclass.com
Document Summary
The quanti ers are related or dualed in that (1) An occurrence of a variable is bound i it is within the scope of a quanti er in a formula. A formula is satis able i there exists a set of states for all p such that = . The precedence of operators is given by (2) A set of formulas is consistent i there does not exist a formula such that. The rule of inference reductio ad absurdum is of which by a25 and 2. 5. 7 follow: The leibniz rule of inference is where c : p, [p := ] [p := ] A b (a b) (b a) (v i) . The cut rule states (3) (4) (5) (6) (7) (8) (9) (10) Metatheorem 2. 6. 6 states (11) ( x) ( x) (14) Substitution of terms into formulas is de ned as. (si[x := t]) s1[x := t] = s2[x = t] s1 = s2.