/sci/ - Science & Math

>>12124831
>>12124823
>this implies that the paper you're citing above is wrong?
Mhm, I don't think it rules out the ZFC<->HA issue at hand. In fact I'm pretty sure that the author of the paper doesn't even care for intuitionistic logic, he's just concerned with ZFC<->PA.

Namely, the idea is that you have an undecidable PA statement and the set theoretical axioms are just so strong that they may imply this and that. I think if he have no ZFC<->PA claim, we can't rule it out.
What's HA_2? If both HA_2 and PA_2 deal with subsets, then it might not be an apt comparison.

>If you're given an integer n and a Turing machine, you can definitely check in a constructive way whether it halts in at most n steps.
I don't follow just yet.
The idea is that ZF proves the existence result with strong axioms while PA is agnostic about it. In that case you'd have a ZF integer but can't compute it's properties (e.g. whether it's a multiple of 7).
This is maybe in analogy to how ZF proves existence of the well-ordering of R, while not allowing us to compute with it.

The only question is whether this can already happen with just arithmetic-like statements..

>>11687446
But then again, who says that it's good prose. I also write a bunch of notes all the time.

>that snuck
?
I don't know of any list of those, if that's what you're asking