Didier Galmiche

Dominique Larchey-Wendling

Some Remarks on Relations between Proofs and Games

Abstract

This paper aims at studying relations between proof systems and games in a given logic and at analyzing what can be the interest and limits of a game formulation as an alternative semantic framework for modelling proof search and also for understanding relations between logics. In this perspective, we firstly study proofs and games at an abstract level which is neither related to a particular logic nor adopts a specific focus on their relations. Then, in order to instantiate such an analysis, we describe a dialogue game for intuitionistic logic and emphasize the adequateness between proofs and winning strategies in this game. Finally, we consider how games can be seen to provide an alternative formulation for proof search and we stress on the possible mix of logical rules and search strategies inside games rules. We conclude on the merits and limits of the game semantics as a tool for studying logics, validity in these logics and some relations between them.

Proofs and Games

In this section, we present a common terminology to present both proof systems and games at a relatively abstract level. Our aim consists in obtaining tools on which bridges can be built between the proof-theoretical approach and the game semantics approach in establishing the (universal) validity of logical formulae. We explain how proofs and games can be viewed as complementary notions. We illustrate how proof trees in calculi correspond to winning strategies in games and vice-versa.

Rule instances in deduction systems

We start with the definition of deduction system: it is composed of a set of statements denoted stm and a set of (rule) instances denoted inst. The notion of statement is basic and depends on the particular deduction system which is currently considered. It intuitively represents objects that can either be valid or invalid. An instance is a pair ([p 1 , . . . , p n ], c) in stm × stm composed of a finite list [p 1 , . . . , p n ] of premises and a conclusion c. Both p 1 , . . . , p n and c are statements. An instance is usually denoted:

p 1 .

. . p n c

In case n = 0, i.e., when the list of premises is empty, the instance is called an axiom. Remark that inst is not the set of all instances but only a selection of some instances. This set is usually described by logical rules which generate instances by substitution of their parameters (see below). Let us illustrate these points through examples.

Examples of deduction systems

Hilbert type systems for classical logic. In this case, statements are just formulae and stm is the set of formulae of classical propositional logic. The set of instances is composed of axioms like for example ([ ], (A ∧ B) ⊃ A) (for any formulae A and B) and the instances of the modus ponens rule ([A, A ⊃ B], B) (for any formulae A and B) denoted by:

(A ∧ B) ⊃ A Ax 1 A A ⊃ B B MP
The axiom Ax 1 has two parameters (A and B) and we denote by Ax 1 (A, B) the instance displayed. For rule MP , the parameters are A and B and the instance displayed is denoted MP (A, B). We might omit the value of parameters when they are obvious.

Gentzen sequent calculus for intuitionistic logic. The statements are sequents of the form A 1 , . . . , A k B, where A 1 , . . . , A k , B are formulae of intuitionistic logic. A 1 , . . . , A k B denotes a pair composed of a multiset of hypotheses A 1 , . . . , A k and a conclusion B. 1 In the case of the sequent calculus, instances look like

Γ, A C Γ, B C Γ, A ∨ B C ∨ L Γ A Γ A ∨ B ∨ R1 Γ B Γ A ∨ B ∨ R2 Γ, A ⊃ B A Γ, B C Γ, A ⊃ B C ⊃ L Γ, A B Γ A ⊃ B ⊃ R
where Γ is an arbitrary multiset of formulae and A, B, C are arbitrary formulae. These instances are denoted

∨ L (Γ, A, B, C), ∨ R1 (Γ, A, B), ∨ R2 (Γ, A, B), ⊃ L (Γ, A, B, C) and ⊃ R (Γ, A, B) respectively.

Validity, derivability and proofs

A validity V ∈ P(stm) is the set of statements which are supposed to be valid. Statements which do not belong to V are considered as invalid. The validity V is said to be closed w.r.t. an instance

([p 1 , . . . , p n ], c) if p 1 , . . . , p n ⊆ V im- plies c ∈ V .
In other words, the conclusion must be valid when the premises are. Usually, validities are defined through semantic means, i.e., by interpreting statements as semantical objects in some mathematical universe.

Any deduction system generates a particular validity called derivability which is the least validity closed under all the instances in the set inst. It is possible to provide an extensional definition of the notion of derivability through the notion of proof. A proof tree is a finite ordered tree labeled with statements such that for any node labeled by c, with a list of sons labeled by p 1 , . . . , p n respectively, the inclusion ([p 1 , . . . , p n ], c) ∈ inst holds. Thus a proof tree is build by composing instances, starting from axioms such as the following tree for Gentzen sequent systems:

Ax A, A ⊃ B A Ax A, B B ⊃ L A, A ⊃ B B
When c appears as the label of the root node of a proof tree T , we say that T is a proof of c. The notion of proof characterizes the notion of derivability because it can be shown that the statements which are derivable are exactly those which have a proof. Thus exhibiting a proof is a necessary and sufficient condition to establish derivability and the notions of derivability and provability are one and the same. The notion of underivability, i.e., the opposite of derivability, can also be defined extensively through the concept of refutation. A refutation tree is also a tree labeled with statements but contrary to proof trees, they can be infinite both in width or depth. The condition is that for each node labeled with c in the refutation tree, there is a one to one correspondance between the sons of c and thoses instances in inst which have c as conclusion and that each son is labeled with one of the premises of its corresponding instance (see [START_REF] Larchey-Wendling | réfutations et contre-modèles dans des logiques intuitionnistes[END_REF] for more detailed presentation).

Games and strategies

Now let us define the notion of game within this setting. A game has two players: the proponent P and the opponent O. Intuitively, the proponent P tries to prove (aka defend in game terminology) statements and O tries to refute (aka attack) the application of rule instances.

Each step of the game is a play by either P or O: first, the player receives the previous move, then he makes some choice (maybe according to a predefined strategy, see later), and finally moves by transmitting its choice to the other player. P plays instances in inst whereas O plays statements in stm.

Formally, a game is a strictly alternating sequence of plays by P and O which is non-empty, either finite or infinite, of the form:

O → c 0 → P → i 1 → O → p 1 → . . . → p k-1 → P → i k → O → p k → . . .

and which verifies the following rules:

1. the first move is by O which transmits a statement c 0 ∈ stm to P; 2. when P receives a move c ∈ stm from O, he choose an instance i ∈ inst for which c is the conclusion, i.e., i must be of the form ([. . .], c), and plays i;

3. when O receives a move i ∈ inst for P, he choose a statement p ∈ stm which is one of the premises of i, i.e., i must be of the form ([. . . , p, . . .], . . .), and plays p.

A game for the statement c is a game where the first move (played by O) is the statement c. A P-game is a (finite) game where the last move is played by P and an O-game is a (finite) game where the last move is played by O. An ∞-game is an infinite game. So each game is either a P-game, an O-game or an ∞-game and these three cases are mutually exclusive.

A game is finished if it cannot be extended anymore, i.e., either it is an ∞-game or when it is finite, the last player's move made it impossible for the other player to move further.

A game is won by P when it is a finished P-game. Thus it is a finite game and O cannot move anymore because the game cannot be extended. This happens when and only when the last move of P is an axiom. A game won by P is also called a winning P-game. Here is an example of winning P-game in the Gentzen system for intuitionistic logic:

O → A, A ⊃ B B → P → ⊃ L → O → A, B B → P → Ax → O
A game is won by O when it is finished and not won by P, i.e., either it is an ∞-game or it is an O-game where P cannot move further, i.e., O played a statement which the conclusion of no instance in inst. A game won by O is also called a winning O-game.

Supposing that X and Y are logical variables, here is a finite winning

O-game: O → X X ∨ Y → P → ∨ R2 → O → X Y → P and an infinite winning O-game: O → X ⊃ Y X → P → ⊃ L → O → X ⊃ Y X → P → • • • cycle
A strategy for P is a procedure that tells P how to move when it is up to him to play, but not necessarily in all circumstances. Thus a strategy can be defined as a partial function from O-games to inst. And a strategy for O is a partial function from P-games to stm.

A game is played according to a strategy ϕ for P if every move of P is determined by the strategy: for every partial game (i.e., prefix of the alternating list of plays) of the game of the form

O → c 0 → P → i 1 → O → p 1 → . . . → p k-1 → P → i k → O we have ϕ(O → c 0 → P → i 1 → O → p 1 → . . . → p k-1 → P) = i k
When a strategy determines the behavior of P, bifurcations might still occur depending on the behavior of O. A strategy for P can be represented by a tree where branches represent the games played according to the strategy (see Figure 1 for an example).

A strategy ϕ is a winning strategy for P on c if ϕ is a strategy for P such that every finished game for c played according to ϕ is won by P. In other words, whatever O does, every game for c in which the behavior of P is determined by ϕ must stop on a move from P which prevents any further move from O.

It is also possible to define winning strategies for O on c as determinations of the behavior of O that either lead to finished O-games (where P cannot move further) or develop ∞-games where P and O play indefinitely.

Proofs vs. Games

The key result that relates proofs and games is the following:

There is a winning strategy for P on c if and only if c has a proof.

The demonstration is done by showing how proofs and strategies correspond to each other. 2 We do not give the details here but illustrate this result with an example. In Figure 1, we consider the sequent (A∨B)⊃(B ∨A) and we display a winning strategy for P on this input. The strategy g is a tree composed of two branches with a bifurcation. It is winning for the sequent (A∨B)⊃(B ∨A) because the two outcomes are winning for P and no other sequence of moves by O could have lead to another outcome.

(A ∨ B) ⊃ (B ∨ A) ⊃ R (∅, A ∨ B, B ∨ A) A ∨ B B ∨ A ∨ L (∅, A, B, B ∨ A) A B ∨ A ∨ R2 ({A}, B, A) A A Ax(∅, A) B B ∨ A ∨ R1 ({B}, B, A) B B Ax(∅, B)
If we compare the strategy with the following Gentzen proof of the same sequent, the correspondece between the proof branches and the branches of the strategy tree is obvious, considering that the proof tree is upside-down compared to the strategy tree:

Ax A A ∨ R2 A B ∨ A Ax B B ∨ R1 B B ∨ A ∨ L A ∨ B B ∨ A ⊃ R (A ∨ B) ⊃ (B ∨ A)

From IL deduction systems to Game rules

Now let us concentrate on the games generated by the Gentzen system for intuitionistic logic. Let us consider the two rules for the intuitionistic implication ⊃:

Γ, A ⊃ B A Γ, B C Γ, A ⊃ B C ⊃ L Γ, A B Γ A ⊃ B ⊃ R
If we focus on rule ⊃ R , it has three parameters: Γ, A and B and the rule generates a set of instances that have two premises when these parameters are substituted with values. Rules represent sets of instances of a particular shape. Now if we interpret the rule ⊃ L in terms of choices of moves for either P or O, it corresponds to the following sequence in the game: For rule ⊃ R , we obtain:

• if P receives the sequent Γ, A ⊃ B C
• if P receives the sequent Γ A ⊃ B and chooses to play the move ⊃ R (Γ, A, B) (aka defend A ⊃ B);
• then O must play Γ, A B (aka grant A and attack B).

At this step we aim at focusing on the development of game rules from proof systems in intuitionistic logic. In this perspective, the next section is devoted to particular games, called dialogue games, introduced by Lorenzen [START_REF] Lorenzen | Logik und Agon[END_REF]. Here we consider such games for intuitionistic logic through a recent formulation by Fermüller et al [START_REF] Fermüller | From intuitionistic logic to Gödel-dummett logic via parallel dialogue games[END_REF]. Let us mention that similar work has been done for intermediate logics, like Gödel-Dummett logics, fuzzy logics and multi-valued logics [START_REF] Fermüller | Parallel dialogue games and hypersequents for intermediate logics[END_REF][START_REF] Fermüller | From intuitionistic logic to Gödel-dummett logic via parallel dialogue games[END_REF][START_REF] Ciabattoni | Uniform rules and dialogue games for fuzzy logics[END_REF][START_REF] Fermüller | Dialogue games for many-valued logics -an overview[END_REF].

Dialogue Games

Logical dialogue games have many forms and versions nowadays. The main formulations are the one in Blass-Abramsky style [START_REF] Abramsky | Semantics of interaction: an introduction to game semantics[END_REF][START_REF] Blass | A Game Semantics for Linear Logic[END_REF] in which logical connectives are game combinators, and the one in Lorenzen style that is based on idealized confrontational dialogues. They all refer in different ways to Lorenzen's idea to identify the logical validity of a formula A with the existence of a winning strategy for a proponent P in a idealized dialogue in which P tries to show A against systematic doubts by an opponent O [START_REF] Lorenzen | Logik und Agon[END_REF]. This idea was first rigorously developed in order to provide an alternative characterization of intuitionistic logic in [START_REF] Felscher | Dialogues, strategies and intuitionistic provability[END_REF]. Here we aim at presenting a version of dialogue games, provided by Fermüller in [START_REF] Fermüller | Parallel dialogue games and hypersequents for intermediate logics[END_REF][START_REF] Fermüller | From intuitionistic logic to Gödel-dummett logic via parallel dialogue games[END_REF], that is well suited for showing the relationship between such games and Gentzen systems and that is equivalent to other versions of dialogue games for intuitionistic logic.

Here an atomic formula (atom) is either a propositional formula or ⊥ (falsum). Compound formulae are built from atoms using the connectives ∧, ∨, ⊃; ¬A abbreviates A ⊃ ⊥. Moreover the signs ?, ? Left ? Right can be stated by players P and O as shown below.

Dialogues games are characterized by two kinds of rules: logical ones and structural ones. The logical dialogue rules define how to attack a compound formula and how to defend against such an attack. They are summarized in the following table:

X: attack from Y defense of X A ∧ B ? Left or ? Right (Y chooses) A or B according the choice of Y A ∨ B ? A or B (X chooses) A ⊃ B A B ¬A A No defense
Note that X and Y can be each one either P or O, according to the state of game. Then both players may launch attacks and defend against attacks during the course of a dialogue.

In this context a dialogue is a sequence of moves which are either attacking or defending statements following the logical rules. Each dialogue refers to a finite multiset of formulae that are initially granted by O and to an initial formula to be defended by P. Moves can be seen as state transitions. In any state of the dialogue the formulae initially granted or stated by O are called granted formulae at this state. The last formula stated by P and that either already has been attacked or must be attacked in O's next move is called active formula. Then in each state of the dialogue we can associate a so-called dialogue sequent Π A where Π denotes the granted formulae and A the active formula.

The structural dialogue rules regulate the succession of moves. A number of different systems of structural rules have been proposed and analyzed in [START_REF] Felscher | Dialogues as a foundation for intuitionistic logic[END_REF][START_REF] Krabbe | Formal systems of dialogue rules[END_REF]. Here these rules are the following:

- Quite a number of different systems of structural rules have been proposed for dialogue games in the literature (see [START_REF] Krabbe | Formal systems of dialogue rules[END_REF] for more details). To complete this presentation we give the winning conditions (for P):

-W: O has attacked a formula that has already been granted, either initially or in an alter move, by O;

-W⊥: O has granted ⊥.

A dialogue tree dt for Π C is a rooted directed tree with nodes labelled with dialogue sequents and edges corresponding to moves, such that each branch of dt is a dialogue with initially granted formula Π and initial formula C. Then the nodes of such trees correspond to states of a dialogue. We have two kinds of nodes, namely P-nodes and O-nodes, depending if it is P's or O's turn to move at the corresponding state.

A finite dialogue tree is a winning strategy (for the player P) if the following conditions hold:

1. Every P-node has at most one successor O-node.

2. All leaf nodes are P-nodes in which the winning conditions for P are fullfiled.

3. Every O-node has a successor node for each move by O that is a permissible continuation of the dialogue at this stage.

In this context a dialogue game can be viewed as a state transition system where moves in the dialogue correspond to transitions between O-nodes and P-nodes. A dialogue then is a possible trace in the system and a winning strategy can be obtained by a systematic "unraveling" of all possible traces. More details are given in [START_REF] Fermüller | From intuitionistic logic to Gödel-dummett logic via parallel dialogue games[END_REF]. displays a winning strategy for P which ends on the winning condition that O attacks a formula he has already granted (attack 3 and attack 3 ).

Let us illustrate in

attack 0 [⊃] grants A ∨ B A ∨ B (A ∨ B) ⊃ (B ∨ A) defense 0 [⊃] states B ∨ A A ∨ B B ∨ A attack 1 [∨] A ∨ B B ∨ A attack 2 uses A ∨ B A ∨ B B ∨ A defense 2 grants A A ∨ B, A B ∨ A defense 1 states A A ∨ B, A A attack 3 [A] A ∨ B, A A defense 2 grants B A ∨ B, B B ∨ A defense 1 states B A ∨ B, B B attack 3 [B] A ∨ B, B B
Having defined such dialogue games for intuitionistic logic, a key step consists in proving their adequateness, namely their soundness and completeness. Such a proof is given by showing that winning strategies can be transformed into proofs in a sequent calculus for intuitionistic logic, and vice-versa. All details about these dialogue games and its adequateness proof can be found in [START_REF] Fermüller | Parallel dialogue games and hypersequents for intermediate logics[END_REF][START_REF] Fermüller | From intuitionistic logic to Gödel-dummett logic via parallel dialogue games[END_REF]. In the next section we aim at studying the real interest of dialogue games for proof search. We have illustrated, through the above dialogue games for intuitionistic logic, the connections between sequent proofs and winning strategies. Many works have been devoted to proof search in intuitionistic logic following different formalisms like standard calculus [START_REF] Dyckhoff | Contraction-free sequent calculi for intuitionistic logic[END_REF] or sequent calculus with labels [START_REF] Balat | Labelled Deduction, volume 17 of Applied Logic Series, chapter Labelled Proof Systems for Intuitionistic Provability[END_REF] or constraints [START_REF] Voronkov | Proof-search in intuitionistic logic based on constraint satisfaction[END_REF] with a focus on the capture of semantics or algorithmic properties, like termination or non-duplication of formulae [START_REF] Galmiche | Structural Sharing and Efficient Proofsearch in Propositional Intuitionistic Logic[END_REF][START_REF] Larchey-Wendling | STRIP: Structural sharing for efficient proof-search[END_REF]. In front of such works and results the real interest and pos-itive impact of dialogue games for proof search in intuitionistic logic cannot be claimed and merit more studies.

Dialogue Games and Proof search

Dialogue games seem to be another way to mimic what happens in some sequent calculi but it is not clear that this formalism is an appropriate formalism in the perspective of improvements in proof search procedures.

It is the case in intuitionistic logic but what about other logics?

A parallel version of dialogue games for intuitionistic logic has been shown to be adequate for a number of intermediate logics [START_REF] Fermüller | Parallel dialogue games and hypersequents for intermediate logics[END_REF]. In this case the soundness and completeness proofs are based on the relations between so-called hypersequent proofs and winning strategies for parallel dialogue games. Hypersequent calculi have been proposed as a flexible type of proof system for many logics. However, the relation between hypersequent proofs and the semantics of the logics is much less clear than in the case of classical and intuitionistic sequents. The hypersequent calculi formulated for intermediate logics like Gödel-Dummett logics (LC) do not directly relate to a semantic foundation of these logics.

In this context, hypersequents have a strong relation to dialogue games that constitute an alternative to standard semantics. Then the proposal of parallel dialogue games appears as semantic foundations for proof search. It allows to understand the claim that LC is related to parallel programs but mainly to study relations between different intermediate logics through game rules. It could be seen also a tool for studying models of parallel proof search but also as a formalism for modelling proof search and to directly represent important proof search strategies.

It appears that logical rules and strategies can be mixed in game rules. It could limit some choices in the proof search process, simplify this one but with an underlying problem that is: what about the adequateness with logical rules in sequent formalisms?

In order to illustrate this point of mixing rules and strategies into game rules we come back to intuitionistic logic and consider a related work on dialogue games which has been developed during these last years by Rahman and his school for a lot of systems of formal logic [START_REF] Rahman | Über Dialoge, Protologische Kategorien und andere Seltenheiten[END_REF][START_REF] Rahman | How to be a Dialogician -A Short Overview on Recent Developments on Dialogues and Games[END_REF]. 3Here we stress on four specific rules in this intuitionistic dialogue: (a) Atoms: every player can assert atomic formulae, but P cannot assume the atomic formula q if q has not before been conceded by O.

(b) Elimination of negation: if one player X asserts ¬ϕ, the attack of the other player Y must be ϕ.

(c) Intuitionistic Round Closure Rule: whenever player X is to play, he can attack any move of Y in so far as the other rules let him do so, or defend against the last attack of Y (the attack in the game with the highest rank), provided he has not already defended against it. A player may postpone a defense as long as there are attacks he can put forth.

(d) Intuitionistic No-Delaying-Tactics Rule: if O has introduced an atomic formula which can be now used by P, then P may perform a repetition of an attack. No other type of repetition is allowed [START_REF] Keiff | Dialogical logic[END_REF].

The rule (a) is in relation to the intuitionistic sequent calculus where the right part of the sequent must be a single formula and not a disjunction of formulae. That is why if atomic formulae cannot be attacked, they are used as attacks by O. For example if the previous P's formula is the sequent p q, then O attacks by playing via the atom p and the attack is p.

Two comments on the rule (b): suppose that ϕ = p (that ϕ is atomic) and that O asserts ¬p, then P cannot attack ¬p if O has not conceded p before. Moreover this rule on negation corresponds to the intuitionistically admissible rule Γ ¬A Γ, A

The structural rule (c) must be put in contrast with the Classical Round Closure Rule: whenever player X is to play, he can attack any move of Y in so far as the other rules let him do so, or defend against any attack of Y (even the ones against which he has already defended). In other terms, players can play again earlier defenses (which makes sense when another move is available). Of course this rule is not compatible with the "intuitionistic closure round rule" [START_REF] Keiff | Dialogical logic[END_REF].

The sequent calculus can both express and justify the previous dialogical rules. The rules (c) and (d) are based on the specific feature of intuitionistic logic which contains non-invertible rules. Let us recall that an inference rule is called "invertible", if the validity of the conclusion of the rule implies the validity of all the premises of the rule. The difference between invertible rules and non-invertible rules is crucial for proof search [START_REF] Larchey-Wendling | réfutations et contre-modèles dans des logiques intuitionnistes[END_REF] and influences the intuitionistic search of proof. To show it, we are going to give two examples.

Intuitionistic dialogue game for the

A

The previous dialogue game proves that the LEM is not intuitionistically valid. It can be understood as a picture of the following failed search for a proof in LJ sequent calculus for intuitionistic logic, read from the bottom to the top:

A ¬ r ¬A ∨ r r A ∨ ¬A
But the proof search in LJ could also give the following failed proof attempt:

¬A ¬ l A ∨ l r A ∨ ¬A
The replacement the Intuitionistic Closure Rule Round by the Classical one would allow the revision of the defense of P and then the dialogue game would prove the LEM:

O O O P P A ∨ ¬A attack 0 [∨] defense 0 [∨] states ¬A ¬A, A ∨ ¬A attack 1 [¬] grants A A A ∨ ¬A revision of defense 0 [∨] states A A A, A ∨ ¬A

Notice that

A ∨ ¬A is proved in three lines only in the LK sequent calculus for classical logic:

Ax A A ¬ r A, ¬A ∨ r A ∨ ¬A
The key point to explain the difference between the LK proof of the validity of the LEM in classical logic and the disproof of its validity in intuitionistic logic lies in the fact that the LK rule

Γ A, B, ∆ Γ A ∨ B, ∆ ∨ r is invertible, while the LJ rules Γ A Γ A ∨ B ∨ l r and Γ B Γ A ∨ B ∨ r r
are not invertible; and that crucial difference between LK (for classical logic) and LJ (for intuitionistic logic) explains that the derivation of the LEM as well as the elimination of the double negation are possible in LK, but not in LJ. That point is translated in dialogue games à la Rahman, by the difference of two structural rules. We are going to conclude this section by an example slightly more difficult, but more interesting.

The dialogue game of Figure 3 proves that the double negation of the LEM is intuitionistically valid. It is the mirror image of the following derivation in LJ, read from the top to the bottom:

Ax A A ∨ l r A A ∨ ¬A ¬ l ¬(A ∨ ¬A), A ¬ r ¬(A ∨ ¬A) ¬A ∨ r r ¬(A ∨ ¬A) A ∨ ¬A ¬ l ¬(A ∨ ¬A), ¬(A ∨ ¬A) contraction l ¬(A ∨ ¬A) ¬ r ¬¬(A ∨ ¬A)
The interest of the previous proof is to shed light on the last structural rule of the dialogue game, which allows the repetition of attack if an atomic formula has been conceded by O. When that proof is read from the bottom to the top, one sees that the repetition of the attack can be made at the penultimate step, just before the Axiom which replies on the attack on the disjunction of the consequent (and which of course does not appear in the sequent calculus style). Notice that the Weakening (resp. the Contraction) rule of the sequent calculus is the rule thanks to which the first attack of P is possible. Contraction and Weakening are the structural rules allowing the duplication or the omission of the hypothesis in the search proof. The fallacious impression that the last structural rule of the intuitionistic dialogue game is maybe ad hoc, 5 disappears when one understands that this structural dialogical rule is closely related with Weakening and Contraction which concern the "management of resources" inside the search of proofs in sequent calculus [START_REF] Larchey-Wendling | réfutations et contre-modèles dans des logiques intuitionnistes[END_REF][START_REF] Fontaine | Logique Dialogique -Une Introduction[END_REF].

attack 0 [¬] grants ¬(A ∨ ¬A) ¬(A ∨ ¬A), ¬(A ∨ ¬A) attack 1 [¬] states A ∨ ¬A ¬(A ∨ ¬A) A ∨ ¬A attack 2 [∨] defense 2 [∨] states ¬A ¬(A ∨ ¬A) ¬A attack 3 [¬] grants A A, ¬(A ∨ ¬A) attack 1 [¬] states A ∨ ¬A A A ∨ ¬A attack 2 [∨] defense 2 [∨] states A A A

Concluding Remarks

The relation between dialogue games and sequent calculus shows how some strategies of proof are already contained in logical rules and structural rules. It shows also that if dialogue games may appear easier to learn and to use, that method of logic is not deeply different from other methods like tableaux methods or sequent calculi. The game semantics in deduction systems does not escape to the logico-mathematical necessity. The trip in the dialogical games is like a linguistic journey to a country where similar laws exist as elsewhere, but expressed differently.

From this perspective the term "dialogical logic" can be seen as an ambigous or misleading expression. 6 The impressive work of Rahman and his school shows that in fact the dialogue games are like a general method of logic allowing to translate a number of different systems of logic. But one must draw a distinction between the ways of expressing rules and calculi, and the logical systems themselves. Strictly speaking there is no "dialogical logic", but there are different dialogue games according different logical systems in different logics. In some cases, dialogue games is a formalism to study relations between some logics and can appear as a semantic framework to study logics.

Another false impression, most seriously flawed, could have its cause in the ease with which it is possible in dialogue games, of passing from intuitionistic tests of validity to classical proofs [START_REF] Fontaine | Logique Dialogique -Une Introduction[END_REF]. This elegant feature of the dialogical method might be a trap for a philosopher who could imagine that one gets, via the dialogue games, a unified logical theory apt to prove both the theorems of intuitionistic logic and the theorems of classical logic:

The semantics stays the same, only the rules change. The relationship between logical systems become more transparent (see [START_REF] Heinzmann | La logique dialogique[END_REF] p. 260).

Unfortunately, too strong an enthusiasm for dialogue games can lead to abandoning of what semantics really is from a logical point of view. The semantics changes with the change of structural rules, and the relations between logical systems become more transparent only if one keeps in mind what the reasons of the rules are and which rules can be changed in order to change of system of deduction. For example, dialogue games do not change the fact that the semantics of intuitionistic logic and the semantics of the classical logic are different, both in the philosophical sense and in the algebraic sense of the word: if one deals with the latter sense of "semantics", in classical logic we adopt an algebra of truth functions over the set of two truth values, and that is not true for the intuitionistic logic. 7 last, from the "philosophical" sense of semantics, one cannot forget that the classical logic gives up the constructivist meaning that the intuitionistic school assigns to the logical connectives. Thus, the slogan of Quine remains relevant: "change of logic, change of subject" [START_REF] Quine | Philosophy of Logic[END_REF], chap. 6.

To conclude this paper, we can wonder the pedagogical analogy that Rahman uses sometimes between logic and the chess play. This analogy seems in agreement with a radical anti-realism and with a "pragmatism" as philosophy of logic: it seems possible to change indefinitely the structural rules of logic, and to indefinitely combine these rules in order to play with systems of deduction. The method of logical games gave birth to the motto on the character "pragmatic" and "dynamic" of logic, which is akin to a post-Wittgensteinian philosophy of logic and to a supplementary critic against Platonism. This article has not even touched the profound and difficult debate on the nature of logic. But if the translation of logical proofs into games is an interesting method or tool, it leaves that philosophical question still open.

Figure 1 :

 1 Figure 1: A winning strategy for P on the sequent (A ∨ B) ⊃ (B ∨ A).

  and chooses to play the move ⊃ L (Γ, A, B, C) (aka attack A ⊃ B in game terminology); • then O can either play Γ, A ⊃ B A (aka attack A) or play Γ, B C (aka grant B and attack C).

Figure 2

 2 the dialogue games defined by Fermüller on the example of the intuitionistic formula (A ∨ B) ⊃ (B ∨ A). The figure B) ⊃ (B ∨ A)

Figure 2 :

 2 Figure 2: A winning strategy for P in Fermüller's dialogue games.

  Law of Excluded Middle (LEM)

Figure 3 :

 3 Figure 3: Dialogue games as proof of ¬¬(A ∨ ¬A).

  Start: O starts by attacking P's initial formula; -Alternate: moves strictly alternate between players O and P; each move of O reacts directly to the immediately preceding move by P. It means that if P attacks a granted formula the O's next move either defends this formula or attacks the formula used by P to launch this attack. If P's last move was a defending one then O has to attack immediately the formula stated by P in that defense move.

	-Atom: atomic formulas (including ⊥) can neither by attacked or de-
	fended by P;
	-E-rule:

Note that in this case, the term conclusion is used both as a qualifier for formulae and for sequents/statements. It is up to the reader to distinguish those two notions depending on the context.

Dually, it is possible to show that there is a winning strategy for O on c if and only if c has a refutation, see[START_REF] Larchey-Wendling | réfutations et contre-modèles dans des logiques intuitionnistes[END_REF].

Thanks a lot to Shahid Rahman whose correspondence was a great encouragement for this inquiry.

Compare with[START_REF] Fermüller | Parallel dialogue games and hypersequents for intermediate logics[END_REF], section 4. The tableau should be read like that: at the top of the player X there is the formula that he receives; his action on the formula is explained in the box and can be seen on the right of the arrow below. At the top of Y there is that attack or defense, received by Y and to which he replies, and so on.

Because it make possible the proof of the intuitionistic validity of every formula like ¬¬(A ∨ ¬B), i.e., every formula belonging to the famous Gödel-Gentzen translation phenomena.

See the title of the papers[START_REF] Heinzmann | La logique dialogique[END_REF][START_REF] Keiff | Dialogical logic[END_REF] and of the book[START_REF] Fontaine | Logique Dialogique -Une Introduction[END_REF].


Joseph Vidal-Rosset
email: joseph.vidal-rosset@laposte.net

DOES GÖDEL'S INCOMPLETENESS THEOREM PROVE THAT TRUTH TRANSCENDS PROOF? *

Introduction

Since their appearance in 1931, Gödel's incompleteness theorems have been the subject of intense philosophical examination. Though the demonstrations of the famous theorems are rather complex, but nevertheless clear, their philosophical implications are far from transparent. Contemporary philosophical logicians disagree on the philosophical significance of the incompleteness theorems, as did Carnap and Gödel themselves, and I believe that the state of the discussion has not changed a lot since the original Carnap-Gödel debate. It is hard to overestimate the difficulty of assessing the debate on this topic, knowing that Gödel himself refused to publish his paper "Is Mathematics Syntax of Language", 1 after six versions of this paper. Though believing Carnap's view of his theorems in The Logical Syntax of Language mistaken, 2 he was not satisfied by his own argument that his theorems supported mathematical realism rather than the formalism favored by Carnap. 3 Gödel's incompleteness theorem shows the existence of a statement (called "Gödel sentence", or "G sentence") true but undecidable in Peano arithmetic. Thus, at least in formal systems, "somehow truth transcends proof". But transcendance of truth is difficult to pin down philosophically. In Gödel's opinion, the incompleteness theorem gives a picture of independent, unlimited, and al-ways new mathematical facts which are irreducible to conventions based on axioms; at the opposite, Carnap denies that mathematics are independent from language, the incompleteness being only the expression of formal hierarchy of mathematical systems. 4 Obviously the philosophical question of the meaning of the truth in mathematics is behind the question of the reading of the incompleteness theorem, and the broader opposition between realism and antirealism is standing further. According to Tennant (in The Taming of the True), the debate about realism concerns the tenability of a realist view of language, thought and the world. He begins his book by citing Russell: On what my be called the realist view of truth, there are 'facts', and there are sentences related to these facts in ways which makes the sentences true or false, quite independently of any way of deciding the alternative. The difficulty is to define the relation which constitutes truth if this view is adopted. 5 This realist view of the truth expressed by Russell is the first basic assertion of any realism (from Plato's to Quine's) and Gödel's incompleteness theorems seem to give strong reasons to believe that this philosophical standpoint is the right one. In this discussion about the significance of Gödel's proof, the realist holds that the burden of the proof is on the anti-realist who must show that any truth-predicate independent of proof is involved in the incompleteness theorems. semantic anti-realism claims that "any thing worthy of the name true in mathematics or natural science is in principle knowable" and consequently denies that, absolutely, truth transcends proof. That is why Tennant aims to show in his paper that a deflationist reading of Gödel's theorems is licit and that the "non conservativeness argument" is not logically apt to throw it overboard. If philosophical interpretations of Gödel's incompleteness theorems have not changed from the Carnap-Gödel debate, logicians have recently shed more light on the problem: the point is to know if the "non-conservativeness argument" can be removed.

It is well known that Hilbert's program of giving finitist proofs of the consistency of mathematics collapsed when Gödel proved the impossibility of such a project in arithmetic. But my goal in this paper is not to develop this historical point but to clarify the contemporary terms of this debate on Gödel's proof and to try to explain why, from a logical and philosophical point of view, there is no scientific refutation of the deflationary theories of truth via Gödel's proof.

In the first part of this paper I show briefly the logical argument involved in Gödel's incompleteness theorems. I will explain in a second step the relations between the deflationist account of the truth and the conservativeness in the one hand, and the "non-conservativeness argument" about Gödel's theorems on the other hand. I will try to show that the question about deflationism and the Gödel phenomena is polemical from a philosophical point of view but not really from a logical point of view. I will compare in conclusion contemporary realist and anti-realist interpretations of Gödel 's incompleteness theo-rems, and wondering about their respective stability I will plead on the latter. More precisely, I point out to contemporary realist that if he is free to reject a deflationary-anti-realist account of Gödel's proof, he is in trouble to avoid the genuine Platonist philosophy of Mathematics and not to betray a sort of discrepancy between his realist ontology and his empiricist epistemology.

2.

The logic of Gödel's incompleteness theorem

Quine's informal explanation

Maybe the easiest and the more elegant way of exposing Gödel's incompleteness theorem is Quine's. But Quine's way of explaining Gödel's result is not only interesting for its pedagogical virtue, but also for Quine's philosophical conclusions.The reminder of the famous Epimenides paradox of the "I'm lying" in its Quinean version is necessary to understand Quine's account of Gödel's proof: "Yields a falsehood when appended to its own quotation" yields a falsehood when appended to its own quotation. In Quine's opinion, Gödel's proof is akin to Epimenides paradox, at least on first sight:

Gödel's proof may conveniently be related to the Epimenides paradox or the pseudomenon in the 'yields a falsehood' version. For 'falsehood' read 'nontheorem' thus:' "Yields a non-theorem when appended to its own quotation" yields an non-theorem when appended to its own quotation.'

This statement no longer presents any antinomy, because it no longer says of itself that it is false. What it does say of itself is that it is not a theorem (of some deductive theory that I have not yet specified). If it is true, here is one truth that that deductive theory, whatever it is, fails to include as a theorem. If the statement is false, it is a theorem, in which event that deductive theory has a false theorem and so is discredited.

[. . . ] [ Gödel] shows how the sort of the talk that occurs in the above statement -talk of non-theoremhood and of appending things to quotation -can be mirrored systematically in arithmetical talk of integers. In this way, with much ingenuity, he gets a sentence purely in the arithmetical vocabulary of number theory that inherits that crucial property of being true if and only if it is not a theorem of number theory. And Gödel's trick works for any deductive system we may choose as defining 'theorem of number theory'. 6 The analogy between Epimenides paradox and the Gödel's sentence G can be confusing. The self-referentiality of the Liar's sentence cannot give the exact structure of Gödel's theorem which, contrarily to the Liar paradox, avoids carefully every flaw in the logical reasoning. Let us sketch more formally how the proof works in "arithmetic talk of integers"

Formal sketch of Gödel's proof

Gödel's proof shows an uncontroversial logico-mathematical truth. It is based on the coding of the syntax of formal system of arithmetic S and on the representability theorem asserting that it is always possible to represent in the arithmetical object language every metamathematical expressions denoted by an arithmetic formula in S. Thanks to the coding, every arithmetical formula ϕ can be associated with its Gödelian expression ϕ. One calls "recursive" such a reasonable base theory where every formula can be expressed by its Gödel's number. Thus every logical relation between metamathematical sentences is, thanks to the coding, perfectly "internalized" by the corresponding arithmetical expressions. In the proof, S is assumed recursively axiomatizable, which implies that the provability predicate of S can be defined so that (1) and (2) below hold. So, if S is a system expressed in first order language and its intended interpretation is over the set of natural number, then we can define the provability predicate for S via the coding:

If n is a proof in S of m, then S P roof S (n, m) (1) If n is not a proof in S of m, then S ¬P roof S (n, m) (2)
where n and m are the respective names of n and m, the Gödel numbers identifying proofs and sentences. Now, thanks to the representability theorem ("every (total) recursive function is representable"), it is possible to define via the coding, in the set of primitive recursive functions of S, the scheme of a crucial formula: S G ⇔ ¬∃y P roof S (y, G)

which represents an arithmetical sentence G which says of itself, in the metamathematical language, that it is not provable in S. To get Gödel's proof one needs to understand that G and ¬∃y P roof S (y, G) are in S inter-deductible via the coding and that this inter-deductibility is proved on the base of the representability theorem. G is a fixed point for the negation of the S-provability predicate. (The fix point theorem says that for any given formula ϕ(x), with one free variable, there is a sentence α such that the biconditional α ↔ ϕ(α) is provable in S, where α is α's Gödel number.) So ( 3) is constructed with thinking of G as a sentence x that, referring to itself via its Gödel number, is saying of itself that it has the property ϕ which is expressed by the formula ¬∃y P roof S (y, x). Now the question is "is G a S-theorem?" the reply is "no" and Gödel's proof of first incompleteness theorem runs as follows:

Consistency and ω-consistency. If we can prove in a system S both ∃xF x and ∀x¬F x, then S is inconsistent. S is said to be ω-inconsistent if both ∃x¬ψx and ψ0, ψ1, ..., ψn, ... are provable in S. A system can be ωinconsistent without being inconsistent. A ω-consistent system is a system which is not ω-inconsistent. Gödel's original proof is " if Peano arithmetic is ω-consistent, then it is incomplete".

If S is consistent, there is no S-proof of G. Suppose that any m codes a proof of G in S, then by (3) one gets:

S G ⇔ ¬P roof S (m, G) (4)
But the surprise lies in the fact that m coding a proof of G codes ¬P roof S (m, G) but that contradicts (1) from which one can infer P roof S (m, G) and violates the consistency of S.

If S is ω-consistent, there is no S-refutation of G. If G is S-refutable, then ¬G is S-provable, and then, by the defining property of G (saying of itself not being provable), ∃y P roof S (y, G) is provable, so at least one m coding a refutation of G in S exists: P roof S (m, G). But we have just proved that G is not S-provable, if S is consistent. That means for every y , ¬P roof S (y, G), consequently ¬P roof S (0, G) is true, ¬P roof S (1, G) is true, ..., ¬P roof S (k, G) is true, etc. But there if ¬G is S-provable, then ∃y P roof S (y, G) is provable, and consequently S is ω-inconsistent.

Conclusion.

Gödel's original first theorem of incompleteness shows that if S is a formal system of arithmetic, there is an

S-undecidable statement G in S, if S is ω-consistent. 7
The second theorem of incompleteness proves that if the assertion of the existence of of a S-proof of the S-consistency is substituted for G, one gets, provided that S is consistent:

S Con(S) (5)
It means that no consistent formal system of arithmetic can prove its own consistency, and the proof can be sketched as follows. The following formula says that it there is no S-proof of the S inconsistency:

¬∃y P roof S (y, ¬Cons(S))

If one takes now the following formula as an instance of:

¬∃yP roof S (y, ¬(0 = 0)) (7)
It is intuitively clear that (7) expresses via the coding the consistency of S: no consistent system of arithmetic can prove that (0 = 0) and to say via the coding, that there is no proof of "(0 = 0)" is S is also to assert the consistency of S.

That there is no proof of ( 7) is proved like the first incompleteness theorem. So every formal system of arithmetic cannot derive the assertion of its own consistency, provided that it is consistent:

Con(S) → ¬∃y P roof S (y, ¬Con(S)) (8)
If S Con(S) then there are there are models of S where Con(S) is satisfied, as the set of natural numbers, and there are models of S where ¬ Con(S) is also satisfied (non standard models).That explains why the Gödel sentence must be true but unprovable. The formal system S being defined with an intended interpretation over the universe of natural numbers, the Gödel sentence has to be satisfied but not proved in the intended models of arithmetic, provided the consistency of S, and that explains why one asserts that Gödel's incompleteness theorem has demonstrated that there are arithmetical sentences, not being logical consequences of a reasonable base theory of numbers, are true but not analytic.

Why do G and the consistency of S have to be asserted? The most important point of that demonstration is that G as well as the consistency of S cannot be asserted in the formal system S but from a stronger system of which S is a proper subset, say S*. Maybe the more intuitive manner to present this fact is to deal with the condition of ω-consistency used by Gödel's original proof.

At this stage, it is helpful to base the argument on the second incompleteness theorem, and we remind that it can be done thanks to a formula like (7). That does not exist a numeral coding the proof of an inconsistency in the arithmetic seems obvious. Following the natural progression of integers, the instantiations in (7) prove:

(0 = 0), (1 = 1), (2 = 2), . . .

and (by soundness):

(0 = 0) : true, (1 = 1) : true, (2 = 2) : true, . . . (10) At one level above S, say S*, one is justified to tell that ∀y ¬P roof S (y, 0 = 0) is true, but it is impossible to infer it from S and it is precisely what Gödel's theorem proves. The explanation is that each standard integer satisfies in S the sentence ¬∃y P roof S (y, ¬(0 = 0)) but it does not entail that such a sentence is a theorem of S for all integers. The sentence ¬∃y P roof S (y, ¬(0 = 0)) asserts its own unprovability and we know from the first incompleteness theorem that if S is ω-consistent, G is undecidable. Suppose that we could get an ω-proof of G showing recursively that ¬∃y P roof S (y, ω = ω) , it would also disprove the assertion of its unprovability, so S would be ω-inconsistent and we could prove ¬G. Last, if ¬G could be proved, S would be ω-inconsistent because it would involve to accept, at the ω-level, the existence of a Gödel number which codes the proof of a contradiction. But this possibility of ωinconsistency of S is not to be confused with inconsistency: a formal system can be ω-inconsistent without being inconsistent. That explains why the condition of ω-consistency can only be done above S, from S*, where, given the axiom scheme of mathematical induction and a primitive truth predicate, we can rightly infer that, if S is consistent, then G is true.

At the end of this section, we are now able to understand what is at stake in the Gödel phenomena: to wonder if it is possible to grasp the meaning of the incompleteness without a notion of truth transcending the base theory S. Shapiro and Ketland have replied "no" to that question and have found in the incompleteness a logical argument against a contemporary theory of truth called "deflationism". Field and Tennant have differently replied to that antideflationist argument, on behalf of deflationism. I am going to analyze now how these logical arguments are philosophically motivated.

Realism against deflationary theories: the argument of non-conservativeness

Quine's account of Gödel's incompleteness theorem is useful for understanding its main logical point and its logical consequences; but the question of the certainty of Quine's philosophical conclusions about Gödel's proof remains open:

Gödel's discovery is not an antinomy but a veridical paradox. That there can be no sound and complete deductive systematization of elementary number theory, much less of pure mathematics generally, is true. It is decidedly paradoxical, in the sense that it upsets crucial preconceptions. We used to think that mathematical truth consisted in provability.

That mathematical truth does not consist in provability is to be understood in Quine's analysis of Gödel's incompleteness theorem. Gödel's negative theorems prove that no mathematical axiomatic system can include every mathematical truth. Consequently, in realist Quine's opinion, because truth is a relation of sentence to facts, undecided mathematical sentences do express our lack of knowledge of mathematical facts existing independently of proof systems. For example, Wiles has proved that Fermat was right in his conjecture because Fermat supposed a property of integers which is independent of knowledge: "if n ≥ 3 there is no positive integer x, y, z such as x n + y n = z n ."

Gödel's incompleteness theorem proves, from the non conservativeness argument that there are truth sentences in every mathematical theory which cannot be known as true without a notion of truth which is transcendent with respect to the base theory. Such an argument is obviously seducing for realist philosophers and it is presented as a logical refutation of deflationary theories of truth. It is now necessary to show clearly the relation between disquotation, deflationism, and conservativeness.

Disquotation is, after Tarski's work, commonly used to define truth. The disquotation scheme is:

The sentence "p" is true if and only if p.

The canonical example given by Tarski is well known: "snow is white" is true if and only if snow is white. Truth is disquotation.

Deflationism is a philosophical interpretation of truth which is often based on the disquotation scheme: truth predicate is nothing else than a logical device for "disquoting" expressions and for expressing in finite sentences a infinite list of true sentences ("God knows every truth"). Both Ketland and Tennant recognize that it is not easy to give an unambiguous definition of deflationism: Ketland says that "deflationism about truth is a pot-pourri" and Tennant describes it as "a broad church". 8 They themselves illustrate the ambiguity of deflationism: reading their respective papers, it is possible to give at least two versions of deflationism, both being expressed on the base of the disquotational theory of Truth. The first one can be called the "strong deflationism". Ketland describes it perfectly: the concept of truth [. . . ] is redundant and "dispensable": [. . . ] we need to "deflate" the correspondence notion that truth expresses a substantial or theoretically significant language-world relation. 9

In my opinion, Tennant adopts a weaker version of deflationism, or more precisely, a version of deflationism akin to his semantic anti-realism. The following quotation makes that point quite clear:

Deflationism has its roots in Ramsey's contention that to assert that φ is true is to do no more than assert φ, unadorned. Truth is not a substantial property whose metaphysical essence could be laid bare. It has no essence; it is as variegated as the grammatical declaratives that would be its bearers. There would therefore appear to be no gap, on the deflationist's view, between claims that are true and assertions that are warranted; or, generally, between truth on the one hand, and, on the other hand, grounds for assertion, or proof. 10 We can notice that in Tennant's version of deflationism truth is not, strictly speaking, dispensable, and that it is not the language-world relation that we need to "deflate", but the idea of substantial existence of truth, as if truth could be more than the label that we put on all sentences that we can check. If truth is always knowable (i.e. checkable) in principle, then to disquote "p" must mean that '"p" is a justified belief and that the truth of "p" is the verified relation between the sentence "p" and the fact x denoted by p.'

To wonder if truth is substantial or non substantial seems maybe obscure and needs to be clarify. The semantic anti-realism advocated by Tennant does not claim that truth is neither substantial nor objective, but that truth does not lie as a substantial property in absolute unprovable sentences: the only licit notion of truth is always epistemologically constrained. 11 Relations between truth and proof and the role of Bivalence are on this point crucial to get the difference between the realist and the semantic anti-realist. Suppose truth as independent from proof, then truth can be imagined as a substantial property of some sentences which are true even though nobody is apt to verify them. Bivalence universally assumed, by definition every declarative sentence is determinately true of false, independently of our means of coming to know whether it is true, or false, and then it would be odd to claim that truth is not a substantial property of sentences. For example, thanks to Bivalence, the Megarians philosophers had constructed a system of Logical Fatalism: if every affirmation or negation about a future is true or false it is necessary or it will be impossible for the corresponding state of affairs to have to exist: the sentence "Jacques Chirac will resign in September, 1st, 2005" has already in itself a truth value before the mentioned date. My point is not to develop the philosophical subtleties which have been made to solve such a puzzle, 12 but to make clear that deflationism à la Tennant tries to dissolve the truth property in verification process: the universality of Bivalence must be rejected.

It is now possible to understand why Tennant tries to find in his paper a strategy to save a deflationary reading of Gödel's theorem. From the semantic anti-realism point of view every mathematical truth must be in principle provable. But a widespread view about Gödel's incompleteness theorem leads to assume, as Quine does, that mathematical truth is not provability, because Gödel has succeeded to show in the syntax of number theory a sentence G which, under the hypothesis of the consistency of the number theory, must be true and unprovable in the number theory. Of course such a demonstration does not affect the general equivalence between mathematical truth and provability in principle, because a proof of G can be done in a meta-theory including the number theory. In other words, Gödel's incompleteness does not affect the tenet of the semantic anti-realism. But an argument about the conservativeness of deflationary theories of truth seems to show that they collapse because of Gödel's result. My point is to show that deflationism in Ketland's meaning effectively collapses, but it is not the case if deflationism is intended in Tennant's meaning.

Ketland has given some important technical results about the conservativeness theories of truth. 13 The main point can be understood without logical formula, and, in order to avoid technical developments, I refer only to the Disquotational Theory (DT) described by Ketland and to the result he has proved: DT added to any (non-semantical) theory S is conservative over S. Intuitively it means only that the truth predicate of DT adds nothing new to true sentences of S, or that any model of S may be expanded to a model of S ∪ DT , or that (S ϕ) ⇔ (S ∪ DT ϕ). Thus DT holds a metaphysically "thin" notion of truth, to repeat Shapiro's word. 14 The goal of Ketland's demonstration is to show that because of the property of conservativeness, the union of any deflationary theory of truth to the Arithmetic of Peano (PA) is unable to show that G is true. On the contrary, it is the union of PA with a Satisfaction theory of truth which is able to prove that G is true: P A(S) G. That theory S is Tarski's inductive definition of truth expressed by this list of four axioms: 1 (T At )(t = u) is true if and only if the value of t = the value of u.

2 (T ¬ )¬ϕ is true if and only if ϕ is not true.

3 (T ∧ )(ϕ ∧ ψ) is true if and only if ϕ is true and ψ is true.

4 (T ∀ )(∀ϕ) is true if and only if, for each n, ϕ(n) is true.
S added to PA, PA(S) is a "truth-theoretic" non-conservative extension of PA. From that union of PA and S, the most important results are that PA(S) proves that anything provable in PA is true, proves also that PA is consistent, and proves that the Gödel sentence G constructed in the syntax of PA is both true and not provable in PA. Thus, the non conservativeness argument about Gödel's proof could be called "The Master Argument of non-conservativeness" against deflationism. I let Ketland sum up the argument:

Stewart Shapiro and I have introduced an innovation in relation to understanding the notion of deflationism about truth. We have proposed that we define "substantial" (for a theory of truth) to mean "non-conservative" (over base theories). We proved that disquotation is conservative, and Tarski's inductive definition is sometimes non-conservative. 15 It means, to speak very generally, that in order to recognize the truth of G sentence constructed via the coding in a theory S, a non conservative theory of truth over S is required. This fact leads, in Shapiro's and Ketland's opinion, to a "thick" or a "substantial" notion of truth. That is why, invoking a full Tarskian theory of truth (i.e. a non conservative theory of truth) Ketland writes:

If I am right, our ability to recognize the truth of Gödel sentences involves a theory of truth (Tarski's) which significantly transcends the deflationary theories. 16 Last but not least, Ketland is convinced that this objection from non-conservativeness is a logico-mathematical refutation of deflationism: because every deflationary theory of truth is conservative (by definition) and because the deflationary philosophy of truth pretends that a theory of truth adds "no content" to a nontruth theoretic base theory, Ketlands concludes that, because it is proved that a non-conservative truth-theoretic extension of PA is necessary to show that all theorems of PA are true, that PA is consistent and that every Gödel sentence in PA is true, then "deflationism is false". 17 Ketland's conclusion is not only interesting from a logico-philosophical point of view; it is also an interesting attitude from what one could call a "metaphilosophical" point of view. Assuming that the non-conservativeness objection is a refutation of deflationism, Ketland presupposes that philosophy can be refuted by science. But even if deflationism is not a philosophical system but only a philosophical opinion about the nature of truth, it is undoubtful that deflationism can be attractive for every anti-Platonist (or anti-realist) philosopher. That is why Ketland uses the non-conservativeness of Tarski's theory of truth as a polemical argument against deflationary view of Field's nominalism for example. Ketland concludes his paper in making an analogy between the indispensability of mathematics for the knowledge of the physical world, and the indispensability of a full Tarskian theory of truth to prove some important sentences.

Believing in nominalism, Field replied to Shapiro that non-conservativeness lies with the notion of natural number and with the notion of mathematical induction, not with the notion of truth: [. . . ] this point about the extension of schemas has nothing to do with truth: we are committed in advance to extending our schemas to all new predicates, not just "true". 18 We will find again later on Field's remark. But we can notice how much uneasy the strict nominalist position becomes with respect to Gödel's theorems. The proper extension of Peano arithmetic involved in the assertion of its consistency as well as the convenient set-theoretic point of view appear as very strong realist arguments. But it is the deflationist theory of truth which is the topic of that discussion. Let see how Tennant has tried to show that deflationism can give a licit reading of Gödel's theorems.

4.

Tennant's deflationist solution

The deflationist use of reflection principles

To justify his philosophical position from a logical point of view, Tennant uses Feferman's reflection principles, proposing a uniform reflection principle compatible with Gödel's proof and anti-realist goals. Feferman's reflection principles are "axiom schemata [. . . ] which express, insofar as is possible without use of the formal notion of truth, that whatever is provable in S is true" 19 The soundness of S for primitive recursive sentences could be expressed by the following reflection principle:

(pa) 20 If ϕ is a primitive recursive sentence and ϕ is provable-in-S, then ϕ.

Tennant's principle of "uniform primitive recursive reflection" is:

(U Rp.r.) Add to S all sentences of the form ∀n (P rovS(ψ(n)) → ∀m ψ(m) where ψ is primitive recursive. 21 Tennant insists on the point that, producing the consistency extension, (U R p.r ) has exactly the logical strength to formalize faithfully the reasoning in Gödel's semantical argument, and that is why, thanks to this reflection principle, Tennant is able to give meta-proofs, in S*, without mention of truth predicate (even in S) that there is neither S-proof nor S-refutation of the G sentence asserting "there is no S-proof of the inconsistency of S". Such meta-proofs explicitly appeal in S* to the consistency of S, to the S-provability of assertable primitive recursive statements, and to the representability of S-proof. It aims at showing that Gödel's proof can be done in "truth-predicate-free" theories.

To Shapiro's demand that the deflationist do justice to the soundness of S, Tennant suggests that he would express the soundness of S by being prepared to assert, in the extending system S*, every instance of the reflection schema:

P rov S (ϕ) → ϕ (11)
So, Tennant, as every logician, recognizes the logical necessity of an extended system to express the soundness of S, but he denies that it is necessary to mention a truth predicate as he denies that Gödel's proof leads to a substantial notion of truth: 22One can agree with Shapiro that the 'deflationist cannot say that all of the theorems of [S] are true'. But the deflationist can instead express (in S*) his willingness, via the soundness principle, to assert any theorem of S. The antideflationist desires to go one step further and embroider upon the same willingness by explicitly using a truth-predicate.

The sentence "all theorems of S are true" is called "the adequacy condition". And it is an important point is that the adequacy condition cannot be asserted in the base theory itself:

Löb's Theorem ensures that this soundness principle (P rovS(ϕ) → ϕ) could not be derived in S without making S inconsistent. But here we are contemplating adopting the soundness principle in the extension S* of S; and this adverts that danger of inconsistency. 23 When Tennant suggests that the deflationist, instead of saying that all Stheorems are true could be prepared to accept, in S*, every theorem of S, he finds again the Wittgensteinian distinction between "to say" and "to show": When the deflationist adopts the soundness principle above, he is allowing that it may have infinitely many instances. 24 I have put aside technical details of Tennant's demonstration in order to stress on the main logical-philosophical issues of the " Gödel phenomena". One could believe that Tennant's work on Gödel's proof consists only in switching the truth-predicate for the proof-predicate, and that such a trick cannot be a refutation of the realist interpretation of Gödel's incompleteness theorems. But such a feeling, in my opinion, betrays a misunderstanding of the philosophical disagreement between Tennant and Ketland and, especially, a misunderstanding of the philosophical meaning of Tennant's defense of deflationism. I will show at the end of this paper that the difference between Ketland and Tennant is not scientific but a strict difference of philosophy.

Ketland's reply: reflection principles are truth-theoretically justified

Ketland has written a reply to Tennant's paper 25 . The first important step of his reply is the definition of what he calls a "conditional epistemic obligation":

Conditional epistemic obligation: If one accepts a mathematical base theory S, then one is committed to accepting a number of further statements in the language of the base theory (and one of these is the Gödel sentence G.) 26 The "further statements" mentioned by Ketland are those which are not provable by the theory S, but which are nevertheless proved as true thanks to a non-conservative extension of S, like the extension produced by the Tarskian theory of satisfaction. Ketland insists on the idea that it is using the notion of truth that we can explain the conditional epistemic obligation. His claim is that the objection of non-conservativeness made against the deflationary theories of truth is in fact a "Reflection Argument": informally we can say that by the use of the notion of truth we can arrive at statements as "all sentences proved in S are true", "G expressed in S is non provable in S and true", "all theorems of S are true", etc. The crucial point of Ketland's argument is that the conditional epistemic obligation can be explained by a non-conservative (or substantial) use of the notion of truth leading the deflationist to the following dilemma:

After a quick and superficial reading of Ketland's and Tennant's paper, it could be surprising to see that, in his reply to Tennant, Ketland uses and mentions Feferman's reflection principles as his own anti-deflationist argument. One can sum up his argument in saying that it is true that G is a theorem of the union of PA with the principle of uniform primitive recursive reflection proposed by Tennant. But he argues against Tennant's deflationist position that the use of Feferman's reflection principles can only being truth-theoretically justified: that is only the use of the notion of truth, or a theory of truth as a Tarskian theory of truth, which can explain and justify the reflection principles. The superiority of the anti-deflationist or the substantialist theory of truth, in Ketland's opinion, is even that it is able to prove the principles of reflection when the deflationist is only able to assume them, without justification, as Tennant seems to do. And then Ketland shows that philosophy is essentially polemical when he writes:

Part of the point of the articles by Feferman, Shapiro and myself was to show how to prove reflection principles, which, "ought to be accepted if one has accepted the basic notions and schematic principles of that theory" (Feferman, 1991, p. 44). On Tennant's proposal, instead of proving the reflection principles in the manner proposed by Fefeferman, Shapiro and myself, the deflationist may simply assume the reflection schemes. As far as I can see, in the absence of the sort of truth-theoretic justification given by Feferman, Shapiro and myself, Tennant's idea is that deflationist may assume these principles without argument. No reason, argument or explanation for adopting the reflection principles is given by Tennant. If we avoid explaining why acceptance of mathematical theory S rationally obliges further acceptance of reflection principles, then this is apparently "philosophically modest". I find this curious. It is rather like saying that if we avoid explaining a phenomenon, we achieve "philosophical modesty". Presumably, the ideal way to achieve such "modesty" in the scientific arena would be to abandon scientific explanation altogether. 28 I aim at showing with modest means -I mean non technically sophisticated from a logico-mathematical point of view -that Ketland is wrong to believe in a scientific difference between his substantialist explanation of Gödel's theorem and Tennant's deflationist reading. In reality, they are twins from a scientific point of view but these twins do not have the same philosophical beliefs, and even if their philosophical beliefs are about science, I am convinced that there is no scientific proof that one is wrong and the other is right. Ketland thinks that a deflationary theory of truth cannot be a good theory of truth because, being logically conservative, it is inadequate to explain why the Gödel phenomena in a theory S requires a non-conservative theory of truth over S (if S is a reasonable base theory). Tennant considers the conservativeness constraint of deflationary theories of truth as a reasonable base for a philosophical understanding of truth and he has consequently to propose a strategy to accommodate the proper extension involved by the truth of the independent sentence G and the conservativeness requirement for deflationism.

The only way I see to understand the philosophical difference between two logicians discussing about the same uncontroversial theorem is to suggest that they do not interpret in the same way the logical hierarchy of object language and metalanguage involved in Gödel's theorem. We have to keep in mind that the topic of their discussion is to wonder if a deflationist reading of Gödel's theorem is licit or not, provided that deflationism is defined by the conservativeness constraint. My position is on behalf of Field and Tennant: deflationism is not at all disproved by the non-conservativeness argument. My position is based on two types of arguments. The first one is logical. I want to stress on the fact that the non-conservativeness argument is based on some hierarchy of formal systems and that involves what Quine called a "semantic ascent" in which we can find truth-predicates among other predicates (to join Field's remark). In my opinion, every reasonable deflationism must respect that semantic ascent and consequently the objection from non-conservativeness is pointless. The second type of argument concerns the philosophical meaning of the deflationary theories of truth (especially the disquotational theory of truth) which Ketland depreciates for philosophical reasons. I will sketch in conclusion my understanding of relations between science and philosophy, trying to show also the specific difficulties of the contemporary mathematical realism inspiring the argument of non-conservativeness.

5.

The non-conservativeness of truth or the semantic ascent I am going to develop in this section a deflationist reply to the non-conservativeness objection. My first point is that it is possible, quoting Field, to "deflate" the argument of non-conservativeness from the Tarskian solution of the Liar paradox: when the Liar say, "I am lying", does his sentence involves a nonconservative theory of true? The anti-deflationist would reply "yes" without hesitation, but the deflationist would be certainly more cautious. We have seen Quine making an analogy between the Liar paradox and Gödel's proof, so, I will just develop that analogy going back to the solution of the former.

It is well known that the solution of the Liar paradox is in the distinction between object language and metalanguage. If the Liar says that he is lying about some other sentence uttered five seconds ago, the paradox vanishes as it does in common language: when one confesses lying one does not mean that the confession itself is false, but the confession is normally understood as a true 1 sentence speaking about false 0 sentences that one asserted as true 0 . Quine comments the Tarskian solution and suggests a finely-shaded opinion about the non-conservativeness of the truth theory involved in the Liar paradox:

For the ith level, for each i, the variables 'xi', 'yi', etc. range over that levels and lower ones; thus 'x0', 'y0', etc. range only over sets. Predicates 'true0',' true1', and so on are then all forthcoming by direct definition. For each i, 'truei' is dependably disquotational in application to sentences containing no bound variables beyond level i. We get a self-contained language with a hierarchy of better and better truth predicates but no best. Truth0 is already good enough for most purposes, including classical mathematics. 29 Quine's opinion seems here in agreement with the anti-deflationist position about truth. As Ketland Quine could assume the idea that the substantiality of truth in a language L is related to the indefinability of truth in L. Ketland has pointed out that it would be misleading to describe Quine as a deflationist. 30 But I would now suggest an explanation of how deflationism works inside to the Tarskian hierarchy in order to see how deflationism can avoid the nonconservativeness objection.

In my opinion, the anti-deflationist reflection argument in unfair with the deflationary (disquotational) theory of truth: the latter has never claimed one and only one level for every truth. On the Foundations of Mathematics electronic list of discussion, 31 Ketland and Franzen have challenged Tennant to give a non-truth-theoretic explanation of the use of the principle of reflection producing the consistency proper extension of PA. But I believe that this challenge is based on a misunderstanding of what means a reasonable version of deflationism. A reasonable deflationary theory of truth, as Tennant seems to advocate, does not claim that we can really throw overboard the notion of truth. Following Quine's lesson we can say that the disquotational theory of truth teaches us only that for every sentences ϕ with no bound variables of level higher than i we are allowed to disquote them when we say that they are true i .

But what is the relevance of my remark on the semantic ascent with Gödel's proof showing that in every consistent arithmetical base theory without predicate we can construct true but unprovable sentences? I mean only that Gödel's proof of S-incompleteness is finally significant from the point of view of a theory S* of higher order than S. The anti-deflationist replies that here is precisely his argument against deflationism: that we can get thanks to the Tarskian theory of truth "a hierarchy of better and better truth predicates but no best." But the deflationist replies that we have to take care of what sort of axioms we need and not precisely to truth-predicates which can be correctly deleted thanks to recursive definitions.

The anti-deflationist reflection argument seems consequently a metaphysical use of logical principles which does not only deal with truth: principles of reflections are logical means to construct different hierarchies of theories and to compare their respective strength. So, when Tennant proposes the principle of uniform primitive recursive reflection to give a meta-proof that G has neither S-proof nor S-refutation, he describes exactly the logical strength, no more, that is needed for the theorem of incompleteness, and, contrarily to Ketland's claim, he has not to prove that principle, because, if I am not mistaken, he would need a stronger one for such a job.

Finally, I remain convinced that the anti-deflationist argument about our ability to "recognize the truth of Gödel sentences" does not pay attention to levels of "truth". It is nevertheless easy to imagine the following situation: being "inside" PA it is impossible to "see" its consistency and so it is impossible to conclude that G is true. On the contrary, every formula ϕ which is a theorem or the negation of a theorem of the arithmetic can be checked thanks to an effective algorithm. One concludes usually that G is a truth of PA but not provable in PA, hence the realist and widespread view about the distinction between truth and proof (the former transcending the latter.) But G being equivalent, modulo PA, to PA consistency statement, it seems obvious that the assertion of G, or the assertion of PA consistency, needs more strength from axioms than PA's and if one want to adorn that assertion of a truth-predicate that one needs an index higher than PA-theorems. The deflationary theory of truth can be understood as the philosophical expression of the attention that one must pay to the level of our truth predicates. Using of truth predicate without index is to be in danger of collapsing in contradiction.

In a very stimulating private correspondence Ketland has replied to me that considerations on a hierarchy of truth-predicates are irrelevant vis-à-vis his argument: PA is a base theory without truth-predicate, and PA(S) proves theorems which are not provable in PA. But I reply that it means also that there are theorems which are proved in PA and consequently these proofs are "truththeoretically explained", to speak in Ketland's language, by a truth-predicate with a level which is lower than theorems proved by PA(S) only. I persist in seeing an intersesting analogy (deserving clarification) between that necessary semantic ascent involved in Gödel's proof and the hierarchy of truthpredicates solving the Liar paradox. Nevertheless it seems to me clear that disquotational process is irrespective of types or orders and, consequently, that the non-conservativeness argument collapses.

Philosophical developments

I said in the introduction of this paper that the philosophical debate about the meaning of Gödel's incompleteness theorem had not changed a lot from the controversy between Carnap and Gödel himself. Vuillemin has pointed out that this discussion was purely philosophical and not strictly scientific (i.e. logico-mathematical) and I agree with him. I see the debate about deflationism and the objection of non-conservativeness as a motivated philosophically one and nobody can prove to be right, nobody can disprove the rejected thesis. The deflationist theory of truth in its disquotational version is in fact a philosophical anti-metaphysical position wearing logical clothes ample enough to avoid the bullet from the non-conservativeness objection. It is more surprising, but no irrational, that such a bullet has been shot by logicians who have learned the lessons of Logical Positivism. The argument of non-conservativeness against deflationism is motivated by mathematical realism. The undefinability of truth seems to stand for transcendence in Ketland's philosophy of mathematics. But the undefinability of truth could be also calculability's (via Church's conjecture), or specifiability's (via set theory), and so one could doubt about the metaphysical significance of the former.

One of the merits of Tennant's position in his paper, is that it does not pretend to "disprove" the anti-deflationist interpretation of Gödel's incompleteness theorem, but only to show that a deflationary account of these famous theorems is licit. This point of his paper seems to involve a pluralist theory of meta-philosophy: there could be several licit philosophical reading of a same scientific result. Such a meta-philosophical pluralism could mean giving up the confusion of philosophy with science.

I believe that the use of reflection principles is philosophically meaningful from Tennant's anti-realist point of view, which denies that truth is significant if truth is not checkable at least in principle. In other words, Tennant holds explicitly an intuitionist notion of truth according to which truth is always epistemically constrained: it makes no sense to say that p is true if we do not have at hand a method of checking the truth value of p. This intuitionist conception of truth is an old and respectable notion of truth adopted by Epicurus, Descartes and Kant, before Brouwer and other logicians. 32 Now one can wonder if the claim that truth is always epistemically constrained is consistent with deflationism: if deflationism is expressed by the disquotational theory of truth, an intuitionist theory of truth says more than "truth is disquotation", but insists on the idea that disquotation in itself is not enough without at least a way of proving the truth. On the contrary, a disquo-tational theory of truth can also fit with realism and with the thesis that truth is the property of true sentences expressing what is the case, independently of any way of checking the so-called correspondence. 33 The only way to reply to this aporia, is to remind that the disquotational theory is philosophically neutral, and that the discussion is on the conservativeness or the non-conservativeness of the truth theory. Shapiro and Ketland hold that the non-conservativeness of truth involved in Gödel's proof implies that truth is transcendent to proof, which is uncontroversial if truth and proof are related to a formal system S. But the question if truth remains meaningful when it is absolutely transcendent to proof is a philosophical question where Gödel's incompleteness theorem has finally little authority. The philosophical debate opposing truth as warranted truth and truth as determined by the universality of Bivalence will remain open and every logician-philosopher can make a free but rational philosophical choice to decide his position. Tennant's solution needs to give up the universality of the principle of Bivalence. From an anti-realist point of view, Bivalence holds only in decidable theories. 34 >From a realist point of view like Quine's, to give up Bivalence would complicate uselessly the logic. 35

Conclusion: towards a positive and philosophically stable interpretation of Gödel's proof

A philosophical system is "stable" if it is not only consistent, but if any of its theses does not create insuperable difficulties vis-à-vis other theses of the system. Quinean realism is, in my opinion, a nice example of an unstable philosophical system: on the one hand empiricism and physicalism stand as dogmas, on the other hand, mathematical entities or mathematical facts belong to our universe, even when the higher parts of set theory have no obvious links with the empirical world. But Gödel shows a philosophical problem starting at the bottom of the mathematical hierarchy, in elementary number theory, where undecidable statements will be always out of reach. There is no strict contradiction between empiricism and mathematical realism, because the former is an epistemological claim and the latter is an ontological one. Nevertheless, even if this distinction between epistemology and ontology leaves a way out, undecidable mathematical statements cause embarrassment: because of the universal application of Bivalence, their truth value is depending on facts which are definitely beyond empirical evidence. The instability of the comes from its effort to both naturalize mathematical knowledge (hence to deny transcendence), and to assume Bivalence and Gödel's proof that mathematics does not consist in provability but in relation to mathematical facts. [START_REF]Gödelian Optimism which denies transcendence but accept bivalence[END_REF] The only way for the Quinean of not to feel uneasy in front of this twofold goal is to believe naively that Plato had only religious motivations to reject empiricism.

At the end of this analysis, I believe that the Gödel phenomena shows that there are only two stable philosophical interpretations of incompleteness theorems. The first is the orthodox realist position, i.e. the genuine Platonism in philosophy of Mathematics which claims that truth is bivalent and transcendent. In order to get stability, the Platonist has to deny empiricism, even if empiricism is not inconsistent with his ontology. Assuming willingly the transcendent existence of a pure intelligible world incompletely described by mathematical theories and various conjectures, the Platonist gives up knowledge for faith and accepts in his philosophy Faith and Mysticism. The unfathomable mystery lies in the impossibility to give a satisfactory answer to the epistemological question: if mathematical objects are really transcendent to our knowledge, and if they are defined only negatively, being neither spatial, nor temporal, etc., then it is very difficult to explain a causal relation to mathematical objects to our brains. That is also why contemporary realism (Quinean realism for example) is not Platonist in the genuine meaning of this term. But, once mystery accepted, the genuine Platonist claims that the burden of the proof is on the anti-realist as well as on the formalist or even on the unauthentic realist (i.e. the Quinean philosopher) who all have to explain what is mathematical content an have to give a plausible explanation of the history of mathematics. Vuillemin, who has finally held the genuine Platonism at the end of his philosophical development, challenged the logical positivism like that. 37 The anti-realism " a la Tennant brings an interpretation of Gödel's incompleteness consistent with the spirit of logical empiricism but without the instability of this latter. Contrarily to Quine's contention, Tennant holds that mathematical truth, and truth in general, consists in provability and he succeeds in showing that it is logically possible to explain Gödel's proof without assuming the substantialist notion of truth but a deflationary-anti-realist account of truth. Then it is possible to explain the history of mathematics as being the history of systems of proofs, without claiming the existence of a transcendent intelligible world that every mathematician brain strives to discover.

To conclude on this point, a sketch of philosophical analysis of Wiles' demonstration of Fermat's conjecture will shed more light on the anti-realist way out. There are differences and analogy between Fermat conjecture and G-sentences. First, Fermat's conjecture is intuitevely clear and simple, when the Gödel sentence is weird. Even if Gödel's theorem is an exploit and appears as one of the most important theorems of Mathematical Logic, it is obviously shorter and less difficult from a technical point of view than Wiles' proof which is developped in two hundred pages and can be checked by very few mathematicians in the world. But the main point is that Wiles has proved that there is no solution to the equation x n + y n = z n when n ≥ 3, that there is no associated curve to this diophantine equation, basing his demonstration on the contemporary Taniyama's conjecture -which is broader than Fermat's -and other mathematical theories taking place later than Fermat. Wiles has turned Fermat's conjecture into a true mathematical statement. There is no need of great mathematical knowledge to see that Gödel's theorem proves abstractly the existence of undecidable statements in number theory, when Wiles has proved generally the non-existence of solution for a defined equation. But an analogy with the lesson of Gödel's theorems can be made: the truth of G can be justified only beyond S, from a S* theory to which S belongs, and, maybe in similar way, the proof of Fermat's conjecture is given from another broader conjecture to which the former appears to be a particular case.

The Platonist is convinced that Wiles' demonstration belongs to the history of mathematical discoveries, and Gödel's proof shows in abstracto the necessity of this historical development, because it shows that Mathematics cannot be conceived as pure syntax, but has content. The indefinite development of History of Mathematics shows concretely that new mathematical truths can always be reached, and Gödel has logically proved that such a development has no end because there are always, in every mathematical axiomatic system, undecidable statements.

The anti-realist philosopher can concede that Carnap was wrong in believing that Mathematics is only purely syntactic, and can concede that Gödel's proof, showing the distinction between logical and mathematical axioms, leads one to acknowledge also that there is mathematical content. But he denies transcendence to mathematical content, which is 'reduced' to proof systems: every mathematical truth is asserted inside some theory and gets its meaning therefrom. There are no mathematical facts that are really independent of proof. So, from the anti-realist point of view, Wiles' demonstration is based on relations of mathematical proof systems, and Gödel's proof shows formal properties of every mathematical proof system in which elementary number theory can be expressed.

If I agree with Vuillemin's thesis that philosophy has its origin in a free but rational choice, I disagree with his last Platonism and I throw overboard Myth, Mysticism, and Faith, to hold only positive and rational explanations in philosophy of knowledge. That is why, to all philosophers who are reluctant to adopt the genuine Platonism, the anti-realist-deflationary account of Gödel's incompleteness theorems should seem to be apt to get the last word on this so fascinating and so difficult logical-philosophical topic.

Notes

1. [Gödel, 1995] 2. [Carnap, 1937] 3. Gödel was convinced that Mathematics is not purely syntactic, but he felt unable to give a positive reply to the question "what is Mathematics?". [Dubucs 1991], pp.53-68

Either abandon the conservative constraint [i.e. the deflationist gives up his claim that truth is conservative or dispensable], thereby becoming some sort of substantialist about truth;

Or abandon the adequacy condition [expressed by the sentence "all theorems of S are true"]. And furthermore, offer some non-truth-theoretic analysis of the conditional epistemic obligation.27