The position of constructive mathematics on Goodstein's theorem

[godelian]

But that's just as vacuous as every Classical claim. Give me just one element in S.

No, if inexpressible numbers exist, not one of them can be expressed.

Since there exists NO real number that cannot be written down on an infinite piece of paper (such as the tape of a TM) then there exists a bijection. between Real numbers and Turing Machines.

That amounts to rejecting Georg Cantor's diagonal argument.

Well what if Cantor's Diagonal argument was itself weaponized against Classical Mathematics?
Diagonalization (itself an infinitary process) is said to produce a unique real, so then perform diagonalization again; and again; and again... ad infinitum.
An "uncomputable real" would have to be something that cannot be produced even by infinite iterations of the very process that classical mathematics uses to prove their existence.

No, because the set of diagonalization algorithms is countable while the reals are uncountable.

I definitely prefer classical mainstream mathematics to constructive mathematics, even though I occasionally acknowledge its concerns.

[Skepdick]

But that's just as vacuous as every Classical claim. Give me just one element in S.

No, if inexpressible numbers exist, not one of them can be expressed.

OK, put expression aside for 1 second. Those numbers aren't only inexpressible - they are unknowable.

For imagine there exists such a number - one you can know but can't express.

Can you at least express the process by which you know it exist? Even if you can't express that which you've come to know.

That amounts to rejecting Georg Cantor's diagonal argument.

Not entirely. I can accept the method and reject its conclusions.

No, because the set of diagonalization algorithms is countable while the reals are uncountable.

That is a meaningless distinction.

The countable/uncountable distinctions are framework-dependent - they are artifacts of our theoretical commitments.
The "uncountability of the reals" isn't a discovery about mathematical reality - it's a consequence of specific definitional choices about how we handle infinity

On a constructive foundation the very question "Are reals uncountable?" is malformed!

In a world where LEM doesn't hold NOT countable doesn't mean uncountable; nor does NOT uncountable mean countable.

Countable and NOT countable are complementary claims.
Uncountable and NOT uncountable are complementary claims.

So you've completely missed the scope and implications of Cantor's argument in a constructive setting:

"Countable" means you can explicitly construct a bijection with natural numbers
"NOT countable" just means you can't construct such a bijection
"Uncountable" means you can prove no such bijection exists
"NOT uncountable" means you can't prove no bijection exists.

I definitely prefer classical mainstream mathematics to constructive mathematics, even though I occasionally acknowledge its concerns.

Do you? You are a programmer. You don't accept LEM universally. You understand that NOT all propositions are decidable (code has exceptions; undefined cases; edge and corner cases).

You understand distributed systems and dynamic processes which contain all those bugs/incompletenesses.
You are telling me you believe in globally/universally/totally completed (closed!) infinitary processes?!?!
Are you telling me that from a distributed systems perspective you believe in a perfect global consensus across infinite nodes; complete termination of all infinite loops; total elimination of all race conditions across infinite processes and absolute consistency with zero edge cases across infinite states?!?!?

That's just a theoretical fantasy!

How can you spend your days working with dynamic, open, undecidable processes, then turn around and claim mathematical infinity consists of static, completed, decidable objects?

How can anyone with intuitive understanding of processes and interactions accept nonsense like "Infinite sets are completed objects"; or "Cardinalities are fixed properties" when cardinalities are clearly symbolic for infinite sets and numeric for finite ones.

Do you see an infinite loop and think to yourself "This is a completed set with cardinality ℵ₀"?

And if you don't universally accept LEM then you don't universally accept the Axiom of Choice;
Then you can't construct the Dedekind Reals.
The Couchy Reals are countable.

[godelian]

In a world where LEM doesn't hold NOT countable doesn't mean uncountable; nor does NOT uncountable mean countable.

That means that countability could be undecidable. Fine, but why would the countability of the reals be undecidable?

In my opinion, the LEM applies by default unless there is a good argument why it does not apply. Sometimes there is such good argument, because it is about a corner case.

In general, in my take on the matter, classical mainstream mathematics can safely be assumed to work fine, unless there is a good argument why it does not work well in a particular corner case.

[Skepdick]

In a world where LEM doesn't hold NOT countable doesn't mean uncountable; nor does NOT uncountable mean countable.

That means that countability could be undecidable. Fine, but why would the countability of the reals be undecidable?

It doesn't mean that. It means that countable vs not-countable is subject to decidability; AND that proving X is not-countable it doesn't make it uncountable.

not-countable ≠ uncountable

In my opinion, the LEM applies by default unless there is a good argument why it does not apply. Sometimes there is such good argument, because it is about a corner case.

From a decidability perspective that's exactly the same as saying "LEM doesn't apply by default unless there is a good argument why it does apply".

You still have to decide case-by-case whether LEM applies. Whether by default; or by exception.

You are smuggling in a philosophical preference as a mathematical necessity.

In general, in my take on the matter, classical mainstream mathematics can safely be assumed to work fine, unless there is a good argument why it does not work well in a particular corner case.

You mean in the particular "corner case" of axiomatic LEM? It entails that ALL propositions are decidable which contradicts the halting problem.

Only, that's not a corner case. It's a universal axiom.

Of course, the psychological explanation as to why people prefer Classical mathematic totally makes sense. They would like to think they are omniscient - they are doing Mathematics as if they are God. It's theology disguised as reason.

All truths are knowable (even if we can't know them)
All propositions are decidable (even if we can't decide them)
All sets are completed objects (even if we can't complete them)
All infinities are actual totalities (even if we can't totalize them)

It's just a power fantasy.

https://ncatlab.org/nlab/show/principle+of+omniscience

In logic and foundations, a principle of omniscience is any principle of classical mathematics that is not valid in constructive mathematics. The idea behind the name (which is due to Bishop (1967)) is that, if we attempt to extend the computational interpretation of constructive mathematics to incorporate one of these principles, we would have to know something that we cannot compute. The main example is the law of excluded middle (LEM); to apply p ∨ ¬ p computationally, we must know which of these disjuncts hold; to apply this in all situations, we would have to know everything (hence ‘omniscience’).

Bishop's principles of omniscience may be seen as principles that extend classical logic from predicates (where LEM may happen to be valid, even constructively, for certain predicates) to their quantifications over infinite domains (where LEM is typically not constructively valid).

[godelian]

not-countable ≠ uncountable

Countable means that the cardinality of the set is ℵ₀. Uncountable means that it is ℵₖ, with k=1,2,3, ... This view implicitly assumes the Continuum hypothesis.

From a decidability perspective that's exactly the same as saying "LEM doesn't apply by default unless there is a good argument why it does apply".

Yes, it is another default position. The classical default is that it applies, while the constructive default is that it doesn't.

You are smuggling in a philosophical preference as a mathematical necessity.

It is not a necessity. It is merely a choice of default.

All truths are knowable (even if we can't know them)
All propositions are decidable (even if we can't decide them)
All sets are completed objects (even if we can't complete them)
All infinities are actual totalities (even if we can't totalize them)

Truths --> No, most are inexpressible and therefore unprovable. Most expressible truths are also unprovable, and therefore not justifiable ("knowable").
Decidable --> No, for most yes/no questions, there is no decision procedure available to answer them in terms of yes or no.
Completed sets --> yes, complete induction is assumed, because it is not useful or even necessary to axiomatize that computation takes time or energy.
Infinities --> the Continuum hypothesis is acceptable and assumed

[Skepdick]

Countable means that the cardinality of the set is ℵ₀ . Uncountable means that it is ℵₖ, with k=1,2,3, ... This view implicitly assumes the Continuum hypothesis.

And we are back to this question: Why are some cardinalities numeric; and some cardinalities symbolic?

Yes, it is another default position. The classical default is that it applies, while the constructive default is that it doesn't.

This is just sophistry.

Default positions are axioms. It applies always.
Default positions with exceptions are decision problems. It applies sometimes.

When does it apply; and when doesn't it apply? That's a contextual decision problem.

It is not a necessity. It is merely a choice of default.

This is a meaningless statement.

When does the default apply; and when doesn't it apply?

This is a decision problem.

Truths --> No, most are inexpressible and therefore unprovable. Most expressible truths are also unprovable, and therefore not justifiable ("knowable").

This is conceptually confused. Surely the order of events is knowledge (first) expression (second)?
I accept that you know something you can't express. I don't accept that you know something; but you can't tell me how you've come to know it.

On a constructivist worldview having a witness amounts to having justification.

You have no witness; so what is it that you call "justification"?

Is the symbol x a witness for an uncomputable number?

Infinities --> the Continuum hypothesis is acceptable and assumed

Continuity with discontinuities (decision-points) is an oxymoron...

[godelian]

You have no witness; so what is it that you call "justification"?

Proof is justification.

[Skepdick]

You have no witness; so what is it that you call "justification"?

Proof is justification.

Excellent! You are in luck.

Proofs are first class Mathematical objects in Agda and Coq, but LEM is not an axiom.

If LEM is only a default choice, but not a universal axiom then please prove when LEM does; or doesn't apply and why. Thanks.

[godelian]

You have no witness; so what is it that you call "justification"?

Proof is justification.

Excellent! You are in luck.

Proofs are first class Mathematical objects in Agda and Coq, but LEM is not an axiom.

If LEM is only a default choice, but not a universal axiom then please prove when LEM does; or doesn't apply and why. Thanks.

Short overview:

DeepSeek: When does the Law of the Excluded Middle apply?

The **Law of the Excluded Middle (LEM)** is a fundamental principle in classical logic stating that for any proposition \( P \), either \( P \) is true or its negation \( \neg P \) is true (symbolically: \( P \lor \neg P \)).

### **When Does LEM Apply?**
1. **In Classical Logic:**
- LEM is universally valid and applies to all well-formed propositions.
- It is one of the three classic laws of thought (along with the Law of Identity and the Law of Non-Contradiction).

2. **In Mathematical Proofs (Classical Mathematics):**
- Used extensively in proofs by contradiction (reductio ad absurdum).
- Many theorems rely on LEM (e.g., "A number is either prime or not prime").

3. **In Bivalent (True/False) Systems:**
- LEM holds in systems where every proposition must be either true or false, with no third option.

### **When Does LEM *Not* Apply?**
1. **In Intuitionistic/Constructive Logic:**
- Rejected or restricted because proofs require explicit construction of truth.
- Just because \( \neg P \) is not provable does not mean \( P \) must be true.

2. **In Many-Valued Logics (e.g., Fuzzy Logic):**
- Propositions can have intermediate truth values (not just true/false).

3. **In Paraconsistent Logics:**
- Some systems allow propositions to be both true and false (dialetheism), making LEM inapplicable.

4. **For Vague or Undefined Statements:**
- If a proposition is ill-defined or meaningless, LEM may not apply (e.g., "The present king of France is bald").

### **Key Takeaway:**
LEM applies in classical logic and mathematics but is rejected or modified in alternative logical systems where truth is not strictly binary.

So, the idea is to first attempt to solve problem in mainstream classical mathematics. If the result is unsatisfactory, it may be a question of exploring the limitations of boolean logic. But then again, something else may have broken instead. There may be other limitations that were reached.

[Skepdick]

So, the idea is to first attempt to solve problem in mainstream classical mathematics. If the result is unsatisfactory, it may be a question of exploring the limitations of boolean logic. But then again, something else may have broken instead. There may be other limitations that were reached.

Rinse, repeat.

When is a result unsatisfactory; and when is it satisfactory? What satisfiability problem are you solving?

Your methodology seems indistinguishable from mathematical masturbation - going through the motions of problem-solving without actually having a well-defined problem to solve.

In which system are you going to specify/encode your SAT() predicate and why? Can you encode this decision procedure?

Of course, this is all rhetorical because I know (even if you don't) that this is recursively impossible

Firstly you needs a SAT() predicate to determine when math is "satisfactory"
SAT(mathematical_result) → {satisfactory, unsatisfactory}

Secondly this SAT() predicate must be encoded in SOME axiom system:
ZFC? → Assumes classical logic, choice, excluded middle
Type Theory? → Assumes constructive foundations, decidability
Modal Logic? → Assumes possibility/necessity operators
First-order Logic? → Assumes particular inference rules

But the very choice of encoding system effectively predetermines the answer:

If you encode SAT() in ZFC, classical results will seem "satisfactory"
If you encode SAT() in constructive type theory, constructive results will seem "satisfactory"

The foundational choice rigs the game! Do you want me to draw you a biiiiig circle?