IA008: Computational Logic
2. First-Order Logic
Achim Blumensath
blumens@fi.muni.cz
Faculty of Informatics, Masaryk University, Brno
Basic Concepts
First-Order Logic
Syntax
▸ variables x, y, z, . . .
▸ terms x, f (t0, . . . , tn)
▸ relations R(t0, . . . , tn) and equality t0 = t1
▸ operators ∧, ∨, ¬, →, ↔
▸ quantifiers ∃xφ, ∀xφ
Semantics
A ⊧ φ(¯a) A = ⟨A, R0, R1, . . . , f0, f1, . . . ⟩
Examples
φ = ∀x∃y[f (y) = x] ,
ψ = ∀x∀y∀z[x ≤ y ∧ y ≤ z → x ≤ z] .
Examples
Structures
• graphs G = ⟨V, E⟩
E ⊆ V × V binary relation
• words W = ⟨W, ≤, (Pa)a⟩
≤ ⊆ W × W linear ordering
Pa ⊆ W positions with letter a
• transition systems S = ⟨S, (Ea)a, (Pi)i⟩
Ea ⊆ V × V binary relation
Pi ⊆ V unary relation
Examples
Graphs G = ⟨V, E⟩, E ⊆ V × V
• ‘The graph is undirected.’ (i.e., E is symmetric)
∀x∀y[E(x, y) → E(y, x)]
• ‘The graph has no isolated vertices.’
∀x∃y[E(x, y) ∨ E(y, x)]
• ‘Every vertex has outdegree 1.’
∀x∃y[E(x, y) ∧ ∀z[E(x, z) → z = y]]
Satisfiability
Theorem
Satisfiability for first-order logic is undecidable.
Proof
Turing machine M = ⟨Q, Σ, ∆, q0, F+, F−⟩
Q set of states
Σ tape alphabet
∆ set of transitions ⟨p, a, b, m, q⟩ ∈ Q × Σ × Σ × {−1, 0, 1} × Q
q0 initial state
F+ accepting states
F− rejecting states
Encoding in FO
Sq(t) state q at time t
h(t) head in field h(t) at time t
Wa(t, k) letter a in field k at time t
s successor function s(n) = n + 1
0 zero
φw = ADM ∧ INIT ∧ TRANS ∧ ACC
Proof
Sq(t) state q at time t
h(t) head in field h(t) at time t
Wa(t, k) letter a in field k at time t
s successor function s(n) = n + 1
0 zero
Admissibility formula
ADM = ∀t ⋀
p≠q
¬[Sp(t) ∧ Sq(t)] unique state
∧ ∀t∀k ⋀
a≠b
¬[Wa(t, k) ∧ Wb(t, k)] unique letter
Proof
Sq(t) state q at time t
h(t) head in field h(t) at time t
Wa(t, k) letter a in field k at time t
s successor function s(n) = n + 1
Initialisation formula for input: a0 . . . an−1
INIT = Sq0 (0) initial state
∧ h(0) = 0 initial head position
∧ ⋀
k<n
Wak
(0, k) ∧ ∀k[k ≥ n → W◻(0, k)] initial tape content
(here k = s(s(⋯s(0))) and k ≥ n = ⋀i<n k ≠ i)
Acceptance formula
ACC = ∃t ⋁
q∈F+
Sq(t) accepting state
Proof
Sq(t) state q at time t
h(t) head in field h(t) at time t
Wa(t, k) letter a in field k at time t
s successor function s(n) = n + 1
Transition formula
TRANS = ∀t ⋁
⟨p,a,b,m,q⟩∈∆
[Sp(t) ∧ Wa(t, h(t)) ∧ Sq(s(t)) ∧
h(s(t)) = h(t) + m ∧ Wb(s(t), h(t))]
∧ ∀t∀k ⋀
a∈Σ
[k ≠ h(t) → [Wa(t, k) ↔ Wa(s(t), k)]]
where
y = x + m =
⎧⎪⎪⎪⎪
⎨
⎪⎪⎪⎪⎩
y = s(x) if m = 1 ,
y = x if m = 0 ,
s(y) = x if m = −1 .
Tableaux
Tableau Proofs
For simplicity: first-order logic without equality
Statements φ true or φ false
Rule
φ σ
ψ τ
. . .
ϑ υ
ψm τm
ϑm υm
Interpretation
If φ σ is possible then so is ψi τi, . . . , ϑi υi, for some i.
Tableaux
Construction
A tableau for a formula φ is constructed as follows:
▸ start with φ false
▸ choose a branch of the tree
▸ choose a statement ψ value on the branch
▸ choose a rule with head ψ value
▸ add it at the bottom of the branch
▸ repeat until every branch contains both statements ψ true and
ψ false for some formula ψ
¬φ true
φ false
¬φ false
φ true
φ ∧ ψ true
φ true
ψ true
φ ∧ ψ false
φ false ψ false
φ ∨ ψ true
φ true ψ true
φ ∨ ψ false
φ false
ψ false
φ → ψ true
φ false ψ true
φ → ψ false
φ true
ψ false
φ ↔ ψ true
φ true
ψ true
φ false
ψ false
φ ↔ ψ false
φ true
ψ false
φ false
ψ true
∀xφ true
φ[x ↦ t] true
∀xφ false
φ[x ↦ c] false
∃xφ true
φ[x ↦ c] true
∃xφ false
φ[x ↦ t] false
c a new constant symbol, t an arbitrary term
Example
(A ∨ B) → ¬(¬A ∧ ¬B) false ¬(¬A ∧ ¬B) → (A ∨ B) false
Example
(A ∨ B) → ¬(¬A ∧ ¬B) false
A ∨ B true
¬(¬A ∧ ¬B) false
¬A ∧ ¬B true
¬A true
¬B true
A false
B false
A true B true
¬(¬A ∧ ¬B) → (A ∨ B) false
¬(¬A ∧ ¬B) true
A ∨ B false
A false
B false
¬A ∧ ¬B false
¬A false ¬B false
A true B true
Example
∃x∀yR(x, y) → ∀y∃xR(x, y) false ∀xR(x, x) → ∀x∃yR(f (x), y) false
Example
∃x∀yR(x, y) → ∀y∃xR(x, y) false
∃x∀yR(x, y) true
∀y∃xR(x, y) false
∀yR(c, y) true
∃xR(x, d) false
R(c, d) true
R(c, d) false
∀xR(x, x) → ∀x∃yR(f (x), y) false
∀xR(x, x) true
∀x∃yR(f (x), y) false
∃yR(f (c), y) false
R(f (c), f (c)) false
R(f (c), f (c)) true
Soundness and Completeness
Theorem
A first-order formula φ is valid if, and only if, there exists a tableau T
for φ false where every branch is contradictory.
Corollary
Validity of first-order formulae is recursively enumerable, but not
decidable.
Soundness and Completeness
Theorem
A first-order formula φ is valid if, and only if, there exists a tableau T
for φ false where every branch is contradictory.
Terminology
A tableau for a statement φ value is a tableau T where the root is
labelled with φ value.
A branch β is contradictory if it contains both statements ψ true and
ψ false, for some formula ψ.
A branch β is consistent with a structure A if
▸ A ⊧ ψ, for all statements ψ true on β and
▸ A ⊭ ψ, for all statements ψ false on β.
A branch β is complete if, for every atomic formula ψ, it contains one
of the statements ψ true or ψ false.
Proof Sketch: Soundness
Lemma
If β is consistent with A and we extend the tableau by applying a rule,
the new tableau has a branch β′
extending β that is consistent with A.
Corollary
If A ⊭ φ, then every tableau for φ false has a branch that is not
contradictory.
Corollary
If φ is not valid, there is no tableau for φ false where all branches are
contradictory.
Proof Sketch: Completeness
Lemma
If every tableau for φ false has a non-contradictory branch, there exists
a tableau for φ false with a branch β that is complete and
non-contradictory.
Lemma
If a branch β is complete and non-contradictory, there exists a
structure A such that β is consistent with A.
Corollary
If every tableau for φ false has a non-contradictory branch, there exists
a structure A with A ⊭ φ.
Natural Deduction
Proof Calculi
Notation
ψ1, . . . , ψn ⊢ φ φ is provable with assumptions ψ1, . . . , ψn
φ is provable if ⊢ φ.
Rules
Γ1 ⊢ φ1 . . . Γn ⊢ φn
∆ ⊢ ψ
premises
conclusion
φ1 ∧ ⋅⋅⋅ ∧ φn ⇒ ψ
Axiom
∆ ⊢ ψ
rule without premises
Remark
Tableaux speak about possibilities while Natural Deduction proofs
speak about necesseties.
Proof Calculi
Derivation
Γ ⊢ φ ∆0 ⊢ ψ0
∆1 ⊢ ψ1 Γ′ ⊢ φ′
Σ ⊢ ϑ
tree of rules
Natural Deduction (propositional part)
(I⊺)
Γ ⊢ ⊺
(Ax)
Γ, φ ⊢ φ
(I∧)
Γ ⊢ φ ∆ ⊢ ψ
Γ, ∆ ⊢ φ ∧ ψ
(E∧)
Γ ⊢ φ ∧ ψ
Γ ⊢ φ
Γ ⊢ φ ∧ ψ
Γ ⊢ ψ
(I∨)
Γ, ¬ψ ⊢ φ
Γ ⊢ φ ∨ ψ
Γ, ¬φ ⊢ ψ
Γ ⊢ φ ∨ ψ
(E∨)
Γ ⊢ φ ∨ ψ ∆, φ ⊢ ϑ ∆′
, ψ ⊢ ϑ
Γ, ∆, ∆′ ⊢ ϑ
(I¬)
Γ, φ ⊢
Γ ⊢ ¬φ
(E¬)
Γ, ¬φ ⊢
Γ ⊢ φ
(I )
Γ ⊢ φ Γ ⊢ ¬φ
Γ ⊢
(E )
Γ ⊢
Γ ⊢ φ
(I→)
Γ, φ ⊢ ψ
Γ ⊢ φ → ψ
(E→)
Γ ⊢ φ ∆ ⊢ φ → ψ
Γ, ∆ ⊢ ψ
(I↔)
Γ, φ ⊢ ψ ∆, ψ ⊢ φ
Γ, ∆ ⊢ φ ↔ ψ
(E↔)
Γ ⊢ φ ∆ ⊢ φ ↔ ψ
Γ, ∆ ⊢ ψ
( + sym.)
Examples
⊢ (φ ∨ ψ) → ¬(¬φ ∧ ¬ψ)
Examples
φ ∨ ψ, ¬φ ∧ ¬ψ ⊢ φ ∨ ψ
φ ⊢ φ
¬φ ∧ ¬ψ ⊢ ¬φ ∧ ¬ψ
¬φ ∧ ¬ψ ⊢ ¬φ
φ, ¬φ ∧ ¬ψ ⊢
⋯
ψ, ¬φ ∧ ¬ψ ⊢
φ ∨ ψ, ¬φ ∧ ¬ψ ⊢
φ ∨ ψ ⊢ ¬(¬φ ∧ ¬ψ)
⊢ (φ ∨ ψ) → ¬(¬φ ∧ ¬ψ)
Natural Deduction (quantifiers and equality)
(I∃)
Γ ⊢ φ[x ↦ t]
Γ ⊢ ∃xφ
(E∃)
Γ ⊢ ∃xφ ∆, φ[x ↦ c] ⊢ ψ
Γ, ∆ ⊢ ψ
(I∀)
Γ ⊢ φ[x ↦ c]
Γ ⊢ ∀xφ
(E∀)
Γ ⊢ ∀xφ
Γ ⊢ φ[x ↦ t]
(I=)
Γ ⊢ t = t
(E=)
Γ ⊢ s = t ∆ ⊢ φ[x ↦ s]
Γ, ∆ ⊢ φ[x ↦ t]
c a new constant symbol, s, t arbitrary terms
Examples
s = t ⊢ t = s s = t ⊢ s = t ⊢ s = s
s = t ⊢ t = s
(E=)
s = t, t = u ⊢ s = u t = u ⊢ t = u s = t ⊢ s = t
s = t, t = u ⊢ s = u
(E=)
∃x∀yR(x, y) ⊢ ∀y∃xR(x, y)
∃x∀yR(x, y) ⊢ ∃x∀yR(x, y)
∀yR(c, y) ⊢ ∀yR(c, y)
∀yR(c, y) ⊢ R(c, d)
(E∀)
∀yR(c, y) ⊢ ∃xR(x, d)
(I∃)
∀yR(c, y) ⊢ ∀y∃xR(x, y)
(I∀)
∃x∀yR(x, y) ⊢ ∀y∃xR(x, y)
(E∃)
Soundness and Completeness
Theorem
A formula φ is provable using Natural Deduction if, and only if, it is
valid.
Corollary
The set of valid first-order formulae is recursively enumerable.
Isabelle/HOL
Isabelle/HOL
Proof assistant designed for software verification.
General structure
theory T
imports T1 ... Tn
begin
declarations, definitions, and proofs
end
Syntax
Two levels:
▸ the meta-language (Isabelle) used to define theories,
▸ the logical language (HOL) used to write formulae.
To distinguish the levels, one encloses formulae of the logical language
in quotes.
datatype 'a list = Nil ("[]")
| Cons 'a "'a list" (infixr "#" 65)
primrec app :: "'a list => 'a list => 'a list"
(infixr "@" 65)
where
"[] @ ys = ys" |
"(x # xs) @ ys = x # (xs @ ys)"
Logical Language
Types
▸ base types: bool, nat, int,…
▸ type constructors: α list, α set,…
▸ function types: α ⇒ β
▸ type variables: 'a, 'b,…
Terms
▸ application: f x y, x + y,…
▸ abstraction: λx.t
▸ type annoation: t α
▸ if b then t else u
▸ let x = t in u
▸ case x of p0 ⇒ t0 | ⋯ | pn ⇒ tn
Formulae
▸ terms of type bool
▸ boolean operations ¬, ∧, ∨, →
▸ quantifiers ∀x, ∃x
▸ predicates ==, <,…
Basic Types
datatype bool = True | False
fun conj :: "bool => bool => bool" where
"conj True True = True" |
"conj _ _ = False"
datatype nat = 0 | Suc nat
fun add :: "nat => nat => nat" where
"add 0 n = n" |
"add (Suc m) n = Suc (add m n)"
lemma add_02: "add m 0 = m"
apply (induction m)
apply (auto)
done
Proofs
lemma add_02: "add m 0 = m"
apply (induction m)
1. add 0 0 = 0
2. ⋀m. add m 0 = m ==> add (Suc m) 0 = Suc m
apply (auto)
datatype 'a list = Nil ("[]")
| Cons 'a "'a list" (infixr "#" 65)
fun app :: "'a list => 'a list => 'a list"
(infixr "@" 65)
where
"[] @ ys = ys" |
"(x # xs) @ ys = x # (xs @ ys)"
fun rev :: "'a list => 'a list" where
"rev [] = []" |
"rev (x # xs) = (rev xs) @ (x # [])"
theorem rev_rev [simp]: "rev (rev xs) = xs"
apply(induction xs)
1. rev (rev Nil) = Nil
2. ⋀x1 xs. rev (rev xs) = xs ==>
rev (rev (Cons x1 xs)) = Cons x1 xs
apply(auto)
1. ⋀x1 xs.
rev (rev xs) = xs ==>
rev (rev xs @ Cons x1 Nil) = Cons x1 xs
lemma app_Nil2 [simp]: "xs @ Nil = xs"
apply(induction xs)
apply(auto)
done
lemma rev_app [simp]: "rev (xs @ ys) = rev ys @ rev xs"
apply(induction xs)
apply(auto)
1. ⋀x1 xs.
rev (xs @ ys) = rev ys @ rev xs ==>
(rev ys @ rev xs) @ Cons x1 Nil =
rev ys @ (rev xs @ Cons x1 Nil)
lemma app_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)"
apply (induction xs)
apply (auto)
done
lemma app_Nil2 [simp]: "xs @ [] = xs"
apply(induction xs)
apply(auto)
done
lemma app_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)"
apply(induction xs)
apply(auto)
done
lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)"
apply(induction xs)
apply(auto)
done
theorem rev_rev [simp]: "rev(rev xs) = xs"
apply(induction xs)
apply(auto)
done
end