I've always been interested in learning formal logic, but I always seem to get frustrated by the ambiguity present in theorems like this, and how non-rigorous statements are. For instance: the first claim is "PA proves that e accepts only finitely many inputs". What exactly does this mean? PA does not have a notion of sets, let alone finite-ness. Perhaps PA proves (\exists n \forall x (accepts(e, x) \implies x <= n)). But in nonstandard models of PA, there could be an infinite number of symbols less than n, so it would not be correct to call this "finite" in contexts like this where we are talking about non-standard models. Maybe the intended statement is "For some standard integer n, PA proves (\forall x (accepts(e, x) \implies x <= n)). But that doesn't seem to jive with the other claims made because then there would be a global bound across all models. So then under our loose definition of finite, is A actually allowed to contain an infinite number of distinct objects in the model, so long as they are bounded by a nonstandard number? Can A contain nonstandard numbers? Can e check cases with nonstandard numbers "before" it checks cases with standard numbers? The article hand-waves away all these problems in ways that make the proof totally non-convincing. Admittedly, I've only got a BA in math, and the article is intended for someone with a lot more experience in the field, but I hit these same conceptual problems whenever I try to learn more.
I'm not an expert in logic, but I can help a bit here.
For reference, here is the theorem in the blog post:
There is a Turing machine program e, such that
(1) PA proves that e accepts only finitely many inputs.
(2) For any particular finite subset A of N, there is a model M of PA such that inside M, the program e accepts all and only the elements of A.
(3) Indeed, for any subset A of N, including infinite sets, there is a model M of PA such that inside M, program e accepts n if and only if n is in A.
What you call the "loose" definition of finite is indeed what's being used here. The way (1) is stated, it implies the definition of "finite" must be within PA itself (otherwise PA couldn't prove it). Your "loose" definition is the only way to define "finite" within PA itself.
You are correct that in the presence of non-standard numbers, a set that PA proves is "finite" could actually be infinite in the model. Indeed, that explains how (3) is even possible!
As for whether A can contain non-standard numbers, the answer is no. Note that A is a variable defined in the meta-theory, since it is in the statement of the theorem (2) and (3). Therefore the "standard" versus "non-standard" label doesn't apply to A. The trick here is that there's an implicit "conversion" that needs to happen when going from A in the metatheory (where it is a subset of N) to A as a set of numbers in M. When that conversion happens, all the elements will be standard. This is a more precise way of phrasing (2) that might help, where I've used quotes to indicate exactly what's a statement in PA (as opposed to meta-theory):
(2') For any particular finite set A in N, there is a model M of PA such that the statement "e accepts n" is true in M iff n is in A.
All non standard models of PA have the natural numbers as the initial segment. There can't be an infinite number of elements less than n where n is a natural number in any nonstandard model of PA.
Is natural number = standard natural number here? I can see why the standard natural numbers must have a finite number of predecessors (one can explicitly prove in PA all statements of the form (x = 0 || x = S0 || ... || x = n || x > n) for each fixed standard n). But for the same reason, each non-standard number is greater than all standard numbers. So while a non-standard model m might be able to prove a finiteness-implying statement like \exists n (P(x) \implies x <= n), the actual n that makes this statement true could be non-standard, and m could contain infinitely many (standard or non-standard) elements with P(x) true so long as they are all less than some non-standard n. The point is, I don't see how PA can have a satisfactory notion of finite-ness as one could use this to define standardness from within PA (x is standard iff there are finitely many y with y < x) which is not supposed to be possible.
The article is about finite subsets of N. N is the initial segment in every non standard model of PA. Hence your in=bjectiinnin your original post is not valid.
I'm not afraid of a theoretical article, but this is, even for me, very dry. While it sounds interesting, I'm not sure what universe even means in this context...
In the real world, Hamkins' program would search forever, never outputting anything. In the context of a "nonstandard" version of the line of natural numbers, "finite" no longer means what you think it means. In this context, Hamkin's program does output something after a "finite" number of steps, and Hamkins can make the program output whatever he wants by changing the meaning of "finite" instead of changing the program.
Goedel's incompleteness theorems guarantee the existence of non-standard models of set theory (and Peano arithmetic). Hamkins cleverly uses non-standard models to construct a single program that can (simplifying a bit) exhibit arbitrary behaviour, depending in which universe (= model of set theory) you interpret it.
I have three questions (insufficiently educated objections?) about this article:
1. It says "Clearly, PA proves that program e accepts only a finite set, since either no such proof is ever found, in which case e accepts nothing (and the empty set is finite), or else such a proof is found, in which case e accepts only that particular finite set. So PA proves that e accepts only finitely many inputs."
It's not at all clear to me that PA can prove this. This seems to be asking PA to prove that, if this program constructs a proof of a statement X (where X is of the form "e accepts such and such"), then X is true. From vague memory, not only is this far from clear, it would be actively problematic if this argument were valid due to Löb's theorem. Wouldn't it follow that PA was inconsistent?
2. In the first theorem in the article, e is explicitly constructable. Take e and search for an accepted input. Suppose such an input n is found in finite time. Then e accepts n. Assuming the theorem is right, there exists a model of PA in which e does not accept n. ISTM that, unless e accepts nothing at all, PA is inconsistent or proves false statements. What gives?
3. I would expect that e, as constructed in the paper, accepts no inputs because there are no proofs of the form it's looking for. If this were the case, the proof would fail at "meanwhile, assuming PA is consistent, then you cannot refute the assertion that program e accepts exactly the elements of some particular finite set A". I think that's an invalid argument. PA can't refute that assertion, but that doesn't mean that a stronger (and still consistent) theory can't refute it.
Unless I'm off base, I would think that, if PA is consistent, then the program never halts on any input, but that this assertion is unprovable in PA.
Edit: I can think of one way to make sense of most of this. Normally, I'd say that a Turing machine M accepts input x if M, given input x, enters a accept state after n steps for some natural number n. This could be extended to say that M nonstandard-accepts if it enters an accept state after n steps for a possibly nonstandard n.
This would permit M to nonstandard-accept inputs that it doesn't accept in the normal sense and for the set of nonstandard-accepted inputs to depend on the model in question. It would make understanding what the Turing machine does much more complicated, and it would be strange to say that the machine doesn't halt on input x (in the normal sense) but nonetheless nonstandard-accepts x.
It also doesn't address my question #1. (I think it resolves #2 and #3 though. e never halts, but it non-standard accepts languages that depend on the model.) And it makes the theorem much less interesting, IMO. If Turing machines are allowed to have a sense of acceptance that depends on the model, then it's not at all surprising to me that there are Turing machines that behave very flexibly depending on the model.
For 1., the fact that the program searches for a proof of a statement is completely irrelevant. It might just as well search for a string that can be appended to the statement to make it MD5-hash to a prime number.
In any case, either it finds such a thing, in which case it accepts the finite set in the statement, or it doesn't find anything, in which case it accepts the (finite) empty set.
The actual condition doesn't matter, PA can always do this kind of case analysis to prove the finiteness of the accepted set.
I still don't get it. The finitely many input part is irrelevant. Suppose we have a program that either produces a valid PA proof of a sentence P or fails to do so. Suppose further that, if the program failed to do so, it was obvious that P was true. This implies that P is true, but how would PA prove that?
In the case in the article, P is "e accepts such-and-such".
The claim is not that P is true. P is "e does not accept exactly {n_1, ..., n_k}". If it produces a proof, it accepts exactly {n_1, ..., n_k}, which is precisely the opposite of P.
If we limit ourselves to the standard model, this program will never terminate, because it tries to prove a false statement. In a nonstandard model, the program may succeed after a nonstandard "number" of steps to find a nonstandard "proof" of a false statement, after which it terminates by accepting the opposite of what the "proof" says it does.
Anyway, what exactly the program does before it accepts anything is actually irrelevant for point 1, which is only about the number of accepted inputs being finite. For that, you only have to look at the last steps, which only accept for a finite number of runs, even those that can never happen in the standard model.
