Mic Detlefsen, Hilbert’s Program
Résumés
Deux thématiques sont développées ici : la première, générale, traite de la notion d’objet, la seconde, plus spécifique mais aussi complexe, aborde la question de la réhabilitation du Programme de Hilbert, rendant hommage au grand travail de Mic Detlefsen. Ce dernier montre comment la destruction de ce programme par le théorème de Gödel est une illusion, en dépit de l’importance de l’œuvre de Gödel dans l’Histoire de la Logique. En nous reconcentrant sur le Programme de Hilbert nous ouvrons des perspectives d’analyse de la notion d’objet et sur l’idée de l’effectivité à laquelle nous invite la pratique mathématique.
Entrées d’index
Motsclés :
objet, programme de Hilbert, finitisme, argument standard, Herbrand, intuitionnisme, formalisme instrumentalisme, stabilité, thématisationKeywords:
object, Hilbert Program, finitism, standard argument, Herbrand Intuitionism, formalism, instrumentalism, stability, thematisationPlan
Haut de pageDédicace
To my friend Mic
Texte intégral
1. Introduction
1Are there conditions which govern mathematical objectivity? At the first level, noncontradiction, the constructibility of objects, then at the second level, the legitimacy of the existence of an object. I am going to show that these conditions maintain relations of another order with objectivity. The fact of being able to show the noncontradiction of elementary arithmetic induces effects on the question of their objectivity.
2I will briefly try to remember the essential features which can define the notion of objectivity. In terms of subject, let us say that there is, first, the psychological subject of the mathematician, who experiences the contingent changes that affect him and test the content of the lived experience of his psychological self. And there is the universal mathematician subject who operates by reactivating the meaning of his operations each time. It carries in it when it operates the inscription of the always repeatable law of the operation. Yet it is always individualized. Mathematical consciousness is always enveloped in advance in the horizon of a domain of idealities already constituted as a domain of truths by means of which it is carried towards the objects of its activity.
 1 ^{ }M. Caveing, Le problème des objets dans la pensée mathématique, Paris, Vrin, 2004.
3Any mathematician participates in a space which can be said to be “omnisubjective” where he operates as a universal subject substitutable for any other and the omnisubjectivity of mathematics consists in that it constitutes a domain of idealities independent of empirical subjects. The argument of omnitemporality (mentioned in History of Philosophy as independance on time) and omnisubjectivity do not constitute the basis of mathematical objectivity but are, as Caveing says, its symptom.1 Objectivity is linked to the way in which mathematical objects exist in the world and our access to them, about which I have said little. It therefore refers to the conditions of their constitution its legitimation which I will now address based on Hilbert’s proposals.
2. Finiteness and objectivity
4Hilbert wanted to establish what I would like to call a standard of the objectivity of mathematical theories: they must be noncontradictory and it is possible to elaborate a method to check if this is the case.
5Hilbert as we know tried to develop a method which would guarantee the^{ }consistency demonstrations, as much as the finite models allow to do it for the consistency of certain sets of postulates, thanks to the analysis of a finite number of structural characteristics of a completely formalized calculation. Hilbert hoped to show by an exhaustive inspection of the structural properties of the formulas of a system that contradictory formulas cannot be obtained from the axioms of that system. One of the essential prerequisites of the original Hilbert program was that consistency proofs do not use any procedure involving either an infinite number of structural properties in the formulas or an infinite number of operations on the formulas. Such a procedure which manages to exclude these infinities is called “finitist”, a demonstration of consistency which fulls this condition is called “absolute”.
6A proof of absolute consistency achieves its goal thanks to the minimum of principles of inference, and without presupposing the consistency of another set of axioms. Thus the proof of the consistency of arithmetic should show by a metamathematic procedure that two contradictory formulas like “0 = 0” and “no 0 = 0” cannot be derived from axioms according to rules of established inference.
7Gödel showed that attempts to construct a finitist method (according to Hilbert’s program therefore) of demonstrating the consistency of a system like that of Russell’s Principia must necessarily fail.
3. Hilbert’s Program
 2 ^{ }Le théorème de Gödel, (E. Nagel et al., eds), Paris, Seuil, 1989, p. 153.
8In a collection of texts on Gödel’s theorem, with Gödel’s original paper (1931), Jean Yves Girard, one of the most important current logicians, notes the following.2 “Hilbert’s Program is stated as follows: show that by simple manipulations we can start from a proof δ of a universal statement A, using abstract methods, construct another proof δ’ of the same statement inside real mathematics”. That means “demonstrate the consistency of usual mathematic in real mathematics with finitary methods”. It is a mechanistic model of mathematics where everything could be reduced to symbol games carried out by a giant computer.
 3 ^{ }The Fall of the House of Usher by E. A. Poe, transl. in French by C. Baudelaire.
9In a cinematographic reference, J. Y. Girard speaks of the fall of the Hilbert House,3 carried out by Gödel. The first theorem of Gödel destroys Hilbert’s Program. The second theorem of G destroys HP in its consistency demonstration form. Theorem 1 says that: if T is consistent there is a true universal statement but not provable in T. Theorem 2: if T is consistent then the universal statement Cons (T) which states the consistency of T is not provable in T.
10Hilbert’s Program survived his panning. We can say: he resists (perhaps) because he gave simple (and even simplistic) answers to basic questions about mathematical activity. But the more interesting is that the domain created by Hilbert is called proof theory, an important domain in logic. In fact, Hilbert’s Program, if it is possible to separate it from the ideology of which it is the bearer, contains deep ideas on mathematics. Moreover, there is Gödel’s completeness theorem. It is a problem of pure logic regarding all possible interpretations (models) and in this case there is completeness.
11Of this Program there remains the idea of objectifying, of geometrizing logical manipulations. And this idea has not finished bearing fruit. For Girard finally, it seems that the essential of what we had to reproach Hilbert for is the forgetting of the dynamics. Obviously, one has without doubt to separate HP from its exaggerated interpretations. The question perhaps is to understand why and on what basis, such an interpretation has become widespread, even among the great logicians.
 4 ^{ }It is the topic which he proposed during his stay in France, and he developed it in many directio (...)
12Apparently, Mic Detlefsen held a position opposite to that which I have just described in a simplistic way. We must emphasize the term “apparently”. He defends it by restoring it to its truth. He methodically applied his position, but you could see to what extent he opened up to Historical Epistemology and also to Category Theory. He forged a Research Program that he intended to develop during his stay in France. The bases of this program lie in his works on Hilbert’s Program. Everything he has achieved (even the ideal of proof4) remains based on this fortress. This is the reason why I will linger at length, if possible, on his book on the HP.
 5 ^{ }M. Detlefsen, Hilbert’s Program. An Essay on Mathematical Instrumentalism, Dordrecht/Boston/Lanca (...)
13It is interesting to begin with the end, viz. the conclusion that Mic Detlefsen drew from his work on Hilbert’s Program. “We cannot claim to have established Hilbert’s Program. Instead, we can only claim to have rescued it from its most powerful and influential adversary (i. e. the SA [the Standard Argument]) and to have revealed some of its heretofore unrecognized philosophical potential”.5 Could we appreciate this judgment with lucidity, adapt our lucidity to that of Mic?
4. Mic Detlefsen’s display of Gödel’s theorem
14Remark. To facilitate the reading of the article, I quote freely from the book “Hilbert’s Program”, Dordrecht 1986, of M. Detlefsen.
15The simplest formulation of Gödels first incompleteness theorem asserts that there is a sentence which is neither provable nor refutable in the theory P under consideration. Gödel’s second incompleteness theorem asserts that for this sentence one can take a formalization in P of the statement that the theory P itself is consistent.
16I am concerned about the philosophical reflexion on Gödel’s theorem proposed in Detlefsen’s book. He refers to what he called the Standard Argument against Hilbert’s Program. And yet according to our philosopher this argument is derived from Gödel’s Second Incompleteness theorem and not from the First one. Before explaining and questioning this argument, I will recall Mic’s argument against those who believe that the traditional argument from G2 (Gödel 2) is not the only, nor even the best, counter to Hilbert’s Program, and that these antiHilbertian use of G1 (Gödel I) in order to stand in Hilbert’s way.
4.1. Gödel’s first theorem
17One recalls Smorynski’s argument.
The Second Theorem clearly destroys the Consistency Program. For, if R cannot prove its own consistency, how can it hope to prove the consistency of I? Even the First Theorem does this since (1) the statement ϕ is real and (2) ϕ is easily seen to be true. (1) requires looking at the construction of ϕ (2) is seen by observing that ϕ asserts its unprovability and is indeed unprovable. Thus, the First Theorem shows that the Conservative Program cannot be carried out and, hence, that the same must hold for the Consistency Program.
 6 ^{ }C. Smorynski, “The incompleteness theorems”, in Handbook of Mathematical Logic, Amsterdam, 1977 e (...)
 7 ^{ }An argument is sound if it is both valid and all of its premises are actually true.
 8 ^{ }See also A. Mostowski, Thirty Years of Foundational Studies, Basi Blackwell Oxford, 1966.
18“R” is taken to stand for a formal system that codifies real or contentual thought, “I” a formal system of ideal reasoning and “ϕ” the undecidable formula of G1.6 The Hilbertian’s search for finitary proofs of the real soundness and consistency of I are termed (respectively) the “Conservation Program” and the “Consistency Program” by Smorynski. Soundness of a deductive system is the property that any sentence that is provable in that deductive system is also true on all interpretations or structures of the semantic theory for the language upon7 which that theory is based. In symbols, where S is the deductive system, L the language together with its semantic theory, and P a sentence of L: “if ⊢s P, then also ⊨l P”.8
5. Some of Detlefsen’s specific topics
19Our philosopher has developed a concept of “instrumentalism” which can be correlated with a reexposure of Hilbert’s Program. He conceives different levels of understanding from a general inspiration to a refutation of various ontologies. He is antirealist and therefore antiPlatonic.
20In his view the basic strategies for explaining applicability or potency of a given piece P of mathematics (e. g. theory, proof, or computation) are of two fundamentally different types:
1 the socalled realist strategies which see the applicability of P as being explicable only by the assignment of an interpretation or meaning to P;
2 the socalled instrumentalist strategies which contend that P can be come applicable through being evaluated even if it is not assigned a meaning.
21Hilbert’s Program, that is supported by Hilbert’s instrumentalism, is a Research Program protected by auxiliary satellites of instrumentalism. This sort of instrumentalism is marked by several features which serve to distinguish it from other forms of instrumentalism. Each of these distinguishing features arises from the acute sensitivity that Hilbertian instrumentalism brings to the two major problems facing the instrumentalist: namely “Frege’s Problem” and the “Dilution Problem”.
22As for Fregean ontology, we have as a body of truths of the subjectmatters with respect to which it serves as useful guide to truth. Such is the essential criticism our philosopher addresses to the neoFregean. He criticizes the Fregean ontology for not living up to its claims. He does not make the subject of mathematics the subject of which they would be a useful guide to the truth. One can comment by saying that this criticism is instrumentalist.
 9 ^{ }M. Detlefsen, Hilbert’s Program…, op. cit.
23The Dilution Problem is outlined in different places of Mic’s book9, which we speak about. I will briefly describe it. Let us replace real objecttheoretic, mathematical proofs of problematic real propositions (Mic calls them “Oproofs”) with metatheoretic proofs (or “Mproofs”) of those propositions. The “Dilution Problem” is the problem of showing that the gains in epistemic expansion that are promised by this replacement are not neutralized or indeed overcome by a corresponding drop in the general quality of our epistemic holdings. These terms, like quality of epistemic holdings, express a judgment on metatheory, a sort of higherlevel argument.
24Let’s consider the argument, about the G1 antiHilbertian. That is (it is possible) the argument from the claim that there is a true real formula that is not provable in R, to the conclusion that Hilbert’s Program can’t work. And Mic adds what sense there might be to saying that there is real formula ϕ that is not provable in R given that R is said to be a codification of real reasoning.
25If truth is understood finitarily then a real formula ϕ will be true only if it is finitarily provable. It is interesting to ask the question of the existence of a true formula but not provable in R, R being the codification of real reasoning.
 10 ^{ }Ibid., p. 162 sq.
26And then the only way that there could be a true real formula that is not provable in R is that not all real reasoning is codified in R. And so we will see that the very conditions of formulation and position of the inference are contradictory. I follow Mic.10
27This could happen for either of two possible reasons:
(i) R itself is not a complete formalization of finitely reasoning, though there might be such.
(ii) R is not a complete formalization of finitary reasoning and nothing that we would want to call a formal system could be. This alternative exhausts the question.
28Such a claim is not plausible. There is no reason to say that the undecidable formula ϕ produced by G1 is finitarily true (i. e. finitarily provable). The only argument for its truth is one designed to show its classical and not its finitary truth. And for this reason, it provides no reason for believing that there is a finitary truth that is not provable in R.
29It is an argument of coherence; it is necessary, we insist, according to our friend of NotreDame, to distinguish the finitary conception of truth from that which is said to be classical.
30This argument is subtle. In the terminology of this philosophy of mathematics, one has to distinguish classical and finitary truth.
31Mic reconstructs the reasoning:
i) ϕ says of itself that it is unprovable in R,
ii) It is true that ϕ is unprovable in R,
iii) ϕ is true.
 11 ^{ }Ibid., p. 26 sq.
32The second premise shows that the argument for the truth of ϕ is an argument for its classical truth and not a finitary proof of ϕ. It provides no reason for believing that there is a finitary truth that is not provable in R. Let us again remark, that Detlefsen’s defense of the Hilbertian arguments consisting of the opposing objections to the antiHilbertian. We will see, the most important is the Fregean, and its consequences. Frege’s Problem, says Mic, asserts that instrumentalism cannot explain why mathematics is a useful device for deriving truths because only an interpretation of as opposed to an evaluation of mathematics can do that. In a nutshell, it is not enough to prove that the instrument is reliable, we must explain why it is reliable. And here is an exemple of Detlefsen’s argumentation.11 What is it that an explanation of reliability is supposed to give us that a proof of reliability based on evaluation rather than interpretation never could? questions Mic. And it is difficult to see what the neoFregean realist is demanding because of the poverty of his own realism. The basic problem is that the realist can interpret mathematics (or ideal mathematics) and thus presents it as a body of truths, but according to Mic’s words, he has no apparent way to interpret it as a body of truths of the subjectmatter(s) with respect to which it serves as useful guide to truth. In this sense the realist has failed to live up to the standard of his own paradigm.
 12 ^{ }Ibid., p. 163 sq.
33Let us briefly consider another argument.12 The fact that ϕ (taken as a finitary truth) is not provable in R does not necessarily promise dire consequences for the Hilbertian. By resuming to give a convincing antiHilbertian argument from G1 as applied to R one would have to establish, according to Detlefsen’s argument
(1) ϕ is a finitary (as opposed to a classical) truth,
(2) there is no formal system expressing all and only finitary proofs,
(3) there is some ideal system proving ϕ to whose defense the Hilbertian is committed.
34We don’t make an argument against (3). The main point is for us that G1as applied to R lacks antiHilbertian force. If we take antiHilbertian impact of G1 as Smorynski, even if (1), (2), (3) are accepted, the mere improvability of ϕ in R cannot be taken as impugning the conservating program (CP).
35But ϕ is not an example of such (one can add even if it taken to be a true real formula) since it is no more provable in I than in R. Conclusion: the existence of ϕ does not imply that there is a real formula provable in I that is not provable in R. And the existence of ϕ does not imply the failure of the Conservation Program for I.
36Detlefsen supposes that we can expand the reasoning that concerns the force of G1 in the following manner. For any ideal system I whatsoever, there is an ideal proof of ϕ (viz. the non finitary argument establishing its intuitive truth).
37Moreover, ϕ is a real formula, and it is not finitarily provable (else it would be provable in R, and hence in I). But if there will always be a real formula that is ideally but not finitarily provable, then the Conservation Program can never be carried out with finality. And finally, the Conservation Program can never be carried out with finality.
 13 ^{ }G. Kreisel, “Hilbert’s Programme”, in P. Benacerraf and H. Putnam (eds.), Philosophy of Mathemati (...)
38Mic cites Kreisel on Gödel,13 who is defending the argument that Hilbert’s aim was to provide certainty that every possible system of ideal reasoning is realsound.
39Strong soundness of a deductive system is the property that any sentence P of the language upon which the deductive system is based that is derivable from a set Γ of sentences of that language is also a logical consequence of that set, in the sense that any model that makes all members of Γ true will also make P true. In symbols where Γ is a set of sentences of L: if Γ ⊢s P then also Γ ⊨l P*.
40* It’s different from completeness. Completness of a deductive system is the property that any sentence P of the language upon which the deductive system is based that is derivable from a set S of sentences of that language is also a logical consequence of that set, in the sense that any model that makes all members of Γ true will also make P true. Γ⊨Φ then Γ⊢Φ.
 14 ^{ }M. Detlefsen, Hilbert’s Program…, op. cit., p. 166.
41According to Kreisel,14 such a method would provide a final solution, at least “in principle”: we would know, here and now, how to decide the consistency of any formal rules we encounter whatever their source (semantic analysis or formal experimentation).
 15 ^{ }Ibid., p. 167.
42Maybe the most important remark lies in the sequel of this argument. The chief source of our (Mic’s) disagreement is the claim that Hilbertian instrumentalism is committed to obtaining “a ‘final solution’ to the problem of foundation for ideal mathematics. … we found no reason to saddle the Hillbertian with the hopeless task of finding a ‘purely mathematical’ defense of the ideal method”.15
 16 ^{ }Ibid., p. 168.
43Mic Detlefsen’s claim, with insistence on it, is the following.16 If the Hilbertian is to be understood in either of these ways, (we will see later it is not the case) his program must surely be regarded as a failure. He recalls, there is no reason to regard even a finitary proof of the reliability of somebody of ideal methods as being infallible or unsusceptible to revision. And he adds that the finitary methods that one would need to use in order to give such a proof are not the most certain finitary methods imaginable. You have here trivial counter arguments against trivial arguments.
44A search for absolute certainty in his proof (of realsoundness) would appear to be an entirely unwarranted thing for the Hilbertian to undertake. We can consider that the main issue lies in Detlefsen’s concept of Hilbert’s instrumentalism. The construction is subtle. It needs instrumentalism to be correlated with facing with Fregean thesis and Dilution Problem. But we (JJ S) consider that his concept of instrumentalism is too strict. But it’s for the sake of the cause. He shatters this hypothesis and makes the Fregeanism to which he is opposed difficult to defend. It is clear that the undertaking to rehabilitate Hilbert’s program must refute the arguments which claim to destroy it and therefore in particular those which claim that Theorem G1 is sufficient for this refutation.
 17 ^{ }See as a survey. Gödel, K. “On formally Undecidable Propositions of Principia Mathematica and Rel (...)
45What is the benefit of this strictness? The substance of Detlefsen’s refutation of the G1 arguments also allows us to characterize more flexibly the instrumental value and the more diverse character of I (the given system of ideal mathematics).17 After this first destruction let’s move on to the main one.
6. The Standard Argument
 18 ^{ }G. Kreisel, “What Have We Learnt from Hilbert’s Second Problem”, AMS Proceedings of Symposium in (...)
46It is the main argument in Mic Detlefsen’s argumentation. The keypoint, let’s remember, in the defense of Hilbert’s Program, since it is the basis of the arguments of the detractors of the HP.18
47I keep that the SA has the following features.
48It is derived from Gödel’s Second Incompleteness Theorem (or G2). It is interesting to start with the weaknesses of the argument of which we can locate three. This manner allows us to give this argument a maximum force.
 19 ^{ }M. Detlefsen, Hilbert’s Program…, op. cit., p. 77.
49(i) the strengthening (or generalization) called for the first weakness is one capable (according to our philosopher19) of showing that the set of properties of a formula which make it a fit expression of consistency for an ideal system subsumes a set of properties guaranteed to make it unprovable in that system.
50This argument is called The Stability Problem. I recall it: to show that every set of properties sufficient to make a formula of T a fit expression of T’s consistency is also sufficient to make that formula unprovable in T (if T is consistent).
51(ii) the strengthening demanded by both the second and third weaknesses (Mic refers to it as: the Convergence Problem and the Problem of Strict Instrumentalism) is this: show G2 to be obtainable in an antiHilbertian form not only for the usual form of formal system T, but also or every formal system capable of reproducing the humanly useable portion of T.
 20 ^{ }Ibid., p. 84.
52I recall the thesis of Strict Instrumentalism. Of the infinitely many ideal proofs constructible in a given system T of mathematics, only finitely many of them are of any value as instruments of human epistemic acquisition.20
53The relation with the humanly portion of T here is what we will call “resorting to human capacity”, a factor that is present in Detlefsen’s different arguments.
 21 ^{ }Ibid.
54The Convergence Problem –I recall it now– runs so: there is no longer any reason to suppose that the set of feasible provable real theorems of ideal system T will subsume the set of finitarily provable formulae, nor is there any reason to suppose that every finitarily provable real theorems of T is more effciently provable by an ideal proof in T than by a purely finitary proof.21
55Mic reconstructs from Gödel’s theorem the general architecture of a system of arguments supposed to refute Hilbert’ s program, called standard argument. I am not reconstructing it here; it is precisely explained in 13 steps in his book.
56We should accept that –according to the SA– the conclusion is radical: Hilbert’s Program cannot be realized in any substantial part of the body of mathematics.
57We have here what our philosopher takes to be the Standard Argument against Hilbert’s Program. And then he will demonstrate what he considers to be some fatal problems concerning it.
7. The criticism of SA
58The claim that the SA does not refute Hilbert’s Program is not to be taken as a consequence of the fact that it fails to give a finitary refutation of it. That is the key point for Detlefsen.
59His criticism consists in charges to the effect that there is no good reason of any kind to accept the SA.
60So arises the Stability Problem: to show that every set of properties sufficient to make a formula of T a fit expression of T’s consistency is also sufficient to make that formula unprovable in T (if T is consistent). And the defender of the SA must find some strengthening of G2 that guarantees the unprovabilityinT of every formula which can be said to express the consistency of T. That is, to isolate a set C of conditions on formulae of T such that every formula of T which is said to express the consistency of T satisfies C. This is a generalization of G2. With this generalization we have:
 22 ^{ }Ibid., p. 82.
61•(GenG2) If T is consistent and Con(T) is a formula of T which satisfies C, then Con(T) is not provable in T.22
62It must be emphasized: the writings on Hilbert’s Program seem to have been oblivious to give a convincing argument to the effect that the generalizing condition C really are conditions able of expressing the consistency of T. It is a general neglect (Mic’s words). The point also for Mic is drastic: no defense of these generalizing conditions can be successful.
8. Strict instrumentalism and the convergence problem
631 I will firstly, explore the problem of instrumentalism. After stating it, we shall see that this causes serious problems for the SA.
 23 ^{ }Ibid., p. 84.
64Here is the Thesis of Strict Instrumentalism (TSI), I remembered above: Of the infinity many ideal proofs constructible in a given system T of ideal mathematics, only finitely many of them are of any value as instruments of human epistemic acquisition. We will consider the length of ideal proof of the system T, meaning the number of occurrences of characters of T’s alphabet that appear in the proof. There are many other measures. But in the argument the essential claim is that there is a finite bound on the number of character occurrences that can appear in a humanly useful ideal proof.23
65The Hilbertian instrumentalist is, strictly speaking, only obliged to establish the realsoundness of a finite number of the ideal proofs constructible in a given system.
662 The Convergence Problem. What the problem consists of? It arises for (3). ((3) is every finitary truth (in particular every truth of the finitary metamathematics of T) can be “expressed” as theorem of T).
 24 ^{ }Ibid., p. 86.
67Regarding TSI, it is no longer clear that the content of the Hilbertian’s ideal mathematics (in the feasible body of ideal proofs of a given system) and the content of finitely reasoning will “converge” in the manner of (3). It is not undubious that the ideal methods to which the Hilbertian is committed theoremwise (the words of Mic24) subsume finitely reasoning.
 25 ^{ }Ibid., p. 89.
68For “elementary number theory”, as conceived in that premise designate an infinite system of proofs. It cannot be contained in any of the finite systems of ideal proofs containing them. The useful part of T can be embedded in an inductively defined set of proofs other than T itself. Mic calls this system the Hilbertian residues of T and designates it as ‘Th’.25 This new concept allows to develop a restricted way to analyze an intrinsic argumentation. This is to be deepened beyond the Mic’s book.
 26 ^{ }Ibid.
69It can be shown that the set of axioms of TH will be finite. And –Mic will show that– the finite axiomatizability of TH is one of the most important features which enables us to pose a “stiff” challenge to the SA and any argument based on a like application of G2.26
70I will return, following Mic’s argumentation’s order, to the Stability Problem.
71If the Gödelian is to find a solution to the Stability Problem for a given system T of Mic Detlefsen’s way of expressing it is specific –he must locate a set C of conditions on formulation of T, (T being an ideal system whose syntax is to be represented or “arithmetized”). This set is such that
(1) every formula of T that can be said to express the consistency of T satisfies the conditions in C,
(2) no formula of T that satisfies C can be proved in T.
 27 ^{ }Ibid., p. 94 sq.
72Mic presents the strategy for generalizing G2 in the following manner. Isolate those features of the provability formula that are crucial to the proof of G1 and show that these are all establishable in T. And then we have the usual generalization of G2. First, we shall give the proof of the generalized version of G1. And this for any provability formula for T (‘Prov_{T} (x)’) satisfying the following three properties27
(I) The Diagonalisation Property (DIAG for short): there is some formula G of T such that ⊢_{T}G≡∼Prov_{T}(⌈G⌉
(II) The Local Provability Completeness Property (LPC) for every formula A of the language of T if ⊢_{T}A then ⊢_{T}Prov_{T}(⌈A⌉).
(III) The Local Provability Soundness Property (LPS) for every formula A of the language of T, if ⊢_{T}Prov_{T}(⌈A⌉) then ⊢_{T}A.
73And from these conditions the proof of the generalized version of G2 proceeds, according to Mic, in two parts.
74For the sake of the completeness of establishing the C conditions we must add conditions that can be concentrated collectively as Derivability Conditions. I cite only one condition amount the four ones, the modus ponens condition. We must require that ‘Prov_{T} (x)’ satisfies the following conditions:
(FMP) for all formulae A, B, of the language of T, ⊢_{T} (Prov_{T} (⌈A ⊃ B⌉) ∧ Prov_{T} (⌈A⌉)) ⊃ Prov_{T} (⌈B⌉).
75We also need formalization of each of the conditions DIAG and LPC, viz. respectively FDIAG and FLP. See below for more precise developments.
 28 ^{ }See also S. Feferman, “The Arithmetization of Metamathematics in a General Setting”, Fundamenta M (...)
76In Mic’s argument the Derivability Conditions will serve as the focal point of the critical discussion of the Stability Problem. Mic explains how the whole enterprise of arithmetization that is supposed to contribute to the evaluation of Hilbert’s Program.28
 29 ^{ }M. Detlefsen, Hilbert’s Program…, op. cit., p. 97 sqq.
77Mic gives for this reason, a very subtle interpretation of the arithmetization.29 Arithmetization is supposed to be a device which allows us to infer that the consistency of T cannot be proven in its informal finitary metamathematics from the hypothesis that a certain formula Con(T) is not provable in T. What is important, according to Mic, is that arithmetization establishes a correlation between Con(T) and the proposition that T is consistent. This correlation is semantical, the correlation between the formula Con(T) and the finitary metamathematical proposition that T is consistent. When it is said that Con(T) “expresses” the consistency of T, one means this correlation. Mic recalls that this relationship of “expression” is more complicated than the usual semantical relationship which links a sentence of formal language with the proposition that is its standard interpretation. The standard interpretation of Con(T) is different: it is not the proposition that T is consistent, but rather a certain arithmetic proposition. The passage from this arithmetical proposition to the metamathematical proposition that T is consistent, an additional step of “interpretation” is necessary. The inverse of the Gödel numbering has to be applied in order to decode the arithmetic proposition which is Con(T)’s standard interpretation.
78In this way we have to conceive two significances of the semantical Gödelian relation. A formula Con(T) interpreted in an arithmetical language, and this is the usual semantical relationship. And this interpretation by Gödel’s numbering gives a purely arithmetic proposition which Con(T)’s standard interpretation that is related with the metamathematical proposition which assertsT’s consistency.
79Mic considers two different components of the semantical relationship between Con(T) and the proposition that T is consistent.
80•One is the usual semantical relationship by which the formula Con(T) is connected to the arithmetic proposition that is its interpretation under the standard semantics for T.
81••The second is that which Gödel’s numbering induces between the genuine arithmetic proposition which is Con(T)’s standard interpretation, and the genuine metamathematical proposition which asserts T’s consistency.
 30 ^{ }Ibid., p. 98.
82We have a bipartite view of the mechanism or arithmetization. And Mic shows that the usual account of the inference from Con(T)’s unprovability in T to the finitary unprovability of T’s consistency fails to justify the proposition in stake namely: the proposition that T is consistent is not finitarily provable.30 Small victory.
83Let us remember that we have to use DIAG (The Diagonalisation Property), LPC (The local Provability Completeness Property), FDIAG: there is some formula of G of the language of T such that ⊢_{T} Prov_{T} (⌈G ≡∼ Prov_{T} (⌈G⌉)⌉), and FLPC: for all formulae A of the language of T ⊢_{T} Prov_{T}(⌈A⌉) ⊃ Prov_{T} (⌈Prov_{T} (⌈A⌉)⌉).
 31 ^{ }Ibid., p. 96.
84If we add to theses conditions the FMP (modus ponens) condition, the net addition that the formalization of Part II makes to C si FLPC and FMP, C is to be taken as comprised of these conditions: DIAG, LPC, FLPC, FMP. If we remember that Con(T) is constructed in a direct way from the formula expressing provability, Mic proposes to think of these conditions (referred collectively as the “Derivability Conditions”) as governing our choice of formal expression of provability and of our formal expressions of consistency.31
85I will comment on this as follows.
86The Derivability Conditions is the set of constraints on consistency expressions which produce a generalization of G2. Mic gives us a construction made of the elements that must be discussed, as necessary premises for the generalization of G2.
 32 ^{ }Ibid., p. 107.
87I would like to add Mic’s general remark. The question is about a formula and a métamathematical notion M. Even in its modified versions, the ability of to express truth regarding M as theorems of T has something to do with its ability to represent M. And that is what is important: the failure of a consistency formula to encode truths concerning the notion of unprovabilityinT would appear to have negative effect on its ability to properly express or represent the notion of T’s consistency.32
88When Mic says that not all truths concerning the notion of unprovabilityinT are Tcodifiable let us remember that that claim is cogent so long as our conception of metamathematical truth is the classical one, because there are all manners of classical true metamathematical propositions that are not Tcodifiable. This distinction (between classical and the finitary conception of metamathematical truth) is also essential. Indeed, it changes when we switch from a classical to a finitary view of metamathematical truth. All of Mic’s exam ples of true but nonTcodifables propositions presuppose the consistency of T.
89And for the usual cases of T, we cannot simply assume that there is a finitary proof of T’s consistency. The finitary truths are at issue.
 33 ^{ }Ibid., p. 129.
90If I go directly to the conclusion of this chapter I note that Mic examined three proposed solutions to the Stability Problem and found them all to be insufficient “in one respect or another”.33 But let us take a step back. I will remember that the second argument of the chapter, i.e. Kreisel’s and Takeuti’s arguments, is not pertinent, because in Mic’s argument, Hilbert’s instrumentalist epistemology is fundamentally responsible for his ability to escape the procedural constraint of Kreisel and Takeuti.
 34 ^{ }The dialogue with Dag Prawitz was important for Mic. He invited him as keynote speaker at the ina (...)
 35 ^{ }D. Prawitz, “Philosophical aspects of proof theory”, in Contemporary Philosophy. A New Survey vol (...)
91In a long section Mic explores the socalled classical proposal, which we can find by Prawitz 34concerning Hilbert’s classical writings on his program35.
92In his 1925 Münster address and in his 1927 Hamburg address Hilbert made remarks concerning consistency proofs and proofs of realsoundness. What is important is that he drew a very tight connection between the two.
 36 ^{ }D. Hilbert, 1927, “The Founadations of Mathematics”, in J. van Heijenoort (ed.), From Frege to Gö (...)
To be sure, one condition, a single but indispensable one, is always attached to the use of method of ideal elements, and that is the proof of consistency, for extension by the addition of ideal elements is legitimate only if no contradiction is thereby brought about in the old narrower domain…36
93What Hilbert describes here is the consistency problem and his concern with the realsoundness problem. This suggests –for Mic’s reflexion– a new defense for the Derivability Conditions (or, better of FLPC, or its generalization to provable Σ^{0}_{1 }–completeness). He refers to Kreisel, Prawitz, Smorynski, Giaquinto.
 37 ^{ }M. Detlefsen, Hilbert’s Program…, op. cit., p. 126.
94Mic reconstitues the argument by means of four claims, I don’t display here. The second argument is very interesting because it is carried out at the level of intuitive, rather than arithmetical, metamathematics. He says that the realsoundness of T can be inferred from its consistency, given two auxiliary premisses:37 i) every true real formula of T is provable in T ii) the denial of a false real sentence is a true real sentence.
95In response to these arguments, we might mention the dubious identification of ProvT (⌈A⌉) ⊃ A with real soundness. This formula is supposed to express the claim that every real Π^{0}_{1}_{ }formula provable in T is finitarily true but how is this proved? This is only a schema, and so does not express a general proposition at all.
 38 ^{ }Ibid., p. 127.
96As regards the second argument, Mic’s reservation concerns the use of assumption (ii), i.e. the claim that the denial of a false real sentence is a true real sentence (according to Prawitz). It is acceptable when restricted to variablefree real sentences. But –as Mic remembers– it would seem to be false when applied to Π^{0}_{1}_{ }real sentences at least if it is correct to assume that some Π^{0}_{1} sentences are to be counted as false, and Mic gives the example: “(x)(x = 0)” or “(x)x = x”. The justification is the following: the denials of such sentences are (equivalent to Σ^{0}_{1}_{ }sentences and “as it is well known Hilbert (and Mic) didn’t countenance such sentences as real sentences at all”.38
 39 ^{ }Ibid., p. 127 sq.
97The argument (not cited here) has its faults, their sources are in the same distinction: it seems only proper to conceive of realsoundness and real completeness in terms of finitary provability rather than classical truth. But if soundness and completeness are conceived in this way, Prawitz’ argument fails. Why? Because we can no longer make our way (again according to Mic’s words) from the hypothesis that T is not realsound, to the claim that there is false real sentence provable in T. Rather all we can say is that there is a real sentence R, provable in T, but not finitary provable. This does not imply that the denial of R is finitary provable. And it follows that realcompleteness cannot be invoked to conclude that the denial of R is provable in T.39
98It may oblige him to give up any hope of turning a proof of T’s consistency into a proof of T’s soundness. But it does not require that he abandons the search for a finitary proof of T ‘s soundness.
99Generally speaking, Mic builds a chain of arguments which lead to its conclusion. Each link in the chain must be as tight as possible. It may be necessary to reinforce arguments that are elements of the chain that are too weak. But that done it can show the untenability of the argument.
100The current defense of the DC thus yields G2 in a form baring only relatively minor consequences for the Hilbertian instrumentalist. It does not defeat his proposal strategy for dealing with the dilution Problem.
9. Some remarks on the convergence problem
101This is a very long and important argumentation. It is concerned with the question whether the epistemic benefits are evenly or unevenly distributed over it. The question is related with material conditions of human work. As I noticed, there are frequent references to the human work, or more generally to the capacities of humans.
 40 ^{ }Ibid., p. 142.
102When the epistemic benefits of a system can be compressed into one of its parts, we say that the system is “localizable”. And Mic says “we believe in localizability”.40 The human epistemic agent operates under the constraints of finite bounds on both the amount of time and effort he can expand on epistemic pursuits. The epistemic benefits of an ideal system are localized by the very finitude of human cognitive capacity. It is an important feature of Mic’s reflexion. This (finitude) is intended to reflect the practical limitations governing humans of ideal proofs as ideal instruments. Therefore, the limitations are realized through the localizations as finite portion of any system of ideal proofs having humanly manageable length and complexity.
103There are many questions about this localization. I cannot explain and answer these questions here.
 41 ^{ }For the synthese see M. Detlefsen. “On an alleged refutation of Hilbert Program”, in Proof, Logic (...)
104We had here a powerful defense of the Hilbert’s Program by means of theconstruction of the Standard Argument. This was the result of a construction which presented the foil of Hilbert’s program but gave maximum strength to the arguments of his opponents.41
10. Some hypotheses
105It is true that it may seem difficult to credit Hilbert on the one hand with such powerful inventions as the notion and construction of metamathematics and on the other hand to reproach him with an erroneous construction and program like the one that we report as the Hilbert’s Program. It is therefore interesting to see that Mic’s positions are quite close to those we can find in the work by Cavaillès except for a few points. Our interpretation (it’s almost a banality) is that Hilbert’s Program is a concentration of Hilbert’s philosophical positions. We will briefly recall Cavaillès’s arguments.
 42 ^{ }K. Gödel, “Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme”, M (...)
106After his presentation and his commentary on Gödel’s theorem, Cavaillès revisits the relation to Hilbert. He says that the reason for this result must be sought in the fact that “the formation of higher and higher types continues in the transfinite, while there is at most a countable infinity in each system”.42
 43 ^{ }J. Cavaillès, Méthodes axiomatiques et formalisme, op. cit., p. 150.
107Hilbert gave the example of a transfinite recursive construction of types for functions: however high the upper bound (class II ordinal number) it can alwaysbe exceeded. We wrongly imagined that we were setting up a new system.43
108A proposition relating to all types (or stating that a relation is true for variables of all types) –therefore of type immediately superior to these– is part of the syntax and not of the system. In general, the “impossible to demonstrate” character is not definable. To get out of the vagueness, you have to come across a proposition whose demonstrability involves contradiction.
 44 ^{ }J.Y. Girard, Le point aveugle, I Cours de Logique, Vers la perfection Hermann, 2006, p. 18.
109Hence the choice made by Gödel of the proposition p(Np) to reach the no saturation (see below for the definition). The application of the rules of use introduces implicit relations which did not appear in the formalism. As Cavaillès (and Girard today) remarks, Gödel resuscitated the paradox of the Liar. And we now know, (see Girard)44 it is a version of the fixed point theorem. Here it is the introduced paradox that counts, and we cannot get out of this paradox.
110And the steps to save saturation are fruitless.
 45 ^{ }J. Cavaillès, Méthodes axiomatiques et formalisme, op. cit., p. 151 sq.
 46 ^{ }Ibid., p. 125 sqq.
111As Bernays said, quoted by Cavaillès,45 Hilbert tried to force the solution, by the introduction of a new rule (using the sign Π which makes it “destroy” the formalism). For the demonstrations of noncontradiction the evil seems less irreparable. We will go back further to the chapter entitled “The demonstrations of noncontradiction”.46 This question must itself be understood in conjunction with more general demonstration problems.
 47 ^{ }Ibid., p. 122.
112To approach again the position of the question of the demonstration of non contradiction, let us add a few more characteristics of the intervention of recursion. Cavaillès underlines the parallelism between the progressive definition of types and the generation of class II ordinals. Passing to a type immediately superior supposes the intervention of the passage to the limit. Hilbert shows that the set of recursive functions has the same power as class II. We have in the demonstration an example of how Cantorian theory is integrated into formalism and of the role of the metamathematical theory. We should consider its imperfections. It is based on the assumption that the transfinite recursion is completely eliminable. One uses two lemmas. On the one hand, lemma II: “if a function of integers has been constructed at the end of a transfinite induction … we can always define it by an ordinary induction, using types of the same origin”; on the other hand, lemma I: “if by the use of functions defined by means of the symbol ε we have been able to give a formalized refutation of the continuum theorem, these functions can always be replaced by functions definable without ε”.47 We recall that the function ε is defined in the schema
A(j_{m}) → A(εx_{n }A(x_{n}))
113The ε function determines the choice of a particular individual when the predicate suits a group of individuals. It is a universal means of passage between variable propositions and individualized propositions.
 48 ^{ }Ibid., p. 123 sq.
114Lemma I refers to a general lemma of metamathematics: “the resolubility of any welldetermined mathematical problem”. It is an act of faith, says Cavaillès in the limitless power of the establishment of formalisms. Lemma II further expresses that the infinity of functions of integers and that of class II are small enough to be dominated by ordinary induction (which is false for the infinitof functions of real variables). No possibility of proof appeared for these two lemmas. It is remarkable that then the very demonstration sketched by Hilbert is metamathematical, whereas it is a question of a mathematical problem. And the tests of specific treatment of the theory of the demonstration bring out its importance. Among these problems arises that of noncontradiction.48
 49 ^{ }Ibid., p. 124.
115The noncontradiction of a sufficiently rich theory cannot be made apparent without artifice.49 The demonstrability of a proposition is not in fact, says Cavaillès, a structural property… “It escapes any finite decision”. It is therefore necessary to resort to an indirect characterization: necessary but not sufficient condition of demonstrability, and such that the negation of a proposition does not satisfy it. For the formal systems of classical analysis and number theory we tried in turn valuation, decay, and effectuation. Problems which we cannot expose have arisen, but this first method results in a partial evaluation. This is the attempt described by Cavaillès and von Neumann. We will retain that for a sensibly more restricted formalism, that of the theory of numbers, with as only function the function of successor and of the variables. Herbrand and Presburger gave a method which proves not only that there is no contradiction, but also that there is saturation and allows one to decide whether or not a proposition is decidable. (I remember that we can say that a theory is saturated if any proposition formulated in its fundamental notions is either demonstrable or refutable (its negation is demonstrable) in the theory).
 50 ^{ }Ibid., p. 144.
116If we hold that the problem of the ground is posed as Hilbert takes it, Gödel takes it in a way from the rear: he tries to determine what of the processes of metalanguage can be formalized in the language.50 The undertaking thus provides an analysis of the crude notion of an intuitive reasoning. And as is well known he creates a one to one way coordination of Gödel with integers, the symbolic material. Concepts and relations of metascience become concepts and arithmetical relations.
117For the main metamathematical properties or relations Gödel gives the actual example of their arithmetical translation: for a sign appearing in a formula will be to be the exponent of the nth term in the product of prime factors representing the formula. To be an axiom will therefore be the function of disjunction between them… to be a “demonstration drawing” is, for a number, the property of decomposing into prime factors each of which has for exponent the number corresponding to an axiom or to a proposition whose number is exponent of one of the above factors etc. We do not develop all of the potentialities of Gödel’s numbering, and we alluded to it in the questions raised by Detlefsen.
 51 ^{ }The rest of this chapter is essentially a translation of (J. Cavaillès, op. cit., p. 147151).
118We write, following Cavaillès:51
R(x_{1} ···x_{n}) ⊃ Démonstrabil r(Nx_{1 }···Nx_{n})
∼ R(x_{1} ···x_{n}) ⊃ Démonstrabil deNeg r(Nx_{1 }···Nx_{n})
119The property Démonstrabil: is a property of the number r which is one of the relations of the metalanguage defined above as a recursive arithmetical relation, that is to say expressible in the language. We then set the relation “x is not a proof for the proposition y to a variable when we make it equal to the number of the number y”. In short
∼ xDy(Ny):
120It is a recursive relationship between the numbers x and y. It involves for itself or its negation the demonstrability in the system of a proposition (in signs of the system) r(Nx;Ny). Let p be the generalization of r with respect to the first variable. if we substitute p for y Gödel’s theorem gives both intuitive implications.
∼ xDp(N p) ⊃ Démonstrabil de r(N x, N p).∗
xDp(N p) ⊃Démonstrabil de r(N x, N p).
121If we had a proof x for the generalization of r(Np) with respect to the first variable, i.e. p(Np), one would have at the same time in the system a proof of the negation of r(Np). The system would be contradictory. The noncontradictionof the system entails the impossibility of proving p(Np).
122The proposition p(Np) has for meaning the assertion of its own undemonstrabilit (there is no proof for proposition number p, when we take the variable equal to the number of this proposition). It is intuitively true. Cavaillès adds in note: since for all x
∼ xDp(Np)
123the implication (*) gives for all x (MP)
Démonstrabil de r (Nx,NP)
124no example can refute p(Np).
125If we represent the noncontradiction of the theory by
(x) ∼ xD(0 ≠ 0)
126(there is no proof for 0), we can write now the implication, which is now formal:
(x) ∼ xD(0 ≠ 0) → (x) ∼ xDp(Np) ∗ ∗.
127and we assume all the abbreviation signs used here which represent the notion of syntax, replaced by the signs of the theory which translate them. But then the second member becomes after the generalization of r(Nx, Np) with respectto the first variable, i.e. p(Np): if there was in the theory a formal proof of its noncontradiction, the implication would ** allow us to derive a proof of p(Np), which is impossible.
128The reasoning applies to any system

whose class of axioms can be defined by induction (as soon as we replace the signs by numbers).

in which any recurrent relation is expressible in the system.
129This is true 1) of any formalism large enough to contain arithmetic and 2) provided with a finite numberof axioms. (e.g. ZermeloFraenkel for set theory). We know that Gödel also introduces the property of 𝜔 noncontradiction for a system: the impossibility of demonstrating both a onevariable proposition (of type 2) for each numerical value of this variable and the negation of the generalization of this proposition.
130If we consider all the previous results, we must say that as r(Nx,Np) whose pNp is the generalization is provable for any value of x the negation, Neg p(Np) must not be demonstrable if the system is non 𝜔contradictory: p(Np) is therefore impossible to decide in the system. A system of axioms satisfying all the conditions 1), 2) and being 𝜔noncontradictory must therefore necessarily unsaturated. We can take, concludes Cavaillès as a proposition impossible to decide the affirmation of its noncontradiction.
 52 ^{ }J. Cavaillès, Méthodes axiomatiques et formalisme, op. cit., p. 150.
131What is the reason for this result? This is because “the formation of higher and higher types continues in the transfinite, while there is at most one countable infinity in each system”52 cited by Gödel. In a proposition the variables always have a determined type, belonging to the system, a proposition relating to all types (or stating that a relation is true for the variables of all types –therefore of type immediately superior to them, is part of the syntax and not of the system. The property “impossible to prove” is not definable. One must have encountered a proposition whose demonstrability involves contradiction, hence Gödel’s choice of the proposition p(Np) to reach the unsaturation.
132Cavailllès explains that there is an essential gap between the complete formalism and the relations it is in charge of expressing. We save the situation by introducing implicit relations by applying the rules of use. These relationships do not appear in the formalism. And here Cavaillès points out that Gödel has resuscitated the Liar paradox (as we remarked above). The paradox is produced in relation exclusively to saturation.
11. Gödel’s position, Hilbert’s position
133Gödel did not prejudice Hilbert’s point of view.
 53 ^{ }K. Gödel, op. cit. p. 197, cité par Cavaillès, op. cit., p. 153.
Let it be expressly noted that the [previous] theorem (and the corresponding results) are in no way at odds with Hilbert’s formalist point of view. For this only supposes the existence of a demonstration of noncontradiction carried out with finite means and it would be conceivable that there are finite demonstrations which cannot be formalized in P [the Principia system] or analogous systems satisfying conditions 1 and 2.53
134And, adds Cavaillès, the théorème only gives a negative criterion against the combinatorial methods used until then. But how can the notion of finite reasoning be extended? Herbrand completes in anticipation by answering this question, those raised by Mic Detlefsen.
135We are quoting only part of Herbrand’s proposition.
We never affirm the existence of an object without giving the means of constructing it … and when we say that a reasoning is true of all x this means that for each x taken in particular it it is possible to repeat the general reasoning in question.
 54 ^{ }J. Cavaillès, Méthodes axiomatiques et formalisme, op. cit., p. 153.
136In this regard, Cavaillès emphasizes that “we are moving from intuitive mathematics to intuitionist mathematics”.54
137He recalls that Hilbert admitted this kinship (between metamathematics and intuitionism) which Brouwer attempted to clarify. In a note Cavaillès states the points of agreement. I keep one.
Distinction between the formal construction of mathematics and the intuitive theory of this construction –with the recognition that for this theory the intuitionist mathematics of the set of integers is indispensable.
138We know that Gödel on the one hand and Bernays and Gentzen, on the other hand, achieved a translation of classical arithmetic into intuitionist arithmetic (formalized by Heyting). The solutions by introducing a new rule, proposed by Hilbert do not work. If proof theory is in bad position, the demonstrations of noncontradiction are apparently better off. The fact remains that the notion of finite reasoning must be broadened. Herbrand had proposed a solution. But then there is no more means of embracing all the steps with glance. We move on to intuitionist mathematics with which Hilbert admits the kinship of metamathematics.
139If we return to Gentzen’s result, we can develop the possibility of a direct translation in intuitionist mathematics …this translation cannot provide a demonstration of noncontradiction.
 55 ^{ }Ibid., p. 157.
On the one hand there is no possible extension to the analysis, and on the other hand for number theory the guarantee of intuitionist evidence seems insufficient (according to the Hilbert point of view).55
140Cavaillès reports and comments on the work of Gentzen who defines a constructivism in terms similar to those of Herbrand. We consider regulated means of always generating new individuals in a system: it is characterized by these construction methods. He uses the sequence of integers. It gives the metamathematics processes sufficient power and safety. Gentzen describes this method.
 56 ^{ }Ibid., p. 158 sqq.
141The proof of its validity is long and interesting. He proceeds to what he calls reductions, well explained by Cavaillès.56 The method is based on the reduction operations. Reduction operations are, as Cavaillès says, a sort of dismantling of the logical architecture of propositions.
142If we complete the indications of Cavaillèss, Gentzen’s theorem says that for any demonstration the reduction operation to be performed immediately is determined by its structure. Gentzen deals with an interesting difficulty which requires the evaluation of the complication of a demonstration. It is evaluated by means of the notion of degree linked with the number of logical signs appearing in the initial sequences. With certain restrictions one can formalize in arithmetic all the preceding reasonings, including the final induction. When the axiom is taken in all its generality, the transfinite is incorporated into the reasoning.
143Let us add that the method does not require that the examined formalism be closed. The transformation of mathematics into fully formal systems by the addition of the ideal transfinite symbols only made sense as long as it allowed a concrete metamathematical processing of these systems they use through the decision process. But, underlines Cavaillès, the process is only applicable to saturated systems (cf. Gödel’s result).
144Metamathematics as Hilbert had defined it and which was to provide its true aspect to the development of mathematics appears without an object. So, we need, as Detlefsen invites, to resituate the scope of Hilbert’s formalist positions, but it will be a modified formalism which makes it possible to construct and in a particularly trenchant way the analyzes of Cavaillès.
145More generally we think that the philosophy of Cavaillès must help us to situate what happens to the Hilbert’s Program, precisely in its philosophical scope.
 57 ^{ }Ibid., p. 171.
However, there remain, not in the radical formalism but in Hilbert’s own analyzes, two themes which, freed from their link with the rest of the doctrine, are not affected by the consequences of Gödel’s theorem and give the classical system in the face of the intuitionist construction an independent meaning: on the one hand the theory of generalization and of the axiomatic method, on the other hand the theory of the sign, the first justifying its own fertility, the second the objective scope of the system.57
146Cavaillès recalls the triple role that the generalization plays.
 58 ^{ }Ibid.
[…] liberation of operations from extrinsic conditions to their accomplishment, dissociation or identification of processes accidentally united or distinguished, finally position of new objects as correlate of operations recognized as autonomous. In all cases, the fruitfulness of effective labor is obtained by these ruptures in the mathematical fabric, this dialectical passage from a theory bearing in itself its limits to a higher theories which ignores it although and because it proceeds from it.58
147I will come back to the question of objects after this quick trip through the arguments, relying on the analyzes of Cavaillès.
The problem is insoluble if we keep the uncritical ontology implicitly assumed in most discussions.
148Having rejected the common Platonism, Cavaillès expresses himself thus. The objects remain linked to a prolonged sensible intuition.
There is no definition and justification of mathematical objects which is not mathematics itself. That is to say, as Brouwer did, unfolding of their history from the dyad with this difference, on the one hand that the unfolding is unique, while for Brouwer there is, it seems, an arbitrariness of creations, and on the other hand that it is not located in a region of consciousness, characterized by an intuition sui generis (which gives their validity to creations).
149And it is then that the most wellknown concepts of Cavaillès can intervene, in this question of objects.
 59 ^{ }Ibid., p. 176177.
The intuition in question here is only the extension of the real sensitive intuition not fixed in the first stages of a fragmentary consciousness: the widening of consciousness and the dialectic development of consciousness coincide. They give rise to the indefinite generation of objects in what we will call the thematic field: we have seen some of these processes of generation, the different kinds of generalizations, the formalizations to which are added the thematizations themselves: transformation of an operation as an element of a higher operating field, example of topology of topological transformations (essential of a general way in group theory. Three kinds of dialectical moments … in reality each incomparable to the others, in originality of the mathematical situation in which it arises.59
150And Cavaillès refers here to Lautman.
151We asked the question of the nature of the production of objects in mathematics, and I went through a rehabilitation of Hilbert’s Program opened by Mic Detlefsen. We were able to detect their indications of analysis of the generation of objects which goes beyond the attempt to resituate Hilbert’s theory.
 60 ^{ }Ibid., p. 178.
 61 ^{ }Ibid., p. 178.
 62 ^{ }J.J. Szczeciniarz, “Cavaillès, Descartes ou Spinoza”, in Pour Cavaillès, Renou (ed.), Atelier mat (...)
152Let us add a few last and too brief details, still in line with Cavailès. “The need for the generation of an object can only be grasped through the observation of success. The existence of a thematic field has meaning only as a correlate of a effective act” and quite generally in an analysis that we are continuing: “the duality ‘objectprocess of action on it’ is the mask of the dialectical going beyond one method by another, the objects posed independently of the second bein the correlates of the first”.60 We will insist on the new relation to objects pronounced by the analyzes of Cavaillès and through which a broader meaning can be attributed to that of Detlefsen and Hilbert. The necessity of the generation of an object, he says, is ever graspable only through the constatation of a success: existence in the thematic field has meaning only as a correlate of an effective act. And Cavaillès takes up the case of real numbers according to Fraenkel. We assume the existence of the whole body and “for it the possibility of performing the operations of classical analysis is the only criterion”. Let us continue following this analysis: if we have a central intuition which directs the variations of the methods and which constitutes the deep unit of a theory, it is “this time graspable in the action”. Examples are not lacking: the Argian calculation in elementary projective geometry, the diagonal method or linearization in Cantor’s theory etc.61 Cavaillès speaks of a modified formalism as a response to logicism and intuitionism. He understands as an element of this modification, the fact that the sensible, immediate concrete consciousness is not abandoned: “it is not leaving it to act on it (any abstract object, obtained for example, by thematization is a gesture on a gesture … a gesture on the primitive sensation)”.62 And here is deployed the philosophical position of Cavaillès: “the thematic field is not located outside the world but is a transformation of it: the effective thought of things is thought of its objects”. It is then that the notion of experience is renewed. For the logicist it is the discourse on the triangle which makes the mathematics.
 63 ^{ }J. Cavaillès, Méthodes axiomatiques et formalisme, op. cit., p. 179.
But discourse is only one particular aspect of the general becoming of consciousness… It is symbolic accompaniment, like any staking out by consciousness of the stages of its action on things, must not be isolated from them, it participates in best cases (systematized language) to the correlative extension of experience.63
 64 ^{ }M. Caveing, Le problème des objets dans la pensée mathématique, op. cit., p. 277.
153This is the effect Mic Detlefsen underlined in his last texts. Mathematics is the creation of the thought of a being “in situation” in the world. But its objectivity is not founded in the empiricism, nor in the being of “objects” whatever their nature, but in the a priori conditions of the relation of a concrete subject to the world.64 Hilbert’s Program can be interpreted in this direction.
Notes
1 ^{ }M. Caveing, Le problème des objets dans la pensée mathématique, Paris, Vrin, 2004.
2 ^{ }Le théorème de Gödel, (E. Nagel et al., eds), Paris, Seuil, 1989, p. 153.
3 ^{ }The Fall of the House of Usher by E. A. Poe, transl. in French by C. Baudelaire.
4 ^{ }It is the topic which he proposed during his stay in France, and he developed it in many directions.
5 ^{ }M. Detlefsen, Hilbert’s Program. An Essay on Mathematical Instrumentalism, Dordrecht/Boston/Lancaster/Tokyo, Reidel, 1986, p. 157.
6 ^{ }C. Smorynski, “The incompleteness theorems”, in Handbook of Mathematical Logic, Amsterdam, 1977 edited by J. Barwise, North Holland, p. 821865, p. 825.
7 ^{ }An argument is sound if it is both valid and all of its premises are actually true.
8 ^{ }See also A. Mostowski, Thirty Years of Foundational Studies, Basi Blackwell Oxford, 1966.
9 ^{ }M. Detlefsen, Hilbert’s Program…, op. cit.
10 ^{ }Ibid., p. 162 sq.
11 ^{ }Ibid., p. 26 sq.
12 ^{ }Ibid., p. 163 sq.
13 ^{ }G. Kreisel, “Hilbert’s Programme”, in P. Benacerraf and H. Putnam (eds.), Philosophy of Mathematics, Selected Readings, PrenticeHall, Englewood Cli, 1964, p. 157180.
14 ^{ }M. Detlefsen, Hilbert’s Program…, op. cit., p. 166.
15 ^{ }Ibid., p. 167.
16 ^{ }Ibid., p. 168.
17 ^{ }See as a survey. Gödel, K. “On formally Undecidable Propositions of Principia Mathematica and Related Systems”, in Van Heijenoort (ed.), From Frege to Gödel, 1931, p. 592617.
18 ^{ }G. Kreisel, “What Have We Learnt from Hilbert’s Second Problem”, AMS Proceedings of Symposium in Pure Mathematics vol. 28, American Mathematical Society, Providence, 1976, p. 111112.
19 ^{ }M. Detlefsen, Hilbert’s Program…, op. cit., p. 77.
20 ^{ }Ibid., p. 84.
21 ^{ }Ibid.
22 ^{ }Ibid., p. 82.
23 ^{ }Ibid., p. 84.
24 ^{ }Ibid., p. 86.
25 ^{ }Ibid., p. 89.
26 ^{ }Ibid.
27 ^{ }Ibid., p. 94 sq.
28 ^{ }See also S. Feferman, “The Arithmetization of Metamathematics in a General Setting”, Fundamenta Mathematicae, n^{o} 49, 1960, p. 3592.
29 ^{ }M. Detlefsen, Hilbert’s Program…, op. cit., p. 97 sqq.
30 ^{ }Ibid., p. 98.
31 ^{ }Ibid., p. 96.
32 ^{ }Ibid., p. 107.
33 ^{ }Ibid., p. 129.
34 ^{ }The dialogue with Dag Prawitz was important for Mic. He invited him as keynote speaker at the inauguration of the chair of excellence in Paris.
35 ^{ }D. Prawitz, “Philosophical aspects of proof theory”, in Contemporary Philosophy. A New Survey vol. 1, The Hague, Martinus Nijhof, 1981.
36 ^{ }D. Hilbert, 1927, “The Founadations of Mathematics”, in J. van Heijenoort (ed.), From Frege to Gödel, Cambridge (Mass.), Harvard Univ. Press, 1981 (1967), p. 464479, p. 471 op. cit. by Mic p. 124 HP.
37 ^{ }M. Detlefsen, Hilbert’s Program…, op. cit., p. 126.
38 ^{ }Ibid., p. 127.
39 ^{ }Ibid., p. 127 sq.
40 ^{ }Ibid., p. 142.
41 ^{ }For the synthese see M. Detlefsen. “On an alleged refutation of Hilbert Program”, in Proof, Logic and Formalization, Detlefsen (ed.), London and New York, Routledge, 1992, p. 199235.
42 ^{ }K. Gödel, “Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme”, Monatsh. f. Math. u. Physik, t. 38 p. 173198, quoted in J. Cavaillès, Méthodes axiomatiques et formalisme, Hermann, 1981, p. 150.
43 ^{ }J. Cavaillès, Méthodes axiomatiques et formalisme, op. cit., p. 150.
44 ^{ }J.Y. Girard, Le point aveugle, I Cours de Logique, Vers la perfection Hermann, 2006, p. 18.
45 ^{ }J. Cavaillès, Méthodes axiomatiques et formalisme, op. cit., p. 151 sq.
46 ^{ }Ibid., p. 125 sqq.
47 ^{ }Ibid., p. 122.
48 ^{ }Ibid., p. 123 sq.
49 ^{ }Ibid., p. 124.
50 ^{ }Ibid., p. 144.
51 ^{ }The rest of this chapter is essentially a translation of (J. Cavaillès, op. cit., p. 147151).
52 ^{ }J. Cavaillès, Méthodes axiomatiques et formalisme, op. cit., p. 150.
53 ^{ }K. Gödel, op. cit. p. 197, cité par Cavaillès, op. cit., p. 153.
54 ^{ }J. Cavaillès, Méthodes axiomatiques et formalisme, op. cit., p. 153.
55 ^{ }Ibid., p. 157.
56 ^{ }Ibid., p. 158 sqq.
57 ^{ }Ibid., p. 171.
58 ^{ }Ibid.
59 ^{ }Ibid., p. 176177.
60 ^{ }Ibid., p. 178.
61 ^{ }Ibid., p. 178.
62 ^{ }J.J. Szczeciniarz, “Cavaillès, Descartes ou Spinoza”, in Pour Cavaillès, Renou (ed.), Atelier mathématique, Pont.
63 ^{ }J. Cavaillès, Méthodes axiomatiques et formalisme, op. cit., p. 179.
64 ^{ }M. Caveing, Le problème des objets dans la pensée mathématique, op. cit., p. 277.
Haut de pagePour citer cet article
Référence papier
JeanJacques Szczeciniarz, « Mic Detlefsen, Hilbert’s Program », Noesis, 38  2022, 4574.
Référence électronique
JeanJacques Szczeciniarz, « Mic Detlefsen, Hilbert’s Program », Noesis [En ligne], 38  2022, mis en ligne le 01 juin 2024, consulté le 31 octobre 2024. URL : http://journals.openedition.org/noesis/6938 ; DOI : https://doi.org/10.4000/11xm7
Haut de pageDroits d’auteur
Le texte et les autres éléments (illustrations, fichiers annexes importés), sont « Tous droits réservés », sauf mention contraire.
Haut de page