1Proof theory and constructive logic
III Logic
1.4 Negative interpretation
Suppose a constructive logician found a classical logician, and then they try to
talk to each other. Then they would find that they disagree on a lot of things.
The classical logician has no problems accepting
¬¬A → A
, but the constructive
logician thinks that is nonsense. Can they make sense of each other?
The classical logician can understand the constructive logician via possible
world semantics. He could think that when the constructive logician says
a proposition is false, they mean there are possible world models where the
proposition fails. This is all fine.
But can a constructive logician make sense of the classical logician? When the
constructivist sees
A ∨ B
, he thinks that either we can prove
A
, or we can prove
B
. However, the classical logician views this as a much weaker statement. It is
more a long the lines of “it is not true that
A
and
B
are both false”. In general,
we can try to interpret classical statements by putting in enough negations:
Classical proposition Constructive interpretation
A ∨ B ¬(¬A ∨ ¬B)
A ∧ B A ∧ B
∃
x
W (x) ¬∀
x
¬W (x)
A → B ¬(A ∧ ¬B)
This gives rise to the negative interpretation of classical logic into constructive
logic, due to G¨odel:
Definition
(Negative interpretation)
.
Given a proposition
φ
, the interpretation
φ
∗
is defined recursively by
– ⊥
∗
= ⊥.
– If ϕ is atomic, then ϕ
∗
= ¬¬ϕ.
– If ϕ is negatomic, then ϕ
∗
= ϕ.
– If ϕ = ψ ∧ θ, then ϕ
∗
= ψ
∗
∧ θ
∗
.
– If ϕ = ψ ∨ θ, then ϕ
∗
= ¬(¬ψ
∗
∧ ¬θ
∗
).
– If ϕ = ∀
x
ψ(x), then (∀
x
)(ψ
∗
(x)).
– If ϕ = ψ → θ, then ϕ
∗
= ¬(ψ
∗
∧ ¬θ
∗
).
– If ϕ = ∃
x
ψ(x), then ϕ
∗
= ¬∀
x
¬ψ
∗
(x).
One can check that we always have
` ϕ → ϕ
∗
. So the constructive version is
always stronger.
Definition (Stable formula). A formula is stable if
` ϕ
∗
→ ϕ.
Lemma.
Any formula built up from negated and doubly negated atomics by
¬
,
∧ and ∀ is stable.
Proof.
By induction on formulae. The base case is immediate, using the fact
that ¬¬¬A → ¬A. This follows from the more general fact that
(((p → q) → q) → q) → p → q.
It is less confusing to prove this in two steps, and we will write
λ
-terms for our
proofs. First note that if we have
f
:
A → B
, then we can obtain
f
T
: (
B →
q) → A → q for any q, using
f
T
= λg
B→q
.λa
A
.g(f(a)).
So it suffices to prove that
p → (p → q) → q,
and the corresponding term is
λx
p
.λg
p→q
.gx
We now proceed by induction.
–
Now assume that we have proofs of
¬¬p → p
and
¬¬q → q
. We want
to prove
p ∧ q
from
¬¬
(
p ∧ q
). It suffices to prove
¬¬p
and
¬¬q
form
¬¬(p ∧ q), and we will just do the first one by symmetry.
We suppose
¬p
. Then we know
¬
(
p ∧ q
). But we know
¬¬
(
p ∧ q
). So we
obtain a contradiction. So we have proved that ¬¬p.
– Note that we have
` ∃
x
¬¬ϕ(x) → ¬¬∃
x
ϕ(x),
but not the other way round. For universal quantification, we have
¬¬∀
x
ϕ(x) → ∀
x
¬¬ϕ(x),
but not the other way round. We can construct a proof as follows:
[∀
x
ϕ(x)]
1
∀-elim
ϕ(a) [¬ϕ(x)]
2
→-elim
→
→-int (1)
¬∀
x
ϕ(x) [¬¬∀
x
ϕ(x)]
3
→-elim
⊥
→-int (2)
¬¬ϕ(a)
∀-int
¬¬∀
x
ϕ(x)
→-int (3)
¬¬∀
x
F (x) → ∀
x
¬¬F (x)
We now want to show that if
ϕ
is stable, then
∀
x
ϕ
(
x
) is stable. In other
words, we want
¬¬∀
x
ϕ
∗
(x) → ∀
x
ϕ
∗
(x).
But form ¬¬∀
x
ϕ
∗
(x), we can deduce ∀
x
¬¬ϕ
∗
(x), which implies ∀
x
ϕ
∗
(x).
So every formula in the range of the negative interpretation is stable. Every
stable formula is equivalent to its double negation (classically). Every formula is
classically equivalent to a stable formula.
So if a constructive logician meets a classical logician who is making some
bizarre assertions about first order logic. To make sense of this, the constructive
logician can translate it to its negative interpretation, which the classical logician
thinks is equivalent to the original one.