A program that accepts exactly any desired finite set, in the right universe
jdh.hamkins.org
jdh.hamkins.org
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.
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.
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.
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.
In the case in the article, P is "e accepts such-and-such".
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.