Torn between classical and constructive mathematics

[Skepdick]

A tautology is obviously always true.

This statement already functions as a model-selector! A filter.

There is no statement that is "always true"! For any statement, we could construct models or logical systems where its negation holds.

All you are doing by saying "A tautology is obviously always true." is setting the domain of discourse. It's an operational limit.

You are excluding (a priori) any model in which the negation holds.

Goodstein's theorem, for example, is not a tautology.

It is if you want it to be. That's the point of axioms.

Declare Goldstein's statement as axiomatic and examine all the universes/models in which it holds.
Ignore all the universes in which it doesn't.

You cannot prove it from PA but you can from ZFC. It is true but unprovable in PA.

Q.E.D it's only "true" (meaning - it holds!) when interpreted in the standard model of PA. But it needs not be "true" (e.g it doesn't hold) in any non-standard models of PA.

What you seem to call "truth" is not only relative to axioms; but it's also relative to the arbitrarily chosen model for those axioms.
So in a deep sense the notion of choice (of a kind very very different to the axiom of choice) is axiomatic in all Mathematical work.

[godelian]

You cannot prove it from PA but you can from ZFC. It is true but unprovable in PA.

Q.E.D it's only "true" (meaning - it holds!) when interpreted in the standard model of PA. But it needs not be "true" (e.g it doesn't hold) in any non-standard models of PA.

Yes, not every nonstandard model of PA can be embedded into a nonstandard model of ZFC.

[Skepdick]

Yes, not every nonstandard model of PA can be embedded into a nonstandard model of ZFC.

Who cares? You can embed whatever you want into whatever you want using however many layers of embedding you want. Maybe the number of embeddings is uncountably infinite?

In the set-theoretic multiverse you never really know where in the hierarchy you are.

Maybe you are in a model which makes X true; but your model is embedded in a model which makes X false.

Any given statement may be true in some hierarchy of universes; and false in another hierarchy. How do you know which multiuniverse/hierarchy you are operating in?

What is it that you want to remain invariant in your theory? Your axioms; or your theorems? Neither?

[godelian]

What is it that you want to remain invariant in your theory? Your axioms; or your theorems? Neither?

Unless I explicitly don't, I operate in PA or ZF-inf.

Since PA and ZF-inf are perfectly bi-interpretable, they are effectively one and the same thing.

In fact, that is what everyone else does too. Unless they explicitly state that they are operating in another theory they are operating in PA (or ZF-inf).

This default is so firmly ingrained that the vast majority of users are not even aware of it. If you open an arbitrary math textbook, it typically does not even mention that it implicitly assumes the default.

Textbook math rarely uses the extra power afforded by full ZFC. You typically do not need the axiom of infinity, and you almost never need the axiom of choice.

It is typically PA/ZF-inf that is the invariant.

[Skepdick]

What is it that you want to remain invariant in your theory? Your axioms; or your theorems? Neither?

Unless I explicitly don't, I operate in PA or ZF-inf.

Implicitly, is that true? I don't believe you.

Since PA and ZF-inf are perfectly bi-interpretable, they are effectively one and the same thing.

Did you prove that bi-interpretability in PA; or ZF-inf?

In fact, that is what everyone else does too. Unless they explicitly state that they are operating in another theory they are operating in PA (or ZF-inf).

That's impossible to be true. Explicitly because determining the bi-interpretability of PA and ZF-inf e.g identifying the invariant structure underneath both theories is done outside of both PA and ZF-inf.

There must be a meta-theory you are unaware of...

This default is so firmly ingrained that the vast majority of users are not even aware of it. If you open an arbitrary math textbook, it typically does not even mention that it implicitly assumes the default.

It's a pity you mis-identified your "default"

Textbook math rarely uses the extra power afforded by full ZFC. You typically do not need the axiom of infinity, and you almost never need the axiom of choice.

It is typically PA/ZF-inf that is the invariant.

So which proof-theoretic system did you use to prove the bi-interpretability of PA and ZF-inf?

Whatever it is; surely it must be capable of representing both systems and reasoning about translations between them.

[godelian]

So which proof-theoretic system did you use to prove the bi-interpretability of PA and ZF-inf?
Whatever it is; surely it must be capable of representing both systems and reasoning about translations between them.

https://projecteuclid.org/journals/notr ... 67707.full

2007

On Interpretations of Arithmetic and Set Theory
Richard Kaye, Tin Lok Wong

Abstract

This paper starts by investigating Ackermann's interpretation of finite set theory in the natural numbers. We give a formal version of this interpretation from Peano arithmetic (PA) to Zermelo-Fraenkel set theory with the infinity axiom negated (ZF−inf) and provide an inverse interpretation going the other way. In particular, we emphasize the precise axiomatization of our set theory that is required and point out the necessity of the axiom of transitive containment or (equivalently) the axiom scheme of ∈-induction. This clarifies the nature of the equivalence of PA and ZF−inf and corrects some errors in the literature.

PA and ZF-inf are bi-interpretable.

[Skepdick]

PA and ZF-inf are bi-interpretable.

Unless I explicitly don't, I operate in PA or ZF-inf.

It's not possible for both of those statements to be true...

Which one isn't?

[godelian]

PA and ZF-inf are bi-interpretable.

Unless I explicitly don't, I operate in PA or ZF-inf.

It's not possible for both of those statements to be true...

Which one isn't?

They are bi-interpretable. So, they are essentially the same thing.

[Skepdick]

PA and ZF-inf are bi-interpretable.

Unless I explicitly don't, I operate in PA or ZF-inf.

It's not possible for both of those statements to be true...

Which one isn't?

They are bi-interpretable. So, they are essentially the same thing.

And yet you haven't explicitly said you don't operate in PA or ZF-inf.

[godelian]

It's not possible for both of those statements to be true...

Which one isn't?

They are bi-interpretable. So, they are essentially the same thing.

And yet you haven't explicitly said you don't operate in PA or ZF-inf.

By default, unless mentioned otherwise, the whole of mathematics operates in PA/ZF-inf.

[Skepdick]

They are bi-interpretable. So, they are essentially the same thing.

And yet you haven't explicitly said you don't operate in PA or ZF-inf.

By default, unless mentioned otherwise, the whole of mathematics operates in PA/ZF-inf.

Contradiction.

You didn't mention otherwise, therefore by default you should have been operating in PA/ZF-inf.

But statements about the bi-interpretability of PA and ZA-inf do not operate in PA/ZA-inf.

[Skepdick]

By default, unless mentioned otherwise, the whole of mathematics operates in PA/ZF-inf.

Furthermore; if we accept the statement "The whole of Mathematics operates in PA/ZF-inf" as an operationalized definition of Mathematics then that which operates outside of PA/ZF-inf is NOT Mathematics.

Then what is it?

[godelian]

Statements about the bi-interpretability of PA and ZA-inf do not operate in PA/ZA-inf.

Gemini

Interpreting PA in ZF-inf:
This can be done using Ackermann encoding, where natural numbers are represented as sets. For example, the number 1 can be represented as {{} (the empty set)}, 2 as {{}}, and so on. This allows PA statements to be translated into ZF-inf statements, and vice versa.

Interpreting ZF-inf in PA:
Similarly, a model of ZF-inf can be constructed within PA by using the natural numbers to encode sets. This requires carefully defining the basic set-theoretic operations like membership (∈), subset (⊆), and set operations (union, intersection, etc.) within the framework of arithmetic.

Bi-interpretability:
The key is that these interpretations are "bi-" - meaning they go both ways, allowing us to express ZF-inf within PA and PA within ZF-inf. This bi-directional translation shows that the two theories are logically equivalent, at least for the statements that can be formulated in both languages.

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

[godelian]

By default, unless mentioned otherwise, the whole of mathematics operates in PA/ZF-inf.

Furthermore; if we accept the statement "The whole of Mathematics operates in PA/ZF-inf" as an operationalized definition of Mathematics then that which operates outside of PA/ZF-inf is NOT Mathematics.

Then what is it?

You are making an incorrect interpretation. 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.

[Skepdick]

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