Torn between classical and constructive mathematics

What is the basis for reason? And mathematics?

Moderators: AMod, iMod

godelian
Posts: 2742
Joined: Wed May 04, 2022 4:21 am

Re: Torn between classical and constructive mathematics

Post by godelian »

Skepdick wrote: Sat Apr 12, 2025 7:54 am Not all subsets of countable sets are countable.
That sounds very counter-intuitive, but apparently, it is a common result in constructive mathematics:
ChatGPT: Is it possible to axiomatically construct a set theory in which not all subsets of a countable set are countable?

Yes, it is possible to construct a set theory in which not all subsets of a countable set are countable, depending on what axioms you adopt — especially regarding the Axiom of Choice (AC) and Power Set Axiom, and how you interpret "countable."

Let's unpack this carefully.

🚩 First, some context and definitions:
A set is countable if it's finite or has the same cardinality as the natural numbers N.
The set N is countable (obviously).
In standard ZFC (Zermelo–Fraenkel with Choice), there exist uncountable subsets of N only if we're talking about subsets of the power set of N — i.e., the power set P(N) is uncountable.
But every individual subset of N is countable (being a subset of a countable set).

❓What does your question really ask?

You’re asking whether it’s possible to axiomatize a set theory where:
N is countable, but
Not all of its subsets are countable, meaning some subsets of a countable set (like N) are uncountable.
This would mean that the set of all subsets of N includes uncountable subsets, despite N being countable.

In ZFC, this is not the case — all subsets of N are themselves at most countable, even though P(N) (the full power set) is uncountable.

✅ The answer is YES, but with caveats.

You can build alternative set theories (often called non-classical set theories) where such a phenomenon could occur, but they require changing foundational assumptions.

Some options:

🔹 1. Dropping the Axiom of Choice (ZF instead of ZFC):
In ZF (without Choice), it's possible that certain subsets of a countable set are not explicitly constructible or not provably countable.
Without AC, "every subset of a countable set is countable" is not provable.
There are models of ZF in which there exists a Dedekind-infinite set (i.e., infinite in the sense of injections) that is not countably infinite in the usual sense.
So some subsets of N might not be countable in such a model.

Still, each such subset is at most countable in cardinality — it's just that you can't construct a bijection with N for it.

🔹 2. Alternative Set Theories (e.g., NFU, Constructive Set Theory, etc.):
In New Foundations with Urelements (NFU) or Constructive Zermelo–Fraenkel (CZF) set theory, different behavior can emerge.
For instance, in Constructive Set Theory, not all subsets of N are necessarily sets in the traditional sense — so some may not be countable (constructively).
These theories reject or weaken the Power Set Axiom and/or the Axiom of Choice, allowing unusual behaviors with subsets of countable sets.

🔹 3. Nonstandard Models / Forcing / Relative Consistency Results:
You can use forcing (from model theory) to construct models of ZF (or ZFC) in which the set of reals is countable, or in which we can’t well-order all subsets of N.
In these models, N remains countable, but P(N) can behave strangely.
You can force models in which certain subsets of N are not countable in the model, even though they are externally.

🔹 4. Constructive or Predicative Mathematics:
In predicative mathematics or intuitionistic logic, certain subsets of N might not be countable because they aren't constructible in a specific sense. You can even say that not all subsets exist as completed totalities — so uncountability emerges for a different reason.

🧠 Summary:

Yes — in certain axiomatic systems that differ from classical ZFC, it's possible to construct a theory in which some subsets of a countable set (like N) are uncountable, especially if you reject or modify:

The Axiom of Choice,
The Power Set Axiom,
Or classical logic itself.

Would you like to explore an example of such a set theory or a model where this happens?

Awesome — let's dive into a concrete example. One of the most interesting and accessible examples comes from constructive set theory, especially when paired with intuitionistic logic and a rejection of the full Power Set Axiom. A good starting point is:

🔹 Example: Subsets of N in Constructive Zermelo–Fraenkel Set Theory (CZF)

In CZF, we do not assume:
The Power Set Axiom, and
The Law of Excluded Middle (so we use intuitionistic logic instead of classical logic).

As a result, the landscape of subsets of N changes dramatically.

📌 What's Different in CZF?

In CZF:
A set of natural numbers A⊆NA⊆N is only a set if it can be explicitly constructed — e.g., by giving a rule or generating procedure.
The total collection of all subsets of N, P(N), does not exist as a set — it's only a proper class (or a "collection").
So while each individual subset may still be countable, there isn't a set of all of them, and not all of them are constructible.
Uncountable collections of subsets of N can exist as classes that do not have a well-defined cardinality.

⚡ Key Consequence:

There exist subsets of N that:
Are not enumerable in the constructive sense,
Cannot be shown to be countable (i.e., no constructively valid bijection to N),
And yet are subsets of a countable set.
So, from a classical ZFC perspective: "Of course they're countable!"
But from a constructive CZF viewpoint, these subsets are not countable, since there’s no constructive method to enumerate them.

🧪 Example of a Non-countable Subset in CZF

Let’s consider the set:
A={n∈N∣P(n)}
Where P(n) is some non-decidable property — like:
"The Turing machine with code n halts on input n" (i.e., the Halting Problem).
In classical logic, this still defines a subset of N, even if we can't compute it. But in constructive logic, we can’t prove that such a set is countable because we lack a constructive method to list its elements.
Hence, in CZF:
The set A exists as a subclass of N,
But it is not countable — because we can't construct a surjection from N to A,
Even though it’s a subset of a countable set.

📚 The Technical Language

In CZF, “countable” typically means "inhabited set with a surjection from N" (constructively given). So if such a function cannot be constructed, the set is not countable — even if it’s a subset of N.

This creates a model where:
✅ N is countable
❌ Not all subsets of N are countable (in the constructive sense)
Skepdick
Posts: 16022
Joined: Fri Jun 14, 2019 11:16 am

Re: Torn between classical and constructive mathematics

Post by Skepdick »

godelian wrote: Sat Apr 12, 2025 9:05 am
Skepdick wrote: Sat Apr 12, 2025 7:54 am Not all subsets of countable sets are countable.
That sounds very counter-intuitive, but apparently, it is a common result in constructive mathematics:
How is it "counter intuitive"? It's so intuitively and trivially true....

The set of all Turing machines is countable.
The subset of non-halting Turing machines isn't.

A classical. mathematician simply tells you "It's countable because there's a bijection to N". But they can't construct the bijection without solving the halting problem first.

Those wankers think they are omniscient.
godelian
Posts: 2742
Joined: Wed May 04, 2022 4:21 am

Re: Torn between classical and constructive mathematics

Post by godelian »

Skepdick wrote: Sat Apr 12, 2025 9:18 am
godelian wrote: Sat Apr 12, 2025 9:05 am
Skepdick wrote: Sat Apr 12, 2025 7:54 am Not all subsets of countable sets are countable.
That sounds very counter-intuitive, but apparently, it is a common result in constructive mathematics:
How is it "counter intuitive"? It's so intuitively and trivially true....

The set of all Turing machines is countable.
The subset of non-halting Turing machines isn't.

A classical. mathematician simply tells you "It's countable because there's a bijection to N". But they can't construct the bijection without solving the halting problem first.

Those wankers think they are omniscient.
The subset of non-halting Turing machines is indeed uncomputable. So, the question is rather what "countable" means in this context. There are other uncomputable sets that are seemingly countable: Kolmogorov-Random numbers, a natural number n is Kolmogorov-random if the shortest program (in some fixed universal Turing machine) that outputs n is at least as long as n itself; Diophantine Equations with No Solution. Most examples mentioned in the search results seem to be related to the halting problem. If you can't know how many but if you could, it would be a natural number, then it is both countable and uncomputable; depending on the definition of "countable", of course.
Skepdick
Posts: 16022
Joined: Fri Jun 14, 2019 11:16 am

Re: Torn between classical and constructive mathematics

Post by Skepdick »

godelian wrote: Sat Apr 12, 2025 9:36 am The subset of non-halting Turing machines is indeed uncomputable. So, the question is rather what "countable" means in this context.
It means the same thing any 5 year old would understand it to mean if I told them to count all the non-red balls in a bag.
Pick out all the non-halting TMs in the "bag" of Turing Machines and count them.

That's why it's called intuitionism.

In the same way a blind person can't perform the task because they can't discern red from non-red; classical mathematicians have a problem.

We must know. We will know. My ass.
You won't know. You can't know!

The set theoretic notion of "countability" is a perfect case of "Professing themselves to be wise, they became fools". Set-theoretic notions of countability is nothing but empty intellectual pride that's disconnected from meaningful mathematics.
godelian
Posts: 2742
Joined: Wed May 04, 2022 4:21 am

Re: Torn between classical and constructive mathematics

Post by godelian »

Skepdick wrote: Sat Apr 12, 2025 9:47 am
godelian wrote: Sat Apr 12, 2025 9:36 am The subset of non-halting Turing machines is indeed uncomputable. So, the question is rather what "countable" means in this context.
It means the same thing any 5 year old would understand it to mean if I told them to count all the non-red balls in a bag.
Pick out all the non-halting TMs in the "bag" of Turing Machines and count them.

That's why it's called intuitionism.

In the same way a blind person can't perform the task because they can't discern red from non-red; classical mathematicians have a problem.

We must know. We will know. My ass.
You won't know. You can't know!

The set theoretic notion of "countability" is a perfect case of "Professing themselves to be wise, they became fools".
I accept the concerns voiced by constructive mathematics about practices in classical mathematics on a case-by-case basis.
Skepdick
Posts: 16022
Joined: Fri Jun 14, 2019 11:16 am

Re: Torn between classical and constructive mathematics

Post by Skepdick »

godelian wrote: Sat Apr 12, 2025 10:09 am I accept the concerns voiced by constructive mathematics about practices in classical mathematics on a case-by-case basis.
This is a particular case; isn't it?

On classical mathematics all subsets of countable sets are countable.
It's not even subject to LEM on case-by-case basis e.g any given subset of a countable set is either countable; or not.

It's that the left disjunct applies to ALL subsets of countable sets. Even to the subsets you can't actually count.
godelian
Posts: 2742
Joined: Wed May 04, 2022 4:21 am

Re: Torn between classical and constructive mathematics

Post by godelian »

Skepdick wrote: Sat Apr 12, 2025 10:15 am
godelian wrote: Sat Apr 12, 2025 10:09 am I accept the concerns voiced by constructive mathematics about practices in classical mathematics on a case-by-case basis.
This is a particular case; isn't it?

On classical mathematics all subsets of countable sets are countable.
It's not even subject to LEM on case-by-case basis e.g any given subset of a countable set is either countable; or not.

It's that the left disjunct applies to ALL subsets of countable sets. Even to the subsets you can't actually count.
It's more a problem of vocabulary.

"Countable" mathematics is a synonym for discrete mathematics. So, all sets in discrete mathematics are "countable" but may not be computable.
Skepdick
Posts: 16022
Joined: Fri Jun 14, 2019 11:16 am

Re: Torn between classical and constructive mathematics

Post by Skepdick »

godelian wrote: Sat Apr 12, 2025 11:19 am
Skepdick wrote: Sat Apr 12, 2025 10:15 am
godelian wrote: Sat Apr 12, 2025 10:09 am I accept the concerns voiced by constructive mathematics about practices in classical mathematics on a case-by-case basis.
This is a particular case; isn't it?

On classical mathematics all subsets of countable sets are countable.
It's not even subject to LEM on case-by-case basis e.g any given subset of a countable set is either countable; or not.

It's that the left disjunct applies to ALL subsets of countable sets. Even to the subsets you can't actually count.
It's more a problem of vocabulary.

"Countable" mathematics is a synonym for discrete mathematics. So, all sets in discrete mathematics are "countable" but may not be computable.
Nothing to do with vocabulary and everything to do with cognition.

Discrete or not - you can’t count something you cannot identify e.g the non-red balls in a bag if you are blind.

You can’t even count the numbers in an arbitrary set when you don’t know what a number is!

You lack the prerequisite information necessary to perform the count.

This is a functional, not a linguistic limitation.

I will grant you the axiom of infinite choice and you still can’t count the things you can’t identity
godelian
Posts: 2742
Joined: Wed May 04, 2022 4:21 am

Re: Torn between classical and constructive mathematics

Post by godelian »

Skepdick wrote: Sat Apr 12, 2025 12:49 pm Discrete or not - you can’t count something you cannot identify e.g the non-red balls in a bag if you are blind.
Is an unknown natural number countable in the sense of being discrete? Yes, even if you don't know its actual value.

In my opinion, it is the same for unknowable natural numbers. The fact that a value is unknowable, does not change its type. You can know a variable's type without knowing its value.

There's not that much difference between "unknown" and "unknowable" in respect to the type of a variable.

In that sense, all subsets of natural numbers are countable, in the sense of discrete; unknown ones too, and even unknowable ones.
godelian
Posts: 2742
Joined: Wed May 04, 2022 4:21 am

Re: Torn between classical and constructive mathematics

Post by godelian »

Skepdick wrote: Sat Apr 12, 2025 7:54 am It is deductively closed. Because the internal language of a topos is higher order intuitionistic logic.
If you copy realizable programs into the realizability topos/chroot, you will trivially be able to script your way out of the topos/chroot. So, the topos/chroot is not "computationally" closed.

The language may be deductively-closed but not the topos/chroot. If premises are true then its deductive consequences are indeed also true. However, if programs are realizable, it does not necessarily mean that their "computational combination" is realizable.

For example, the "set of subsets" program will not be realizable, if you apply it to the realizable/countable set of reals.

You can trivially escape the realizability topos/chroot, because you can still end up trying to output ineffable objects.
godelian
Posts: 2742
Joined: Wed May 04, 2022 4:21 am

Re: Torn between classical and constructive mathematics

Post by godelian »

Skepdick wrote: Sat Apr 12, 2025 12:49 pm You can’t even count the numbers in an arbitrary set when you don’t know what a number is!
Well, for example, the type of the cardinality of the set halting Turing machines is a natural number. You do not need to actually count them to assert this. The axiom of choice is also perfectly sustainable because you can pinpoint at least one machine in the set.
Skepdick
Posts: 16022
Joined: Fri Jun 14, 2019 11:16 am

Re: Torn between classical and constructive mathematics

Post by Skepdick »

godelian wrote: Sun Apr 13, 2025 1:19 am
Skepdick wrote: Sat Apr 12, 2025 12:49 pm Discrete or not - you can’t count something you cannot identify e.g the non-red balls in a bag if you are blind.
Is an unknown natural number countable in the sense of being discrete? Yes, even if you don't know its actual value.

In my opinion, it is the same for unknowable natural numbers. The fact that a value is unknowable, does not change its type. You can know a variable's type without knowing its value.


There's not that much difference between "unknown" and "unknowable" in respect to the type of a variable.

In that sense, all subsets of natural numbers are countable, in the sense of discrete; unknown ones too, and even unknowable ones.
That doesn't work in dependent type theory - all types depend on values.

Members of sets aren't countable as "numbers" if you don't know that any given element is a number.

take the set {"a", "b", "c", 1, 2, 3}. If I told you that x is in that set is x a number?

I can tell you the cardinality of the set. The subset of numbers isn't countable unless you can construct that subset first. By identifying the relevant elements.
Skepdick
Posts: 16022
Joined: Fri Jun 14, 2019 11:16 am

Re: Torn between classical and constructive mathematics

Post by Skepdick »

godelian wrote: Sun Apr 13, 2025 3:43 am
Skepdick wrote: Sat Apr 12, 2025 12:49 pm You can’t even count the numbers in an arbitrary set when you don’t know what a number is!
Well, for example, the type of the cardinality of the set halting Turing machines is a natural number. You do not need to actually count them to assert this.
Yeah. And? You don't count types - you count values.

The type of the cardinality of the set of non-red balls is a natural number.

Still can't count them if you can't evaluate whether any given ball you've chosen is red or not.
godelian wrote: Sun Apr 13, 2025 3:43 am The axiom of choice is also perfectly sustainable because you can pinpoint at least one machine in the set.
OK. And? Having picked out a machine from the set hasn't helped you determine if that particular machine is a member of the non-halting.

So do you count it; or not?
Skepdick
Posts: 16022
Joined: Fri Jun 14, 2019 11:16 am

Re: Torn between classical and constructive mathematics

Post by Skepdick »

godelian wrote: Sun Apr 13, 2025 1:48 am If you copy realizable programs into the realizability topos/chroot, you will trivially be able to script your way out of the topos/chroot. So, the topos/chroot is not "computationally" closed.

The language may be deductively-closed but not the topos/chroot. If premises are true then its deductive consequences are indeed also true. However, if programs are realizable, it does not necessarily mean that their "computational combination" is realizable.
I have no idea what that means. Proofs don't output anything.

When the proof is correct and it passes type-checking and terminates.
There are no IO/effects on success.
Only on errors.

Here's the proof.

Code: Select all

module OnePlusOneIsTwo where

-- Define natural numbers
data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

-- Define addition
_+_ : ℕ → ℕ → ℕ
zero + n = n
suc m + n = suc (m + n)

-- Define 1 and 2
one : ℕ
one = suc zero

two : ℕ
two = suc one

-- Define propositional equality
data _≡_ {A : Set} : A → A → Set where
  refl : {x : A} → x ≡ x

infixl 6 _+_
infix 4 _≡_

-- Proof that 1+1=2
one-plus-one-is-two : (one + one) ≡ two
one-plus-one-is-two = refl
Here's the exit code...

Code: Select all

❯ agda OnePlusOneIsTwo.agda && echo $?
0
OK... 1+1=2 is a theorem in this construction.

What computational output do you expect?
godelian wrote: Sun Apr 13, 2025 1:48 am For example, the "set of subsets" program will not be realizable, if you apply it to the realizable/countable set of reals.

You can trivially escape the realizability topos/chroot, because you can still end up trying to output ineffable objects.
The powerset of a countable set is just an infinite datastream.
godelian
Posts: 2742
Joined: Wed May 04, 2022 4:21 am

Re: Torn between classical and constructive mathematics

Post by godelian »

Skepdick wrote: Sun Apr 13, 2025 2:08 pm The subset of numbers isn't countable unless you can construct that subset first..
The type for the cardinality of a subset of the natural numbers is a natural number. You do not need to construct that subset first.
Skepdick wrote: Sun Apr 13, 2025 2:08 pm take the set {"a", "b", "c", 1, 2, 3}. If I told you that x is in that set is x a number?
It's not about the type of the elements. It is about the type of the cardinality. Your set has 6 elements, and 6 is a natural number. It does not matter of what type the elements are. If you add x, then the cardinality of that set will be 7 instead of 6. It is immaterial what x exactly is.
Skepdick wrote: Sun Apr 13, 2025 2:21 pm Having picked out a machine from the set hasn't helped you determine if that particular machine is a member of the non-halting.
There are programs that are guaranteed to halt, such as the empty program. There are also programs that are guaranteed not to halt, such as "while(true);". So, you can always pick one program from the halting set and one program from the non-halting set. Hence, the axiom of choice is sustainable in that context.
Skepdick wrote: Sun Apr 13, 2025 2:29 pm The powerset of a countable set is just an infinite datastream.
Most elements in the powerset of a countable infinite set -- which is uncountable -- are ineffable. They cannot be expressed in language. So, most of the elements of such powerset cannot participate in that infinite datastream. Hence, the topos of realizability is not computationally closed. It is trivially easy to produce ineffable objects in the topos, regardless of how carefully you copy programs/constructs into its "chroot".
Post Reply