PeterDonis said:
Doesn't the proof referred to in the OP, that H1 does not exist (and similarly for F3 based on follow-up posts), contradict this claim?
The proof in the OP shows that:
"There is
no computer program computing a (total) function ##f:\mathbb{N}^2 \rightarrow \{0,1\}## such that:
(a) If the program with index ##a## halts on input ##b## then ##f(a,b)=1##.
(b) If the program with index ##a## loops forever on input ##b## then ##f(a,b)=0##.
"
Now if we think
[for example, based on concerns raised by constructivism
] that all the (total) functions ##f:\mathbb{N}^2 \rightarrow \{0,1\}## must necessarily be those that are computed by some computer program then what you wrote would indeed be correct and H1 would not exist.
============================
Note that when we say that much of mainstream mathematics is formalized by ZFC , then this also includes results like incompleteness theorems, halting problem etc. That is, they are theorems of ZFC. Of course this debate can go philosophical on "what comes first or not"
[and honestly, I am not qualified to comment on this
]. Nevertheless, there would be a (finite) proof of these results in ZFC.
For example, we will have an actual predicate ##P(x,y)## in language of set theory such that:
##P(x,y)=Halt(x,y)## for all ##x,y \in \omega##
Similarly:
"##Halt:\mathbb{N}^2 \rightarrow \{0,1\}## is not a computable function.
"
would be a theorem of ZFC and many weaker theories.
Of course actually formalizing this requires much more understanding and attention to quite a bit of details (and tbh I don't know the details well at all ..... only the basic idea).