[Tarski’s theorem] asserts that there’s no first-order description of what statements are true in a system that lies in the system.
You’d need be careful about what “system” or “description” are you talking about, since you can weakly represent, say, the set of statements true in Robinson arithmetic (which is recursively enumerable), in Robinson arithmetic. There is a formula s(-) with one free variable such that
Q |- s(gn(f)) iff Q |- f
where gn(f) is the Gödel number of (arbitrary) statement f and Q is Robinson arithmetic.
Yes, I know that. I was being deliberately imprecise because it is very easy in this case to get lost in the technical details. My intention was not to convey the theorem’s precise statement but rather convey to Tim why it doesn’t apply in the context he’s trying to use it.
I know you know that, but I couldn’t quite naturally interpret your informal statement as saying the formally correct thing, so had to make the clarification.
You’d need be careful about what “system” or “description” are you talking about, since you can weakly represent, say, the set of statements true in Robinson arithmetic (which is recursively enumerable), in Robinson arithmetic. There is a formula s(-) with one free variable such that
Q |- s(gn(f)) iff Q |- f
where gn(f) is the Gödel number of (arbitrary) statement f and Q is Robinson arithmetic.
Yes, I know that. I was being deliberately imprecise because it is very easy in this case to get lost in the technical details. My intention was not to convey the theorem’s precise statement but rather convey to Tim why it doesn’t apply in the context he’s trying to use it.
I know you know that, but I couldn’t quite naturally interpret your informal statement as saying the formally correct thing, so had to make the clarification.