%%%%%%%%%%%%%%% Tekst glowny \documentstyle[12pt]{article} \oddsidemargin -2mm \evensidemargin 6mm \marginparwidth 0pt \marginparsep 0pt \topmargin 0mm \headheight 0pt \headsep 0pt \topskip 0pt \footheight 0pt %\footskip 0pt \textheight 235mm \textwidth 152mm %\renewcommand{\baselinestretch}{1.2} \newcommand{\m}{mathematics} \newcommand{\ma}{mathematical} \newcommand{\ph}{philosophy} \newcommand{\pha}{philosophical} \newcommand{\kr}[1]{\overline{#1}} \newcommand{\N}{{\bf N}} \newcommand{\g}[1]{\ulcorner {#1} \urcorner} \newtheorem{thm}{Theorem} \newtheorem{defin}[thm]{Definition} \newtheorem{cor}[thm]{Corollary} \input amssym11.def \input amssym \title{On the distinction proof--truth in mathematics\footnote{This text is the invited lecture presented at the 11th International Congress of Logic, Methodology and Philosophy of Science held in Cracow (Poland), 20--26 August 1999. An abbreviated version of it will appear in the volume of proceedings of the Congress (to be published by Kluwer Academic Publishers in the Synthese Library Series).}} \begin{document} \author{Roman Murawski\\ {\small Adam Mickiewicz University}\\ {\small Faculty of Mathematics and Comp. Sci.}\\ {\small ul. Matejki 48/49}\\ {\small 60--769 Pozna\'n, Poland}\\ {\small E-mail: {\tt rmur@math.amu.edu.pl}}} \date{} \maketitle \begin{abstract} The paper is devoted to some historical, philosophical and logical considerations connected with the distinction between proof and truth in mathematics. The crucial r\^{o}le of G\"odel's incompleteness theorems as well as of the undefinability of truth vs. definability of provability and the r\^{o}le of finitary vs. infinitary methods are stressed. The problem of the need of extending the available methods by new rules of inference and new axioms is also considered. \end{abstract} It is a truism that the basic aim of any science (and any scientist), and in particular of mathematics (and of a mathematician) is to establish truth and true knowledge (about mathematical world). Since Plato, Aristotle and Euclid the best method to justify and to organize mathematical knowledge was considered the axiomatic method. The first mature and most representative example of its usage in \m\ were {\it Elements} of Euclid. They established a pattern of a scientific theory and in particular a paradigm in \m. Since Euclid till the end of the nineteenth century mathematics was developed as an axiomatic (in fact rather a quasi-axiomatic) theory based on axioms and postulates. Proofs of theorems contained several gaps --- in fact the lists of axioms and postulates were not complete, one freely used in proofs various ``obvious'' truths or refered to the intuition. Consequently proofs were only partially based on axioms and postulates. In fact proofs were informal and intuitive, they were rather demonstrations and the very concept of a proof was of a psychological (and not of a logical) nature. Note that almost no attention was paid to the precization and specification of the language of theories --- in fact the language of the theories was simply the unprecise colloquial language. One should also note here that in fact till the end of the nineteenth century mathematicians were convinced that axioms and postulates should be simply true statements, hence sentences describing the real state of affairs (in the \ma\ reality). It seems to be connected with Aristotle's view that a proposition is demonstrated (proved to be true) by showing that it is a logical consequence of propositions already known to be true. Demonstration was conceived here of as a deduction whose premises are known to be true and a deduction was conceived of as a chaining of immediate inferences. Add that the Euclid's approach (connected with Platonic idealism) to the problem of the development of \m\ and the justification of its statements (which found its fulfilment in the Euclidean paradigm), i.e. justification by deduction (by proofs) from explicitly stated axioms and postulates, was not the only approach and method which was used in the ancient Greek (and later). The other one (call it heuristic) was connected with Democritean materialism. It was applied for example by Archimedes who used not only deduction but any methods, such as intuition or even experiments (not only mental ones), to solve problems. Though the Euclidean approach won and dominated in the history, one should note that it formed rather an ideal and not the real scientific practice of mathematicians. In fact rigorous, deductive \m\ was rather a rare phenomenon. On the contrary, intuition and heuristic reasoning were the animating forces of \ma\ research practice. The vigorous but rarely rigorous \ma\ activity produced ``crises'' (for example the pythagoreans' discovery of the incommensurability of the diagonal and side of a square, Leibniz's and Newton's problems with the explanation of the nature of infinitesimals, Fourier's ``proof'' that any function is representable in a Fourier series, antinomies connected with Cantor's imprecise and intuitive notion of a set). Basic concepts underlying the Euclidean paradigm have been clarified on the turn of the nineteenth century. In particular the intuitive (and rather psychological in nature) concept of an informal proof (demonstration) was replaced by a precise notion of a formal proof and of a consequence. Several events and achievements contributed to the revision of the Euclidean paradigm, in particular the origin and the development of set theory (G.~Cantor), arithmetization of analysis (A.~Cauchy and K.~Weierstrass, R.~Dedekind), axiomatization of the arithmetic of natural numbers (G.~Peano), non-Euclidean geometries (N.I.~Lobachewsky, J.Bolayi, C.F.~Gauss), axiomatization of geometry (M.~Pasch, D.~Hilbert), the development of mathematical logic (G.~Boole, A.~de Morgan, G.~Frege, B.~Russell). Beside those ``positive'' factors there was also a ``negative'' factor, viz., the discovery of paradoxes in set theory (C.~Burali-Forti, G.~Cantor, B.~Russell) and of semantical antinomies (G.D.~Berry, K.~Grelling). They forced the revision of some basic ideas and stimulated in particular metamathematical investigations. %\renewcommand{\baselinestretch}{1.2} One of the directions of those foundational investigations was the program of David Hilbert and his {\it Beweistheorie}. Note at the very beginning that ``this program was never intended as a comprehensive philosophy of mathematics; its purpose was instead to legitimate the entire corpus of \ma\ knowledge'' (cf. Rowe, 1989, p.~200). Note also that Hilbert's views were changing over the years, but always took a formalist direction. Hilbert sought to justify mathematical theories by means of formal systems, i.e., using the axiomatic method. He viewed the latter as holding the key to a systematic organization of any sufficiently developed subject. This idea was very well stated already in a letter of 29th December 1899 to G.~Frege where Hilbert explained his motives of axiomatizing the geometry and wrote (cf. Frege 1976, p.~67): \newpage \begin{quote} {\small Ich bin zu der Aufstellung meines Systems von Axiomen durch die Not gezwungen: ich wollte die M\"oglichkeit zum Verst\"andnis derjenigen geometrischen S\"atze geben, die ich f\"ur die wichtigsten Ergebnisse der geometrischen Forschungen halte: dass das Parallelenaxiom keine Folge der \"ubrigen Axiome ist, ebenso das Archimedische etc.\footnote{``I was forced to construct my systems of axioms by a necessity: I wanted to have a possibility to understand those geometrical propositions which in my opinion are the most important results of geometrical researches: that the Parallel Postulate is not a consequence of other axioms, and similarly for the Archimedean one, etc.''} } \end{quote} In ``Axiomatisches Denken'' (1918, p.~405) Hilbert wrote: \begin{quote} {\small Wenn wir die Tatsachen eines bestimmten mehr oder minder umfassenden Wissensgebiete zusammenstellen, so bemerken wir bald, da\ss\ diese Tatsachen einer Ordnung f\"ahig sind. Diese Ordnung erfolgt jedesmal mit Hilfe eines gewissen {\it Fachwerkes von Begriffen} in der Weise, da\ss\ dem einzelnen Gegenstande des Wissensgebietes ein Begriff dieses Fachwerkes und jeder Tatsache innerhalb des Wissensgebietes eine logische Beziehung zwischen den Begriffen entspricht. Das Fachwerk der Begriffe ist nicht Anderes als die {\it Theorie} des Wissensgebietes.\footnote{``When we put together the facts of a given more or less comprehensive field of our knowledge, then we notice soon that those facts can be ordered. This ordering is always introduced with the help of a certain {\it network of concepts} in such a way that to every object of the given field corresponds a concept of this network and to every fact within this field corresponds a logical relation between concepts. The network of concepts is nothing else than the {\it theory} of the field of knowledge.''} } \end{quote} By Hilbert the formal frames were contentually motivated. First-order theories were viewed by him together with suitable non-empty domains, {\it Bereiche}, which indicated the range of the individual variables of the theory and the interpretations of the nonlogical vocabulary. But Hilbert, as a mathematician, was not interested in establishing precisely the ontological status of mathematical objects. Moreover, one can say that his program was calling on people to turn their mathematical and philosophical attention away from the problem of the object of mathematical theories and turn it toward a critical examination of the methods and assertions of theories. On the other hand he was aware that once a formal theory has been constructed, it can admit various interpretations. Recall here his famous sentence from a letter to G.~Frege quoted already above: \begin{quote} {\small Ja, es ist doch selbsverst\"andlich eine jede Theorie nur ein Fachwerk oder Schema von Begriffen nebst ihren nothwendigen Beziehungen zu einander, und die Grundelemente k\"onnen in beliebiger Weise gedacht werden. Wenn ich unter meinen Punkten irgendwelche Systeme von Dingen, z.B. das System: Liebe, Gesetz, Schornsteinfeger \ldots, denke und dann nur meine s\"amtlichen Axiome als Beziehungen zwischen diesen Dingen annehme, so gelten meine S\"atze, z.B. der Pythagoras auch von diesen Dingen. Mit anderen Worten: eine jede Theorie kann stets auf unendliche viele Systeme von Grundelementen angewandt werden.\footnote{``Yes, it is evident that one can treat any such theory only as a network or schema of concepts besides their necessary interrelations, and to think of basic elements as being any objects. If I think of my points as being any system of objects, for example the system: love, law, chimney-sweep \ldots, and I treat my axioms as [expressing] interconnections between those objects, then my theorems, e.g. the theorem of Pythagoras, hold also for those things. In other words: any such theory can always be applied to infinitely many systems of basic elements.''} } \end{quote} The essence of the axiomatic study of mathematical truths was for him to clarify the position of a given theorem (truth) within the given axiomatic system and the logical interconnections between propositions.\footnote{He wrote in (1902/03, p.~50): ``Unter der axiomatischen Erforschung einer mathematischen Wahrheit verstehe ich eine Untersuchung, welche nicht dahin zieht, im Zusammenhange mit jener Wahrheit neue oder allgemeinere S\"atze zu entdecken, sondern die vielmehr die Stellung jenes Satzes innerhalb des Systems der bekannten Wahrheiten und ihren logischen Zusammenhang in der Weise klarzulegen sucht, dass sich sicher angeben l\"asst, welche Voraussetzungen zur Begr\"undung jener Wahrheit notwendig und hinreichend sind. (Under the axiomatic study of any mathematical truth I understand a study whose aim is not to discover new or more general propositions with the help of given truths, but a study whose purpose is to determine a position of a given theorem within the system of known truths and their logical connections in such a way that one can clearly see which assumptions are necessary and sufficient to justify the considered truth.)} Hilbert sought to secure the validity of mathematical knowledge by syntactical considerations without appeal to semantic ones. The basis of his approach was the distinction between the unproblematic, `finitistic' part of mathematics and the `infinitistic' part that needed justification. Finitistic \m\ deals with so called real propositions, which are completely meaningful because they refer only to given concrete objects. Infinitistic \m\ on the other hand deals with so called ideal propositions that contain reference to infinite totalities. Hilbert proposed to base \m\ on finitistic \m\ via proof theory ({\it Beweistheorie\/}). The latter was planned as a new mathematical discipline in which one studies mathematical proofs by mathematical methods. Its main goal was to show that proofs which use ideal elements (in particular actual infinity) in order to prove results in the real part of \m\ always yield correct results. One can distinguish here two aspects: consistency problem and conservation problem. The consistency problem consists in showing (by finitistic methods, of course) that the infinitistic \m\ is consistent; the conservation problem consists in showing by finitistic methods that any real sentence which can be proved in the infinitistic part of \m\ can be proved also in the finitistic part. One should stress here the emphasis on consistency (instead of correctness). To realize this program one should formalize mathematical theories (even the whole of mathematics) and then study them as systems of symbols governed by specified and fixed combinatorial rules. The advantage of this approach was the fact that references to ideal objects were replaced by reasonings of a purely finitary character, reasonings applied not to mathematical entities themselves but to the symbols of a formal language in which the concepts had been axiomatized, i.e., by syntactical considerations without appeal to the semantic ones. Another advantage was the fact that, as P.~Bernays put it, ``the problems and difficulties that present themselves in the foundations of \m\ can be transferred from the epistemological-philosophical to the properly mathematical domain''. The formal axiomatic system should satisfy three conditions: it should be complete, consistent and based on independent axioms. The consistency of a given system was the criterion for mathematical truth and for the very existence of mathematical objects.\footnote{Cf. Hilbert's letter to G.~Frege of 29th December 1899 where he claimed that: ,,Wenn sich die willk\"urlich gesetzten Axiome nicht einander widersprechen mit s\"amtlichen Folgen, so sind sie wahr, so existieren die durch die Axiome definierten Dinge'' (If the arbitrary given axioms do not contradict one another with all their consequences, then they are true and the things defined by the axioms exist) (Frege, 1976, p.~66).} It was also presumed that any consistent theory would be categorical, that is, would (up to isomorphism) characterize a unique domain of objects. This demand was connected with the completeness. The meaning and understanding of completeness by Hilbert plays a crucial r\^{o}le from the point of view of our subject. Note at the beginning that in the {\it Grundlagen der Geometrie} completeness was postulated as one of the axioms (the axiom was not present in the first edition, but was included first in the French translation and then in the second edition of 1903). In fact the axiom V(2) stated that it is not possible to extend the system of points, lines and planes by adding new entities so that the other axioms are still satisfied. In Hilbert's lecture at the Congress at Heidelberg in 1904 (cf. 1905a) one finds such an axiom for the real numbers. Later there appears completeness as a property of a system. In lectures ``Logische Principien des mathematischen Denkens'' (1905, p.~13) Hilbert explains the demand of the completeness as the demand that the axioms suffice to prove all ``facts'' of the theory in question. He says: ``wir werden verlangen m\"ussen, dass alle \"ubrigen Thatsachen des vorgelegten Wissensbereiches Folgerungen aus den Axiomen sind'' (We will have to demand that all other facts of the given field are consequences of the axioms). On the other hand one can say that Hilbert's early conviction as to the solvability of every mathematical problem --- expressed for example in his 1900 Paris lecture\footnote{``Diese \"Uberzeugung von der L\"osbarkeit eines jeden mathematischen Problems ist uns ein kr\"aftiger Ansporn w\"ahrend der Arbeit; wir h\"oren in uns den steten Zuruf: {\it Da ist das problem, suche die L\"osung. Du kannst sie durch reines Denken finden; denn in der Mathematik gibt es kein Ignorabimus!} (Hilbert, 1901, p.~298). (The conviction of the solvability of any mathematical problem is for us a strong motive in this work; we hear the whole time the call: {\it There is a problem, look for a solution. You can find it by a pure thinking; there is no Ignorabimus in the \m.)}} (cf. Hilbert 1901) and repeated in his opening address ``Naturerkennen und Logik'' (cf. Hilbert, 1930) before the Society of German Scientists and Physicians in K\"onigsberg in September 1930\footnote{``F\"ur den Mathematiker gibt es kein Ignorabimus, und meiner Meinung nach auch f\"ur die Naturwissenschaft \"uberhaupt nicht. \ldots\ Der wahre Grund, warum es [niemand] nicht gelang, ein unl\"osbares Problem zu finden, besteht meiner Meinung nach darin, da\ss\ es ein unl\"osbares Problem \"uberhaupt nicht gibt. Statt des t\"orichten Ignorabimus hei\ss e im Gegenteil unsere Losung: Wir m\"ussen wissen, Wir werden wissen.'' (For the mathematician there is no Ignorabimus, and, in my opinion, not at all for natural science either. \ldots\ The true reason why [no one] has succeeded in finding an unsolvable problem is, in my opinion, that there is {\it no} unsolvable problem. In contrast to the foolish Ignorabimus, our credo avers: We must know, We shall know.)} --- can be treated as informal reflection of a belief in completeness. In his 1900 Paris lecture Hilbert spoke about completeness in the following words (see the second problem, pp.~299--300): %sense of categoricity. In the second problem he said: \begin{quote} {\small Wenn es sich darum handelt, die Grundlagen einer Wissenschaft zu untersuchen, so hat man ein System von Axiomen aufzustellen, welche eine genaue und vollst\"andige Beschreibung derjenigen Beziehungen enthalten, die zwischen den elementaren Begriffen jener Wissenschaft stattfinden. Die aufgestellten Axiome sind zugleich die Definitionen jener elementaren Begriffe, und jede Aussage innerhalb des Bereiches der Wissenschaft, deren Grundlage wir pr\"ufen, gilt uns nur dann als richtig, falls sie sich mittels einer endlichen Anzahl logischer Schl\"usse aus den aufgestellten Axiomen ableiten l\"a\ss t.\footnote{``When we are engaged in investigating the foundations of a science, we must set up a system of axioms which contains an exact and complete description of the relations subsisting between the elementary ideas of that science. The axioms so set up are at the same time the definitions of those elementary ideas; and no statement within the realm of the science whose foundations we are testing is held to be correct unless it can be derived from those axioms by means of a finite number of logical steps.''} } \end{quote} One can take the ``exact and complete description'' to be complete enough to decide the truth or falsity of every statement. Semantically such completeness follows from categoricity, i.e., from the fact that any two models of a given axiomatic system are isomorphic; syntactically it means that every sentence or its negation is derivable from the given axioms. Hilbert's own axiomatizations were complete in the sense of being categorical. But notice that they were not first-order, indeed his axiomatization of geometry from {\it Grundlagen} as well as his axiomatization of arithmetic published in 1900 were second-order.\footnote{Each of those system had a second-order Archimedean axiom and both had a ``completeness axiom'' stating that the structure under consideration was maximal with respect to the remaining axioms. Note that this axiom was not even properly a second-order axiom.} The demand discussed here would imply that a system of axioms complete in this sense is possible only for sufficiently advanced theories. On the other hand Hilbert called for complete systems of axioms also for theories being developed.\footnote{In ``Mathematische Probleme'' (1901, p.~295) he wrote: ``\ldots\, wo immer von erkenntnistheoretischer Seite oder in der Geometrie oder aus den Theorien der Naturwissenschaft mathematische Begriffe auftauchen, erw\"achst der Mathematik die Aufgabe, die diesen Begriffen zugrunde liegenden Prinzipien zu erforschen und dieselben durch einfaches und vollst\"andiges System von Axiomen \ldots\, festzulegen''. (\ldots\, wherever mathematical concepts emerge from epistemological considerations or from geometry or from theories of science, \m\ aquires the task of investigating the principles lying at the basis of these concepts and defining \ldots\, these through a simple and complete system of axioms.)} One should also add here that Hilbert admitted the possibility that a mathematical problem may have a negative solution, i.e., that one can show the impossibility of a positive solution on the basis of a considered axiom system.\footnote{In ``Mathematische Probleme'' he wrote: ``Mitunter kommt es vor, da\ss\ wir die Beantwortung unter ungen\"ugenden Voraussetzungen oder in unrichtigem Sinne erstreben und infolgedessen nicht zum Ziele gelangen. Es entsteht dann die Aufgabe, die Unm\"oglichkeit der L\"osung des Problems unter den gegebenen Voraussetzungen und in dem verlangten Sinne nachzuweisen. \ldots\ alte schwierige Probleme \ldots\ eine v\"ollig befriedigende und strenge L\"osung gefunden haben. Diese merkw\"urdige tatsache neben anderen philosophischen Gr\"unden ist es wohl, welche in uns eine \"uberzeugung entstehen l\"asst \ldots\ da\ss\ ein jedes bestimmte mathematische Problem einer strengen Erledigung notwendig f\"ahig sein m\"usse, sei es, da\ss\ es gelingt die Beantwortung der gestellten Frage zu geben, sei es, da\ss\ die Unm\"oglichkeit seiner L\"osung and damit die Notwendigkeit des Mi\ss lingens aller Versuche dargetan wird.'' (p.~297). (Occasionally it happens that we seek the solution under insufficient hypotheses or in an incorrect sense, and for this reason we do not succeed. The problem then arises: to show the impossibility of the solution under the given hypotheses, or in the sense contemplated \ldots\, and we perceive that old and difficult problems \ldots\, have finally found fully satisfactory and rigorous solutions, although in another sense than that originally intended. It is probably {\it this} important fact along with other philosophical reasons that give rise to the conviction \ldots\, that every definite mathematical problem must necessarily be susceptible of an exact settlement, either in the form of an actual answer to the question asked, or by a proof of the impossibility of its solution and therewith the necessary failure of all attempts.} In Hilbert's lectures from 1917--18 (cf. Hilbert, 1917--18) one finds completeness in the sense of maximal consistency, i.e., a system is complete if and only if for any non-derivable sentence, if it is added to the system then the system becomes inconsistent.\footnote{``Wenden wir uns nun zu der Frage der {\it Vollst\"andigkeit}. Wir wollen das vorgelegte Axiomen-System vollst\"andig nennen, falls durch die Hinzuf\"ugung einer bisher nicht ableitbaren Formel zu dem System der Grundformeln stets ein widerspruchsvolles Axiomensystem entsteht'' (Hilbert, 1917--18, 152). (Let us now turn to the question of {\it completeness}. We want to call the system of axioms under consideration complete if we always obtain an inconsistent system of axioms by adding a formula which is so far not derivable to the system of basic formulas.)} In his lecture at the International Congress of Mathematicians in Bologna in 1928 Hilbert stated two problems of completeness, one for the first-order predicate calculus (completeness with respect to validity in all interpretations, hence the semantic completeness) and the second for a system of elementary number theory (formal completeness, in the sense of maximal consistency, i.e. Post-completeness, hence the syntactical completeness) (cf. Hilbert, 1930). The emphasis on the finitary and syntactical methods together with the demand of (and belief in) the completeness of formal systems seems to be by Hilbert the source and reason of the fact that, as G\"odel put it (cf. Wang, 1974, p.~9), ``\ldots\, formalists considered formal demonstrability to be an {\it analysis\/} of the concept of mathematical truth and, therefore were of course not in a position to {\it distinguish\/} the two''. Indeed, the informal concept of truth was not commonly accepted as a definite mathematical notion at that time. As G\"odel wrote in a crossed-out passage of a draft of his reply to a letter of the student Yossef Balas: ``\ldots\, a concept of objective mathematical truth as opposed to demonstrability was viewed with greatest suspicion and widely rejected as meaningless'' (cf. Wang 1987, 84--85).\footnote{Compare this with the following comment of R.~Carnap. When he invited A.~Tarski to speak on the concept of truth at the September 1935 International Congress for Scientific Philosophy, ``Tarski was very sceptical. He thought that most philosophers, even those working in modern logic, would be not only indifferent, but hostile to the explication of the concept of truth''. And indeed at the Congress ``\ldots\, there was vehement opposition even on the side of our philosophical friends'' (cf. Carnap, 1963, 61--62).} Therefore Hilbert prefered to deal in his metamathematics solely with the forms of the formulas, using only finitary reasoning which were considered to be save --- contrary to semantical reasonings which were non-finitary and consequently not save. Non-finitary reasonings in \m\ were considered to be meaningful only to the extent to which they could be interpreted or justified in terms of finitary meta\m.\footnote{Cf. G\"odel's letter to Hao Wang dated 7th December 1967 --- see Wang 1974, p.~8.} On the other hand there was no clear distinction between syntax and semantics at that time. Recall for example that, as indicated earlier, the axiom systems came by Hilbert often with a built-in interpretation. Add also that the very notions necessary to formulate properly the difference syntax--semantics were not available to Hilbert. \vspace{10mm} %\newpage The problem of the completeness of the first-order logic, i.e., the fourth problem of Hilbert's Bologna lecture, was also posed as a question in the book by Hilbert and Ackermann {\it Grundz\"uge der theoretischen Logik} (1928). It was solved by Kurt G\"odel in his doctoral dissertation (1929, cf. also 1930) where he showed that the first-order logic is complete, i.e., every true statement can be derived from the axioms. Moreover he proved that, in the first-order logic, every consistent axiom system has a model. More exactly G\"odel wrote that by completeness he meant that ``every valid formula expressible in the restricted functional calculus \ldots\, can be derived from the axioms by means of a finite sequence of formal inferences''. And added that this is equivalent to the assertion that ``Every consistent axiom system [formalized within that restricted calculus] \ldots\, has a realization'' and to the statement that ``Every logical expression is either satisfiable or refutable'' (this is the form in which he actually proved the result). The importance of this result is, according to G\"odel, that it justifies the ``usual method of proving consistency''. In fact the completeness theorem shows in a sense an equivalence of truth and demonstrability, an equivalence of semantical and syntactical approach. It shows that the logical methods admitted by the notion of derivability are appropriate and sufficient. One should notice here that the notion of truth in a structure, central to the very definition of satisfiability or validity, was nowhere analyzed in either G\"odel's dissertation or his published revision of it. There was in fact a long tradition of use of the informal notion of satisfiability (compare the work of L\"owenheim, Skolem and others). Some months later, in 1930, G\"odel solved three other problems posed by Hilbert in Bologna by showing that arithmetic of natural numbers and all richer theories are essentially incomplete (provided they are consistent) (cf. G\"odel, 1931). It is interesting to see how did G\"odel arrived at this result. Hao Wang, on the basis of his discussions with G\"odel, reports this in the following way (see 1981): \begin{quote} {\small [G\"odel] represented real numbers by formulas \ldots\, of number theory and found he had to use the concept of truth for sentences in number theory in order to verify the comprehension axiom for analysis. He quickly ran into the paradoxes (in particular, the Liar and Richard's) connected with truth and definability. He realized that truth in number theory cannot be defined in number theory and therefore his plan \ldots\ did not work. } \end{quote} G\"odel himself wrote on his discovery in a draft reply to letter dated 27th May 1970 from Yossef Balas, then a student at the University of Northern Iowa (cf. Wang, 1987, 84--85). G\"odel indicated there that it was precisely his recognition of the contrast between the formal definability of provability and the formal undefinability of truth that led him to his discovery of incompleteness. One finds also there the following statement: \begin{quote} {\small (\ldots) long before, I had found the {\it correct\/} solution of the semantic paradoxes in the fact that truth in a language cannot be defined in itself. } \end{quote} %\newpage %\nopagebreak[4] On the base of this quotation one can argue that %From this quotation one that G\"odel obtained the result on the undefinability of truth independently of A.~Tarski (cf. Tarski, 1933; German translation --- 1936, English translation --- 1956).\footnote{For the problem of the priority of proving the undefinability of truth see Wole\'nski (1991) and Murawski (1998).} Note also that G\"odel was convinced of the objectivity of the concept of mathematical truth. In a latter to Hao Wang (cf. Wang, 1974, 9) he wrote: \begin{quote} {\small I may add that my objectivist conception of \m\ and metamathematics in general, and of transfinite reasoning in particular, was fundamental also to my other work in logic. How indeed could one think of {\it expressing\/} metamathematics {\it in\/} the mathematical systems themselves, if the latter are considered to consist of meaningless symbols which acquire some substitute of meaning only {\it through\/} metamathematics \ldots\ it should be noted that the heuristic principle of my construction of undecidable number theoretical propositions in the formal systems of \m\ is the highly transfinite concept of `objective mathematical truth' as {\it opposed\/} to that of `demonstrability' (cf. M.~Davis, {\it The Undecidable\/}, New York 1965, p. 64 where I explain the heuristic argument by which I arrive at the incompleteness results), with which it was generally confused before my own and Tarski's work. } \end{quote} In this situation one should ask why G\"odel did not mention the undefinability of truth in his writings. In fact, G\"odel even avoided the terms ``true'' and ``truth'' as well as the very concept of being true (he used the term ``richtige Formel'' and not the term ``wahre Formel''). In the paper `\"Uber formal unentscheidbare S\"atze \ldots' (1931) the concept of a true formula occurs only at the end of Section 1 where G\"odel explains the main idea of the proof of the first incompleteness theorem (but again the term ``inhaltlich richtige Formel'' and not the term ``wahre Formel'' appears here). Indeed, talking about the construction of a formula which should express its own unprovability invokes the interpretation of the formal system. At the very end of the introductory section one finds the following remarks (see G\"odel, 1931, 175--176): \begin{quote} {\small Die eben auseinandergesetzte Beweismethode l\"a\ss t sich offenbar auf jedes formale System anwenden, das erstens inhaltlich gedeutet \"uber gen\"ugend Ausdrucksmittel verf\"ugt, um die in der obigen \"Uberlegung vorkommenden Begriffe (insbesondere den Begriff ``beweisbare Formel'') zu definieren, und in dem zweitens jede beweisbare Formel auch inhaltlich richtig ist. Die nun folgende exakte Durchf\"uhrung des obigen Beweises wird unter anderem die Aufgabe haben, die zweite der eben angef\"uhrten Voraussetzungen durch eine rein formale und weit schw\"achere zu ersetzen.\footnote{``The method of proof just explained can clearly be applied to any formal system that, first, when interpreted as representing a system of notions and propositions, has at its disposal sufficient means of expression to define the notions occurring in the argument above (in particular, the notion ``provable formula'') and in which, second, every provable formula is true in the interpretation considered. The purpose of carrying out the above proof with full precision in what follows is, among other things, to replace the second of the assumptions just mentioned by a purely formal and much weaker one.'' (English translation see G\"odel, {\it Collected Works}, vol.~I, 151) } } \end{quote} On the other hand the term ``truth'' occurred in G\"odel's lectures on the incompleteness theorems at the Institute for Advanced Study in Princeton in the spring of 1934.\footnote{Notes of G\"odel's lectures taken by S.C.~Kleene and J.B.~Rosser were published in Davis's book in 1965 (cf. G\"odel, 1934).} He discussed there, among other things, the relation between the existence of undecidable propositions and the possibility of defining the concept ``true (false) sentence'' of a given language in the language itself. Considering the relation of his arguments to the paradoxes, in particular to the paradox of ``The Liar'', G\"odel indicates that the paradox disappears when one notes that the notion ``false statement in a language $B$'' cannot be expressed in $B$. Even more, `the paradox can be considered as a proof that ``false statement in $B$'' cannot be expressed in $B$.' In the footnote 25 (added to the version published in Davis, 1965) G\"odel wrote: \begin{quote} {\small For a closer examination of this fact see A.~Tarski's papers published in: {\it Trav. Soc. Sci. Lettr. de Varsovie}, Cl. III, No. 34, 1933 (Polish) (translated in: {\it Logic, Semantics, Metamathematics. Papers from 1923 to 1938 by A.~Tarski}, see in particular p. 247 ff.) and in Philosophy and Phenom. Res. 4 (1944), p. 341--376. In these two papers the concept of truth relating to sentences of a language is discussed systematically. See also: R.~Carnap, {\it Mon. Hefte f. Math. u. Phys.} 4 (1934), p. 263. } \end{quote} The reasons for the incompleteness results were also explicitly mentioned in G\"odel's reply to a letter of A.W.~Burks. This reply is quoted in von Neumann's {\it Theory of Self-Reproducing Automata}, 1966, pp.~55--56. G\"odel wrote: \begin{quote} {\small I think the theorem of mine which von Neumann refers to is not that on the existence of undecidable propositions or that on the length of proofs but rather the fact that a complete epistemological description of a language A cannot be given in the same language A, because the concept of truth of sentences of A cannot be defined in A. It is this theorem which is the true reason for the existence of the undecidable propositions in the formal systems containing arithmetic. I did not, however, formulate it explicitly in my paper of 1931 but only in my Priceton lectures of 1934. The same theorem was proved by Tarski in his paper on the concept of truth published in 1933 in {\it Act. Soc. Sci. Lit. Vars.}, translated on pp. 152--278 of {\it Logic, Semantics and Metamathematics}. } \end{quote} What were the reasons of avoiding the concept of truth by G\"odel? An answer can be found in a crossed-out passage of a draft of G\"odel's reply to a letter of the student Yossef Balas (mentioned already above). G\"odel wrote there: \begin{quote} {\small However in consequence of the philosophical prejudices of our times 1. nobody was looking for a relative consistency proof because [it] was considered axiomatic that a consistency proof must be finitary in order to make sense, 2. a concept of objective mathematical truth as opposed to demonstrability was viewed with greatest suspicion and widely rejected as meaningless. } \end{quote} Hence it leads us to the conclusion formulated by S.~Feferman in (1984) in the following way: \begin{quote} {\small (\ldots) G\"odel feared that work assuming such a concept [i.e., the concept of mathematical truth --- R.M.] would be rejected by the foundational establishment, dominated as it was by Hilbert's ideas. Thus he sought to extract results from it which would make perfectly good sense even to those who eschewed all non-finitary methods in mathematics. } \end{quote} Though he tried to avoid concepts not accepted by the foundational establishment, G\"odel's own philosophy of \m\ was in fact platonist. He was convinced that (cf. Wang Hao, 1996, p.~83): \begin{quote} {\small It was the anti-Platonic prejudice which prevented people from getting my results. This fact is a clear proof that the prejudice is a mistake. } \end{quote} Note that A.~Tarski was free of such limitations. In fact in the Lvov-Warsaw School no restrictive initial preconditions were assumed before the proper investigation could start. The main demands were clarity, anti-speculativeness and scepticism towards many fundamental problems of traditional philosophy. The principal method that should be used was logical analysis. The Lvov-Warsaw School was not so radical in its criticism of metaphysics as the Vienna Circe.\footnote{See, for example, Wole\'nski (1989) and (1995).} Tarski pointed out on many occasions that mathematical and logical research should not be restricted by any general philosophical views. In particular he wrote in (1930): \begin{quote} {\small In conclusion it should be noted that no particular philosophical standpoint regarding the foundations of mathematics is presupposed in the present work. } \end{quote} \noindent And in (1954) he wrote: \begin{quote} {\small As an essential contribution of the Polish school to the development of metamathematics one can regard the fact that from the very beginning it admitted into metamathematical research all fruitful methods, whether finitary or not. } \end{quote} Hence Tarski, though indicating his sympathies with nominalism, freely used in his logical and mathematical studies the abstract and general notions that a nominalist seeks to avoid. It is known that Tarski showed not only the undefinability but --- and this is his main merit here --- he gave the precise inductive definition of satisfiability and truth. In connection with this one should ask whether G\"odel saw the necessity to give an analysis of the concept of truth (note that in his doctoral dissertation {\it \"Uber die Vollst\"andigkeit des Logikkalk\"uls} (1929) and in his paper `Die Vollst\"andigkeit der Axiome des logischen Funktionenkalk\"uls' (1930) on the completeness of the first-order predicate calculus the notion of the validity was understood in an informal way what was in fact a long tradition --- cf. L\"owenheim and Skolem). The answer is affirmative. Indeed, in a letter to R.~Carnap of 11th September 1932 he wrote: \begin{quote} {\small Ich werde auf Grund dieses Gedankens im II. Teil meiner Arbeit eine Definition f\"ur `wahre' geben und ich bin der Meinung, da\ss\ sich die Sache anders nicht machen l\"a\ss t und da\ss\ man den h\"oheren Induktionenkalk\"ul nicht semantisch [d.h. damals syntaktisch!] auffassen kann.\footnote{Quotation according to K\"ohler, 199?.} } \end{quote} K\"ohler explains in (199?) that ``II. Teil meiner Arbeit'' means here the joint project of G\"odel together with A.~Heyting to write a survey of the current investigations in mathematical logic for Springer-Verlag (Berlin). Heyting wrote his part while the part by G\"odel was never written (the reasons were his problems with the health). One can assume that G\"odel planned to develop there a theory of truth based on the set theory. G\"odel's theorem on the completeness of first-order logic and his discovery of the incompleteness phenomenon together with the undefinability of truth vs. definability of formal demonstrability showed that formal provability cannot be treated as an analysis of truth, that the former is in fact weaker than the latter. It was also shown in this way that Hilbert's dreams to justify classical mathematics by means of finitistic methods cannot be fully realized. Those results together with Tarski's definition of truth (in the structure) and Carnap's work on the syntax of a language led also to the establishing of syntax and semantics in the 1930s. On the other hand it should be added that G\"odel shared Hilbert's ``rationalistic optimism'' (to use Hao Wang's term) insofar as informal proofs were concerned. In fact G\"odel retained the idea of \m\ as a system of truth, which is complete in the sense that ``every precisely formulated yes-or-no question in \m\ must have a clear-cut answer'' (cf. G\"odel, 1970). He rejected however --- in the light of his incompleteness theorem --- the idea that the basis of these truths is their derivability from axioms. In his Gibbs lecture of 1951 G\"odel distinguishes between the system of all true \ma\ propositions from that of all demonstrable \ma\ propositions, calling them, respectively, \m\ in the objective and subjective sense. He claimed also that it is objective \m\ that no axiom system can fully comprise. \vspace{10mm} G\"odel's incompleteness theorems and in particular his recognition (before Tarski) of the undefinability of the concept of truth indicated a certain gap in Hilbert's programme and showed in particular, roughly speaking, that (full) truth cannot be established (achieved) by provability and, generally, by syntactic means. The former can be only approximated by the latter. Hence there arose a problem: how should one extend Hilbert's finitistic point of view? Hilbert in his lecture in Hamburg in December 1930 (cf. Hilbert, 1931) proposed to admit a new rule of inference to be able to realize his program. This rule is similar to the $\omega$-rule, but it has rather informal character and a system obtain by admitting it would be semi-formal. In fact Hilbert proposed that whenever $A(z)$ is a quantifier-free formula for which it can be shown (finitarily) that $A(z)$ is a correct (richtig) numerical formula for each particular numerical instance $z$, then its universal generalization $\forall x A(x)$ may be taken as a new premise (Ausgangsformel) in all further proofs. In Preface to the first volume of Hilbert and Bernays' monograph {\it Grundlagen der Mathematik} (1934/1939) Hilbert wrote:\footnote{For remarks on some connections between those ideas of Hilbert and some ideas of Leibniz see (Murawski, 199?). } \begin{quote} {\small \ldots\ the occasionally held opinion, that from the results of G\"odel follows the non-executability of my Proof Theory, is shown to be erroneous. This result showes indeed only that for more advanced consistency proofs one must use the finite standpoint in a deeper way than is necessary for the consideration of elementary formalism. } \end{quote} G\"odel pointed in many places that new axioms are needed to settle both undecidable arithmetical and set-theoretic propositions. In the footnote $48^{a}$ (evidently an afterthought) to (1931) he wrote: \begin{quote} {\small As will be shown in Part II of this paper, the true reason for the incompleteness inherent in all formal systems of \m\ is that the formation of ever higher types can be continued into the transfinite \ldots\ while in any formal system at most denumerably many of them are available. For it can be shown that the undecidable propositions constructed here become decidable whenever appropriate higher types are added (for example, the type $\omega$ to the system P). An analogous situation prevails for the axiom system of set theory.\footnote{English translation taken from Heijenoort (1967, p. 610).} } \end{quote} In (1931?, p.~35) he stated that ``\ldots\, there are number-theoretic problems that cannot be solved with number-theoretic, but only with analytic or, respectively, set-theoretic methods''. And in (1933, p.~48) he wrote: ``there are arithmetic propositions which cannot be proved even by analysis but only by methods involving extremely large infinite cardinals and similar things''. In (1970) G\"odel proposed ``cultivating (deepening) knowledge of the abstract concepts themselves which lead to the setting up of these mechanical systems''. In (1972) (this paper was a rivised and expanded English version of (1958)) G\"odel claimed that concrete finitary methods are insufficient to prove the consistency of elementary number theory and some abstract concepts must be used in addition. He wrote (pp. 271--273): \begin{quote} {\small Since finitary \m\ is defined \ldots\ as the \m\ of {\it concrete intuition}, this seems to imply that {\it abstract concepts} are needed for the proof of consistency of number theory. \ldots\ By abstract concepts, in this context, are meant concepts which are essentially of the second or higher level, i.e., which do not have as their content properties or relations of {\it concrete objects} (such as combinations of symbols), but rather of {\it thought structures} or {\it thought contents} (e.g., proofs, meaningful propositions, and so on), where in the proofs of propositions about these mental objects insights are needed which are not derived from a reflection upon the combinatorial (space-time) properties of the symbols representing them, but rather from a reflection upon the {\it meanings} involved. } \end{quote} In the paper (1946) G\"odel explicitely called for an effort to use progressively more powerful transfinite theories to derive new arithmetical theorems. He wrote there (p.~151): \begin{quote} {\small Let us consider, e.g., the concept of demonstrability. It is well known that, in whichever way you make it precise by means of a formalism, the contemplation of this very formalism gives rise to new axioms which are exactly as evident and justified as those with which you started, and that this process of extension can be iterated into the transfinite. So there cannot exist any formalism which would embrace all these steps; but this does not exclude that all these steps (or at least all of them which give something new for the domain of propositions in which you are interested) could be described and collected together in some non-constructive way. } \end{quote} These remarks correspond with the words of R.~Carnap who wrote in (1934, p.~274): \begin{quote} {\small \ldots\ {\it alles Mathematische ist formalisierbar; aber die Mathematik ist nicht durch Ein System ersch\"opfbar\/}, sondern erfordert eine Reihe immer rei\-cherer Spra\-chen.\footnote{``\ldots\ {\it all that is mathematical can be formalized; yet the whole of \m\ cannot be grasped by one system\/} but an infinite series of still richer and richer languages is necessary.''} } \end{quote} One can compare the above remarks with those of Turing from his paper (1939). In the introduction to this paper Turing wrote:\footnote{See also Feferman (1962) and (1988) where Turing's idea and its development are discussed.} \begin{quote} {\small The well-known theorem of G\"odel (1931) shows that every system of logic is in a certain sense incomplete, but at the same time it indicates means whereby from a system $L$ of logic a more complete system $L'$ may be obtained. By repeating the process we get a sequence $L$, $L_{1} = L'$, $L_{2} = L_{1}^{'}$, \ldots\ each more complete than the proceeding. A logic $L_{\omega}$ may then be constructed in which the provable theorems are the totality of theorems provable with the help of logics $L$, $L_{1}$, $L_{2}$, \ldots\ Proceeding in this way we can associate a system of logic with any constructive ordinal. It may be asked whether such a sequence of logics of this kind is complete in the sense that to any problem $A$ there corresponds an ordinal $\alpha$ such that $A$ is solvable by means of the logic $L_{\alpha}$. } \end{quote} Also Zermelo proposed to allow infinitary methods to overcome restrictions revealed by G\"odel. According to Zermelo the existence of undecidable propositions was a consequence of the restriction of the notion of proof to finitistic methods (he said here about ``finitistic prejudice''). This situation could be changed if one used a more general ``scheme'' of proof. Zermelo had here in mind an infinitary logic, in which there were infinitely long sentences and rules of inference with infinitely many premises. In such a logic, he insisted, ``{\it all\/} propositions are decidable!''\footnote{Note that that time was not yet ripe for such an infinitary logic. Systems of such a logic, though in a more restricted form than demanded by Zermelo, and without escaping incompleteness, were constructed in the mid-fifties in works of Henkin, Karp and Tarski (cf. Barwise, 1980 and Moore, 1980).} He thought of quantifiers as infinitary conjunctions or disjunctions of unrestricted cardinality and conceived of proofs not as formal deductions from given axioms but as metamathematical determinations of the truth or falsity of a proposition. Thus syntactic considerations played no role in his thinking. \vspace{10mm} To give a rough account of how those suggestions and proposals to extend the finitistic point of view do in fact work let us quote some technical results. We restrict ourselves to the case of the arithmetic of natural numbers, more exactly to Peano arithmetic PA. Generally speaking one can obtain completions of PA by: \begin{itemize} \item admitting the $\omega$-rule, \item adding new axioms (in particular reflection principles), \item adding (partial) notion(s) of truth. \end{itemize} Let us start by considering the case of the $\omega$-rule, i.e., of the following rule:\footnote{It seems that Tarski has been the first person to formulate the $\omega$-rule (cf. Feferman, 1986; Isaacson, 1992). He discussed it in 1926 and presented in a lecture in 1927, though he did not publish the idea until 1933 (cf. Tarski, 1933a, p.~294; see also p.~279, footnote~2; Tarski, 1933, pp.~259--261). He called it `the rule of infinite induction'. The $\omega$-rule was published for the first time in %appeared also in Ajdukiewicz (1928) where it was called `the rule of complete quasi-induction'. Tarski knew quite well the Ajdukiewicz's book (1928) and quoted it several times. However, he never refered to it when writing about the $\omega$-rule. He refered to Hilbert who formulated this rule in an implicitly constructive form in (1931, pp.~491--492) and used it further in (1931a). In (1931) he gave no characteristic name of the rule and called it merely `a new rule of inference'. Later (1931a) he designated it as `transfinite axiom and inference schemata'. The $\omega$-rule was also formulated by Carnap (1934, Section 14, p.~38; 1935). He did not use any description of it, labeling it DC2 (one of the two rules of Direct Consequence for his language I). Rosser (1937) decided to call the $\omega$-rule `Carnap's rule'. The very name `$\omega$-rule' occured for the first time in Grzegorczyk {\it et al.} (1958) (in fact the phrase `rule $\omega$' was used there). For the problem of motivations and reasons of introducing the $\omega$-rule by various authors as well as the problem of (in)dependency see Isaacson (1992). } $$ \frac{\varphi(0), \varphi(\kr{1}), \varphi(\kr{2}), \ldots \quad \mbox{$(n \in \N)$}}{\forall x \varphi(x)}. $$ Denote by (PA)$_{\omega}$ Peano arithmetic PA with the $\omega$-rule. One can easily see that (PA)$_{\omega}$ is complete --- it follows from the fact that its unique model up to isomorphism is the standard model ${\cal N}_{0} = \langle \N, S, 0, +, \cdot \rangle$. Hence (PA)$_{\omega}$ = Th(${\cal N}_{0}$). One can ask: how many times must the $\omega$-rule be applied to obtain a complete extension of PA? To give an answer let us define the following hierarchy of theories where T is any first-order theory in the language L(PA) of Peano arithmetic: \vspace{1em} \begin{tabular}{lcp{100mm}} ${\rm T}^{0}$ & = & T, \\[0.5em] ${\rm T}^{\alpha + \frac{1}{2}}$ & = & ${\rm T}^{\alpha} \cup \{ \varphi:$ $\varphi$ is of the form $\forall x \psi(x)$ and $\psi(\kr{n}) \in {\rm T}^{\alpha}$ for every $n \in \N$\}, \\[0.5em] ${\rm T}^{\alpha + 1}$ & = & the smallest set of formulas containing ${\rm T}^{\alpha + \frac{1}{2}}$ and closed under the rules of inference of PA, \\[0.5em] ${\rm T}^{\lambda}$ & = & ${\displaystyle \bigcup_{\alpha < \lambda}} {\rm T}^{\alpha}$ for $\lambda$ limit. \end{tabular} \vspace{1em} One can now prove that \begin{thm} ${\rm Th}({\cal N}_{0}) = {\rm (PA)}_{\omega} = {\rm PA}^{\omega}.$ \end{thm} Recall the hierarchy of formulas of the language L(PA). Let $\Sigma^{0}_{0} = \Pi^{0}_{0} = \Delta_{0}^{0}$ be the set of all quantifier free formulas and all formulas with bounded quantifiers. Define $\Sigma^{0}_{n+1}$ to be the set of all formulas of the form $\exists x \psi$ for $\psi \in \Pi^{0}_{n}$ and $\Pi^{0}_{n+1}$ to be the set of all formulas of the form $\forall x \psi$ for $\psi \in \Sigma^{0}_{n}$. We also define $\Delta^{0}_{n}$ as the set of all formulas equivalent (in PA) to a $\Sigma^{0}_{n}$ formula and to a $\Pi^{0}_{n}$ formula. One can prove that \begin{thm} For every $n \in \N$ the theory PA$^{n}$ is complete with respect to $\Sigma_{2n+1}^{0}$ sentences. \end{thm} In PA one can define partial notions of truth, i.e., one can define satisfaction and truth for formulas of a given class of the arithmetical hierarchy. Denote by $Sat_{\Sigma^{0}_{n}}$ the definition of satisfaction for $\Sigma^{0}_{n}$ formulas; similarly let $Sat_{\Pi^{0}_{n}}$ denote the definition of satisfaction for $\Pi^{0}_{n}$ formulas. Note that $Sat_{\Sigma^{0}_{0}}$ and $Sat_{\Pi^{0}_{0}}$ are $\Sigma^{0}_{1}$ formulas and that $Sat_{\Sigma^{0}_{n}}$ and $Sat_{\Pi^{0}_{n}}$ (for $n \geq 1$) are $\Sigma^{0}_{n}$ and $\Pi^{0}_{n}$, respectively. Let further $Tr_{\Sigma_{n}^{0}}$ and $Tr_{\Pi_{n}^{0}}$ denote truth predicates for $\Sigma^{0}_{n}$ and $\Pi^{0}_{n}$ sentences.\footnote{Construction of $Sat_{\Sigma^{0}_{n}}$ and $Sat_{\Pi^{0}_{n}}$ can be found in Kaye (1991) and Murawski (1999).} In the sequel we shall identify formulas defining satisfaction and truth and their extensions in the standard model~${\cal N}_{0}$. The previous theorem can now be formulated as: $$ {\rm PA}^{n} \supseteq {\rm PA} + Tr_{\Sigma_{2n+1}^{0}}. $$ In the definition of the hierarchy T$^{\alpha}$ no restriction was put on formulas to which the $\omega$-rule was applied. Consider now a hierarchy in which such a restriction is put. So let T be any theory in the language L(PA). Define the following hierarchy of theories (cf. Niebergall, 1996): \vspace{1em} \begin{tabular}{lcp{100mm}} ${\rm T}^{(0)}$ & = & T, \\[0.5em] ${\rm T}^{(\alpha + \frac{1}{2})}$ & = & ${\rm T}^{(\alpha)} \cup \{ \varphi:$ $\varphi$ is of the form $\forall x \psi(x)$ and $\psi(x) \in \Sigma^{0}_{2 \alpha+1}$ and $\psi(\kr{n}) \in {\rm T}^{(\alpha)}$ for every $n \in \N$\}, \\[0.5em] ${\rm T}^{(\alpha + 1)}$ & = & the smallest set of formulas containing ${\rm T}^{(\alpha + \frac{1}{2})}$ and closed under the rules of inference of PA, \\[0.5em] ${\rm T}^{(\lambda)}$ & = & ${\displaystyle \bigcup_{\alpha < \lambda}} {\rm T}^{(\alpha)}$ for $\lambda$ limit. \end{tabular} \vspace{1em} \noindent Hence the $\omega$-rule is now applied at stage $n$ to $\Sigma^{0}_{2n+1}$ formulas only. One has the following \begin{thm}[Niebergall, 1996] For any $n \in \N$, $$ {\rm PA}^{(n)} = {\rm PA} + Tr_{\Sigma_{2n+1}^{0}}. $$ \end{thm} Consider still another modification of the hierarchy of theories (cf. Niebergall, 1996): \vspace{1em} \begin{tabular}{lcp{100mm}} $(\Sigma^{k}{\rm T})^{0}$ & = & T, \\[0.5em] $(\Sigma^{k}{\rm T})^{\alpha + \frac{1}{2}}$ & = & $(\Sigma^{k}{\rm T})^{\alpha} \cup \{ \varphi:$ $\varphi$ is of the form $\forall x \psi(x)$ and $\psi(x) \in \Sigma^{0}_{k}$ and $\psi(\kr{n}) \in (\Sigma^{k}{\rm T})^{\alpha}$ for every $n \in \N$\}, \\[0.5em] $(\Sigma^{k}{\rm T})^{\alpha + 1}$ & = & the smallest set of formulas containing $(\Sigma^{k}{\rm T})^{\alpha + \frac{1}{2}}$ and closed under the rules of inference of PA, \\[0.5em] $(\Sigma^{k}{\rm T})^{\lambda}$ & = & ${\displaystyle \bigcup_{\alpha < \lambda}} (\Sigma^{k}{\rm T})^{\alpha}$ for $\lambda$ limit. \end{tabular} \vspace{1em} One has of course $$ (\Sigma^{k}{\rm T})^{n} \subseteq (\Sigma^{k+1}{\rm T})^{n} \subseteq \ldots \subseteq {\rm T}^{n}. $$ If T is a theory whose set of (G\"odel numbers of) theorems is strongly representable in PA then denote by $RFN({\rm T})$ the uniform reflection principle for T, i.e., the scheme $$ \forall x {\it Pr}_{{\rm T}}(\g{\varphi(x)}) \rightarrow \forall x \varphi(x) $$ for $\varphi(x)$ formula of L(T) with at most one free variable. If one restricts the class of formulas to a class $\Gamma$ (for example $\Sigma^{0}_{k}$ or $\Pi^{0}_{k}$) then one obtains $RFN_{\Gamma}({\rm T})$. The following theorems hold: \begin{thm}[Niebergall, 1996] For any $n \in \N$: {\rm (a)} ${\rm PA}^{n+1} = {\rm PA} + Tr_{\Sigma^{0}_{2n+3}} + RFN({\rm PA}^{n})$. {\rm (b)} $({\rm PA} + Tr_{\Sigma^{0}_{k}})^{n} = {\rm PA}^{n} + Tr_{\Sigma^{0}_{k + 2n}}$. {\rm (c)} ${\rm PA} + Tr_{\Sigma^{0}_{2n}} \subseteq (\Sigma^{2n-2}{\rm PA})^{n}$ for $n \geq 1$. \end{thm} \begin{thm}[Niebergall, 1996] {\rm (a)} For any $k, n \in \N$: $$ (\Sigma^{k}{\rm PA})^{n+1} \subseteq {\rm PA} + Tr_{\Sigma^{0}_{2n+3}} + RFN_{\Sigma^{0}_{k}}((\Sigma^{k}{\rm PA})^{n}). $$ {\rm (b)} For any $n \in \N$: $$ (\Sigma^{k}{\rm PA})^{n+1} = {\rm PA} + Tr_{\Sigma^{0}_{2n+3}} + RFN((\Sigma^{k}{\rm PA})^{n}) \quad \mbox{if} \quad k \geq 2n+1, $$ and $$ (\Sigma^{k}{\rm PA})^{n+1} = {\rm PA} + Tr_{\Sigma^{0}_{k+2}} \quad \mbox{if} \quad k \leq 2n. $$ \end{thm} The above theorems\footnote{Note that many of those theorems hold not only for Peano arithmetic PA but for a broad class of theories --- cf. Niebergall (1996).} indicate interconnections between Peano arithmetic augmented with the $\omega$-rule and the partial truths as well as the reflection principles. Other connections between them can be formulated in the language of interpretability. So let ${\rm S} \preccurlyeq {\rm T}$ denote that a theory S is relatively interpretable in the theory T (in the sense of (Tarski, 1953)). We have now the following facts (cf. Niebergall, 1996): \begin{thm} Let ${\rm Con}_{S}$ {\rm (}for an appropriate theory S{\rm )} denote a statement of {\rm L(PA)} stating that S is consistent. Then $$ {\rm PA}^{n} \preccurlyeq {\rm PA} + Tr_{\Sigma^{0}_{2n+1}} + {\rm Con}_{{\rm PA}^{n}}, $$ $$ {\rm PA}^{n} \preccurlyeq {\rm PA} + Tr_{\Sigma^{0}_{2n+2}}, $$ $$ {\rm PA} + {\rm Con}_{{\rm PA} + Tr_{\Sigma^{0}_{n}}} \preccurlyeq {\rm PA} + Tr_{\Sigma^{0}_{2}}, $$ $$ {\rm PA} + {\rm Con}_{{\rm PA}^{n}} \preccurlyeq {\rm PA} + Tr_{\Sigma^{0}_{2}}. $$ \end{thm} The above theorems indicate that the arithmetical truth, i.e., the set Th(${\cal N}_{0}$) of all arithmetical sentences true in the standard model ${\cal N}_{0}$, can be approximated by syntactical methods, i.e., by demonstrability --- though not by finitary means (one uses here the $\omega$-rule). This phenomenon is used sometimes as a justification for the thesis that the distinction between syntax and semantics is apparent and arbitrary.\footnote{For example Niebergall writes in (1996, p.~2) : ``Damit halte ich intuitive und formale Syntax-Semantik-Unterscheidung f\"ur problematisch und willk\"urlich''.} So far we have considered Peano arithmetic and partial truths. Ask now: what about PA and the full truth? G\"odel's and Tarski's theorem shows that the truth predicate for L(PA) cannot be defined in PA. But one can extend the language L(PA) by adding a new binary predicate $S$ called satisfaction class and characterizing it axiomatically by adding to Peano arithmetic PA axioms being an appropriate modification of Tarski's definition of satisfaction (cf. Krajewski, 1976, where this notion was introduced, or Murawski, 1997). Note that since those axioms form a finite set of axioms one can write them as a single formula of the language L(PA) $\cup$ $S$. Denote this theory as PA + ``$S$ is a satisfaction class''. One can extend this theory by adding new axioms stating special properties of $S$. In particular one can demand that $S$ is full, i.e., $S$ decides any formula of L(PA) on any valuation or that $S$ is $\Gamma$-inductive for $\Gamma$ being a given class of formulas of the language L(PA) $\cup$ $S$, i.e., that the induction axiom holds for all formulas of the class $\Gamma$ (if $\Gamma$ is the class of all formulas of L(PA) $\cup$ $S$ then one says about inductive satisfaction class). Since theories T of the indicated type are extensions of PA one can ask what about natural numbers can be proved in T, i.e., one can consider theories of the type $$ {\rm PA}^{{\rm T}} = \{ \varphi \in {\rm L(PA)} : {\rm T} \vdash \varphi \}. $$ Theorems of ${\rm PA}^{\rm T}$ are those sentences of the language L(PA) of Peano arithmetic (hence sentences about natural numbers) which can be proved in the stronger theory T. A natural problem of finding an axiomatics of the theory ${\rm PA}^{\rm T}$ arises. %\newpage One can easily see that the following theories are conservative extensions of PA: \begin{itemize} \item[(a)] PA + ``$S$ is a satisfaction class'', \item[(b)] PA + ``$S$ is a full satisfaction class'', \item[(c)] PA + ``$S$ is an inductive satisfaction class''. \end{itemize} This means that one can prove in those theories exactly the same theorems about natural numbers (i.e., formulas of the language L(PA)) as in Peano arithmetic PA. Hence the addition of a new notion, i.e., of a notion of a satisfaction class (and consequently a notion of truth), with properties indicated in (a)--(c) does not increase the prooftheoretical power of a theory with respect to sentences of the language L(PA). On the other hand the assumption that a satisfaction class is full and $\Delta_{0}^{0}$-inductive gives a nonconservative extension of PA. In fact one can prove in this theory the consistency of PA. The theories ${\rm PA}^{{\rm T}}$ for T being PA + ``$S$ is a full ($\Sigma^{0}_{m}$-)inductive satisfaction class'' can be characterized by transfinite induction or the consistency of appropriate $\omega$-logics. Denote by $\Gamma-{\rm PA}(S)$ the theory PA + ``$S$ is a full $\Gamma$-inductive satisfaction class'' and by PA($S$) the theory PA + ``$S$ is a full inductive satisfaction class''. Consider the following sequence of formulas of the language L(PA) (one uses here arithmetization): $$ \Gamma_{0}(\varphi) = ``{\rm PA} \vdash \varphi``, $$ $$ \Gamma_{n+ \frac{1}{2}} (\varphi) = ``\varphi \; \; \mbox{{\it is of the form}} \; \; \eta \vee \forall z \psi (z) \; \; \mbox{{\it and}} \; \; \forall z \Gamma_{n}(\eta \vee \psi (S^{z}0))``, $$ \begin{eqnarray*} \lefteqn{\Gamma_{n+1} (\varphi) = ``\mbox{{\it there exists a proof of the formula}} \; \; \varphi } \hspace{30mm} \\ & \mbox{{\it based on}} \; \; {\rm PA} \cup \{ \psi: \Gamma_{n+ \frac{1}{2}} (\psi)\}``. \end{eqnarray*} Observe that in this system of $\omega$-logic only the application of the $\omega$-rule increases the degree of complexity of a proof. \begin{thm}[Kotlarski, 1986] ${\rm PA}^{\Delta^{0}_{0}-{\rm PA}(S)} = {\rm PA} \cup \{ \neg \Gamma_{n} (0=1): n \in {\bf N} \}.$ \end{thm} It can also be proved (cf. Kotlarski, 1986) that the theory $\Delta^{0}_{0}-{\rm PA}(S)$ is equal to the theory $$ {\rm PA} + S \: \mbox{is a full satisfaction class} + \forall \varphi [ ({\rm PA} \vdash \varphi) \rightarrow S(\varphi) ]. $$ The last sentence can be read as: ``$S$ makes all theorems of PA true''. It is equivalent to the $\Delta^{0}_{0}$-inductiveness of the satisfaction class $S$. The system of $\omega$-logic described above can be iterated in the transfinite. So let us fix a ``natural'' system of notations for ordinals $< \varepsilon_{0}$ (one gets it by Cantor's Normal Form Theorem). By transfinite induction on $\alpha < \varepsilon_{0}$ we define theories $T^{\alpha}$ and formulas $\Gamma^{\alpha}_{n}$ in the following way: %\newpage $$ T^{0} = {\rm PA}, $$ $$ \Gamma^{0}(\varphi) = ``{\rm PA} \vdash \varphi``, $$ $$ \Gamma^{\alpha}_{0} (\varphi) = ``T^{\alpha} \vdash \varphi``, $$ $$ \Gamma^{\alpha}_{n + \frac{1}{2}} (\varphi) = `` \varphi \; \mbox{{\it is of the form}} \; \; \eta \vee \forall z \psi (z) \; \; \mbox{{\it and}} \; \; \forall z \Gamma^{\alpha}_{n} (\eta \vee \psi (z))``, $$ $$ \Gamma^{\alpha}_{n+1} (\varphi) = ``T^{\alpha} \cup \Gamma^{\alpha}_{n + \frac{1}{2}} \vdash \varphi``, $$ $$ T^{\alpha + 1} = T^{\alpha} \cup \{ \neg \Gamma^{\alpha}_{n}(0 = 1): n \in {\bf N} \}, $$ $$ T^{\lambda} = \bigcup _{\alpha < \lambda} T^{\alpha}, \; \lambda \; \mbox{{\it limit}}. $$ Using Recursion Theorem one can formalize those definitions in PA. Define now for an ordinal $\alpha$ a sequence $\omega_{m}(\alpha)$ in the following way: $\omega_{0}(\alpha) = \alpha, \omega_{m+1}(\alpha) = \omega^{\omega_{m}(\alpha)}$. The following theorem holds. \begin{thm}[Kotlarski and Ratajczyk, 1990] Let $m$ be a natural number. Then $$ {\rm PA}^{\Sigma^{0}_{m}-{\rm PA}(S)} = {\rm PA} \cup \{ \neg \Gamma^{\omega_{m}(k)}_{k} (0=1): k \in \N \}. $$ $$ {\rm PA}^{{\rm PA}(S)} = {\rm PA} \cup \{ \neg \Gamma_{n}^{\omega_{n}}(0=1): n \in \N \} $$ where $\omega_{n} = \omega_{n}(\omega).$ \end{thm} Let now $TI(\rho)$, where $\rho$ is an ordinal, denote the scheme of transfinite induction up to $\rho$. Then the following theorem holds. \begin{thm}[Kotlarski and Ratajczyk, 1990a] Let $m$ be a natural number. Then $$ {\rm PA}^{\Sigma^{0}_{m}-{\rm PA}(S)} = {\rm PA} \cup \{TI \: (\varepsilon_{\omega_{m}(k)}): k \in \N \}. $$ $$ {\rm PA}^{{\rm PA}(S)} = {\rm PA} \cup \{TI \: (\varepsilon_{\omega_{k}}): k \in \N \}. $$ \end{thm} The above theorems show how strong is Peano arithmetic augmented with an appropriate notion of satisfaction (and truth). One can see that only by assuming that the added notion of satisfaction (truth) is full and at least $\Delta_{0}^{0}$-inductive one obtains a proper extension of PA. It is interesting that such extensions are equivalent to PA extended by appropriate forms of transfinite induction or by the statements of the consistency of appropriate systems of $\omega$-logic. In other words, they show in particular that what can be proved about natural numbers using Peano axioms and the notion of satisfaction (truth) that is assumed to be full and $\Sigma^{0}_{m}$-inductive is exactly the same as what can be proved in PA plus transfinite induction for ordinals $\varepsilon_{\omega_{m}(k)}$ (for all $k \in \N$) or in PA plus appropriate consistency statements. Similarly for PA plus full inductive satisfaction (truth) on the one hand and PA plus transfinite induction for ordinals $\varepsilon_{\omega_{k}}$ (for all $k \in \N$) or PA plus appropriate consistency statements on the other. They show also that by adding to PA the notion of a satisfaction (truth) and assuming that it is full and makes all theorems of PA true one obtains a theory with exactly the same theorems about natural numbers as by taking PA augmented with a concept of a full and $\Delta_{0}^{0}$-inductive satisfaction (truth) or PA plus appropriate consistency statements. \vspace{2em} In the above (historical, philosophical and logical) considerations about connections between proof and truth in mathematics we restricted ourselves to formal proofs and to the semantical notion of truth {\it in} mathematics. We tried to show how was developing the awareness of differences between them (from the hopes that formal proofs provide sufficient means to exhaust the mathematical truth to the discovery of various limitations of them). Let us finish with some general remarks. Concepts of proof and truth are (even in mathematics) ambiguous. It is commonly accepted that proof is the ultimate warrent for a mathematical proposition, that proof is a source of truth in \m. One can say that a proposition $A$ is true if it holds in a considered structure or if we can prove it. But what is a proof? One should distinguish between working proofs of everyday \m\ and idealized formal proofs used by logicians. On the other hand a proof in \m\ has various aspects and can be studied from various points of view. One can distinguish psychological, social, cultural and logical aspects of proofs. A proof can be studied as a mathematical or as an epistemological object. The former is precisely defined on the basis of mathematical logic, the latter is a vague concept. The former is an idealization of proofs occurring in a research practice of mathematicians, is a reconstruction of them. Recently one can observe in the philosophy of \m\ a tendency to concentrate on the actual research practice of mathematicians rather than on idealized foundational reconstructions of it and consequently to study the methods actually used by mathematicians. Similar distinctions can be made with respect to the concept of truth. The semantical concept of truth precisely defined by Tarski is in fact a mathematical notion. It provides a definition of truth {\it in} \m, it is the concept of truth for a model in a formal language (its essential feature is to define truth in terms of reference or satisfaction on the basis of a particular kind of syntactico-semantical analysis of the language).\footnote{One should also distinguish the truth {\it in} \m\ and the truth {\it of} \m.} But one can also speak about epistemic truth --- cf. for example Isaacson (1987) and (1992) where it is argued that Peano arithmetic is complete with respect to an epistemic notion of arithmetical truth.\footnote{The concept of the arithmetical truth is defined in Isaacson (1987) and (1992) by saying that a proposition in a language of arithmetic is arithmetical if its truth or falsity is perceivable directly on the basis of an articulation of our grasp of the fundamental nature and structure of the natural numbers, or directly from statements which themselves are arithmetical. In the indicated papers it is argued that in the sentences undecidable in Peano arithmetic there are hidden higher-order concepts (via coding by natural numbers of various metamathematical or set-theoretical concepts) and that this is the reason of their undecidability. Peano arithmetic ``consists of those truths which can be perceived as such directly from the purely arithmetical content of a categorical conceptual analysis of the notion of a natural number. The truths expressible in the (first-order) language of arithmetic which lie beyond that region are such that there is no way by which their truth can be perceived in purely arithmetical terms'' (Isaacson, 1987, p.~147).} The distinction between proof and truth in \m\ presupposes of course some philosophical assumptions. In fact for pure formalists and for intuitionists there exists no truth/proof problem. For them a \ma\ statement is true just in case it is provable, and proofs are syntactic or mental constructions of our own making. In the case of a platonist (realist) philosophy of mathematics the situation is different. One can say that platonist approach to \m\ enabled G\"odel to state the problem and to be able to distinguish between proof and truth, between syntax and semantics.\footnote{Note that, as indicated above, Hilbert was not interested in \pha\ questions and did not consider them.} \section*{References} {\small \hang{\noindent Ajdukiewicz, K.: 1928, {\it G\l \'owne zasady metodologii nauk i logiki formalnej\/} (Main Principles of the Methodology of Science and Formal Logic), Nak\l adem Ko\-mi\-sji Wy\-daw\-ni\-czej Ko\l a Ma\-te\-ma\-tycz\-no-Fi\-zycz\-ne\-go S\l u\-cha\-cz\'ow Uni\-wer\-sy\-te\-tu War\-szaw\-skie\-go, War\-sza\-wa.} \vspace{0.3em} \hang{\noindent Barwise, J.: 1980, `Infinitary Logics'. In: Agazzi, E. (Ed.) {\it Modern Logic --- A Survey}, D.~Reidel Publ. Comp., Dordrecht, pp. 3--112.} \vspace{0.3em} \hang{\noindent Carnap, R.: 1934, `Die Antinomien und die Unvollst\"andigkeit der Mathematik', {\it Monatshefte f\"ur Mathematik und Physik} {\bf 41}, 263--284.} \vspace{0.3em} \hang{\noindent Carnap, R.: 1935, `Ein G\"ultigkeitskriterium f\"ur die S\"atze der klassischen Mathematik', {\it Monatshefte f\"ur Mathematik und Physik\/} {\bf 42}, 163--190.} \vspace{0.3em} \hang{\noindent Carnap R.: 1963, `Intellectual Autobiography'. In: Paul A. Schilpp (Ed.), {\it The Philosophy of Rudolf Carnap}, La Salle, Ill., Open Court Publishing Co., pp.~3--84} \vspace{0.3em} \hang{\noindent Davis, M. (Ed.): 1965, {\it The Undecidable: Basic Papers on Undecidable Propositions, Unsolvable Problems, and Computable Functions\/}, Hewlett, N.Y. (Raven Press).} \vspace{0.3em} \hang{\noindent Feferman, S.: 1962, `Transfinite Recursive Progeressions of Aximatic Theories', {\it Journal of Symbolic Logic} {\bf 27}, 259--316.} \vspace{0.3em} \hang{\noindent Feferman, S.: 1984, `Kurt G\"odel: Conviction and Causation'. In: {\it Philosophia Naturalis}, a special issue, Weingartner, P. {\it et al.} (Eds.) {\it Philosophy of Science --- History of Science. A Selection of Contributed Papers of the 7th International Congress of Logic, Methodology and Philosophy of Science, Salzburg, 1983}, Meisenheim/Glan (Verlag Anton Hain). Reprinted in: Shanker, S.G. (Ed.) {\it G\"odel's Theorem in Focus\/}, London 1988 (Croom Helm), pp. 96--114.} \vspace{0.3em} \hang{\noindent Feferman, S.: 1986, Introductory note to: ``Review of Hilbert, `Die Grundlegung der elementaren Zahlentheorie'\,''. In: G\"odel, K. {\it Collected Works\/}, vol. I, ed. by Feferman,~S. {\it et al.}, Oxford University Press, New York and Clarendon Press, Oxford, 1986, pp. 208--213.} \vspace{0.3em} \hang{\noindent Feferman, S.: 1988, `Turing and the Land of $O(z)$'. In: Herken, R. (Ed.) {\it The Universal Turing Machine --- A Half-Century Survey\/}, Oxford University Press, New York and Oxford, pp. 113--147.} \vspace{0.3em} \hang{\noindent Frege G.: 1976, {\it Wissenschaftlicher Briefwechsel}, Hrsg. G.~Gabriel, H.~Hermes, F.~Kambartel, Ch.~Thiel, A.~Veraart, Felix Meiner Verlag, Hamburg.} \vspace{0.3em} \hang{\noindent G\"odel, K.: 1929, `\"Uber die Vollst\"andigkeit des Logikkalk\"uls', doctoral dissertation, submitted in 1929; published and translated in: G\"odel, K. {\it Collected Works\/}, vol. I, ed. by Feferman,~S. {\it et al.}, Oxford University Press, New York and Clarendon Press, Oxford, 1986, pp. 60--101. } \vspace{0.3em} \hang{\noindent G\"odel, K.: 1930, `Die Vollst\"andigkeit der Axiome des logischen Funktionenkalk\"uls', {\it Monatshefte f\"ur Mathematik und Physik\/} {\bf 37}, 349--360. Reprinted with English translation `The Completeness of the Axioms of the Functional Calculus of Logic' in: G\"odel, K. {\it Collected Works\/}, vol. I, ed. by Feferman,~S. {\it et al.}, Oxford University Press, New York and Clarendon Press, Oxford, 1986, pp. 102--123. } \vspace{0.3em} \hang{\noindent G\"odel, K.: 1931, `\"Uber formal unentscheidbare S\"atze der `Principia Mathematica' und verwandter Systeme. I', {\it Monatshefte f\"ur Mathematik und Physik} {\bf 38}, 173--198. Reprinted with English translation `On Formally Undecidable Propositions of Principia Mathematica and Related Systems' in: G\"odel, K. {\it Collected Works\/}, vol. I, ed. by Feferman,~S. {\it et al.}, New York (Oxford University Press) and Oxford (Clarendon Press) 1986, pp. 144--195. } \vspace{0.3em} \hang{\noindent G\"odel, K.: 1931?, `\"Uber unentscheidbare S\"atze'; first published (German text and English translation `On undecidable sentences') in: G\"odel, K. {\it Collected Works\/}, vol. III, ed. by Feferman,~S. {\it et al.}, Oxford University Press, New York and Oxford 1995, 30--35.} \vspace{0.3em} \hang{\noindent G\"odel, K.: 1933, `The present situation in the foundations of mathematics'; first published in: G\"odel, K. {\it Collected Works\/}, vol. III, ed. by Feferman,~S. {\it et al.}, Oxford University Press, New York and Oxford 1995, 45--53.} \vspace{0.3em} \hang{\noindent G\"odel, K.: 1934, {\it On Undecidable Propositions of Formal Mathematical Systems\/} (mi\-me\-o\-graphed lecture notes, taken by S.C.~Kleene and J.B.~Rosser), Princeton; reprinted with revisions in: Davis, M. (Ed.) {\it The Undecidable: Basic Papers on Undecidable Propositions, Unsolvable Problems, and Computable Functions\/}, Hewlett, N.Y. (Raven Press) 1965, pp. 39--74. Also in G\"odel, K. {\it Collected Works\/}, vol. I, ed. by Feferman,~S. {\it et al.}, New York (Oxford University Press) and Oxford (Clarendon Press) 1986, pp. 346--371. } \vspace{0.3em} \hang{\noindent G\"odel, K.: 1946, `Remarks Before the Princeton Bicentennial Conference on Problems in Mathematics', 1--4; first published in: Davis, M. (Ed.) {\it The Undecidable: Basic Papers on Undecidable Propositions, Unsolvable Problems, and Computable Functions\/}, Raven Press, Hewlett, N.Y., 1965, pp. 84--88. Reprinted in: G\"odel, K. {\it Collected Works\/}, vol. II, ed. by Feferman,~S. {\it et al.}, Oxford University Press, New York and Oxford, 1990, pp. 150--153. } \vspace{0.3em} \hang{\noindent G\"odel, K.: 1951, Some basic theorems on the foundations of mathematics and their implications; first published in: G\"odel, K. {\it Collected Works\/}, vol. III, ed. by Feferman,~S. {\it et al.}, Oxford University Press, New York and Oxford 1995, 304--323.} \vspace{0.3em} \hang{\noindent G\"odel, K.: 1958, `\"Uber eine bisher noch nicht ben\"utzte Erweiterung des finiten Standpunktes', {\it Dialectica\/} {\bf 12}, 280--287. Reprinted with English translation `On a Hitherto Unutilized Extension of the Finitary Standpoint' in: G\"odel, K. {\it Collected Works\/}, vol. II, ed. by Feferman,~S. {\it et al.}, Oxford University Press, New York and Oxford, 1990, pp. 240--251. } \vspace{0.3em} \hang{\noindent G\"odel, K.: 1970, The modern development of the foundations of mathematics in the light of philosophy; first published (German text and English translation) in: G\"odel, K. {\it Collected Works\/}, vol. III, ed. by Feferman,~S. {\it et al.}, Oxford University Press, New York and Oxford 1995, 374--387.} \vspace{0.3em} \hang{\noindent G\"odel, K.: 1972, `On an Extension of Finitary Mathematics Which Has Not Yet Been Used', revised and expanded English version of (G\"odel, 1958), to have appeared in {\it Dialectica}, first published in: K.~G\"odel {\it Collected Works}, vol. II, ed. by Feferman,~S. {\it et al.}, Oxford University Press, New York-Oxford 1990, pp. 271--280.} \vspace{0.3em} \hang{\noindent Grzegorczyk, A., Mostowski, A. and Ryll-Nardzewski, C.: 1958, `The Classical and the $\omega$-Complete Arithmetic', {\it Journal of Symbolic Logic\/} {\bf 23}, 188--206.} \vspace{0.3em} \hang{\noindent Heijenoort, J. van (Ed.): 1967, {\it From Frege to G\"odel. A Source Book in Mathematical Logic, 1879--1931\/}, Harvard University Press, Cambridge, Mass.} \vspace{0.3em} \hang{\noindent Hilbert D.: 1899, {\it Grundlagen der Geometrie. Festschrift zur Feier der Enth\"ullung des Gauss-Weber-Denkmals}, B.G.~Teubner, Leipzig, pp.~3--92.} \vspace{0.3em} \hang{\noindent Hilbert D., 1900, \"Uber den Zahlbegriff, {\it Jahresbericht der Deutschen Mathematikervereinigung} {\bf 8}, 180--184. } \vspace{0.3em} \newpage \hang{\noindent Hilbert, D.: 1901, `Mathematische Probleme', {\it Archiv der Mathematik und Physik\/} {\bf 1}, 44--63 and 213--237. Reprinted in: Hilbert, D. {\it Gesammelte Abhandlungen\/}, Verlag von Julius Springer, Berlin, Bd.~3, pp. 290--329. English translation: `Mathematical Problems', {\it Bulletin of the American Mathematical Society} 8 (1901--2), 437--479; also in: Browder, F. (Ed.) {\it Mathematical Developments Arising from Hilbert's Problems\/}, Proceedings of the Symposia in Pure Mathematics 28, American Mathematical Society, Providence, RI, 1976, pp. 1--34.} \vspace{0.3em} \hang{\noindent Hilbert D., 1902/03, \"Uber den Satz von der Gleichheit der Basiswinkel im gleichschenkligen Dreieck, {\it Proceedings of the London Mathematical Society} {\bf 35}, 50--68. } \vspace{0.3em} \hang{\noindent Hilbert D., 1903, {\it Grundlagen der Geometrie}, 2nd edition, Leipzig, Teubner. } \vspace{0.3em} \hang{\noindent Hilbert D., 1905, Logische Principien des mathematischen Denkens, Lecture notes by Ernst Hellinger, Mathematisches Institut, Georg-August-Universit\"at G\"ottingen, Som\-mer-Se\-mes\-ter 1905. Unpublished manuscript.} \vspace{0.3em} \hang{\noindent Hilbert D., 1905a, `\"Uber die Grundlagen der Logik und der Arithmetik'. In: Krazer A. (Ed.), {\it Verhandlungen des dritten Internationalen Mathematiker-Kongresses in Heidelberg vom 8. bis 13. August 1904}, Teubner, Leipzig, pp.~174--185. English translation: `On the foundations of logic and arithmetic' in: Heijenoort, J. van (Ed.) 1967, {\it From Frege to G\"odel. A Source Book in Mathematical Logic, 1879--1931\/}, Harvard University Press, Cambridge, Mass., pp.~129--138.} \vspace{0.3em} \hang{\noindent Hilbert D., 1917--18, Prinzipien der Mathematik, Lecture notes by Paul Bernays. Mathematisches Institut, Georg-August-Universit\"at G\"ottingen, Wintersemester 1917--18. Unpublished typescript. } \vspace{0.3em} \hang{\noindent Hilbert D., 1918, Axiomatisches Denken, {\it Ma\-the\-ma\-ti\-sche An\-na\-len} 78, 405--415. Re\-prin\-ted in: Hilbert, D. {\it Gesammelte Abhandlungen\/}, Verlag von Julius Springer, Berlin, Bd.~3, pp.~146--177. } \vspace{0.3em} \hang{\noindent Hilbert D., 1930, Probleme der Grundlegung der Mathematik, {\it Mathematische Annalen} {\bf 102}, 1--9. } \vspace{0.3em} \hang{\noindent Hilbert, D.: 1930a, Naturerkennen und Logik, {\it Naturwissenschaften} {\bf 18}, 959--963; reprinted in: Hilbert,~D., {\it Gesammelte Abhandlungen}, Bd.~3, Verlag von Julius Springer, Berlin 1935, 378--387. } \vspace{0.3em} %\newpage \hang{\noindent Hilbert D., 1931, Die Grundlegung der elementaren Zahlentheorie, {\it Mathematische Annalen} {\bf 104}, 485--494; reprinted in: Hilbert, D., {\it Gesammelte Abhandlungen}, Bd.~3, Verlag von Julius Springer, Berlin 1935, 192--195. } \vspace{0.3em} \hang{\noindent Hilbert, D.: 1931a, `Beweis des Tertium non datur', {\it Nachrichten der Gesellschaft der Wissenschaften zu G\"ottingen\/}, 120--125.} \vspace{0.3em} \hang{\noindent Hilbert, D. and Ackermann, W.: 1928, {\it Grundz\"uge der theoretischen Logik\/}, Verlag von Julius Springer, Berlin. English translation of the second edition: {\it Principles of Mathematical Logic}, Chelsea Publishing Company, New York 1950. } \vspace{0.3em} \hang{\noindent Hilbert, D. and P. Bernays (1934/1939): {\it Grundlagen der Mathematik}, Sprin\-ger--Ver\-lag, Ber\-lin, Bd.~I 1934, Bd.~II 1939.} \vspace{0.3em} \hang{\noindent Isaacson, D.: 1987, `Arithmetical truth and hidden higher-order concepts'. In: The paris Logic Group (Eds.) {\it Logic Colloquium'85}, Elsevier Science Publishers B.V. (North-Holland), Amsterdam, pp.~147--169.} \vspace{0.3em} \hang{\noindent Isaacson, D.: 1992, `Some Considerations on Arithmetical Truth and the $\omega$-Rule'. In: Detlefsen, M. (Ed.) {\it Proof, Logic and Formalization\/}, Routledge, London and New York, pp. 94--138.} \vspace{0.3em} \hang{\noindent Kaye, R.: 1991, {\it Models of Peano Arithmetic\/}, Clarendon Press, Oxford.} \vspace{0.3em} \hang{\noindent Kotlarski, H. (1986). Bounded Induction and Satisfaction Classes. {\it Zeitschrift f\"{u}r Mathematische Logik und Grundlagen der Mathematik} {\bf 32}, 531--544.} \vspace{0.3em} \hang{\noindent Kotlarski H. and Z. Ratajczyk (1990). Inductive Full Satisfaction Classes. {\it Annals of Pure and Applied Logic} {\bf 47}, 199--223. } \vspace{0.3em} \hang{\noindent Kotlarski H. and Z. Ratajczyk (1990a). More on Induction in the Language with a Full Satisfaction Class. {\it Zeitschrift f\"{u}r Mathematische Logik und Grundlagen der Mathematik} {\bf 36}, 441--454. } \vspace{0.3em} \hang{\noindent K\"ohler, E.: 199?, `G\"odel und der Wiener Kreis'. In: Schimanovich, W. (Hrsg.) {\it Kurt G\"odel --- Wahrheit und Beweisbarkeit\/}, Wien (H\"older-Pichler-Tempsky) (to appear).} \vspace{0.3em} \hang{\noindent Krajewski, S.: 1976, Non-standard Satisfaction Classes. In: W.~Ma\-rek, M.~Srebrny, A.~Zarach (Eds.), {\it Set Theory and Hierarchy Theory}, Proc. Bierutowice Conf. 1975, Lecture Notes in Mathematics 537, Berlin--Heidelberg--New York: Springer Verlag, 121--144. } \vspace{0.3em} \hang{\noindent Moore, G.H.: 1980, `Beyond First-Order Logic: The Historical Interplay Between Mathematical Logic and Axiomatic Set Theory', {\it History and Philosophy of Logic\/} {\bf 1}, 95--137.} \vspace{0.3em} \hang{\noindent Murawski, R.: 1997, Satisfaction classes --- a survey, in: {\it Euphony and Logos}, eds. R.~Murawski and J.~Pogonowski, Editions Rodopi, Amsterdam--Atlanta, GA, 259--281.} \vspace{0.3em} \hang{\noindent Murawski R., 1998, Undefinability of truth. The problem of the priority: Tarski vs G\"odel, {\it History and Philosophy of Logic} {\bf 19}, 153--160.} \vspace{0.3em} \hang{\noindent Murawski, R.: 1999, {\it Recursive Functions and Metamathematics}, Kluwer Academic Publishers, Dordrecht.} \vspace{0.3em} \hang{\noindent Murawski R., 199?, Leibniz's and Kant's philosophical ideas and the development of Hilbert's programme, in: {\it Logos, Being and Mathematics}, ed. J.~Perzanowski, Editions Rodopi, Amsterdam--Atlanta, GA (to appear). } \vspace{0.3em} \hang{\noindent Neumann von, J.: 1966, {\it Theory of Self-Reproducing Automata}, ed. A.W.~Burks, Urbana (University of Illinois).} \vspace{0.3em} %\newpage \hang{\noindent Niebergall, K.-G.: 1996, {\it Zur Metamathematik nichtaxiomatisierbarer Theorien}, Centrum f\"ur Informations- und Sprachverarbeitung Ludwig-Maximilians-Universit\"at M\"unchen, Bericht 96--87. } \vspace{0.3em} \hang{\noindent Rowe, D.E.: 1989, `Klein, Hilbert, and the G\"ottingen mathematical tradition', {\it Osiris} {\bf (2) 5}, 186--213. } \vspace{0.3em} \hang{\noindent Rosser, J.B.: 1937, `G\"odel Theorems for Non-Constructive Logics', {\it Journal of Symbolic Logic\/} {\bf 2}, 129--137.} \vspace{0.3em} \hang{\noindent Tarski, A.: 1930, `Fundamentale Begriffe der Methodologie der deduktiven Wissen\-schaf\-ten. I', {\it Monatshefte f\"ur Mathematik und Physik} {\bf 37}, 361--404. English translation: `Fundamental Concepts of the Methodology of the Deductive Sciences'. In: {\it Logic, Semantics, Metamathematics. Papers From 1923 To 1938\/}, Oxford (Clarendon Press) 1956, pp. 60--109.} \vspace{0.3em} \hang{\noindent Tarski, A.: 1933, {\it Poj\c{e}cie prawdy w j\c{e}zykach nauk dedukcyjnych\/} (The Notion of Truth in Languages of Deductive Sciences), Na\-k\l a\-dem To\-wa\-rzyst\-wa Na\-u\-ko\-we\-go War\-szaw\-skie\-go, Warszawa. English translation: `The Concept of Truth in Formalized Languages', in: {\it Logic, Semantics, Metamathematics: Papers From 1923 To 1938 by Alfred Tarski}, Oxford University Press, Oxford 1956; second edition with corrections and emendations, ed. by J.~Corcoran, Hackett, Indianapolis, IN, 1983, pp.~152--278. } \vspace{0.3em} \hang{\noindent Tarski, A.: 1933a, `Einige Betrachtungen \"uber die Begriffe $\omega$-Wi\-der\-spruchs\-frei\-heit und der $\omega$-Vollst\"andigkeit', {\it Monatshefte f\"ur Mathematik und Physik\/} {\bf 40}, 97--112. English translation: `Some Observations on the Concepts of $\omega$-consistency and $\omega$-completeness', in: {\it Logic, Semantics, Metamathematics: Papers From 1923 To 1938 by Alfred Tarski}, Oxford University Press, Oxford 1956; second edition with corrections and emendations, ed. by J.~Corcoran, Hackett, Indianapolis, IN, 1983, pp.~279--295.} \vspace{0.3em} \hang{\noindent Tarski, A.: 1936, `Der Wahrheitsbegriff in den formalisierten Spra\-chen', {\it Studia Philosophica} {\bf 1}, 261--405 (offprints dated 1935).} \vspace{0.3em} \hang{\noindent Tarski, A.: 1953, `A General Method in Proofs of Undecidability'. In: Tarski,A., Mos\-tow\-ski,~A. and Robinson, R.M., {\it Undecidable Theories\/}, North-Holland Publ. Comp., Amsterdam 1953, pp. 1--35.} \vspace{0.3em} \hang{\noindent Tarski, A.: 1954, `Contributions to the discussion of P.~Bernays, {\it Zur Beurteilung der Si\-tu\-a\-tion in der beweistheoretischen Forschung\/}', {\it Revue Internationale de Philosophie} {\bf 8}, 16--20.} \vspace{0.3em} \hang{\noindent Tarski, A.: 1956, `The Concept of Truth in Formalized Languages'. In: {\it Logic, Semantics, Metamathematics. Papers From 1923 To 1938\/}, Oxford (Clarendon Press) 1956, pp. 152--278.} \vspace{0.3em} \hang{\noindent Turing, A.: 1939, `Systems of Logic Based on Ordinals', {\it Proc. London Math. Soc.\/}, ser. 2 {\bf 45}, 161--228. } \vspace{0.3em} \hang{\noindent Wang, Hao: 1974, {\it From Mathematics to Philosophy}, London (Routledge and Kegan Paul).} \vspace{0.3em} \hang{\noindent Wang, Hao: 1981, `Some facts about K.~G\"odel', {\it Journal of Symbolic Logic} {\bf 46}, 653--659. } \vspace{0.3em} \hang{\noindent Wang, Hao: 1987, {\it Reflections on Kurt G\"odel\/}, Cambridge, Mass. (M.I.T. Press). } \vspace{0.3em} \hang{\noindent Wang, Hao, 1996, {\it A Logical Journey. From G\"odel to Philosophy}, The MIT Press, Cambridge, Massachusetts and London, England.} \vspace{0.3em} \hang{\noindent Wole\'nski, J.: 1989, {\it Logic and Philosophy in the Lvov-Warsaw School}, Dordrecht (Klu\-wer Academic Publishers).} \vspace{0.3em} %\newpage \hang{\noindent Wole\'nski, J.: 1991, `G\"odel, Tarski and the Undefinability of Truth'. In: {\it Yearbook 1991 of the Kurt G\"odel Society} (Jahrbuch 1991 der Kurt-G\"odel-Gesellschaft), Wien, pp.~97--108. Reprinted in: J.~Wole\'nski, {\it Essays in the History of Logic and Logical Philosophy}, Jagiellonian University Press, Krak\'ow 1999, pp.~134--138.} \vspace{0.3em} \hang{\noindent Wole\'nski, J.: 1995, `Mathematical Logic in Poland 1900--1939: People, Circles, Institutions, Ideas', {\it Modern Logic} {\bf 5}, 363--405.} } \end{document} It can be done by: (1) extending the scope of axioms, (2) extending the scope of admissible rules of inference and (3) adding higher types.