Tarskiโ€™s result on the undefinability of truth

Assume ๐‹ is a logic which is under contradictory negationMathworldPlanetmath and has the usual truth-functional connectivesMathworldPlanetmath. Assume also that ๐‹ has a notion of formulaMathworldPlanetmathPlanetmath with one variable and of substitution. Assume that T is a theory of ๐‹ in which we can define surrogates for formulae of ๐‹, and in which all true instances of the substitution relationMathworldPlanetmath and the truth-functional connective relations are provable. We show that either T is inconsistent or T canโ€™t be augmented with a truth predicateMathworldPlanetmathPlanetmath ๐“๐ซ๐ฎ๐ž for which the following T-schema holds


Assume that the formulae with one variable of ๐‹ have been indexed by some suitable set that is representable in T (otherwise the predicate ๐“๐ซ๐ฎ๐ž would be next to useless, since if thereโ€™s no way to speak of sentencesMathworldPlanetmath of a logic, thereโ€™s little hope to define a truth-predicate for it). Denote the i:th element in this indexing by Bi. Consider now the following open formula with one variable


Now, since ๐‹๐ข๐š๐ซ is an open formula with one free variableMathworldPlanetmathPlanetmath itโ€™s indexed by some i. Now consider the sentence ๐‹๐ข๐š๐ซโข(i). From the T-schema we know that


and by the definition of ๐‹๐ข๐š๐ซ and the fact that i is the of ๐‹๐ข๐š๐ซโข(x) we have


which clearly is absurd. Thus there canโ€™t be an of T with a predicate ๐“๐ซ๐ฎ๐ญ๐ก for which the T-schema holds.

We have made several assumptionsPlanetmathPlanetmath on the logic ๐‹ which are crucial in order for this proof to go through. The most important is that ๐‹ is closed under contradictory negation. There are logics which allow truth-predicates, but these are not usually closed under contradictory negation (so that itโ€™s possible that ๐“๐ซ๐ฎ๐žโข(๐‹๐ข๐š๐ซโข(i)) is neither true nor false). These logics usually have stronger notions of negation, so that a sentence ยฌโขP says more than just that P is not true, and the propositionPlanetmathPlanetmathPlanetmath that P is simply not true is not expressible.

An example of a logic for which Tarskiโ€™s undefinability result does not hold is the so-called Independence Friendly logic, the semantics of which is based on game theory and which allows various generalised quantifiersMathworldPlanetmath (the Henkin branching quantifier, etc.) to be used.

Title Tarskiโ€™s result on the undefinability of truth
Canonical name TarskisResultOnTheUndefinabilityOfTruth
Date of creation 2013-03-22 13:49:19
Last modified on 2013-03-22 13:49:19
Owner mathcam (2727)
Last modified by mathcam (2727)
Numerical id 14
Author mathcam (2727)
Entry type Theorem
Classification msc 03B99
Related topic IFLogic