1
$\begingroup$

I am using ZFC as a tool to demonstrate my problematic logic.

In zfc we construct a proof system for zfc in zfc (a simulation of a proof is what I mean); we will call it inner proof system. We establish that if there is a proof in this inner proof system that concludes A then A holds. Turing machines can be formalized in zfc with the notions of halting and not halting. The whole question relies upon the argument that the zfc can prove that for every halting turing machine on a certain input there exists a proof of this in the inner system (which I am not entirely sure it is provable in zfc without further assumptions).

A turing machine that takes an input (and treats it like an incoding of a turing machine and also as an input) and goes through all possible proofs (in the inner proof system) that conclude that the input halts on itself or does not halt. If such a valid proof was found our machine does the opposite of the proof's conclusion (meaning that if the proof demonstrated halting the machine would enter an infinite loop and if the proof demonstrated not haulting the machine would halt). Under the assumption that zfc is consistent it holds that this turing machine does not halt on itself. This is a construction used to demonstrate the first and second incompleteness theorems in zfc for computer scientists.

Assuming the consistency of zfc, the statement that the aforementioned turing machine does not halt on itself cannot be proven by zfc and thus cannot be proven by the inner proof system. Assuming the consistency of zfc, according to the completeness theorem there exists a model of zfc where the statement: "the aforementioned turing machine does not halt on itself" is true and another with this statement false.

My problem is with the model in which it holds that this statement is false. This means that the relevant turing machine halts. It follows that there is a proof of that in the inner proof system. It follows that the inner proof system is inconsistent.

I know there is something wrong with this logic but I cannot pinpoint it (obiously because I did not formalize this argument sufficiently). Where in this sketch of a proof does the argument fail (for example because a statement is not directly provable from zfc without certain assumptions)?

Note: my backgroung is in computer science

$\endgroup$
7
  • 1
    $\begingroup$ "My problem is with the model in which it holds that this statement is false. This means that the relevant Turing machine halts. It follows that there is a proof of that in the inner proof system. " But that is the gist of GIT: wrt a suitable theory T we construct a statement G such that neither G nor not-G are provable in T. But in the meta-theory (e.g. ZFC) we "know" that one of them is true (e.g. the T-statement G asserting that G itself is unprovable in T). Thus, on what ground you says: "It follows that there is a proof of that in the inner proof system"? $\endgroup$ Commented Aug 23, 2023 at 11:25
  • $\begingroup$ It would be helpful if you could sharpen your question by specifying when you speak of ZFC as the background meta-language, and when - as the object language. $\endgroup$ Commented Aug 23, 2023 at 11:47
  • $\begingroup$ @MauroALLEGRANZA the statement in question is "the aforementioned turing machine does not halt on itself". If it is false in the model then the turing machine does halt on itself. If the following argument is provable in zfc "for every halting turing machine on a certain input there exists a proof of this in the inner system" then there exists a proof that the relevant turing machine does halt in the inner proof system. if the last argument is not provable in zfc then this answers my question. $\endgroup$
    – Anonymous
    Commented Aug 23, 2023 at 11:50
  • 1
    $\begingroup$ "it means that the relevant Turing machine halts. It follows that there is a proof of that in the inner proof system. " Why so? If we conclude form the fact that we know that a "fact" about T machine holds, than there is a proof of that fact in the theory, we are simply assuming the "completeness" (wrt to the "standard model", that of GIT, and not the completeness wrt validity, that of G's Completeness Th) of the theory T, and this is exactly what GIT denies. $\endgroup$ Commented Aug 23, 2023 at 11:59
  • $\begingroup$ @MikhailKatz everytime I did not mention the inner system I mean zfc $\endgroup$
    – Anonymous
    Commented Aug 23, 2023 at 12:00

1 Answer 1

0
$\begingroup$

It's a bit difficult to pin down the issue without sufficient formalization. Here is my attempt.

Given a Turing machine $T$, such that $T$ halts or not is independent of ZFC. This implies that $T$ doesn't halt for otherwise there is a proof in ZFC by simulating its behavior. Assuming ZFC is consistent, then ZFC + " $T$ halts " is still consistent, and by the completeness theorem, there must be a model of it.

How to interpret $T$ halts in terms of set theory? One way is to use the simulation or a proof of halting as the definition of halting. Just like Godel replaced "This is false" by "This cannot be proved", the new system doesn't say "$T$ halts" but "There is a proof that $T$ halts".

So the new axiom is really there exists a number that encodes a proof of "$T$ halts". This is not the same as to say there really is such a proof, because the number in the model might be non-standard!

I learned this from Tim Chow:

suppose someone proves on the basis of ZFC a theorem that states that the Goldbach conjecture is false, i.e., a theorem of the form "there exists an integer k that refutes the GC." Again, a priori we still can't conclude automatically that the GC is indeed false (for the standard integers) even if we assume that ZFC is consistent.

In other words, consistency doesn't buy you everything that you might want from a formal system---it tells you that models of the system exist, but it doesn't tell you that there are any models where the "integers" are isomorphic to the standard integers, so you can't necessarily "trust" theorems of the system.

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .