constructivity:intuitionism
CONSTRUCTIVITY
AND INTUITIONISM
1
Yoshihiro Maruyama
co-taught with Pascal Bercher
on the legacy of John Slaney
CANTOR’S CLASSICAL PARADISE AND ITS COLLAPSE
asd
2
➤ The Crisis of Math as caused by Russell’s paradox in Cantor’s classical set theory led to
different views on foundations of math, one of which is intuitionism/constructivism.
MORE NUANCED LOGIC
➤ Let P be “I am happy”, and Q “It is not that I am not happy”.
➤ Are they equivalent with each other?
➤ In classical logic, they are indeed equivalent with each other.
➤ In intuitionistic logic, they are not equivalent with each other.
➤ It’s more nuanced than classical logic, allowing us to distinguish the subtle
differences that are ignored in classical logic.
➤ Put another way, intuitionistic logic does not allow the Double Negation Elimination.
asd
3
CONSTRUCTIVE EXISTENCE
➤ Two kinds of reductio ad absurdum:
➤ (1) Assume “not A”, derive a contradiction, and conclude “not not A”.
➤ (2) Assume “not A”, derive a contradiction, and conclude just “A”.
➤ Assume, e.g., there does not exist something satisfying a property P. Assume it leads
to a contradiction. Then (2) allows us to conclude there exists something satisfying P.
➤ This is problematic because we don’t know what that “something” really is, i.e.,
there is no construction of x such that P(x). We only know the pure existence.
➤ How can we know that something exists without knowing what that really is?
asd
4
CONSTRUCTIVE EXISTENCE (CONT’D)
➤ More formally:
➤ Assume that is provable in classical logic (the logic you learned first).
➤ This does not imply that there exists a term such that is provable.
➤ It is no problem in classical logic that there is no such term at all.
➤ But then how can we justify the existence without having no such term?
➤ Intuitionism supports the view that it is totally unjustifiable and unacceptable; i.e.,
if is provable, then there must be such a term that is provable.
➤ In other words: when something exists, we can construct it concretely as a term.
∃xA(x)
c A(c)
∃xA(x) c A(c)
5
CONSTRUCTIVE DISJUNCTION
➤ Assume that “A or B” holds.
➤ Does that mean we know which of A,B actually holds? If we don’t know which one
actually holds, why can we conclude “A or B”?
➤ In intuitionism, “A or B” means either we have a proof of A or we have a proof of B.
➤ Formally: if is provable, either is provable or is provable.
➤ It’s called the disjunction property; the last one the existence property.
➤ NB: existential quantification may be regarded as infinitary disjunction (and
universal quantification as infinitary conjunction).
A ∨ B A B
asd
6
BHK (BROUWER-KOLMOGOROV-HEYTING) INTERPRETATION
➤ is valid iff there are proofs for both and .
➤ is valid iff there is a proof for at least one of and .
➤ is valid iff there is a function (construction; mechanical procedure such as
program) that turns a proof of into a proof .
➤ is valid iff there is a function turning a proof of into a proof of contradiction.
➤ is valid iff there is a term such that is provable.
➤ is valid iff there is a function that turns a term into a proof .
A ∧ B A B
A ∨ B A B
A → B
A B
¬A A
∃xA(x) t A(t)
∀xA(x) t A(t)
asd
7
FACETS OF INTUITIONISM
➤ Intuitionistic logic is the logic of computer science.
➤ Whenever there is a proof in intuitionistic logic, there is a functional program
corresponding to it.
➤ It’s called program extraction from proofs, and studied in the field of
constructive programming.
➤ At the same time, intuitionistic logic is the logic of topology and geometry.
➤ Classical logic is the logic of sets. Intuitionistic logic is the logic of open sets.
8
HISTORY OF INTUITIONISM
➤ Brouwer is the originator of intuitionism and constructive mathematics.
➤ At that time, there were three positions in foundations of mathematics.
➤ Logicism: Russell, Frege, Carnap (with precursors such as Dedekind); all of the
mathematics are reducible to logic; math is independent of the human mind.
➤ Intuitionism: Brouwer (with precursors such as Poincare and Kronecker); math is
a human mental activity; mathematical objects are created by human intuition.
➤ Formalism/finitism: Hilbert; math can be formalised as a symbol manipulation
game, and meaningful math is limited to its finitary part, so that infinitary math
must be grounded upon finitary math, esp. in terms of formal consistency.
asd
9
HISTORY OF INTUITIONISM (CONT’D)
➤ Logicism failed because Frege’s system was proven to be inconsistent and Russell’s
was proven to be incomplete …
➤ … in the sense of the first incompleteness; i.e., there are undecidable propositions in
any finitary proof system if it is expressive enough to include weak arithmetic.
➤ Is there any infinity in between the natural numbers and the real numbers? This is
called Cantor’s Continuum Hypothesis, which is indeed undecidable.
➤ It is not true that all mathematical questions are answered simply by yes or no!
➤ There are some propositions which are not provable, and whose negations are not
provable, either (which is the definition of undecidable propositions).
asd
10
HISTORY OF INTUITIONISM (CONT’D)
➤ Formalism failed because it is impossible to give a finitary proof of the consistency
of math (which is what the second incompleteness tells us).
➤ There are some modern methods to do something similar, though.
➤ Intuitionism did not fail, but was not accepted, neither, esp. in pure mathematics.
➤ It flourished in theoretical computer science, instead.
➤ Intuitionism is revisionism in mathematics while the other twos are not.
➤ Intuitionism requires math to revise its practice and follow more restricted rules.
Some mathematicians supported intuitionism (van der Waerden, H. Weyl, etc.),
but many mathematicians rather supported classical mathematics.
11
PROOF SYSTEM FOR INTUITIONISTIC LOGIC
➤ The intuitionistic sequent calculus: just allow a single conclusion in the sequent
calculus we learned before, so that it’s sequent calculus for intuitionistic logic.
➤ Single-conclusion sequent calculus, from a logical point of view, is arguably more
natural than multiple-conclusion sequent calculus, since arguments in natural
language usually have only one conclusion.
➤ Let’s see what it looks like.
➤ Note that we don’t really need the negation rules, since we have equivalence
between and (even in intuitionistic logic).¬A A → ⊥
asd
12
INTUITIONISTIC SEQ. CAL.
13
X, A ⊢ A
Axiom
X, A, B ⊢ A
X, A ∧ B ⊢ A
∧ ⊢
X2, B ⊢ CX1, A ⊢ C
X1, X2, A ∨ B ⊢ C
∨ ⊢
X ⊢ A
¬ ⊢
X, ¬A ⊢
X1 ⊢ A
X1, X2, A → B ⊢ C
→ ⊢
X2, B ⊢ C
X, A ⊢ B
X, ∀xA ⊢ B
∀ ⊢
X, A ⊢ B
X, ∃xA ⊢ B
∃ ⊢x does not appear as a free variable in X,Y
X2 ⊢ BX1 ⊢ A
X1, X2 ⊢ A ∧ B
⊢ ∧
X ⊢ A
X ⊢ A ∨ B
⊢ ∨
X ⊢ A ∨ B
X ⊢ B
X, A ⊢
⊢ ¬
X ⊢ ¬A
X, A ⊢ B
X ⊢ A → B
⊢ →
X ⊢ A
X ⊢ ∀xA
⊢ ∀ x does not appear as a free variable in X,Y
X ⊢ A
X ⊢ ∃xA
⊢ ∃
X2, A ⊢ BX1 ⊢ A
X1, X2 ⊢ B
Cut
X, ⊥ ⊢ A
⊥ ⊢
X ⊢ ⊤
⊢ ⊤
WHAT PROOFS ARE JUSTIFIED IN INTUITIONISTIC LOGIC?
14
⊢ A ∨ ¬A
⊢ ∨
⊢ A, ¬A
A ⊢ A
⊢ ¬
Ax
⊢ →
⊢ →
Ax
⊢ →
→ ⊢
⊢ ¬ ¬ ⊢
A ⊢ A
Ax
B ⊢ B
Ax
⊢ A → (B → A)
A ⊢ B → A
A, B ⊢ A
¬B → ¬A ⊢ A → B
A, ¬B → ¬A ⊢ B
¬A, A ⊢⊢ ¬B, B
Are they intuitionistic proofs?
EACH CONNECTIVE HAS ITS OWN IRREDUCIBLE MEANING
➤ In classical logic, it suffices to have negation, conjunction, and universal quantifier.
➤ Everything else is definable by combining them in a suitable way.
➤ In intuitionistic logic, any logical connective is not reducible to any others (except for
negation defined as implying falsity).
➤ Each has its own unique irreducible meaning.
➤ Classical logic makes it collapse, and intuitionistically different things become
equivalent (if we allow multiple conclusions in sequent calculus; or add DNE).
15
CONTINUITY PRINCIPLE AND COMPUTABLE ANALYSIS
➤ Brouwer’s intuitionistic mathematics contradicts classical mathematics.
➤ His continuity principle, e.g., asserts that all functions from real numbers to real
numbers are continuous.
➤ There are no discontinuous functions!
➤ This sounds strange, but there is also a classical interpretation of intuitionistic
mathematics (e.g., realisability interpretations as formalising the BHK one).
➤ Computable analysis: all computable functions from reals to reals are continuous.
Computability implies continuity! Intuitionism accepts computable functions only.
➤ NB: computability on real numbers is defined, e.g., by type-two Turing machines.
16
A CONSTRUCTIVE
VIEW OF TRUTH
17
ALTERNATIVE VIEW OF TRUTH
➤ Let’s discuss the intuitionistic conception of truth.
➤ One of the fundamental assumptions underpinning classical logic is the Law of the
Excluded Middle (LEM):
➤ According to this assumption, given any proposition , either is a correct description
of reality or else its negation is. (Dummett: classical logic is the logic of realism.)
p p
⊢ p ∨ ¬p
asd
18
ALTERNATIVE VIEW OF TRUTH (CONT’D)
➤ In light of claims like “there is a table”, we tend to think that the truth value of such
a statement is given by the physical reality.
➤ And the physical reality doesn’t depend on whether or when we investigate the
statements made about it.
➤ This view may be summarised as follows:
➤ We discover truth rather than create truth.
➤ However, when we consider applying such a view to other uses of language, it
becomes hardly convincing.
19
asd
ALTERNATIVE VIEW OF TRUTH (CONT’D)
➤ Take mathematics as an example, the view that we merely discover truth suggests a
unified mathematical reality exists “out there” independent of our mathematical
theories. This sounds strange sometimes:
We can easily make statements and reason about a three-element set. But did
ancient mathematician or Cantor (originator of set theory) discover such a set in
some existing mathematics universe?
Moreover, the law of excluding middle dictates that there is an answer to every
question. This seems quite impossible in the domain of mathematics.
The continuum hypothesis indeed is neither provable nor refutable.
There are actually no answers to many questions regarding large infinities.
20
INTUITIONISTIC THREE-VALUED MODEL
➤ Truth is not given by the nature of “stuff out there” but rather constructed by us as
we go along.
➤ Building upon this intuitionist view, let’s consider a very much simplified version of
intuitionistic logic:
For any proposition there are two stages: Before investigation and after
investigation.
We think of investigating a proposition as constructing “more truth”.
asd
21
INTUITIONISTIC THREE-VALUED MODEL (CONT’D)
➤ Then we have three truth values for a proposition:
T true both before and after investigation
i indeterminate before, true after
F never true
➤ The conjunction and disjunction are interpreted as follows:
∧ T i F
T
i
F
T i F
i i F
F F F
∨ T i F
T
i
F
T T T
T i i
T i F asd
22
INTUITIONISTIC THREE-VALUED MODEL (CONT’D)
➤ Intuitionistic implication is different from any of relevant and fuzzy implications.
23
→ T i F
T
i
F
T i F
T T F
T T T
T
i
F
F
F
T
¬AA
asd
INTUITIONISTIC THREE-VALUED MODEL (CONT’D)
➤ How to interpret quantifiers?
➤ The domain may expand as more objects are constructed.
➤ Once an object is constructed, it cannot be destroyed.
Before it is constructed, however, it is does not exist.
➤ Platonistically, everything already exists in the Platonist universe, but intuitionism
does not accept such a pre-existing, immutable, universal Platonist universe.
Everything must be constructed at some point (if we want it to exist).
24
asd
INTUITIONISTIC THREE-VALUED MODEL (CONT’D)
➤ The universal quantifier is interpreted as referring to all entities that exists now and
in the future (and in the past).
is saying all the s are s but it also includes any future F which
has not yet been constructed.
➤ The existential quantifier, on the other hand, is interpreted as saying that something
satisfying a description exists at present (rather than in the future).
∀(x : Fx) Gx F G
25
asd
INTUITIONISTIC THREE-VALUED MODEL (CONT’D)
➤ A sequent is valid on the intuitionistic three-valued semantics iff every
interpretation that makes every formula in X true also makes A true.
➤ is not valid (recall that it was valid in the relevant and fuzzy logics):
Consider:
1. Assign the value of i.
2. now has a value of F.
3. Therefore has value T, but has a value of i.
X ⊢ A
¬¬p ⊢ p
p
¬p
¬¬p p
26
asd
27
➤ Many classical valid sequents are no longer valid for similar reasons:
VARIOUS LAWS BECOME INVALID
⊢ p ∨ ¬p
¬p → q ⊢ p ∨ q
¬p → q ⊢ ¬q → p
(p → q) → p ⊢ p
¬∀x¬Fx ⊢ ∃xFx
∀x (Fx ∨ Gx) ⊢ ∀xFx ∨ ∃xGx
asd
INTUITIONISTIC NATURAL DEDUCTION
➤ We can obtain a natural deduction system for intuitionistic logic in two steps:
➤ First, we remove from the classical system the DNE rule .
We can also regard negation as a defined connective: means .
and then become special cases of and .
➤ Second, we obtain intuitionistic natural deduction by adding a rule for the falsity ,
which intuitively represents a contradictory proposition:
The new rule for says the falsity (contradiction) implies any formula .
NB: it’s not paraconsistent, due to this rule.
¬¬E
¬A A → ⊥
¬I ¬E → I → E
⊥
⊥ ⊥ A
28
asd
INTUITIONISTIC NATURAL DEDUCTION (CONT’D)
➤ All rules in classical natural deduction except for remain valid in intuitionistic
logic.
➤ Every classical proof of an intuitionistically invalid sequent depends upon .
➤ Remarks: to be precise, “intuitionistic” and “constructive” are slightly different, but
it does not matter here.
➤ Intuitionistic logic is constructive, but there are some other constructive logics.
➤ At the same time, there are intuitionistic versions of both relevant and fuzzy logics
➤ They made the double negation elimination valid, but we can remove it (or just
allow single conclusions in sequent calculus), so that they become intuitionistic.
¬¬E
¬¬E
29
asd
CONSISTENCY STRENGTH
➤ Are you an intuitionist or classicist?
➤ Intuitionistic math is generally more robust to inconsistency than classical math (cf.
double negation interpretation), but Hilbert was strongly against intuitionism, and
even excluded Brouwer from the best math journal at that time.
➤ Even if classical math is inconsistent, intuitionistic math can still be consistent.
➤ Hilbert: “Taking the principle of excluded middle from the mathematician would be
the same, say, as proscribing the telescope to the astronomer or to the boxer the use
of his fists. To prohibit existence statements and the principle of excluded middle is
tantamount to relinquishing the science of mathematics altogether.”
asd
30
REACTIONS TO INCONSISTENCY OF CANTOR’S SET THEORY
asd
31
LOGICAL BASIS OF METAPHYSICS
➤ Michael Dummett, arguably the greatest British philosopher in the second half of
the twentieth century, developed his metaphysics on the basis of intuitionistic logic.
asd
32https://opinionator.blogs.nytimes.com/2012/01/04/remembering-michael-dummett/
Realism vs. Antirealism Classical vs. Intuitionistic Logic
cf. Denotationalism vs. Inferentialism
Michael Dummett is a precursor of
Proof-Theoretic Semantics.