fbpx
Wikipedia

Tarski's undefinability theorem

Tarski's undefinability theorem, stated and proved by Alfred Tarski in 1933, is an important limitative result in mathematical logic, the foundations of mathematics, and in formal semantics. Informally, the theorem states that "arithmetical truth cannot be defined in arithmetic".[1]

The theorem applies more generally to any sufficiently strong formal system, showing that truth in the standard model of the system cannot be defined within the system.

History edit

In 1931, Kurt Gödel published the incompleteness theorems, which he proved in part by showing how to represent the syntax of formal logic within first-order arithmetic. Each expression of the formal language of arithmetic is assigned a distinct number. This procedure is known variously as Gödel numbering, coding and, more generally, as arithmetization. In particular, various sets of expressions are coded as sets of numbers. For various syntactic properties (such as being a formula, being a sentence, etc.), these sets are computable. Moreover, any computable set of numbers can be defined by some arithmetical formula. For example, there are formulas in the language of arithmetic defining the set of codes for arithmetic sentences, and for provable arithmetic sentences.

The undefinability theorem shows that this encoding cannot be done for semantic concepts such as truth. It shows that no sufficiently rich interpreted language can represent its own semantics. A corollary is that any metalanguage capable of expressing the semantics of some object language (e.g. a predicate is definable in Zermelo-Fraenkel set theory for whether formulae in the language of Peano arithmetic are true in the standard model of arithmetic[2]) must have expressive power exceeding that of the object language. The metalanguage includes primitive notions, axioms, and rules absent from the object language, so that there are theorems provable in the metalanguage not provable in the object language.

The undefinability theorem is conventionally attributed to Alfred Tarski. Gödel also discovered the undefinability theorem in 1930, while proving his incompleteness theorems published in 1931, and well before the 1933 publication of Tarski's work (Murawski 1998). While Gödel never published anything bearing on his independent discovery of undefinability, he did describe it in a 1931 letter to John von Neumann. Tarski had obtained almost all results of his 1933 monograph "The Concept of Truth in the Languages of the Deductive Sciences" between 1929 and 1931, and spoke about them to Polish audiences. However, as he emphasized in the paper, the undefinability theorem was the only result he did not obtain earlier. According to the footnote to the undefinability theorem (Twierdzenie I) of the 1933 monograph, the theorem and the sketch of the proof were added to the monograph only after the manuscript had been sent to the printer in 1931. Tarski reports there that, when he presented the content of his monograph to the Warsaw Academy of Science on March 21, 1931, he expressed at this place only some conjectures, based partly on his own investigations and partly on Gödel's short report on the incompleteness theorems "Einige metamathematische Resultate über Entscheidungsdefinitheit und Widerspruchsfreiheit" [Some metamathematical results on the definiteness of decision and consistency], Austrian Academy of Sciences, Vienna, 1930.

Statement edit

We will first state a simplified version of Tarski's theorem, then state and prove in the next section the theorem Tarski proved in 1933.

Let   be the language of first-order arithmetic. This is the theory of the natural numbers, including their addition and multiplication, axiomatized by the first-order Peano axioms. This is a "first-order" theory: the quantifiers extend over natural numbers, but not over sets or functions of natural numbers. The theory is strong enough to describe recursively defined integer functions such as exponentiation, factorials or the Fibonacci sequence.

Let   be the standard structure for   i.e.   consists of the ordinary set of natural numbers and their addition and multiplication. Each sentence in   can be interpreted in   and then becomes either true or false. Thus   is the "interpreted first-order language of arithmetic".

Each formula   in   has a Gödel number   This is a natural number that "encodes"   In that way, the language   can talk about formulas in   not just about numbers. Let   denote the set of  -sentences true in   and   the set of Gödel numbers of the sentences in   The following theorem answers the question: Can   be defined by a formula of first-order arithmetic?

Tarski's undefinability theorem: There is no  -formula   that defines   That is, there is no  -formula   such that for every  -sentence     holds in  .

Informally, the theorem says that the concept of truth of first-order arithmetic statements cannot be defined by a formula in first-order arithmetic. This implies a major limitation on the scope of "self-representation". It is possible to define a formula   whose extension is   but only by drawing on a metalanguage whose expressive power goes beyond that of  . For example, a truth predicate for first-order arithmetic can be defined in second-order arithmetic. However, this formula would only be able to define a truth predicate for formulas in the original language  . To define a truth predicate for the metalanguage would require a still higher metametalanguage, and so on.

To prove the theorem, we proceed by contradiction and assume that an  -formula   exists which is true for the natural number   in   if and only if   is the Gödel number of a sentence in   that is true in  . We could then use   to define a new  -formula   which is true for the natural number   if and only if   is the Gödel number of a formula   (with a free variable  ) such that   is false when interpreted in   (i.e. the formula   when applied to its own Gödel number, yields a false statement). If we now consider the Gödel number   of the formula  , and ask whether the sentence   is true in  , we obtain a contradiction. (This is known as a diagonal argument.)

The theorem is a corollary of Post's theorem about the arithmetical hierarchy, proved some years after Tarski (1933). A semantic proof of Tarski's theorem from Post's theorem is obtained by reductio ad absurdum as follows. Assuming   is arithmetically definable, there is a natural number   such that   is definable by a formula at level   of the arithmetical hierarchy. However,   is  -hard for all   Thus the arithmetical hierarchy collapses at level  , contradicting Post's theorem.

General form edit

Tarski proved a stronger theorem than the one stated above, using an entirely syntactical method. The resulting theorem applies to any formal language with negation, and with sufficient capability for self-reference that the diagonal lemma holds. First-order arithmetic satisfies these preconditions, but the theorem applies to much more general formal systems, such as ZFC.

Tarski's undefinability theorem (general form): Let   be any interpreted formal language which includes negation and has a Gödel numbering   satisfying the diagonal lemma, i.e. for every  -formula   (with one free variable  ) there is a sentence   such that   holds in  . Then there is no  -formula   with the following property: for every  -sentence     is true in  .

The proof of Tarski's undefinability theorem in this form is again by reductio ad absurdum. Suppose that an  -formula   as above existed, i.e., if   is a sentence of arithmetic, then   holds in   if and only if   holds in  . Hence for all  , the formula   holds in  . But the diagonal lemma yields a counterexample to this equivalence, by giving a "liar" formula   such that   holds in  . This is a contradiction. QED.

Discussion edit

The formal machinery of the proof given above is wholly elementary except for the diagonalization which the diagonal lemma requires. The proof of the diagonal lemma is likewise surprisingly simple; for example, it does not invoke recursive functions in any way. The proof does assume that every  -formula has a Gödel number, but the specifics of a coding method are not required. Hence Tarski's theorem is much easier to motivate and prove than the more celebrated theorems of Gödel about the metamathematical properties of first-order arithmetic.

Smullyan (1991, 2001) has argued forcefully that Tarski's undefinability theorem deserves much of the attention garnered by Gödel's incompleteness theorems. That the latter theorems have much to say about all of mathematics and more controversially, about a range of philosophical issues (e.g., Lucas 1961) is less than evident. Tarski's theorem, on the other hand, is not directly about mathematics but about the inherent limitations of any formal language sufficiently expressive to be of real interest. Such languages are necessarily capable of enough self-reference for the diagonal lemma to apply to them. The broader philosophical import of Tarski's theorem is more strikingly evident.

An interpreted language is strongly-semantically-self-representational exactly when the language contains predicates and function symbols defining all the semantic concepts specific to the language. Hence the required functions include the "semantic valuation function" mapping a formula   to its truth value   and the "semantic denotation function" mapping a term   to the object it denotes. Tarski's theorem then generalizes as follows: No sufficiently powerful language is strongly-semantically-self-representational.

The undefinability theorem does not prevent truth in one theory from being defined in a stronger theory. For example, the set of (codes for) formulas of first-order Peano arithmetic that are true in   is definable by a formula in second order arithmetic. Similarly, the set of true formulas of the standard model of second order arithmetic (or  -th order arithmetic for any  ) can be defined by a formula in first-order ZFC.

See also edit

References edit

  1. ^ Cezary Cieśliński, "How Tarski Defined the Undefinable," European Review 23.1 (2015): 139–149.
  2. ^ Joel David Hamkins; Yang, Ruizhi (2013). "Satisfaction is not absolute". arXiv:1312.0670 [math.LO].

Primary sources edit

  • Tarski, A. (1933). Pojęcie Prawdy w Językach Nauk Dedukcyjnych (in Polish). Nakładem Towarzystwa Naukowego Warszawskiego.
  • Tarski, A. (1936). (PDF). Studia Philosophica (in German). 1: 261–405. Archived from the original (PDF) on 9 January 2014. Retrieved 26 June 2013.
    • Tarski, A. (1983). "The Concept of Truth in Formalized Languages" (PDF). In Corcoran, J. (ed.). Logic, Semantics, Metamathematics. Translated by J. H. Woodger. Hackett. English translation of Tarski's 1936 article.

Further reading edit

  • Bell, J. L.; Machover, M. (1977). A Course in Mathematical Logic. North-Holland.
  • Boolos, G.; Burgess, J.; Jeffrey, R. (2002). Computability and Logic (4th ed.). Cambridge University Press.
  • Lucas, J. R. (1961). . Philosophy. 36 (137): 112–27. doi:10.1017/S0031819100057983. S2CID 55408480. Archived from the original on 2007-08-19.
  • Murawski, R. (1998). . History and Philosophy of Logic. 19 (3): 153–160. doi:10.1080/01445349808837306. Archived from the original on 2011-06-08.
  • Smullyan, R. (1991). Godel's Incompleteness Theorems. Oxford Univ. Press.
  • Smullyan, R. (2001). "Gödel's Incompleteness Theorems". In Goble, L. (ed.). The Blackwell Guide to Philosophical Logic. Blackwell. pp. 72–89.

tarski, undefinability, theorem, this, article, includes, list, general, references, lacks, sufficient, corresponding, inline, citations, please, help, improve, this, article, introducing, more, precise, citations, august, 2023, learn, when, remove, this, temp. This article includes a list of general references but it lacks sufficient corresponding inline citations Please help to improve this article by introducing more precise citations August 2023 Learn how and when to remove this template message Tarski s undefinability theorem stated and proved by Alfred Tarski in 1933 is an important limitative result in mathematical logic the foundations of mathematics and in formal semantics Informally the theorem states that arithmetical truth cannot be defined in arithmetic 1 The theorem applies more generally to any sufficiently strong formal system showing that truth in the standard model of the system cannot be defined within the system Contents 1 History 2 Statement 3 General form 4 Discussion 5 See also 6 References 6 1 Primary sources 7 Further readingHistory editIn 1931 Kurt Godel published the incompleteness theorems which he proved in part by showing how to represent the syntax of formal logic within first order arithmetic Each expression of the formal language of arithmetic is assigned a distinct number This procedure is known variously as Godel numbering coding and more generally as arithmetization In particular various sets of expressions are coded as sets of numbers For various syntactic properties such as being a formula being a sentence etc these sets are computable Moreover any computable set of numbers can be defined by some arithmetical formula For example there are formulas in the language of arithmetic defining the set of codes for arithmetic sentences and for provable arithmetic sentences The undefinability theorem shows that this encoding cannot be done for semantic concepts such as truth It shows that no sufficiently rich interpreted language can represent its own semantics A corollary is that any metalanguage capable of expressing the semantics of some object language e g a predicate is definable in Zermelo Fraenkel set theory for whether formulae in the language of Peano arithmetic are true in the standard model of arithmetic 2 must have expressive power exceeding that of the object language The metalanguage includes primitive notions axioms and rules absent from the object language so that there are theorems provable in the metalanguage not provable in the object language The undefinability theorem is conventionally attributed to Alfred Tarski Godel also discovered the undefinability theorem in 1930 while proving his incompleteness theorems published in 1931 and well before the 1933 publication of Tarski s work Murawski 1998 While Godel never published anything bearing on his independent discovery of undefinability he did describe it in a 1931 letter to John von Neumann Tarski had obtained almost all results of his 1933 monograph The Concept of Truth in the Languages of the Deductive Sciences between 1929 and 1931 and spoke about them to Polish audiences However as he emphasized in the paper the undefinability theorem was the only result he did not obtain earlier According to the footnote to the undefinability theorem Twierdzenie I of the 1933 monograph the theorem and the sketch of the proof were added to the monograph only after the manuscript had been sent to the printer in 1931 Tarski reports there that when he presented the content of his monograph to the Warsaw Academy of Science on March 21 1931 he expressed at this place only some conjectures based partly on his own investigations and partly on Godel s short report on the incompleteness theorems Einige metamathematische Resultate uber Entscheidungsdefinitheit und Widerspruchsfreiheit Some metamathematical results on the definiteness of decision and consistency Austrian Academy of Sciences Vienna 1930 Statement editWe will first state a simplified version of Tarski s theorem then state and prove in the next section the theorem Tarski proved in 1933 Let L displaystyle L nbsp be the language of first order arithmetic This is the theory of the natural numbers including their addition and multiplication axiomatized by the first order Peano axioms This is a first order theory the quantifiers extend over natural numbers but not over sets or functions of natural numbers The theory is strong enough to describe recursively defined integer functions such as exponentiation factorials or the Fibonacci sequence Let N displaystyle mathcal N nbsp be the standard structure for L displaystyle L nbsp i e N displaystyle mathcal N nbsp consists of the ordinary set of natural numbers and their addition and multiplication Each sentence in L displaystyle L nbsp can be interpreted in N displaystyle mathcal N nbsp and then becomes either true or false Thus L N displaystyle L mathcal N nbsp is the interpreted first order language of arithmetic Each formula f displaystyle varphi nbsp in L displaystyle L nbsp has a Godel number g f displaystyle g varphi nbsp This is a natural number that encodes f displaystyle varphi nbsp In that way the language L displaystyle L nbsp can talk about formulas in L displaystyle L nbsp not just about numbers Let T displaystyle T nbsp denote the set of L displaystyle L nbsp sentences true in N displaystyle N nbsp and T displaystyle T nbsp the set of Godel numbers of the sentences in T displaystyle T nbsp The following theorem answers the question Can T displaystyle T nbsp be defined by a formula of first order arithmetic Tarski s undefinability theorem There is no L displaystyle L nbsp formula T r u e n displaystyle mathrm True n nbsp that defines T displaystyle T nbsp That is there is no L displaystyle L nbsp formula T r u e n displaystyle mathrm True n nbsp such that for every L displaystyle L nbsp sentence A displaystyle A nbsp T r u e g A A displaystyle mathrm True g A iff A nbsp holds in N displaystyle mathcal N nbsp Informally the theorem says that the concept of truth of first order arithmetic statements cannot be defined by a formula in first order arithmetic This implies a major limitation on the scope of self representation It is possible to define a formula T r u e n displaystyle mathrm True n nbsp whose extension is T displaystyle T nbsp but only by drawing on a metalanguage whose expressive power goes beyond that of L displaystyle L nbsp For example a truth predicate for first order arithmetic can be defined in second order arithmetic However this formula would only be able to define a truth predicate for formulas in the original language L displaystyle L nbsp To define a truth predicate for the metalanguage would require a still higher metametalanguage and so on To prove the theorem we proceed by contradiction and assume that an L displaystyle L nbsp formula T r u e n displaystyle mathrm True n nbsp exists which is true for the natural number n displaystyle n nbsp in N displaystyle mathcal N nbsp if and only if n displaystyle n nbsp is the Godel number of a sentence in L displaystyle L nbsp that is true in N displaystyle mathcal N nbsp We could then use T r u e n displaystyle mathrm True n nbsp to define a new L displaystyle L nbsp formula S m displaystyle S m nbsp which is true for the natural number m displaystyle m nbsp if and only if m displaystyle m nbsp is the Godel number of a formula f x displaystyle varphi x nbsp with a free variable x displaystyle x nbsp such that f m displaystyle varphi m nbsp is false when interpreted in N displaystyle mathcal N nbsp i e the formula f x displaystyle varphi x nbsp when applied to its own Godel number yields a false statement If we now consider the Godel number g displaystyle g nbsp of the formula S m displaystyle S m nbsp and ask whether the sentence S g displaystyle S g nbsp is true in N displaystyle mathcal N nbsp we obtain a contradiction This is known as a diagonal argument The theorem is a corollary of Post s theorem about the arithmetical hierarchy proved some years after Tarski 1933 A semantic proof of Tarski s theorem from Post s theorem is obtained by reductio ad absurdum as follows Assuming T displaystyle T nbsp is arithmetically definable there is a natural number n displaystyle n nbsp such that T displaystyle T nbsp is definable by a formula at level S n 0 displaystyle Sigma n 0 nbsp of the arithmetical hierarchy However T displaystyle T nbsp is S k 0 displaystyle Sigma k 0 nbsp hard for all k displaystyle k nbsp Thus the arithmetical hierarchy collapses at level n displaystyle n nbsp contradicting Post s theorem General form editTarski proved a stronger theorem than the one stated above using an entirely syntactical method The resulting theorem applies to any formal language with negation and with sufficient capability for self reference that the diagonal lemma holds First order arithmetic satisfies these preconditions but the theorem applies to much more general formal systems such as ZFC Tarski s undefinability theorem general form Let L N displaystyle L mathcal N nbsp be any interpreted formal language which includes negation and has a Godel numbering g f displaystyle g varphi nbsp satisfying the diagonal lemma i e for every L displaystyle L nbsp formula B x displaystyle B x nbsp with one free variable x displaystyle x nbsp there is a sentence A displaystyle A nbsp such that A B g A displaystyle A iff B g A nbsp holds in N displaystyle mathcal N nbsp Then there is no L displaystyle L nbsp formula T r u e n displaystyle mathrm True n nbsp with the following property for every L displaystyle L nbsp sentence A displaystyle A nbsp T r u e g A A displaystyle mathrm True g A iff A nbsp is true in N displaystyle mathcal N nbsp The proof of Tarski s undefinability theorem in this form is again by reductio ad absurdum Suppose that an L displaystyle L nbsp formula T r u e n displaystyle mathrm True n nbsp as above existed i e if A displaystyle A nbsp is a sentence of arithmetic then T r u e g A displaystyle mathrm True g A nbsp holds in N displaystyle mathcal N nbsp if and only if A displaystyle A nbsp holds in N displaystyle mathcal N nbsp Hence for all A displaystyle A nbsp the formula T r u e g A A displaystyle mathrm True g A iff A nbsp holds in N displaystyle mathcal N nbsp But the diagonal lemma yields a counterexample to this equivalence by giving a liar formula S displaystyle S nbsp such that S T r u e g S displaystyle S iff lnot mathrm True g S nbsp holds in N displaystyle mathcal N nbsp This is a contradiction QED Discussion editThe formal machinery of the proof given above is wholly elementary except for the diagonalization which the diagonal lemma requires The proof of the diagonal lemma is likewise surprisingly simple for example it does not invoke recursive functions in any way The proof does assume that every L displaystyle L nbsp formula has a Godel number but the specifics of a coding method are not required Hence Tarski s theorem is much easier to motivate and prove than the more celebrated theorems of Godel about the metamathematical properties of first order arithmetic Smullyan 1991 2001 has argued forcefully that Tarski s undefinability theorem deserves much of the attention garnered by Godel s incompleteness theorems That the latter theorems have much to say about all of mathematics and more controversially about a range of philosophical issues e g Lucas 1961 is less than evident Tarski s theorem on the other hand is not directly about mathematics but about the inherent limitations of any formal language sufficiently expressive to be of real interest Such languages are necessarily capable of enough self reference for the diagonal lemma to apply to them The broader philosophical import of Tarski s theorem is more strikingly evident An interpreted language is strongly semantically self representational exactly when the language contains predicates and function symbols defining all the semantic concepts specific to the language Hence the required functions include the semantic valuation function mapping a formula A displaystyle A nbsp to its truth value A displaystyle A nbsp and the semantic denotation function mapping a term t displaystyle t nbsp to the object it denotes Tarski s theorem then generalizes as follows No sufficiently powerful language is strongly semantically self representational The undefinability theorem does not prevent truth in one theory from being defined in a stronger theory For example the set of codes for formulas of first order Peano arithmetic that are true in N displaystyle mathcal N nbsp is definable by a formula in second order arithmetic Similarly the set of true formulas of the standard model of second order arithmetic or n displaystyle n nbsp th order arithmetic for any n displaystyle n nbsp can be defined by a formula in first order ZFC See also editChaitin s incompleteness theorem Measure of algorithmic complexityPages displaying short descriptions of redirect targets Godel s completeness theorem Fundamental theorem in mathematical logic Godel s incompleteness theorems Limitative results in mathematical logicReferences edit Cezary Cieslinski How Tarski Defined the Undefinable European Review 23 1 2015 139 149 Joel David Hamkins Yang Ruizhi 2013 Satisfaction is not absolute arXiv 1312 0670 math LO Primary sources edit Tarski A 1933 Pojecie Prawdy w Jezykach Nauk Dedukcyjnych in Polish Nakladem Towarzystwa Naukowego Warszawskiego Tarski A 1936 Der Wahrheitsbegriff in den formalisierten Sprachen PDF Studia Philosophica in German 1 261 405 Archived from the original PDF on 9 January 2014 Retrieved 26 June 2013 Tarski A 1983 The Concept of Truth in Formalized Languages PDF In Corcoran J ed Logic Semantics Metamathematics Translated by J H Woodger Hackett English translation of Tarski s 1936 article Further reading editBell J L Machover M 1977 A Course in Mathematical Logic North Holland Boolos G Burgess J Jeffrey R 2002 Computability and Logic 4th ed Cambridge University Press Lucas J R 1961 Mind Machines and Godel Philosophy 36 137 112 27 doi 10 1017 S0031819100057983 S2CID 55408480 Archived from the original on 2007 08 19 Murawski R 1998 Undefinability of truth The problem of the priority Tarski vs Godel History and Philosophy of Logic 19 3 153 160 doi 10 1080 01445349808837306 Archived from the original on 2011 06 08 Smullyan R 1991 Godel s Incompleteness Theorems Oxford Univ Press Smullyan R 2001 Godel s Incompleteness Theorems In Goble L ed The Blackwell Guide to Philosophical Logic Blackwell pp 72 89 Retrieved from https en wikipedia org w index php title Tarski 27s undefinability theorem amp oldid 1182054115, wikipedia, wiki, book, books, library,

article

, read, download, free, free download, mp3, video, mp4, 3gp, jpg, jpeg, gif, png, picture, music, song, movie, book, game, games.