Any consistent and sufficiently strong system of first-order formal arithmetic fails to decide some independent Gödel sentence. We examine consistent first-order extensions of such systems. Our purpose is to discover what is minimally required by way of such extension in order to be able to prove the Gödel sentence in a non-trivial fashion. The extended methods of formal proof must capture the essentials of the so-called 'semantical argument' for the truth of the Gödel sentence. We are concerned to show that (...) the deflationist has at his disposal such extended methods-methods which make no use or mention of a truth-predicate. This consideration leads us to reassess arguments recently advanced-one by Shapiro and another by Ketland-against the deflationist's account of truth. Their main point of agreement is this: they both adduce the Gödel phenomena as motivating a 'thick' notion of truth, rather than the deflationist's 'thin' notion. But the so-called 'semantical argument', which appears to involve a 'thick' notion of truth, does not really have to be semantical at all. It is, rather, a reflective argument. And the reflections upon a system that are contained therein are deflationarily licit, expressible without explicit use or mention of a truth-predicate. Thus it would appear that this anti-deflationist objection fails to establish that there has to be more to truth than mere conformity to the disquotational T-schema. (shrink)

Proofs of Gödel's First Incompleteness Theorem are often accompanied by claims such as that the gödel sentence constructed in the course of the proof says of itself that it is unprovable and that it is true. The validity of such claims depends closely on how the sentence is constructed. Only by tightly constraining the means of construction can one obtain gödel sentences of which it is correct, without further ado, to say that they say of themselves that they are unprovable (...) and that they are true; otherwise a false theory can yield false gödel sentences. (shrink)

Hintikka makes a distinction between two kinds of games: truthconstituting games and truth-seeking games. His well-known game-theoretical semantics for first-order classical logic and its independence-friendly extension belongs to the first class of games. In order to ground Hintikka’s claim that truth-constituting games are genuine verification and falsification games that make explicit the language games underlying the use of logical constants, it would be desirable to establish a substantial link between these two kinds of games. Adapting a result from Thierry Coquand, (...) we propose such a link, based on a slight modification of Hintikka’s games, in which we allow backward playing for ∃loïse. In this new setting, it can be proven that sequent rules for first-order logic, including the cut rule, are admissible, in the sense that for each rule, there exists an algorithm which turns winning strategies for the premisses into a winning strategy for the conclusion. Thus, proofs, as results of truth-seeking games, can be seen. (shrink)