Kripke Completeness of First-Order
Constructive Logics with Strong Negation
Ichiro HASUO
hasuo2@is.titech.ac.jp

Department of Mathematical and Computing Sciences,
Tokyo Institute of Technology

NASSLLI 2003 Student Session – p.1/28

Overview• Introducing Strong Negation andNelson’s Constructive Logic N• Introducing variants of N,

esp. by the Axiom of Potential Omniscience• Completeness proofs are given by theTree-Sequent method

NASSLLI 2003 Student Session – p.2/28

Notations• Logical Symbols:∧ , → , ∀,¬ (Heyting’s negation), ∼ (strong negation)• ∨ and ∃ can be defined:A ∨ B ≡ ∼(∼A ∧ ∼B),

∃xA ≡ ∼∀x∼A• Γ ⇒ ∆: A sequent.

Γ and ∆ are finite sets of formulas• A ↔ B is for (A → B) ∧ (B → A)
• GL: Gentzen-style sequent system for logic L.

TL: Tree-sequent system for L.

NASSLLI 2003 Student Session – p.3/28

Strong Negation ∼A
Introduced by Nelson and Markov, axiomatized by:
A → (∼A → B),∼(A ∧ B) ↔ ∼A ∨ ∼B,∼(A ∨ B) ↔ ∼A ∧ ∼B,∼(A → B) ↔ A ∧ ∼B,∼∼A ↔ A∼∀xA ↔ ∃x∼A,∼¬A ↔ A,∼∃xA ↔ ∀x∼A.

Nelson’s constructive logic N, is Int plus ∼.

NASSLLI 2003 Student Session – p.4/28

Strong Negation vs. Heyting’s One
Heyting’s Negation¬A ↔ (A → ⊥),NASSLLI 2003 Student Session – p.5/28

Strong Negation vs. Heyting’s One
Heyting’s Negation¬A ↔ (A → ⊥),“the compound sentences are not a product ofexperiment, they arise from reasoning. This concerns
also negation: we see that the lemon is yellow, we donot see that it is not blue” (Grzegorczyk)

NASSLLI 2003 Student Session – p.5/28

Strong Negation vs. Heyting’s OneHeyting’s Negation¬A ↔ (A → ⊥),Negative information is reduced to positive one.
“the compound sentences are not a product ofexperiment, they arise from reasoning. This concerns
also negation: we see that the lemon is yellow, we donot see that it is not blue” (Grzegorczyk)

NASSLLI 2003 Student Session – p.5/28

Strong Negation vs. Heyting’s One
Heyting’s Negation¬A ↔ (A → ⊥),Negative information is reduced to positive one.

Strong Negation

NASSLLI 2003 Student Session – p.5/28

Strong Negation vs. Heyting’s One
Heyting’s Negation¬A ↔ (A → ⊥),Negative information is reduced to positive one.

Strong Negation“we can not only verify a simple proposition such as
This door is locked. by direct inspection, but also falsify it” (Kracht)
NASSLLI 2003 Student Session – p.5/28

Strong Negation vs. Heyting’s One
Heyting’s Negation¬A ↔ (A → ⊥),Negative information is reduced to positive one.

Strong Negation
Negative/Positive informations are equallyprimitive!

NASSLLI 2003 Student Session – p.5/28

Kripke Semantics for N
Int-model:(M, ≤, U, I + )NASSLLI 2003 Student Session – p.6/28

Kripke Semantics for N
N-model:(M, ≤, U, I + , I − )NASSLLI 2003 Student Session – p.6/28

Kripke Semantics for N
N-model:(M, ≤, U, I + , I − )I + : verum interpretation
I − : falsum interpretation

NASSLLI 2003 Student Session – p.6/28

Kripke Semantics for N
N-model:(M, ≤, U, I + , I − )I + : verum interpretation
extended to a|=+ A (a verifies A).
I − : falsum interpretation
extended to a|=− A (a falsifies A).

NASSLLI 2003 Student Session – p.6/28

Kripke Semantics for N+I + (a)a|= p(u1 , . . . , um )⇐⇒(u1 , . . . , um ) ∈ pa|=+ A ∧ B⇐⇒

a|=+ Aand a|=+ B ;a|=+ A → B⇐⇒

for every b ≥ a, b|=+ A;

implies b|=+ B ;a|=+ ¬A⇐⇒for every b ≥ a, b  |=+ A ;a|=+ ∼A⇐⇒a|=− A ;a|=+ ∀xA⇐⇒

for every b ≥ a and every u ∈ U (b),b|=+ A[u/x] ;NASSLLI 2003 Student Session – p.7/28

Kripke Semantics for N−I − (a)a|= p(u1 , . . . , um )⇐⇒(u1 , . . . , um ) ∈ pa|=− A ∧ B⇐⇒

a|=− Aor a|=− B ;a|=− A → B⇐⇒

a|=+ Aand a|=− B ;a|=− ¬A⇐⇒a|=+ A ;a|=− ∼A⇐⇒a|=+ A ;a|=− ∀xA⇐⇒

for some u ∈ U (a),;a|=− A[u/x] .

NASSLLI 2003 Student Session – p.8/28

Kripke Semantics for N

verified formulas

Int-model
NASSLLI 2003 Student Session – p.9/28

Kripke Semantics for N

verified formulas
falsified formulas

N-model
NASSLLI 2003 Student Session – p.9/28

Sequent System GN∼-free partA⇒AΓ ⇒ ∆, A A, Γ ⇒ ∆(Cut)Γ⇒∆Γ⇒∆(Weakening)Σ, Γ ⇒ ∆, ΠA, B, Γ ⇒ ∆(∧L)
A ∧ B, Γ ⇒ ∆(Identity)Γ ⇒ ∆, A Γ ⇒ ∆, B(∧R)Γ ⇒ ∆, A ∧ BΓ ⇒ ∆, A B, Γ ⇒ ∆(→L)
A → B, Γ ⇒ ∆Γ ⇒ ∆, A(¬L)¬A, Γ ⇒ ∆A[y/x], Γ ⇒ ∆(∀L)∀xA, Γ ⇒ ∆(Equal to Maehara’s LJ )A, Γ ⇒ B
(→R)S
Γ⇒A→B
A, Γ ⇒(¬R)SΓ ⇒ ¬AΓ ⇒ A[z/x](∀R)S, VCΓ ⇒ ∀xANASSLLI 2003 Student Session – p.10/28

Sequent System GNA, ∼A ⇒Introducing ∼(Ex Falso)∼A, Γ ⇒ ∆ ∼B, Γ ⇒ ∆(∼∧L)∼(A ∧ B), Γ ⇒ ∆A, ∼B, Γ ⇒ ∆(∼→L)∼(A → B), Γ ⇒ ∆Γ ⇒ ∆, ∼A, ∼B(∼∧R)Γ ⇒ ∆, ∼(A ∧ B)

Γ ⇒ ∆, A Γ ⇒ ∆, ∼B(∼→R)Γ ⇒ ∆, ∼(A → B)

A, Γ ⇒ ∆(∼¬L)∼¬A, Γ ⇒ ∆Γ ⇒ ∆, A(∼¬R)Γ ⇒ ∆, ∼¬AA, Γ ⇒ ∆(∼∼L)∼∼A, Γ ⇒ ∆Γ ⇒ ∆, A(∼∼R)Γ ⇒ ∆, ∼∼A∼A[z/x], Γ ⇒ ∆(∼∀L)VC∼∀xA, Γ ⇒ ∆Γ ⇒ ∆, ∼A[y/x](∼∀R)Γ ⇒ ∆, ∼∀xANASSLLI 2003 Student Session – p.11/28

The Axiom of Potential Omniscience
Extensions of intermediate logics by ∼ have been
considered,but,

NASSLLI 2003 Student Session – p.12/28

The Axiom of Potential Omniscience
Extensions of intermediate logics by ∼ have been
considered,but,axioms unique to N (with both ¬ and ∼) have not!

NASSLLI 2003 Student Session – p.12/28

The Axiom of Potential Omniscience
Extensions of intermediate logics by ∼ have been
considered,but,axioms unique to N (with both ¬ and ∼) have not!
The axiom of potential omniscience¬¬(A ∨ ∼A)

NASSLLI 2003 Student Session – p.12/28

The Axiom of Potential Omniscience
Extensions of intermediate logics by ∼ have been
considered,but,axioms unique to N (with both ¬ and ∼) have not!
The axiom of potential omniscience¬¬(A ∨ ∼A)

Introduced by Hasuo, interpreted as:
We can eventually either verify or falsify astatement, with proper additional information.
NASSLLI 2003 Student Session – p.12/28

Variants of N
N: Int plus ∼.
D: Add ∀x(A(x) ∨ B) → ∀xA(x) ∨ B , the axiom ofconstant domain

NASSLLI 2003 Student Session – p.13/28

Variants of N
N: Int plus ∼.
D: Add ∀x(A(x) ∨ B) → ∀xA(x) ∨ B , the axiom ofconstant domain ⇒ contant domain models

NASSLLI 2003 Student Session – p.13/28

Variants of N
N: Int plus ∼.
D: Add ∀x(A(x) ∨ B) → ∀xA(x) ∨ B , the axiom of

constant domain ⇒ contant domain models
L: (A → B) ∨ (B → A)

NASSLLI 2003 Student Session – p.13/28

Variants of N
N: Int plus ∼.
D: Add ∀x(A(x) ∨ B) → ∀xA(x) ∨ B , the axiom ofconstant domain ⇒ contant domain models
L: (A → B) ∨ (B → A) ⇒ linearly ordered models

NASSLLI 2003 Student Session – p.13/28

Variants of N
N: Int plus ∼.
D: Add ∀x(A(x) ∨ B) → ∀xA(x) ∨ B , the axiom ofconstant domain ⇒ contant domain models
L: (A → B) ∨ (B → A) ⇒ linearly ordered models
O: Add ¬¬(A ∨ ∼A), the axiom of potential

omniscience

NASSLLI 2003 Student Session – p.13/28

Variants of N
N: Int plus ∼.
D: Add ∀x(A(x) ∨ B) → ∀xA(x) ∨ B , the axiom ofconstant domain ⇒ contant domain models
L: (A → B) ∨ (B → A) ⇒ linearly ordered models
O: Add ¬¬(A ∨ ∼A), the axiom of potential

omniscience
for a ∈ M and A (closed formula),∃b ≥ a s.t. b|=+ A or b|=− A.

NASSLLI 2003 Student Session – p.13/28

Variants of N
N: Int plus ∼.
D: Add ∀x(A(x) ∨ B) → ∀xA(x) ∨ B , the axiom ofconstant domain ⇒ contant domain models
L: (A → B) ∨ (B → A) ⇒ linearly ordered models
O: Add ¬¬(A ∨ ∼A), the axiom of potentialomniscience
for a ∈ M and A (closed formula),∃b ≥ a s.t. b|=+ A or b|=− A.
P: Omit the axiom A → (∼A → B).
NASSLLI 2003 Student Session – p.13/28

Variants of N
N: Int plus ∼.
D: Add ∀x(A(x) ∨ B) → ∀xA(x) ∨ B , the axiom of

constant domain ⇒ contant domain models
L: (A → B) ∨ (B → A) ⇒ linearly ordered models
O: Add ¬¬(A ∨ ∼A), the axiom of potentialomniscience
for a ∈ M and A (closed formula),∃b ≥ a s.t. b|=+ A or b|=− A.
P: Omit the axiom A → (∼A → B).
I + and I − are not disjoint ⇒ paraconsistency!
NASSLLI 2003 Student Session – p.13/28

Corresponding Kripke Models

IntNNOND

NLO

NLNPNASSLLI 2003 Student Session – p.14/28

Logics in Consideration –The N-family
Those without P:-- NDLO
6NLO
6NL

- NDL

66+L
N+O-

- NDO
-NO+D

- ND

For the enclosed , completeness is shown.
N: van Dalen (1986), ND: Thomason (1969)
The others: Hasuo

NASSLLI 2003 Student Session – p.15/28

Logics in Consideration –The N-family
Those with P:- NDLOP
6NLOP-6NLP- NDLP

66+LNP- NDOP-NOP+O -+D- NDP

For the enclosed , completeness is shown.
N: van Dalen (1986), ND: Thomason (1969)
The others: Hasuo

NASSLLI 2003 Student Session – p.15/28

Completeness Proofs
for Logics without O
The Tree-Sequent method (Kashima) gives unified
proofs for N[D][L][P](also for Int and intermediate logics e.g. CD, LC).
Sloppily, the tree-sequent (TS) method isa kind of semantic tableaux.

NASSLLI 2003 Student Session – p.16/28

Tree-Sequent and its Counter ModelγβΦ⇒ΨΣ⇒ΠαΓ⇒∆NASSLLI 2003 Student Session – p.17/28

Tree-Sequent and its Counter Modelverified
falsifiedγβΦ⇒ΨΣ⇒ΠαΓ⇒∆Formulas in LHS are verified,those in RHS are not verified.

NASSLLI 2003 Student Session – p.17/28

Outline of the Tree-Sequent method
For logic L,

NASSLLI 2003 Student Session – p.18/28

Outline of the Tree-Sequent method
For logic L,
1. Define the TS system TL.
A TS of TN is a tree of sequents, since N-models aretrees.
Accordingly a TS of TNL is a sequence of sequents.

NASSLLI 2003 Student Session – p.18/28

Outline of the Tree-Sequent method
For logic L,
1. Define the TS system TL.
2. Completeness of the TS system, i.e.
TL  T
⇒ T has a counter modelis easy.
Extend T into a saturated TS, which induces acounter model.

NASSLLI 2003 Student Session – p.18/28

Outline of the Tree-Sequent method
For logic L,
1. Define the TS system TL.
2. Completeness of the TS system, i.e.
TL  T
⇒ T has a counter modelis easy.
3. Define formulaic translation T f of a TS,and prove TL  T ⇒ GL  T fe.g. in TN,
T1···αΓ⇒∆Tkf→−→∀α (Γ) → (ff ∆) ∨ T1 ∨ · · · ∨ TkNASSLLI 2003 Student Session – p.18/28

Outline of the Tree-Sequent method
For logic L,
1. Define the TS system TL.
2. Completeness of the TS system, i.e.
TL  T
⇒ T has a counter modelis easy.
3. Define formulaic translation T f of a TS,
and prove TL  T ⇒ GL  T f
4. Let GL A.

αThen TL   ⇒ A by 3,
hence A has a counter model by 2.
NASSLLI 2003 Student Session – p.18/28

TN – TS system for logic N······

α······αΓ ⇒ ∆, A

B, Γ ⇒ ∆..
.

..
.

(→L)

NASSLLI 2003 Student Session – p.19/28

TN – TS system for logic N·········α···αΓ ⇒ ∆, A

B, Γ ⇒ ∆..
.

..
.

······(→L)

αA → B, Γ ⇒ ∆..
.

NASSLLI 2003 Student Session – p.19/28

TN – TS system for logic N·········βA, Σ ⇒ Πα

Γ⇒∆

..
.

(Drop)NASSLLI 2003 Student Session – p.20/28

TN – TS system for logic N·········βA, Σ ⇒ Πα

Γ⇒∆

..
.

···

···

(Drop)β···Σ⇒ΠαA, Γ ⇒ ∆..
.
NASSLLI 2003 Student Session – p.20/28

TN – TS system for logic N···

∅

A⇒Bα

Γ⇒∆..
.

(→R)

NASSLLI 2003 Student Session – p.21/28

TN – TS system for logic N···∅A⇒BαΓ⇒∆···..
.
(→R)(trimmed!)αΓ ⇒ ∆, A → B..
.

NASSLLI 2003 Student Session – p.21/28

Completeness Proofs
for Logics with O (1)(Again) O is for the axiom of potential omniscience.

NASSLLI 2003 Student Session – p.22/28

Completeness Proofs
for Logics with O (1)(Again) O is for the axiom of potential omniscience.
How can we obtain omniscient worlds(where every closed formula is either verified orfalsified)?
···aag..
.

NASSLLI 2003 Student Session – p.22/28

Completeness Proofs
for Logics with O (1)(Again) O is for the axiom of potential omniscience.
How can we obtain omniscient worlds(where every closed formula is either verified orfalsified)?
One of our proofs– Utilizes an embedding of LK

NASSLLI 2003 Student Session – p.22/28

Completeness Proofs
for Logics with O (1)(Again) O is for the axiom of potential omniscience.
How can we obtain omniscient worlds(where every closed formula is either verified orfalsified)?
One of our proofs– Utilizes an embedding of LK
Replacing an arbitrary number of ¬ by ∼,we obtain A∼¬ from A.
[Lemma] (Embedding)
LK  Γ ⇒ ∆ iff GN[D][L]O  Γ∼¬ , ∼∆∼¬ ⇒NASSLLI 2003 Student Session – p.22/28

Completeness Proofs
for Logics with O (1)T∞······

M

···

M

αa : Γa ⇒a ∆a induces

aa..
.

..
.

ag..
.

GNO  Γa ⇒ ∆aEmbedding

LK  (Γa )¬ ⇒Completenessinducescounter Cl-modelomniscient world

NASSLLI 2003 Student Session – p.23/28

Completeness Proofs
for Logics with O (2)The other proof is By Tree-Sequents with Guardians.
···

αβaa : Γa ⇒a ∆a ↑ Σa ⇒ Πa..

The second sequent is guardian, a seed of anomniscient world.

NASSLLI 2003 Student Session – p.24/28

Completeness Proofs
for Logics with O (2)The other proof is By Tree-Sequents with Guardians.
···βaαa : Γa ⇒a ∆a ↑ Σa ⇒ Πa..

The second sequent is guardian, a seed of anomniscient world.
···

βaag : Σa ⇒ Πaαa : Γa ⇒a ∆a..
NASSLLI 2003 Student Session – p.24/28

Completeness Proofsfor Logics with O (2)The other proof is By Tree-Sequents with Guardians.
···βaαa : Γa ⇒a ∆a ↑ Σa ⇒ Πa..

The second sequent is guardian, a seed of anomniscient world.
···

βaag : Σa ⇒ Πaαa : Γa ⇒a ∆a..

Proofs are just like in the TS method.

NASSLLI 2003 Student Session – p.24/28

Problem (1):Logics with Both O and PThose without P:-- NDLO
6NLO
6NL- NDL

66+L
N+O-- NDO
-NO+D- ND

logic : completeness by TS
logic : completeness by embedding or TSg
NASSLLI 2003 Student Session – p.25/28

Problem (1):Logics with Both O and P
Those with P:- NDLOP
6NLOP

-

6NLP

- NDLP

66+LNP- NDOP-NOP+O -+D- NDP

logic : completeness by TS
NASSLLI 2003 Student Session – p.25/28

Problem (1):Logics with Both O and P
Two methods here,
embedding of LK,
tree-sequent with guardianscannot be applied.

NASSLLI 2003 Student Session – p.25/28

Problem (1):Logics with Both O and P
Two methods here,cannot be applied.
Double Negation Shift (DNS), ∀x¬¬A → ¬¬∀xA

NASSLLI 2003 Student Session – p.25/28

Problem (1):Logics with Both O and P
Two methods here,cannot be applied.
Double Negation Shift (DNS), ∀x¬¬A → ¬¬∀xANOP  (DNS), since we have a counter model.

NASSLLI 2003 Student Session – p.25/28

Problem (1):Logics with Both O and P
Two methods here,cannot be applied.
Double Negation Shift (DNS), ∀x¬¬A → ¬¬∀xA
NOP  (DNS), since we have a counter model.

[Gabbay, 1981] MH (= Int plus (DNS)) is characterized
by the frames s.t.
for ∀a ∈ M , ∃b ≥ as.t. b is maximal.

NASSLLI 2003 Student Session – p.25/28

Problem (1):Logics with Both O and P
Two methods here,cannot be applied.
Double Negation Shift (DNS), ∀x¬¬A → ¬¬∀xA
NOP  (DNS), since we have a counter model.

[Gabbay, 1981] MH (= Int plus (DNS)) is characterized
by the frames s.t.
for ∀a ∈ M , ∃b ≥ as.t. b is maximal.

Counter models by our methods satisfy the above
property! (Omniscient worlds are maximal)
NASSLLI 2003 Student Session – p.25/28

Problem (2): Completeness of(NO plus ¬A ∨ ¬¬A)
prop-Int plus ¬A ∨ ¬¬A(The weak law of excluded middle) is characterized
by frames with their maximums.

NASSLLI 2003 Student Session – p.26/28

Problem (2): Completeness of(NO plus ¬A ∨ ¬¬A)
prop-Int plus ¬A ∨ ¬¬A

is characterized by frames with their maximums.
[Question] (Quantified)
Is (NO plus ¬A ∨ ¬¬A) characterized by N-models
with its maximum omniscient?

NASSLLI 2003 Student Session – p.26/28

Problem (2): Completeness of(NO plus ¬A ∨ ¬¬A)
prop-Int plus ¬A ∨ ¬¬A

is characterized by frames with their maximums.
[Question] (Quantified)
Is (NO plus ¬A ∨ ¬¬A) characterized by N-models
with its maximum omniscient?

...
...

NASSLLI 2003 Student Session – p.26/28

Problem (2): Completeness of(NO plus ¬A ∨ ¬¬A)
[Corsi and Ghilardi, 1989]
KC (= Int plus ¬A ∨ ¬¬A) is characterized by directedframes,i.e.
a ≤ b, a ≤ c ⇒ ∃d s.t. b ≤ d, c ≤ d.
(Existence of the maximum is too strong!)

NASSLLI 2003 Student Session – p.27/28

Problem (2): Completeness of(NO plus ¬A ∨ ¬¬A)
[Corsi and Ghilardi, 1989]
KC (= Int plus ¬A ∨ ¬¬A) is characterized by directed
frames,(Existence of the maximum is too strong!)[Fact] NO  (DNS).

NASSLLI 2003 Student Session – p.27/28

Problem (2): Completeness of(NO plus ¬A ∨ ¬¬A)
[Corsi and Ghilardi, 1989]
KC (= Int plus ¬A ∨ ¬¬A) is characterized by directed
frames,(Existence of the maximum is too strong!)[Fact] NO  (DNS).
[Ono, 1987]
Int + ¬A ∨ ¬¬A + ∀x¬¬A → ¬¬∀xA (DNS)+ (the axiom of constant domain)ischaracterized by constant domain frames with themaximum.
NASSLLI 2003 Student Session – p.27/28

Thank You for Your Attention

NASSLLI 2003 Student Session – p.28/28