IA008: Computational Logic
8. Many-Valued Logics
Achim Blumensath
blumens@fi.muni.cz
Faculty of Informatics, Masaryk University, Brno
Basic Concepts
Many-valued logics: Motivation
To some sentences we cannot – or do not want to – assign a truth
value since
▸ they make presuppositions that are not fulfilled
John regrets beating his wife.
John does not regret beating his wife.
▸ they refer to non-existing objects
吀he king of Paris has a pet lion.
▸ they are too vague
吀he next supermarket is far away.
▸ we have insufficient information
吀he favourite colour of Odysseus was blue.
▸ we cannot determine their truth
吀he Goldbach conjecture holds.
吀his leads to logics with truth values other than ‘true’ and ‘false’.
3-valued logic
truth values ‘false’ , ‘uncertain’ u, and ‘true’ ⊺.
A ¬A
⊺
u u
⊺
∧ u ⊺
u u u
⊺ u ⊺
∨ u ⊺
u ⊺
u u u ⊺
⊺ ⊺ ⊺ ⊺
Kleene K3
→ u ⊺
⊺ ⊺ ⊺
u u uuu ⊺
⊺ u ⊺
Łukasiewicz L3
→ u ⊺
⊺ ⊺ ⊺
u u ⊺⊺⊺ ⊺
⊺ u ⊺
Example
A B A ∧ (A → B) A ∧ (A → B) → B
⊺
u ⊺
⊺ ⊺
u u u
u u u u/⊺
u ⊺ u ⊺
⊺ ⊺
⊺ u u u/⊺
⊺ ⊺ ⊺ ⊺
Fuzzy logic
Truth values: v ∈ [0,1] measuring how true a statement is.
0 means ‘false’ and 1 means ‘true’.
Several possible semantics:
¬A A ∧ B A ∨ B A → B
1 − A A ⋅ B 1 − (1 − A)(1 − B) 1 − A(1 − B)
1 − A min(A,B) max(A,B) max(1 − A,B)
1 − A max(A + B − 1,0) min(A + B,1) min(1 − A + B,1)
Example
A ∧ (A → B) → B = max(1 − min(A,max(1 − A,B)),B)
0 1
0
1
Tableaux for L3
statements: t ≤ φ, φ ≤ t, t ≰ φ, or φ ≰ t, for t ∈ { ,u,⊺}
Construction
A tableau for a formula φ is constructed as follows:
▸ start with 1 ≰ φ
▸ choose a branch of the tree
▸ choose a statement σ on the branch
▸ choose a rule with head σ
▸ add it at the bottom of the branch
▸ repeat until every branch contains one of the following
contradictions
≰ φ s ≤ t with s ≰ t s ≤ φ and t ≰ φ with t ≤ s
φ ≰ ⊺ s ≰ t with s ≤ t φ ≤ s and φ ≰ t with s ≤ t
where s,t ∈ { ,u,⊺} and φ is a formula
Tableaux Rules
t ≰ φ
φ ≤ s
t ≤ φ
φ ≰ s
φ ≰ t
s ≤ φ
φ ≤ t
s ≰ φ
s maximal < t
t ≤ ¬φ
φ ≤ ¬t
t ≰ ¬φ
φ ≰ ¬t
t ≤ φ ∧ ψ
t ≤ φ
t ≤ ψ
t ≰ φ ∧ ψ
t ≰ φ t ≰ ψ
φ ∨ ψ ≤ t
φ ≤ t
ψ ≤ t
φ ∨ ψ ≰ t
φ ≰ t ψ ≰ t
t ≠
⊺ ≰ φ → ψ
u ≤ φ ⊺ ≤ φ
u ≰ ψ ⊺ ≰ ψ
u ≰ φ → ψ
u ≤ φ
u ≰ ψ u ≤ φ → ψ
u ≰ φ u ≤ ψ
⊺ ≤ φ → ψ
⊺ ≰ φ ⊺ ≤ ψ
⊺ ≤ φ → ψ
u ≰ φ u ≤ ψ
Example
u ≰ [(u → A) ∧ (⊺ → (A → B))] → B
u ≤ (u → A) ∧ (⊺ → (A → B))
u ≰ B
u ≤ u → A
u ≤ ⊺ → (A → B)
u ≰ u u ≤ A
u ≰ ⊺ u ≤ A → B
u ≰ A u ≤ B
Intuitionistic Logic
吀he constructivists view
▸ We are not interested in truth but in provability.
▸ To prove the existence of an object is to give a concrete
example.
prove ∃xφ(x) ⇔ find t with φ(t)
▸ To prove a disjunction is to prove one of the choices.
prove φ ∨ ψ ⇔ prove φ or prove ψ
Goal
A variant of first-order logic that captures these ideas.
Boolean algebras
In classical logic the truth values form a boolean algebra with
operations
∧, ∨, ¬, ⊺,
Properties of negation:
x ∧ ¬x = x ∨ ¬x = ⊺
Heyting algebras
In intuitionistic logic the truth values form instead a Heyting
algebra with operations
∧, ∨, →, ⊺,
Properties of implication:
z ≤ x → y iff z ∧ x ≤ y
(that is x → y is the largest element satisfying (x → y) ∧ x ≤ y)
x ∧ (x → y) = x ∧ y x → x = ⊺
y ∧ (x → x) = y x → (y ∧ z) = (x → y) ∧ (x → z) .
Heyting algebras
In intuitionistic logic the truth values form instead a Heyting
algebra with operations
∧, ∨, →, ⊺,
Properties of implication:
z ≤ x → y iff z ∧ x ≤ y
(that is x → y is the largest element satisfying (x → y) ∧ x ≤ y)
x ∧ (x → y) = x ∧ y x → x = ⊺
y ∧ (x → x) = y x → (y ∧ z) = (x → y) ∧ (x → z) .
Negation ¬x = x →
satisfies x ∧ ¬x = , but not x ∨ ¬x = ⊺
Forcing Frames
Definition
Transition system S = ⟨S,≤,(Pi)i∈I,s0⟩ with one edge relation ≤
that forms a partial order:
▸ reflexive s ≤ s
▸ transitive s ≤ t ≤ u implies s ≤ u
▸ anti-symmetric s ≤ t and t ≤ s implies s = t
吀he forcing relation
S forcing frame, s ∈ S state, φ formula
s ⊩ Pi :iff t ∈ Pi for all t ≥ s
s ⊩ φ ∧ ψ :iff s ⊩ φ and s ⊩ ψ
s ⊩ φ ∨ ψ :iff s ⊩ φ or s ⊩ ψ
s ⊩ ¬φ :iff t ⊮ φ for all t ≥ s
s ⊩ φ → ψ :iff t ⊩ φ implies t ⊩ ψ for all t ≥ s
吀he truth value of φ in S is
⟦φ⟧S = { s ∈ S s ⊩ φ} ,
which is upwards-closed with respect to ≤.
Intuition
Intuitionistic logic speaks about the limit behaviour of φ for large s.
Example
P
P
P P
P P P P
Q
Q Q
Q Q Q Q
Example
φ = P P
P
P P
P P P P
Q
Q Q
Q Q Q Q
Example
φ = P P
P
P P
P P P P
Q
Q Q
Q Q Q Q
Example
φ = ¬P P
P
P P
P P P P
Q
Q Q
Q Q Q Q
Example
φ = ¬P P
P
P P
P P P P
Q
Q Q
Q Q Q Q
Example
φ = P ∨ ¬P P
P
P P
P P P P
Q
Q Q
Q Q Q Q
Example
φ = P ∨ ¬P P
P
P P
P P P P
Q
Q Q
Q Q Q Q
Example
φ = Q → P P
P
P P
P P P P
Q
Q Q
Q Q Q Q
Example
φ = Q → P P
P
P P
P P P P
Q
Q Q
Q Q Q Q
Tableaux for Intuitionistic Logic
Statements
s ⊩ φ s ⊮ φ s ≤ t
s,t state labels, φ a formula
Rules
s ⊩ φ
s ⊩ ψ0
. . .
s ⊮ θ0
s ⊮ ψm s ⊩ θn
s ⊩ φ
t ⊩ φ
φ atomic, t ≥ s arbitrary
s ⊮ φ
φ atomic
s ⊩ ¬φ
t ⊮ φ
t ≥ s arbitrary
s ⊮ ¬φ
s ≤ t
t ⊩ φ
t news ⊩ φ ∧ ψ
s ⊩ φ
s ⊩ ψ
s ⊮ φ ∧ ψ
s ⊮ φ s ⊮ ψ
s ⊩ φ ∨ ψ
s ⊩ φ s ⊩ ψ
s ⊮ φ ∨ ψ
s ⊮ φ
s ⊮ ψ
s ⊩ φ → ψ
t ⊮ φ t ⊩ ψ
t ≥ s arbitrary
s ⊮ φ → ψ
s ≤ t
t ⊩ φ
t ⊮ ψ
t new
s ⊩ ∃xφ
s ⊩ φ(c)
c new
s ⊮ ∃xφ
s ⊮ φ(c)
c arbitrary
s ⊩ ∀xφ
t ⊩ φ(c)
c, t arbitrary with s ≤ t
s ⊮ ∀xφ
s ≤ t
t ⊮ φ(c)
c, t new(‘c arbitrary’ means either new or appearing somewhere
on the same branch.)
s ⊮ A → (B → A)
s ≤ t
t ⊩ A
t ⊮ B → A
t ≤ u
u ⊩ B
u ⊮ A
u ⊩ A
s ⊮ ∃x(φ ∨ ψ) → (∃xφ ∨ ∃xψ)
s ≤ t
t ⊩ ∃x(φ ∨ ψ)
t ⊮ ∃xφ ∨ ∃xψ
t ⊩ φ(c) ∨ ψ(c)u
t ⊮ ∃xφ
t ⊮ ∃xψ
t ⊮ φ(c)
t ⊮ ψ(c)
t ⊩ φ(c) t ⊩ ψ(c)
s ⊮ ∀x(φ ∧ ψ) → (∀xφ ∧ ∀xψ)
s ≤ t
t ⊩ ∀x(φ ∧ ψ)
t ⊮ ∀xφ ∧ ∀xψ
t ⊮ ∀xφ
t ≤ u
u ⊮ φ(c)
u ⊩ φ(c) ∧ ψ(c)
u ⊩ φ(c)
u ⊩ ψ(c)
t ⊮ ∀xψ
t ≤ u′
u′
⊮ ψ(d)
u′
⊩ φ(d) ∧ ψ(d)
u′
⊩ φ(d)
u′
⊩ ψ(d)