The position of constructive mathematics on the axiom of infinity is outright unsustainable

[Skepdick]

I have no clue. I don't know more about this particular error message than what the various AI agents have compiled from their databases. They merely insist that the other error messages and error reasons such as "undecidable" or "uncomputable" are not applicable to this corner case.

That's just backwards logic.

It's not that something is not applicable to "this corner case"

It's that corner cases emerge precisely when the decidable suddenly becomes undecidable, the defined suddenly become undefined, the knowable suddenly becomes unknowable.

The property loss creates the corner case, not the other way around.

There is no principled reason for this sudden amnesia when an infinite set is "completed"

[godelian]

It's not that something is not applicable to "this corner case"

Countable infinity, ℵ₀, literally is a corner case. It is the boundary that you reach after traversing all the natural numbers.

There is nothing that guarantees that the usual arithmetic operators would still function under the same rules in this corner.

For example, the addition operator starts absorbing in this corner:

ℵ₀ + 1 = ℵ₀

It blocks further progression.

We can still see some things on the map when reaching ℵ₀ but it is clear that not everything that worked over the natural numbers, still works for ℵ₀.

[Skepdick]

It's not that something is not applicable to "this corner case"

Countable infinity, ℵ₀, literally is a corner case. It is the boundary that you reach after traversing all the natural numbers.

Did you even read my whole post instead of cherry-picking out bits?

It's a corner-case of your own making! A corner case that does not exist right until you invent the "boundary"; and pretend to have crossed over it.

The "boundary" isn't a mathematical necessity. It's an artificial construct created by treating open sets as completed totalities.

There is nothing that guarantees that the usual arithmetic operators would still function under the same rules in this corner.

For example, the addition operator starts absorbing in this corner:

ℵ₀ + 1 = ℵ₀

It blocks further progression.

Geewiz! The insight! When you change the rules the old rules no longer apply?!?!

When you invent an imaginary boundary the successor function loses its meaning?!?

Who would've thought?

We can still see some things on the map when reaching ℵ₀ but it is clear that not everything that worked over the natural numbers, still works for ℵ₀.

But can you see it clearly that ℵ₀ doesn't exist? Except as a non-terminating datastream. The flow-rate of the datastream is what ℵ₀ is!

Isn't it poetic that that ℵ₀ is somehow real enough to have a special property like absorption, but not real enough to have basic properties like parity?
Somehow, magically - you discovered a fixed point to absorb addition.

Speaking of which do you remember my fixed point?
The one that absorbs everything, including the powerset?

[godelian]

The "boundary" isn't a mathematical necessity. It's an artificial construct created by treating open sets as completed totalities.

PA does not support that but ZFC does.

The practice is so firmly ingrained in calculus and algebra, that I do not really see an alternative.

[Skepdick]

The "boundary" isn't a mathematical necessity. It's an artificial construct created by treating open sets as completed totalities.

PA does not support that but ZFC does.

The practice is so firmly ingrained in calculus and algebra, that I do not really see an alternative.

No, the practice is not ingrained. Only the theory is ingrained. In Mathematics departments.

If you actually pay attention to how actual practitioners (like physicists) do mathematics you will actually realize they are; in fact; doing intuitionistic mathematics. They have completely abandoned the rules/instruction they were indoctrinated with for pragmatic reasons.

So "the battle" isn't really over anything practical. In practice nothing changes.
"The Battle" is literally over the difference between how Mathematics is taught vs how Mathematics is actually done in science.

Theory vs practice.

https://math.andrej.com/2008/08/13/intu ... r-physics/

[godelian]

No, the practice is not ingrained. Only the theory is ingrained. In Mathematics departments.

In my opinion, they are not dishonest.

For example, let's look at the Basel problem, first proposed by Pietro Mengoli in 1644 and solved by Leonhard Euler in 1734:

∑(n=1,∞) 1/n² = π²/6

The summation on the left-hand side would not make sense, if it does not terminate somehow. So, this problem only makes sense, if in some Platonic realm, the summation process actually does terminate.

Now, the problem is that a proof must be verifiable by physical computation. That is why the number of computation steps in the proof must be finite. Hence, we cannot prove the Basel identity by trying to execute an infinite number of Platonic computation steps, because in that case the physical verification will not terminate.

So, we have to devise a judicious workaround that will terminate in a finite number of physical computation steps.

Leonard Euler noticed that sin(x)/x has at least two alternative infinite expansions: (1) Its Taylor polynomial expansion (2) What would later become known as its Weierstrass product expansion. By equating the term in x² in both expansions, he obtains the solution. Hence, Euler managed to verify the infinite Platonic sum in a finite number of physical computation steps.

This kind of algebra does not make sense, if infinite sums do not terminate. They only do, if we can truly traverse the natural numbers from start to finish. Infinite sums do terminate, and we can traverse the natural numbers from start to finish, but only in the Platonic realm.

[Skepdick]

No, the practice is not ingrained. Only the theory is ingrained. In Mathematics departments.

In my opinion, they are not dishonest.

For example, let's look at the Basel problem, first proposed by Pietro Mengoli in 1644 and solved by Leonhard Euler in 1734:

∑(n=1,∞) 1/n² = π²/6

The summation on the left-hand side would not make sense, if it does not terminate somehow. So, this problem only makes sense, if in some Platonic realm, the summation process actually does terminate.

Now, the problem is that a proof must be verifiable by physical computation. That is why the number of computation steps in the proof must be finite. Hence, we cannot prove the Basel identity by trying to execute an infinite number of Platonic computation steps, because in that case the physical verification will not terminate.

So, we have to devise a judicious workaround that will terminate in a finite number of physical computation steps.

Leonard Euler noticed that sin(x)/x has at least two alternative infinite expansions: (1) Its Taylor polynomial expansion (2) What would later become known as its Weierstrass product expansion. By equating the term in x² in both expansions, he obtains the solution. Hence, Euler managed to verify the infinite Platonic sum in a finite number of physical computation steps.

This kind of algebra does not make sense, if infinite sums do not terminate. They only do, if we can truly traverse the natural numbers from start to finish. Infinite sums do terminate, and we can traverse the natural numbers from start to finish, but only in the Platonic realm.

Look dude. This conversation is not going anywhere. We are operating from very different fundamentals.

And that stuff is all under the floorboards, festering. Getting in the way of true understanding.

In constructive mathematics the apartness relation (≠, or is it #? symbols! symbols! what do they mean?) is more fundamental than equality.

The default position is; in fact that x ≠ x is ALWAYS false (which does NOT mean it's true!); so x = y requires positive proof of equality; and x # y requires positive proof of apartness. Absent of which the default holds - which is x is neither apart nor unequal to y. x and y are NOT related!

This is where classical logic sneaks in: Absent any evidence of distinctness then they are NOT distinct e.g -(x # y).
Absent evidence of distinctness we simply don't know if they're distinct or not (constructive reasoning retains uncertainty).
Whereas classical reasoning jumps to certainty: absence of evidence is evidence of absence. They are NOT distinct e.g they are identical.

Absence of proof is not proof of absence!

The debate as to whether an "infinite sum terminates" is downstream from there and it's purely proof theoretic.
It terminates IF you accept some axiom(s)
It doesn't terminate IF you don't accept some axiom(s)

It all depends on your foundational assumptions about what mathematics even is. Different axiom systems create different mathematical universes.

[godelian]

The debate as to whether an "infinite sum terminates" is downstream from there and it's purely proof theoretic.
It terminates IF you accept some axiom(s)
It doesn't terminate IF you don't accept some axiom(s)

It all depends on your foundational assumptions about what mathematics even is. Different axiom systems create different mathematical universes. Sometimes these universes have objects that behave similarly enough that we use the same names for them, but they're not necessarily "the same" object in any meaningful sense.

The Basel identity is provable from ZFC.

ChatGPT: Does the solution for the Basel problem rest on the axiom of infinity?

Why the Axiom of Infinity is required

The Axiom of Infinity is one of the axioms of ZFC (and many other foundational systems). It states that there exists an infinite set — usually taken to be the set of natural numbers N.

This axiom is foundational for:
Defining infinite sequences
Defining limits via sequences or series
Formalizing real analysis, including the real numbers R, which are constructed using infinite processes (e.g., Dedekind cuts or Cauchy sequences of rationals)

This involves:
Quantification over all natural numbers (an infinite set)
Taking the limit of partial sums, which involves reasoning about infinite sequences
The use of π, which is a transcendental real number defined via infinite processes (like the limit of a series, or a solution to a transcendental equation)
Thus, none of this is possible without assuming the existence of infinite sets — i.e., the Axiom of Infinity.

Could you prove the Basel problem without the Axiom of Infinity?
No — at least not in full generality or rigor.

So, let's get back to the main point. Algebra and calculus, as we know it today, rest on ZFC and its Axiom of Infinity. You can try to use other axiom systems but they won't be able to prove the same theorems.

[Skepdick]

The Basel identity is provable from ZFC.

Sigh. It's not an identity. It's an equality.

It's a theorem in ZFC.

The "=" symbol here is doing heavy lifting - it's invoking all the ZFC machinery about limits, real numbers, convergence, etc.

So, let's get back to the main point. Algebra and calculus, as we know it today, rest on ZFC and its Axiom of Infinity. You can try to use other axiom systems but they won't be able to prove the same theorems.

No, they don't. I am doing algebra without any axiomatic baggage - the fundamental algebraic manipulations are more primitive than set-theoretic foundations.

And you can do calculus using synthetic differential geometry. It uses infinitesimals as primitive entities. It uses topos theory, not ZFC as its foundation; and it does direct geometric reasoning, not ε-δ limits

You are treating ZFC as some kind of mathematical necessity; when it's just a historical coincidence.

But seriously! Did you even bother to read/understand the link I pasted or are you just shooting from the hip?

the potential existence of non-zero infinitesimals, prove the fundamental theorem of calculus in two lines

And now back to the question of whether mathematics is invented or discovered... It's SYNTHETIC!

[godelian]

No, they don't. I am doing algebra without any axiomatic baggage - the fundamental algebraic manipulations are more primitive than set-theoretic foundations.

And you can do calculus using synthetic differential geometry. It uses infinitesimals as primitive entities. It uses topos theory, not ZFC as its foundation; and it does direct geometric reasoning, not ε-δ limits

You are treating ZFC as some kind of mathematical necessity; when it's just a historical coincidence.

But seriously! Did you even bother to read/understand the link I pasted or are you just shooting from the hip?

the potential existence of non-zero infinitesimals, prove the fundamental theorem of calculus in two lines

And now back to the question of whether mathematics is invented or discovered... It's SYNTHETIC!

My own goal is to (mostly) understand mathematical literature when I run into it. I do not try to discover new theorems or even new axiom systems.

ChatGPT: Does mathematical literature assumes ZFC by default?

Yes, most modern mathematical literature assumes ZFC (Zermelo–Fraenkel set theory with the Axiom of Choice) as the default foundational framework unless stated otherwise. Here’s a breakdown of why and how this works:

Why ZFC is the Default
Standardization: ZFC provides a well-understood and widely accepted foundation for nearly all of classical mathematics.
Expressiveness: It is powerful enough to formalize the majority of mathematical objects and arguments (numbers, functions, spaces, etc.).
Consensus: Most mathematicians working in fields like analysis, algebra, topology, and number theory take ZFC for granted without stating it explicitly.

When ZFC is Not Assumed
There are cases where the literature explicitly uses a different foundation, for example:
Category theory or type theory (e.g. Homotopy Type Theory)
Constructive or intuitionistic mathematics (which might reject the Law of the Excluded Middle or the Axiom of Choice)
Reverse mathematics (which analyzes which axioms are required for which theorems)
Foundations research, logic, or philosophy of mathematics (where different systems like NBG, MK, or ZF without Choice may be studied)
Computer-assisted proof systems, which often rely on type-theoretic foundations (like Coq or Lean)

Implicit Assumption

In most mathematical writing:
The foundational assumptions are rarely mentioned unless relevant.
If a theorem relies on something stronger than ZFC (like the Generalized Continuum Hypothesis or a large cardinal), that will usually be noted explicitly.

Summary

Yes, ZFC is the default foundational system assumed in most mathematical literature, unless a different system is stated. It acts like the "operating system" of mainstream mathematics.

I am not interested in getting rid of this foundation, unless the entire existing body of literature does that first.

[Skepdick]

My own goal is to (mostly) understand mathematical literature when I run into it. I do not try to discover new theorems or even new axiom systems.

That's an open-ended goal. What does "understanding" even amount to?

Why are you reading the literature in the first place?

I am not interested in getting rid of this foundation, unless the entire existing body of literature does that first.

That's an incoherent approach to stuff.

Is what you call "understanding" foundation-agnostic or not?

If you are committed to reading with "classical goggles" would you understand a constructive text which doesn't state its foundations explicitly?
If you are committed to reading with "constructive goggles" would you understand a constructive text which doesn't state its foundations explicitly?

You can't understand mathematics without understanding the frameworks that make mathematical statements meaningful.

What you get when you are committed to a foundation is restricted comprehension.
What you get when you are not committed to a foundation unrestricted comprehension.

Foundations create blind spots.

[godelian]

Why are you reading the literature in the first place?

I originally started out reading on Galois theory, because I found it fascinating. I couldn't imagine how anybody could prove Abel-Ruffini, until I finally could. Another strand of reading back then was on compiler construction and on how parser generation worked, LL,LR,SLR, LALR generators. After using compilers and script interpreters for years, I wanted to know how they worked. At some point, probably a decade ago, I also got interested in Gödel's incompleteness theorems and Tarski's undefinability of the truth. I don't remember what got me started, but I kept reading ever since. Proving an impossibility is fascinating, because at first glance, it seems almost impossible to do. Nowadays, I read extensively on zkSNARK, i.e. zero-knowledge succint non-interactive arguments of knowledge. What it does, is incredibly powerful. This field has the potential to take over finance.

Is what you call "understanding" foundation-agnostic or not?

No. Absolutely not. However, I gradually became foundation-aware.

What you get when you are committed to a foundation is restricted comprehension.

That's like saying that committing to a particular compiler is a restriction. In a sense, that is true.

What you get when you are not committed to a foundation unrestricted comprehension.

Not committing to any compiler at all means that you cannot compile anything.

Foundations create blind spots.

Of course, they do. But then again, you can to some extent become aware of these blind spots. It is the literature that chooses the foundations. If you do not like that, then you cannot use the literature.

[Skepdick]

Not committing to any compiler at all means that you cannot compile anything.

It means you can understand compiler internals before you try to understand the programs they spit out.

Until you understand the compiler internals - you can't really compile the theory in your own head. You know - in order to understand it.

Being committed to one foundation is like only knowing how to use one compiler without understanding compilation itself.
It's like understanding JavaScript without understanding that the syntax doesn't matter to computations.

Most mathematical education teaches people to be users of mathematical programs, not creators who understand the underlying compilation process. My compiler-focused approach creates mathematical engineers rather than mathematical consumers.

Of course, they do. But then again, you can to some extent become aware of these blind spots. It is the literature that chooses the foundations. If you do not like that, then you cannot use the literature.

Whether I can; or I cannot use the literature is a meaningless question when trying to bridge pure mathematics with practical problems.

You don't even know what the invariants are; or supposed to be.
Let alone encode them into mathematical structures.
How do you map real-world invariance to mathematical invariance?

Real mathematical work often requires creating new mathematical structures that appropriately capture real-world invariants. When you capture those relationships in Mathematics you have yourself a theorem.

It MUST hold - whatever the axioms. The rest is just finding tractable models (which may well be itself an intractable search).

This is why foundational debates are completely irrelevant. Whether you prove something in ZFC or constructively doesn't help if you still can't compute anything with it in practice.

Mathematics is just computational engineering under structural constraints.

[godelian]

Whether I can; or I cannot use the literature is a meaningless question when trying to bridge pure mathematics with practical problems.

I was not reading about Gödel's incompleteness theorems or Tarski's undefinability of the truth in order to solve practical problems. This was more an exploration of the limits of what the map can show about the territory. Not everything is on the map. Some of what is on the map, could actually be wrong. Sometimes I do read with a view on possibly applying it some day, such as in the case of zkSNARK. Most of the time, however, it is just a hobby.

Sometimes, I moved from applying things to curiosity about why it works, such as in the case of compiler construction. A compiler is itself a program. So, after creating lots of programs, you could end up interested in the very tools that allow you to do that.

[Skepdick]

Whether I can; or I cannot use the literature is a meaningless question when trying to bridge pure mathematics with practical problems.

I was not reading about Gödel's incompleteness theorems or Tarski's undefinability of the truth in order to solve practical problems. This was more an exploration of the limits of what the map can show about the territory. Not everything is on the map. Some of what is on the map, could actually be wrong. Sometimes I do read with a view on possibly applying it some day, such as in the case of zkSNARK. Most of the time, however, it is just a hobby.

Sometimes, I moved from applying things to curiosity about why it works, such as in the case of compiler construction. A compiler is itself a program. So, after creating lots of programs, you could end up interested in the very tools that allow you to do that.

Your very premise is incoherent in my worldview.

The map can show everything if you don't need it to DO anything.

Let X be the map of the entire universe.
Or suppose you have a complete computational simulation of the universe.

You don't care about its fidelity because you don't need to do any computations with it.

The two are functionally equivalent.

Your predicament strikes me as the one Asimov outlined in The Last Question.

https://users.ece.cmu.edu/~gamvrosi/thelastq.html