Torn between classical and constructive mathematics

[Skepdick]

You are making an incorrect interpretation.

No, I am not.

Most of mathematics operates in PA/ZF-inf. Not all of it.

The part that doesn't, however, explicitly states what additional (or even other) axioms it is using.

Irrelevant. You said that UNLESS explicitly stated otherwise you are operating in PA/ZF-inf.

You didn't explicitly state otherwise. Therefore your claims about bi-interpretability are to be interpreted in PA or ZF-inf.
Only; such statements cannot be expressed in PA or ZF-inf.

So even though you haven't explicitly stated otherwise; it's necessarily true that you are operating outside of PA/ZF-inf when asserting bi-interpretability. Thus directly contradicting your stated principle.

[godelian]

Bi-interpretability consists of two statements, one expressed in PA and one expressed in ZF-inf.

No; it doesn't.

You are missing a two interpratation functions:
f: PA -> ZF-inf
g: ZF-inf -> PA

Such that forall statements x in PA; y in ZF: f(x) = y AND g(y) = x

Check the issue you have by consulting "On Interpretations of Arithmetic and Set Theory" by Richard Kaye and Tin Lok Wong. It is their result and not mine.

[Skepdick]

Check the issue you have by consulting "On Interpretations of Arithmetic and Set Theory" by Richard Kaye and Tin Lok Wong. It is their result and not mine.

Irrelevant. It's your assertions that I am challenging.

To prove that two systems are bi-interpretable you need to construct a transpiler.

https://en.wikipedia.org/wiki/Source-to-source_compiler

e.g you need a function which translates back and forth between formal languages while preserving meaning.

[godelian]

Irrelevant. You said that UNLESS explicitly stated otherwise you are operating in PA/ZF-inf.

Yes, but that is in itself not a theorem provable or disprovable in mathematics. You have to wait for that until I claim the provability of a particular theorem.

Actually, calculus seems to require the axiom of infinity. So, PA/ZF-inf may not be enough for quite a bit of mathematics. The funny thing is that calculus textbooks never mentions anywhere that they rely on the axiom of infinity.

[Skepdick]

Irrelevant. You said that UNLESS explicitly stated otherwise you are operating in PA/ZF-inf.

Yes, but that is in itself not a theorem provable or disprovable in mathematics.

You have to wait for that until I claim the provability of a particular theorem.

Doesn't matter. You believe it to be a true statement ABOUT mathematical practice.

Even though there exists sufficient evidence to the contrary.

[godelian]

Doesn't matter. You believe it to be a true statement ABOUT mathematical practice.

Even though there exists sufficient evidence to the contrary.

Apparently, the construction of the reals requires the axiom of infinity.

ChatGPT: Construction of the Real Numbers

The real numbers are usually constructed via:

Dedekind cuts of , or
Cauchy sequences of rationals

Both constructions involve infinite sets (e.g., an infinite sequence of rationals).

So, apparently, every time you rely on an infinite sum or some other infinitely repeating operation, you are using the axiom of infinity. I wasn't aware of that.

[Skepdick]

Doesn't matter. You believe it to be a true statement ABOUT mathematical practice.

Even though there exists sufficient evidence to the contrary.

Apparently, the construction of the reals requires the axiom of infinity.

ChatGPT: Construction of the Real Numbers

The real numbers are usually constructed via:

Dedekind cuts of , or
Cauchy sequences of rationals

Both constructions involve infinite sets (e.g., an infinite sequence of rationals).

So, apparently, every time you rely on an infinite sum or some other infinitely repeating operation, you are using the axiom of infinity. I wasn't aware of that.

Duh.

Infinite sum require infinite operations.

[godelian]

Infinite sum == infinite operations.

Yes, but it is not obvious that it requires the existence of the fully inducted set of the natural numbers. Now that I think about it, it dawns upon me that this is indeed necessary. I just wonder why no textbook ever mentions that it means that we rely on the axiom of infinity. You can study calculus at any level. It is never mentioned.

[godelian]

[You believe it to be a true statement ABOUT mathematical practice.

It is ZF(C) that is the default basis for most mathematics. Infinitely repeating operation is the norm in so many subdisciplines that we cannot easily dispense of the axiom of infinity.

[Skepdick]

[You believe it to be a true statement ABOUT mathematical practice.

It is ZF(C) that is the default basis for most mathematics. Infinitely repeating operation is the norm in so many subdisciplines that we cannot easily dispense of the axiom of infinity.

That doesn't follow either.

Your statement was about the default context of Mathematical practice when not stated explicitly.

We can trivially dispense of the axiom of infinity when we use lazily-evaluated programming languages.
If you want infinite anything - you need not only infinite space (ticker tape) but also infinite time. Good luck!

Until then; we get to play a game. Name the largest number...

https://www.scottaaronson.com/writings/bignumbers.html

[godelian]

Your statement was about the default context of Mathematical practice when not stated explicitly.

Yes. Things like calculus only function when the axiom of infinity is allowed, at the very level of the definition of things. For example, the integral operator is an infinite sum.