[nyrikki]

A Turing machine as an infinite long tape, and even if it takes 10 times the time to the heat death of the universe x<y will halt.

Finite time is not practical time.

Given two Turing machines A and B approximating numbers a and b, where a ≠ b, you can use an epsilon to prove a > b, that is 'sufficient' for a proof.

You are trying to convert that one sided, semi-decidable 'a>b' into a two sided a>b f Id yes and a≤b is no.

That is undecidable.

Even if you change the ≤ into <, which does imply the exitance of b. It doesn't prove equality.

You have to resort to tactics like normalization for that.

Type theory is probably a good path to understand why. You seem to be coming from a set perspective and you will run into the limits of ZFC that way.

[nequo]

> A Turing machine as an infinite long tape, and even if it takes 10 times the time to the heat death of the universe x<y will halt.

> Finite time is not practical time.

Sorry for my daftness but if x and y are both a transcendental number, for example pi, then x and y have infinitely many digits so the Turing machine that determines whether x < y is true will not halt, even with an infinitely long tape, or will it? What am I misunderstanding?

If you could recommend a source that explains the basics of these arguments, I’d appreciate it.

[nyrikki]

Pi is transcendental but computable.

For an introduction to real real analysis is an old book typically called the 'Baby Rudin' Principles of Mathematical Analysis by Walter Rudin.

It is tiny and expensive, as most college math text books are once you get past a certain level. No idea if there is something better now, it is from the 1950's and there are used copies in most used book shops for cheap (or there was). It has no definition of 'equals' but does have a concept of equivalent relations.

Dummit and Foote's Abstract Algebra book is a great reference, especially with the problem with AI pollution. Coming from a General Relativity background, it still took me two years to work through on my own.

I don't know any suggestions on a more modern approach of starting with type or category theory.

I am not really interested in constructivist math, it is a problem to get around for me, so maybe someone who is can chime in on a better path.

While not rigorous, this paper does a good job at explaining just how muddy the concept of 'equality' is.

https://arxiv.org/abs/2405.10387