IA: Computational Logic
. 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
The king of Paris has a pet lion.
▸ they are too vague
The next supermarket is far away.
▸ we have insufficient information
The favourite colour of Odysseus was blue.
▸ we cannot determine their truth
The Goldbach conjecture holds.
This leads to logics with truth values other than ‘true’ and ‘false’.
-valued logic
truth values ‘false’ , ‘uncertain’ u, and ‘true’ ⊺.
A ¬A
⊺
u u
⊺
∧ u ⊺
u u u
⊺ u ⊺
∨ u ⊺
u ⊺
u u u ⊺
⊺ ⊺ ⊺ ⊺
Kleene K
→ u ⊺
⊺ ⊺ ⊺
u u uuu ⊺
⊺ u ⊺
Łukasiewicz L
→ 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 ∈ [, ] measuring how true a statement is.
 means ‘false’ and  means ‘true’.
Several possible semantics:
¬A A ∧ B A ∨ B A → B
 − A A ⋅ B  − ( − A)( − B)  − A( − B)
 − A min(A, B) max(A, B) max( − A, B)
 − A max(A + B − , ) min(A + B, ) min( − A + B, )
Example
A ∧ (A → B) → B = max( − min(A, max( − A, B)), B)
 


Tableaux for L
statements: t ≤ φ, φ ≤ t, t ≰ φ, or φ ≰ t , for t ∈ { , u, ⊺}
Construction
A tableau for a formula φ is constructed as follows:
▸ start with  ≰ φ
▸ 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 s ≤ t
φ ≰ ⊺ s ≰ t with s ≤ t φ ≤ s and φ ≰ t with t ≤ s
where s, t ∈ { , u, ⊺} and φ is a formula
Tableaux Rules
t ≰ φ
φ ≤ s
t ≤ φ
φ ≰ s
φ ≰ t
s ≤ φ
φ ≤ t
s ≰ φ
s < t maximal
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
The 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, s⟩ 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
The 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
The 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 ⊩ ψ
. . .
s ⊮ ϑ
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 ⊩ B
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)