Talk:Tarski's undefinability theorem

Indefinability?

Not really an English word, even though for some odd reason it does get a fair number of Google hits. Should be moved to Tarski's undefinability theorem, or better, Tarski's theorem on the undefinability of truth, which I think is the standard name. --Trovatore 05:42, 9 March 2006 (UTC)

Looking it up in www.m-w.com, I find "indefinable" is an English word, which I suppose I knew. I still maintain it's not a mathematical English word. It's used for qualities like someone's indefinable charm, not for sets that have no definition of a specified form. --Trovatore 05:49, 9 March 2006 (UTC)

• JA: Personally, I prefer TIT to TUT. Jon Awbrey 07:06, 9 March 2006 (UTC)

References

I edited the article and addeda a references tag. The following points need to be addressed:

• I could swear I read (with my own eyes) a footnote by Tarski where he claims he independently proved the theorem, apart from Godel's work. The article right now is self-contradictory on this issue. I'll dig up my reference.
• The last paragraph says (or does it?) that negation is not necessary. The proof given clearly uses negation. A reference for the last paragraph would be helpful.

By the way, I agree with Trovatore that indefinability is not the right word. CMummert 03:37, 18 July 2006 (UTC)

I have verified to my satisfaction that Tarski did state in print that he developed his theorem independently of Gödel's work. By the way, my memory is that he believed, after seeing Gödel's paper, that he was only a few years short of proving the same thing. CMummert 03:54, 18 July 2006 (UTC)

I think this is discussed in Feferman and Feferman's biography of Tarski. —Preceding unsigned comment added by 207.241.238.233 (talk) 05:46, 25 September 2007 (UTC)

See: Roman Murakowski, "Undefinability of truth. The problem of the priority: Tarski vs. Gödel", History and Philosophy of Logic 19 (1998), 153-160.[1] I think this reference should be useful for expanding the article and correcting a few mistakes in it.

Paraconsistency

I would really like a reference for this claim: "Although some have claimed otherwise, Tarski's Theorem is not restricted to bivalent classical logic. For example, it can be generalized to interpreted languages based on many-valued logic, such as fuzzy logic, and to dialetheism, paraconsistent logic, etc." I think this claim is incorrect and Tarski's theorem does not hold in a paraconsistent language, because the proof of the theorem uses reductio ad absurdum, and absurdities are allowed in paraconsistent logics. (Analogously for Gödel's incompletess theorem.) 130.37.20.20 15:58, 11 January 2007 (UTC)

Although some have claimed otherwise, Tarski's Theorem is not restricted to bivalent [[classical logic]]. For example, it can be generalized to interpreted languages based on [[many-valued logic]], such as [[fuzzy logic]], and to [[dialetheism]], [[paraconsistent logic]], etc

I never liked that sentence anyway, so I will move it here. I left the rest of the paragraph, which is correct. CMummert · talk 16:55, 11 January 2007 (UTC)

You are misreading the claim. It does not claim that the theorem can be proven *with* paraconsistent logic, it states that the theorem can be proven *for* paraconsistent logics. 84.208.71.48 (talk) 19:58, 30 March 2016 (UTC)

That is plausible. Is there a paper or book that we could use as a reference? There are so many claims in the sentence: four different logic, and an "etc", and the suggestion that "some have claimed otherwise". It's hard to tell where to start to explain the details of the sentence. — Carl (CBM · talk) 18:36, 2 April 2016 (UTC)

Gödel numbers

The proof does assume that every L-formula has a Gödel number, Does this mean that the result does not hold for languages that are uncountable sets? Taemyr (talk) 18:48, 10 January 2008 (UTC)

If you could define a language that consists of an uncountable infinite set of formulas, this proof probably wouldn't hold anymore. However, proofs in such a language are not machine-checkable, and such a language must allow infinitely long formulas, i.e. formulas with infinitely many symbols. So such a language would certainly not be usefull in mathematical logic, and it is arguable if it can be considered a formal language at all. Somejan (talk) 09:53, 1 July 2008 (UTC)

Such a language needn't involve infinitely long formulas; it could just have an uncountable number of constants, for example. Anyway, the proof would still go through, for a suitably expanded notion of Gödel number. The point is, there can be no definable surjection from T to the definable predicates on T, whatever the type T is (be it integers, strings, real numbers, pizza toppings, or anything else). (Of course, this is just Cantor's theorem in the category of definable maps, as was essentially pointed out by Lawvere). -Chinju (talk) 08:57, 21 November 2008 (UTC)

fragments of L

I'm not sure, but it seems to me that there is a $\Sigma _{0}^{1}$ formula $T(\phi )$ that defines the truth of $\Pi _{0}^{1}$ sentences $\phi$ (this basically is the halting problem). Is that correct? Does it keep going that way up the arithmetic hierarchy, i.e. for arbitrary k, is there an arithmetic formula (of quantifier depth greater than k) that defines the truth of sentences at level k? It would be nice if the article were explicit about this. 67.117.147.249 (talk) 07:12, 10 August 2009 (UTC)

Your notation seems to be backwards, so I am not sure exactly what you mean. But the answer to the question you seem to be asking is Post's theorem. This gives as a corollary that one can define the truth of $\Sigma _{k}^{0}$ formulas with a $\Sigma _{k}^{0}$ formula, and for $\Pi _{k}^{0}$ formulas with a $\Pi _{k}^{0}$ formula. The formulas used to define truth will be so-called universal $\Sigma _{k}^{0}$ and $\Pi _{k}^{0}$ formulas.

But there is no $\Sigma _{1}^{0}$ formula ψ(x) with the property that, for every $\Pi _{1}^{0}$ formula φ,

$(\mathbb {N} \vDash \phi )\Leftrightarrow (\mathbb {N} \vDash \psi (\#(\phi )))$

This also follows from Post's theorem. I will try to add some information about universal formulas to that article at some point. — Carl (CBM · talk) 12:24, 10 August 2009 (UTC)

second order arithmetic

If I understand the hyperarithmetical theory article, the truth predicate for PA can be written as a formula in second-order arithmetic. Is that correct? Should this article mention it? 66.127.55.192 (talk) 14:37, 7 February 2010 (UTC)

It would be an example that the truth predicate for one language can be expressed in a stronger language. It's not really surprising, and does not contradict the theorem. Taemyr (talk) 17:05, 7 February 2010 (UTC)

Of course it doesn't contradict the theorem, but it's not obvious to a non-expert. I only realized it after looking at that other article earlier. 66.127.55.192 (talk) 20:31, 7 February 2010 (UTC)

I added a paragraph; is that what you meant? — Carl (CBM · talk) 23:43, 7 February 2010 (UTC)

Yes, thanks. 66.127.55.192 (talk) 00:10, 8 February 2010 (UTC)

Error?: "However, T* is $\Sigma^0_k$ complete for all $k$." Should "complete" be "hard" instead?

I'm familiar with "complete" as used in complexity (Complete_(complexity)). For that usage, "complete" is wrong here (because the arithmetical hierarchy does not collapse, as stated in the proof containing the referenced sentence). I would expect the term "hard" here instead. —Preceding unsigned comment added by Enoksrd (talk • contribs) 20:37, 22 June 2010 (UTC)

You're completely correct. Thanks for pointing this out. — Carl (CBM · talk) 23:12, 22 June 2010 (UTC)

Theorem formulation

I have trouble believing the theorem statement is actually correct. I think that the formula True(x) cannot be a function of another formula, but must be a function of the code number of x, as usual practice when the diagonalization lemma is invoked. For instance, the hypothetic True is assumed to define the set of code numbers of true sentences, so it should be a predicate on code numbers. Moreover, in the proof, how do you otherwise define a formula S referring to itself?

Hence, I would guess that the correct statement of the theorem is the following.

Let L be the language of first-order arithmetic, and let N be the standard structure for L. Thus (L, N) is the "interpreted first-order language of arithmetic." Let T denote the set of L-sentences true in N, T* the set of code numbers of the sentences in T, and g the function taking L-sentences to their code numbers. The following theorem answers the question: Can T* be defined by a formula of first-order arithmetic?

Tarski's undefinability theorem: There is no L-formula True(x) which defines T*. That is, there is no L-formula True(x) such that for every L-formula x, True(g(x)) ↔ x is true.

A similar change needs to be done in the subsequent proof sketch. --Blaisorblade (talk) 15:09, 3 February 2012 (UTC)

Thank you for the correction, you're quite right. — Carl (CBM · talk) 12:24, 4 February 2012 (UTC)

what does "holds" mean in theorem and proof?

"holds" appears in the text:

1: ... B ↔ A(g(B)) holds

2: ... True(g(A)) ↔ A holds

3: ...such that S ↔ ¬True(g(S)) holds

which does it mean:

1a: B is provable if and only if A(g(B)) is provable

1b: B ↔ A(g(B)) is provable

2a: True(g(A)) ↔ A is true in N

2b: ???

3a: S ↔ ¬True(g(S)) is true in N

3b: S ↔ ¬True(g(S)) is provable

3c: S is provable ↔ ¬True(g(S)) is provable

seems to me it is 1b, 2a, 3b. which is very inconsistent for the word "holds". or is it a defined term in logic, please clarify.

btw, i guess 3b implies 3a.

and, to help me make it clear, in ZFC set theory, all this means is that True() cannot be equivalent to Provable() because Provable is definable, and thus the problem is only with such S that is neither provable nor disprovable.

Itaj Sherman (talk) 22:07, 27 March 2018 (UTC)

It doesn't really mean anything. For example, this sentence

That is, there is no L-formula True(n) such that for every L-formula A, True(g(A)) ↔ A holds.

has exactly the same meaning if the word "holds" is simply deleted:

That is, there is no L-formula True(n) such that for every L-formula A, True(g(A)) ↔ A.

Using "holds" in the first sentence is just a style of writing so that there is a verb in prose in the clause after the comma, rather than only a formula. in the context of that paragraph, there is a model N of the formal system, so asserting a formula, saying a formula is true, or saying a formula holds all mean the formula is true in N. — Carl (CBM · talk) 23:18, 27 March 2018 (UTC)

Oh, I think then the text would be much clearer if it is stated explicitly "true in N" wherever this is what it means, instead of only in some places, and remove "holds" in these places. --Itaj Sherman (talk) 23:59, 27 March 2018 (UTC)

I see you already changed some places, that's better, thanks. Still some cases like B ↔ A(g(B)) holds in N, where it would be better to always say "true in N" and not "holds in N" (in some places and not others).--Itaj Sherman (talk) 00:04, 28 March 2018 (UTC)

I don't know if it's just me, but when I see different words in math text, it always makes me think it was deliberately written so because they should mean different things (like true/hold).--Itaj Sherman (talk) 00:08, 28 March 2018 (UTC)

That's understandable, and one of the arguments against elegant variation, particularly in technical material. Still, "holds" seems to me to be the natural word here, the one that would typically be used by mathematicians. --Trovatore (talk) 00:48, 28 March 2018 (UTC)