1Proof theory and constructive logic
III Logic
1.5 Constructive mathematics
We now end with some remarks about how we can do mathematics “construc-
tively”, and the subtleties we have to be careful of.
We first discuss the notion of finiteness. Even classically, if we do not have
the axiom of choice, then we have many distinct notions of “finite set”. When
we go constructive, things get more complicated.
We can produce (at least) two different definitions of finiteness.
Definition
(Kuratowski finite)
.
We define “finite” recursively:
∅
is Kuratowski
finite. If x is Kuratowski finite, then so is x ∪ {y}.
There is a separate definition of N-finiteness:
Definition
(
N
-finite)
. ∅
is
N
-finite. If
x
is
N
-finite, and
y 6∈ x
, then
x ∪ {y}
is
N-finite.
These two definitions are not the same! In a
N
-finite set, we know any
two things are either equal, or they are not, as this is built into the definition
of an
N
-finite set. However, in the case of Kuratowski finite, this is not true,
since we don’t have the law of excluded middle. We say
N
-finite sets have
decidable equality. If we want to do constructive arithmetic, the correct notion
is N-finiteness.
We can still define natural numbers as the smallest set containing
∅
and is
closed under successor. This gives us
N
-finite sets, but the least number principle
is dodgy. It turns out the least number principle implies excluded middle.
There are also subtleties involving the notion of a non-empty set!
Definition (Non-empty set). A set x is non-empty if ¬∀
y
y 6∈ x.
Definition (Inhabited set). A set x is inhabited if ∃
y
y ∈ x.
They are not the same! Being inhabited is stronger than being non-empty!
We shall not go into more details about constructive mathematics, because,
disappointingly, very few people care.