9 ms·

> but at the same time there is no "right answer"—all of these axioms, after all, are independent of ZFC, and it's "ok" to add any of them. Minor quible: Just

> but at the same time there is no "right answer"—all of these axioms, after all, are independent of ZFC, and it's "ok" to add any of them. Minor quible: Just because a potential axiom is independent of ZF(C) doesn't make it necessarily "okay" to add. Potential axioms can be unsound, for example if they prove new / untrue Sigma_1 statements. As an example, even in the likely circumstance that ¬Con(ZFC) is independent of ZFC, it wouldn't be "okay" to add ¬Con(ZFC). While the resulting system would be consistent, and does have models, the resulting system is unsound (in the sense of Tarski) because it asserts the existence of natural numbers that have no "written form" (i.e. the existance of natural numbers that are larger than any term you can write to denote a natural number). That said, Martin's axiom, like the CH (or the axiom of choice), does not have any arithmetic consequences, and thus doesn't fall into this category of problematic axioms.

tgflynn 5y ago
> he resulting system is unsound (in the sense of Tarski) because it asserts the existence of natural numbers that have no "written form" (i.e. the existance of natural numbers that are larger than any term you can write to denote a natural number). Isn't that basically the definition of the natural numbers, ie. if you write down any natural number (say n) I can always construct a natural number that is larger than it (like n+1) ?
- chongli 5y ago
  If you can write down the natural number n, you can write down n+1. Of course, you can't write down the entire set of natural numbers but that is not a natural number.
  - skybrian 5y ago
    On any storage system you will eventually run out of memory, so there will always be a maximum integer that you can write down with what you have, and we can only write down a vanishingly small subset of the natural numbers. Of course, this isn’t what mean when they talk about “writing down” a number, but I’ve long thought that assuming the existence of natural numbers that you can’t write down is poetically apt. In some sense, the set of natural numbers is “too big” to be about everyday finite numbers alone and it seems fitting to acknowledge that our usual axioms can’t exclude weirdo large finite numbers that are simply too big to ever reach.
- kmill 5y ago
  This surprisingly doesn't mean repeatedly adding 1 will exhaust all natural numbers -- there are models for the natural numbers with elements that can't be reached this way! The ultrafilter construction gives one such model. You take the set of all sequences of natural numbers (n1, n2, n3, ...) then use an ultrafilter to decide which of these sequences are considered to be equal. The usual operations of natural numbers are defined term-by-term. You can think of the usual natural numbers as being the sequences (0,0,0,...), (1,1,1,...), (2,2,2,...) and so on. However, there are many additional numbers in this system, like (0,1,2,...) that are strictly greater than all the usual numbers, and these cannot be reached by repeatedly adding one. (The reason (0,1,2,...) is greater than (n,n,n,...) is that if we do the comparison term-by-term we get (false,false,...,false,true,true,true,...), and the ultrafilter will decide the comparison is true because it is true for all but finitely many terms. Ultrafilters are devices to consistently turn infinite sequences of trues and falses into a single decision, but every ultrafilter will make a true decision in the case there are only finitely many falses.) Counter-intuitively, proofs by induction still work for this system... speaking with no authority here, maybe an intuition is that it's doing a hypercomputation.
  - R0b0t1 5y ago
    Can you explain what use these have? If natural numbers are (n, n, n, ...) then you have just made a new type of number not comparable to natural numbers.
    - kmill 5y ago
      A theoretical use is that it shows that the axioms of the natural numbers (the Peano axioms) aren't enough to pin down what we think the natural numbers should be -- there are these crazy non-standard natural numbers out there! In context of the discussion, this non-standard model of the natural numbers gives some intuition about what happens if the consistency of ZFC is independent of ZFC and you add in the axiom that ZFC is inconsistent: your natural numbers will have to be something similarly weird. > you have just made a new type of number not comparable to natural numbers But they are comparable. The everyday natural numbers are embedded in this new system, which is what these (n,n,n,...) elements represent. One way to interpret what we've done here is to add in infinities to the number system so that all the normal operations still work, and there's even a total ordering on them! Using the real numbers instead of the naturals, you get the so-called nonstandard real numbers, which is the number system used in nonstandard analysis. Nonstandard analysis is a way to do analysis without epsilon-delta proofs. Nonstandard reals include infinitesimals and infinities, similar to nonstandard naturals having infinities. There are even textbooks on the subject -- I haven't read them, but they claim it makes analysis easier. The last thing that comes to mind is that nonstandard numbers of this exact type show up when you study certain infinite-dimensional number systems and calculate the points (like in the end of my comment).
- rssoconnor 5y ago
  Dropping down to Peano Arithmetic for a moment. We can consider adding a new constant 'c' for a natural number to the language along with the following infinite list of axioms about this remarkable constant: - 0 < c - 1 < c - 2 < c - 3 < c ... Adding all these axioms is consistent. I.e. you can do induction upto 'c', whatever it is. Why is it consistent? Because if there was a contradiction, the proof of such a contradiction would be finite, and hence can only use a finite number of these new axioms (this is a so-call compactness argument). But clearly any finite subset of this list of axioms is consistent because it has a model where c is just defined to be 1 more than the largest numeral appearing in that list. But all those infinite number of axioms taken together creates an unsound system because it claims that 'c' denotes a natural number that is larger than every written numeral. Heading back to ZFC land, it turns out that (assuming ¬Con(ZFC) is independent of ZFC) adding ¬Con(ZFC) to ZFC similarly is similarly unsound in that it yields only models that have elements that are larger than every written numeral.
  - skissane 5y ago
    > in that it yields only models that have elements that are larger than every written numeral. Are these like hyperintegers (or should I say hypernaturals), as in the hyperrreal numbers used in non-standard analysis?
  - im3w1l 5y ago
    This sounds a little bit like an argument against systems with an infinite number of axioms to me. Or maybe it's fine but only under certain conditions?
- hypersoar 5y ago
  You can find a natural number that is bigger than any one natural number, but you can't write one down that's bigger than every natural number in the ZFC sense.
  - dwohnitmok 5y ago
    > that's bigger than every natural number in the ZFC sense. I'm not sure what you mean by this. Even for nonstandard models of the natural numbers there will never be a single number larger than all other numbers, since that violate the Peano axioms. Did you mean by "in the ZFC sense" "the standard model?"
  - gooberwonder 5y ago
    45,000,000,001?
    - agalunar 5y ago
      Look around you!
  - munk-a 5y ago
    Do you mean that given finite resources (like time and matter) we would be unable to express the number? Or are you talking about a sort of recursive thing where writing down a number which is a sum of all natural numbers up to and including itself is impossible since that number is bigger each time you look at it?
- l33t2328 5y ago
  I don’t believe a consequence of the axioms discussed is that there exist natural numbers with no “written form.” Do you have a proof or citation?
  - rssoconnor 5y ago
    For this entire argument I will be operating under the assumption that ¬Con(ZFC) is independent of ZFC. ZFC+¬Con(ZFC) proves "there EXISTS a natural number x such that x is an encoding of a proof in ZFC of 0=1". Now suppose there is actually a numeral n, i.e. a specific written term written using symbols, e.g. (+,*,1), such that ZFC+¬Con(ZFC) proves that "n is an encoding of a proof in ZFC of 0=1". We can mechanically decode such a n and check if it is indeed a proof that that ZFC proves "0=1" or not. There are two possibilities: (a) the check is successful and thus we have found proof of a contradiction in ZFC. But if ZFC is inconsistent, then it proves everything. In particular ZFC proves ¬Con(ZFC), which violates our assumption that ¬Con(ZFC) is independent of ZFC. Alternatively (b) our check fails and n does not encode a proof in ZFC of 0=1. But that statement "n does not encode a proof in ZFC of 0=1" is a true Delta_0 statement, and we can prove by induction that ZFC proves every true Delta_0 statement. Thus we can prove that ZFC proves "n does not encode a proof 0=1", and hence ZFC+¬Con(ZFC) proves "n does not encode a proof 0=1". But now we have found a statement Q such that ZFC+¬Con(ZFC) proves both Q and also ¬Q. This means that ZFC+¬Con(ZFC) is inconsistent. But if ZFC+¬Con(ZFC) is inconsistent, by the deduction theorem, ZFC proves ¬¬Con(ZFC), or equivalently ZFC proves Con(ZFC). This contradicts our assumption that ¬Con(ZFC) is independent of ZFC (it also implies that ZFC is inconsistent). Thus we are left with the conclusion that there is no such numeral n. However it is still the case that ZFC+¬Con(ZFC) proves "there EXISTS a natural number x such that x is an encoding of a proof in ZFC of 0=1", and the only way this can be the case is any such x is a "natural number" which has no numeral that denotes it.
lupire 5y ago
why is that "unsound"? what's wrong with an unwritable natural? Almost all reals are unwritable.
- dogecoinbase 5y ago
  Soundness in this sense (sigma_1 soundness) is defined by equivalency to the standard model (specifically, all sentences provable in the system must be provable in the standard model).
  - dwohnitmok 5y ago
    It is defined by equivalency to a standard model. Whether there is a single standard model is a philosophical question (which granted most, but not all, set theorists tend to agree with). Hence sigma_1 soundness is from a purely mathematical point of view a relative statement.
- rssoconnor 5y ago
  Mostly because it implies that some Turing machines halt that actually do not halt. That is unless you are willing to accept that a Turing machine can halt in some number of steps that is beyond any number that can be written. And I don't mean can't be written in the sense that we don't have enough paper. Just cannot be written in principle at all by our notation for numbers.
  - bryan0 5y ago
    But isn’t this what the busy beaver numbers are? Numbers that we cannot write for arbitrary n but they do exist?
    - rssoconnor 5y ago
      I think this is a great question. The difference here is that with busy beaver numbers, e.g. BB(101) we can, presumably, write their values with our notation; it's just that we often cannot prove that any particular value written in our notation does indeed denote the value for that function. So if we write 100000...0000 with an unholy number of 0s there, it might be the value of BB(101), in particular we might not be able to prove that it isn't. On the other hand, for a non-standard number, c, it is definitely the case that 100000...0000 is not c, because, whatever c is, it is strictly greater than 100000...0000, or any other number we can write down. And thus when it comes to proofs about the termination of Turing machines that do not actually terminate, the unsound system is claiming that some machine terminates, but it doesn't terminate in 1 step, nor 2 steps, nor 3 steps, nor ... nor 100000...0000 steps, nor 100000...0001 steps, nor 100000...0002 steps, nor .... However, regarding the BB(101), the (presumably) sound systems we use such as PA, or ZFC, do not claim that BB(101) isn't 100000...0000. They just may not be able to prove anything one way or the other.
pavpanchekha 5y ago
You're absolutely right. ZFC + ¬Con(ZFC) is a weird set of axioms, and no mathematician really studies it. I skipped this point, because we weren't really discussing such axioms, but it's an important point that there are different levels of mathematical / philosophical commitments, and realism and PA are way stronger commitments than the ones people have about cardinalities.
Someone 5y ago
> because it asserts the existence of natural numbers that have no "written form" I don’t see why that should imply it wouldn't be "okay" to add ¬Con(ZFC). It may be highly counterintuitive, but the history of mathematics is full of counterintuitive results that nowadays are accepted as true in mainstream mathematics. Well-known examples are the existence of irrational numbers, the claim that the set of natural numbers has the same size as that of the rational numbers, the existence of hyperbolic geometry, and the Banach-Tarski paradox.
- rssoconnor 5y ago
  It's not "okay" because such a system proves that various particular Turing machines halt when, in fact, those machines do not halt. See https://news.ycombinator.com/item?id=27847719 https://news.ycombinator.com/item?id=27847719. But to be a bit more specific, ¬Con(ZFC) says that the Turing machine that searches for a contradiction in ZFC does indeed halt. However (in all likelihood) such a machine does not actually halt, in the sense that it does not halt in 1 step, and it does not halt in 2 steps, and it does not halt in 3 steps, etc., and indeed (in all likelihood) for each numeral n, ZFC even proves that the machine does not halt in n steps. (Now there is a small possibility that maybe such a machine does halt in some particular number of steps. If it does actually halt, that means it has found a proof that ZFC is inconsistent. But this scenario is even worse, because it means that ZFC itself is not only unsound, but inconsistent, (and hence ZFC+¬Con(ZFC) is also inconsistent). In particular ZFC+¬Con(ZFC) being inconsistent means it proves that every Turing machine halts, which is even more wrong in general, even if it happens to be right about this particular machine.)
  - a1369209993 5y ago
    > such a system proves that various particular Turing machines halt when, []in fact[], those machines do not halt. Er, no. The fact is that there is no fact of the matter as to whether those particular Turing machines either a: do not halt at all, or b: halt after a (colloquially) infinite number of steps. (A implication of there being no fact of the matter is that, empirically, we can't tell the difference by running them, but we can't tell the difference for a machine that halts in 2^(2^(2^256)) steps (or not at all) either, so that's not very interesting on it's own.) (As you note, we don't actually know that (for example) a Turing machines looking for contradictions in ZFC is one of those particular machines; indeed I'm not sure offhand if we actually know of any specific example of such a machine. But that's presumably not the issue here.)
thaumasiotes 5y ago
> the resulting system is unsound (in the sense of Tarski) because it asserts the existence of natural numbers that have no "written form" (i.e. the existance of natural numbers that are larger than any term you can write to denote a natural number). Isn't this a straightforward implication of nonstandard analysis?
ummonk 5y ago
'because it asserts the existence of natural numbers that have no "written form"' I mean, mainstream axiomatic systems assert the existence of real numbers that have no written form (after all, only countably many entities can have a written form), so how is this any different?

tgflynn 5y ago

> he resulting system is unsound (in the sense of Tarski) because it asserts the existence of natural numbers that have no "written form" (i.e. the existance of natural numbers that are larger than any term you can write to denote a natural number). Isn't that basically the definition of the natural numbers, ie. if you write down any natural number (say n) I can always construct a natural number that is larger than it (like n+1) ?

chongli 5y ago
If you can write down the natural number n, you can write down n+1. Of course, you can't write down the entire set of natural numbers but that is not a natural number.
- skybrian 5y ago
  On any storage system you will eventually run out of memory, so there will always be a maximum integer that you can write down with what you have, and we can only write down a vanishingly small subset of the natural numbers. Of course, this isn’t what mean when they talk about “writing down” a number, but I’ve long thought that assuming the existence of natural numbers that you can’t write down is poetically apt. In some sense, the set of natural numbers is “too big” to be about everyday finite numbers alone and it seems fitting to acknowledge that our usual axioms can’t exclude weirdo large finite numbers that are simply too big to ever reach.
kmill 5y ago
This surprisingly doesn't mean repeatedly adding 1 will exhaust all natural numbers -- there are models for the natural numbers with elements that can't be reached this way! The ultrafilter construction gives one such model. You take the set of all sequences of natural numbers (n1, n2, n3, ...) then use an ultrafilter to decide which of these sequences are considered to be equal. The usual operations of natural numbers are defined term-by-term. You can think of the usual natural numbers as being the sequences (0,0,0,...), (1,1,1,...), (2,2,2,...) and so on. However, there are many additional numbers in this system, like (0,1,2,...) that are strictly greater than all the usual numbers, and these cannot be reached by repeatedly adding one. (The reason (0,1,2,...) is greater than (n,n,n,...) is that if we do the comparison term-by-term we get (false,false,...,false,true,true,true,...), and the ultrafilter will decide the comparison is true because it is true for all but finitely many terms. Ultrafilters are devices to consistently turn infinite sequences of trues and falses into a single decision, but every ultrafilter will make a true decision in the case there are only finitely many falses.) Counter-intuitively, proofs by induction still work for this system... speaking with no authority here, maybe an intuition is that it's doing a hypercomputation.
- R0b0t1 5y ago
  Can you explain what use these have? If natural numbers are (n, n, n, ...) then you have just made a new type of number not comparable to natural numbers.
  - kmill 5y ago
    A theoretical use is that it shows that the axioms of the natural numbers (the Peano axioms) aren't enough to pin down what we think the natural numbers should be -- there are these crazy non-standard natural numbers out there! In context of the discussion, this non-standard model of the natural numbers gives some intuition about what happens if the consistency of ZFC is independent of ZFC and you add in the axiom that ZFC is inconsistent: your natural numbers will have to be something similarly weird. > you have just made a new type of number not comparable to natural numbers But they are comparable. The everyday natural numbers are embedded in this new system, which is what these (n,n,n,...) elements represent. One way to interpret what we've done here is to add in infinities to the number system so that all the normal operations still work, and there's even a total ordering on them! Using the real numbers instead of the naturals, you get the so-called nonstandard real numbers, which is the number system used in nonstandard analysis. Nonstandard analysis is a way to do analysis without epsilon-delta proofs. Nonstandard reals include infinitesimals and infinities, similar to nonstandard naturals having infinities. There are even textbooks on the subject -- I haven't read them, but they claim it makes analysis easier. The last thing that comes to mind is that nonstandard numbers of this exact type show up when you study certain infinite-dimensional number systems and calculate the points (like in the end of my comment).
rssoconnor 5y ago
Dropping down to Peano Arithmetic for a moment. We can consider adding a new constant 'c' for a natural number to the language along with the following infinite list of axioms about this remarkable constant: - 0 < c - 1 < c - 2 < c - 3 < c ... Adding all these axioms is consistent. I.e. you can do induction upto 'c', whatever it is. Why is it consistent? Because if there was a contradiction, the proof of such a contradiction would be finite, and hence can only use a finite number of these new axioms (this is a so-call compactness argument). But clearly any finite subset of this list of axioms is consistent because it has a model where c is just defined to be 1 more than the largest numeral appearing in that list. But all those infinite number of axioms taken together creates an unsound system because it claims that 'c' denotes a natural number that is larger than every written numeral. Heading back to ZFC land, it turns out that (assuming ¬Con(ZFC) is independent of ZFC) adding ¬Con(ZFC) to ZFC similarly is similarly unsound in that it yields only models that have elements that are larger than every written numeral.
- skissane 5y ago
  > in that it yields only models that have elements that are larger than every written numeral. Are these like hyperintegers (or should I say hypernaturals), as in the hyperrreal numbers used in non-standard analysis?
- im3w1l 5y ago
  This sounds a little bit like an argument against systems with an infinite number of axioms to me. Or maybe it's fine but only under certain conditions?
hypersoar 5y ago
You can find a natural number that is bigger than any one natural number, but you can't write one down that's bigger than every natural number in the ZFC sense.
- dwohnitmok 5y ago
  > that's bigger than every natural number in the ZFC sense. I'm not sure what you mean by this. Even for nonstandard models of the natural numbers there will never be a single number larger than all other numbers, since that violate the Peano axioms. Did you mean by "in the ZFC sense" "the standard model?"
- gooberwonder 5y ago
  45,000,000,001?
  - agalunar 5y ago
    Look around you!
- munk-a 5y ago
  Do you mean that given finite resources (like time and matter) we would be unable to express the number? Or are you talking about a sort of recursive thing where writing down a number which is a sum of all natural numbers up to and including itself is impossible since that number is bigger each time you look at it?
l33t2328 5y ago
I don’t believe a consequence of the axioms discussed is that there exist natural numbers with no “written form.” Do you have a proof or citation?
- rssoconnor 5y ago
  For this entire argument I will be operating under the assumption that ¬Con(ZFC) is independent of ZFC. ZFC+¬Con(ZFC) proves "there EXISTS a natural number x such that x is an encoding of a proof in ZFC of 0=1". Now suppose there is actually a numeral n, i.e. a specific written term written using symbols, e.g. (+,*,1), such that ZFC+¬Con(ZFC) proves that "n is an encoding of a proof in ZFC of 0=1". We can mechanically decode such a n and check if it is indeed a proof that that ZFC proves "0=1" or not. There are two possibilities: (a) the check is successful and thus we have found proof of a contradiction in ZFC. But if ZFC is inconsistent, then it proves everything. In particular ZFC proves ¬Con(ZFC), which violates our assumption that ¬Con(ZFC) is independent of ZFC. Alternatively (b) our check fails and n does not encode a proof in ZFC of 0=1. But that statement "n does not encode a proof in ZFC of 0=1" is a true Delta_0 statement, and we can prove by induction that ZFC proves every true Delta_0 statement. Thus we can prove that ZFC proves "n does not encode a proof 0=1", and hence ZFC+¬Con(ZFC) proves "n does not encode a proof 0=1". But now we have found a statement Q such that ZFC+¬Con(ZFC) proves both Q and also ¬Q. This means that ZFC+¬Con(ZFC) is inconsistent. But if ZFC+¬Con(ZFC) is inconsistent, by the deduction theorem, ZFC proves ¬¬Con(ZFC), or equivalently ZFC proves Con(ZFC). This contradicts our assumption that ¬Con(ZFC) is independent of ZFC (it also implies that ZFC is inconsistent). Thus we are left with the conclusion that there is no such numeral n. However it is still the case that ZFC+¬Con(ZFC) proves "there EXISTS a natural number x such that x is an encoding of a proof in ZFC of 0=1", and the only way this can be the case is any such x is a "natural number" which has no numeral that denotes it.

lupire 5y ago

why is that "unsound"? what's wrong with an unwritable natural? Almost all reals are unwritable.

dogecoinbase 5y ago
Soundness in this sense (sigma_1 soundness) is defined by equivalency to the standard model (specifically, all sentences provable in the system must be provable in the standard model).
- dwohnitmok 5y ago
  It is defined by equivalency to a standard model. Whether there is a single standard model is a philosophical question (which granted most, but not all, set theorists tend to agree with). Hence sigma_1 soundness is from a purely mathematical point of view a relative statement.
rssoconnor 5y ago
Mostly because it implies that some Turing machines halt that actually do not halt. That is unless you are willing to accept that a Turing machine can halt in some number of steps that is beyond any number that can be written. And I don't mean can't be written in the sense that we don't have enough paper. Just cannot be written in principle at all by our notation for numbers.
- bryan0 5y ago
  But isn’t this what the busy beaver numbers are? Numbers that we cannot write for arbitrary n but they do exist?
  - rssoconnor 5y ago
    I think this is a great question. The difference here is that with busy beaver numbers, e.g. BB(101) we can, presumably, write their values with our notation; it's just that we often cannot prove that any particular value written in our notation does indeed denote the value for that function. So if we write 100000...0000 with an unholy number of 0s there, it might be the value of BB(101), in particular we might not be able to prove that it isn't. On the other hand, for a non-standard number, c, it is definitely the case that 100000...0000 is not c, because, whatever c is, it is strictly greater than 100000...0000, or any other number we can write down. And thus when it comes to proofs about the termination of Turing machines that do not actually terminate, the unsound system is claiming that some machine terminates, but it doesn't terminate in 1 step, nor 2 steps, nor 3 steps, nor ... nor 100000...0000 steps, nor 100000...0001 steps, nor 100000...0002 steps, nor .... However, regarding the BB(101), the (presumably) sound systems we use such as PA, or ZFC, do not claim that BB(101) isn't 100000...0000. They just may not be able to prove anything one way or the other.

pavpanchekha 5y ago

You're absolutely right. ZFC + ¬Con(ZFC) is a weird set of axioms, and no mathematician really studies it. I skipped this point, because we weren't really discussing such axioms, but it's an important point that there are different levels of mathematical / philosophical commitments, and realism and PA are way stronger commitments than the ones people have about cardinalities.

Someone 5y ago

> because it asserts the existence of natural numbers that have no "written form" I don’t see why that should imply it wouldn't be "okay" to add ¬Con(ZFC). It may be highly counterintuitive, but the history of mathematics is full of counterintuitive results that nowadays are accepted as true in mainstream mathematics. Well-known examples are the existence of irrational numbers, the claim that the set of natural numbers has the same size as that of the rational numbers, the existence of hyperbolic geometry, and the Banach-Tarski paradox.

rssoconnor 5y ago
It's not "okay" because such a system proves that various particular Turing machines halt when, in fact, those machines do not halt. See https://news.ycombinator.com/item?id=27847719 https://news.ycombinator.com/item?id=27847719. But to be a bit more specific, ¬Con(ZFC) says that the Turing machine that searches for a contradiction in ZFC does indeed halt. However (in all likelihood) such a machine does not actually halt, in the sense that it does not halt in 1 step, and it does not halt in 2 steps, and it does not halt in 3 steps, etc., and indeed (in all likelihood) for each numeral n, ZFC even proves that the machine does not halt in n steps. (Now there is a small possibility that maybe such a machine does halt in some particular number of steps. If it does actually halt, that means it has found a proof that ZFC is inconsistent. But this scenario is even worse, because it means that ZFC itself is not only unsound, but inconsistent, (and hence ZFC+¬Con(ZFC) is also inconsistent). In particular ZFC+¬Con(ZFC) being inconsistent means it proves that every Turing machine halts, which is even more wrong in general, even if it happens to be right about this particular machine.)
- a1369209993 5y ago
  > such a system proves that various particular Turing machines halt when, []in fact[], those machines do not halt. Er, no. The fact is that there is no fact of the matter as to whether those particular Turing machines either a: do not halt at all, or b: halt after a (colloquially) infinite number of steps. (A implication of there being no fact of the matter is that, empirically, we can't tell the difference by running them, but we can't tell the difference for a machine that halts in 2^(2^(2^256)) steps (or not at all) either, so that's not very interesting on it's own.) (As you note, we don't actually know that (for example) a Turing machines looking for contradictions in ZFC is one of those particular machines; indeed I'm not sure offhand if we actually know of any specific example of such a machine. But that's presumably not the issue here.)

thaumasiotes 5y ago

> the resulting system is unsound (in the sense of Tarski) because it asserts the existence of natural numbers that have no "written form" (i.e. the existance of natural numbers that are larger than any term you can write to denote a natural number). Isn't this a straightforward implication of nonstandard analysis?

ummonk 5y ago

'because it asserts the existence of natural numbers that have no "written form"' I mean, mainstream axiomatic systems assert the existence of real numbers that have no written form (after all, only countably many entities can have a written form), so how is this any different?