Synthese DOI 10.1007/s11229-013-0389-7

Visions of Henkin María Manzano · Enrique Alonso

Received: 30 July 2013 / Accepted: 16 December 2013 © Springer Science+Business Media Dordrecht 2013

Abstract Leon Henkin (1921–2006) was not only an extraordinary logician, but also an excellent teacher, a dedicated professor and an exceptional person. The first two sections of this paper are biographical, discussing both his personal and academic life. In the last section we present three aspects of Henkin’s work. First we comment part of his work fruit of his emphasis on teaching. In a personal communication he affirms that On mathematical induction, published in 1969, was the favourite among his articles with a somewhat panoramic nature and not meant exclusively to specialists. This subject is covered in the first subsection. Needless to say that we also analyse Henkin’s better known contribution: his completeness method. His renowned results on completeness for both type theory and first order logic were part of his thesis, The Completeness of Formal Systems, presented at Princeton in 1947 under the advise of Alonzo Church. It is interesting to note that he obtained the proof of completeness for first order logic readapting the argument for the theory of types. The last subsection is devoted to philosophy. The work most directly related to philosophy is an article entitled: Some Notes on Nominalism which appeared in the Journal of Symbolic Logic in 1953. Unfortunately, we are not covering his contribution to the field of cylindric algebras. As a matter of fact, Henkin spent many years investigating algebraic structures with Alfred Tarski and Donald Monk, among others. Keywords

Leon Henkin · Completeness · History of logic

M. Manzano Universidad de Salamanca, Salamanca, Spain E. Alonso (B) Universidad Autónoma de Madrid, Madrid, Spain e-mail: [email protected]

123

Synthese

1 His life Leon Henkin was born in 1921 in New York, in Brooklyn, in the heart of a Jewish family that originally came from Russia. He died at the beginning of November in 2006, as we are told by mutual friends from the same cause as the mathematician Eratosthenes of Cyrene. He in fact died in Oakland, since some years previously he had to move there with his wife Ginette, leaving behind his beautiful, simple, avantgarde, and minimalist home in the Berkeley Hills, decorated with exquisite objects d’art, among which those from American Indian cultures were outstanding. From his dining room you could look out over the gorgeous sight of the Golden Gate of San Francisco. From 1953 he was a member of the Department of Mathematics at the University of California at Berkeley. From 1991 until his death he was at Mills College. He was an extraordinary logician, an excellent teacher, a dedicated professor and an exceptional person overall. His heart was huge and he was passionately devoted to his ideas of pacifism and socialism (in the sense of belonging to the left). He did not only believe in equality but also worked actively to see that it was brought about. In the obituary1 of the University of California at Berkeley, we read: “Leon Albert Henkin, eminent logician, leader in mathematics education, and pioneering and persistent activist in the effort to bring more underrepresented minorities and women into mathematics, died November 1, 2006, after a brief illness.” In the obituary in the San Francisco Chronicle [November 20, 2006 SF Chronicle], we read: “You could say he was an academic triple threat—very strong in teaching, very strong in research, very strong in administration,” said J.W. Addison, also a UC Berkeley emeritus math professor. Leon Henkin left us an important collection of documents, some of them so exciting as his proof of the theorem of completeness—both for the theory of types and for firstorder logic—by means of an innovative and highly versatile method which was later to be used in many other logics, even in those known as non-classical. For some of his results we know the process of discovery, which observed facts he was trying to explain, and why he ended up discovering things that were not originally the target of his enquiries. Thus, in these cases we do not have to engage in risky hypotheses or explain his ideas on the mere basis of the later, cold elaboration of scientific articles. It is well known that the logic of discovery is not what is adopted on organising the final exposition of our research through its different propositions, lemmas, theorems and corollaries. Henkin was an extraordinary insightful professor in the clarity of his expositions and was well loved by his students, who on his last day of class in the academic years would applaud his efforts with great emotion. Indeed, Henkin always wondered whether his classes should be easy to follow or whether they should force his students to make important efforts. Many of us who knew him believe that he reached a perfect balance and that he would never be obscure on purpose.

1 Written by John Addison, William Craig, Caroline Kane and Alan Schoenfeld.

123

Synthese

He was the Director of the Department of Mathematics at the University of California at Berkeley on at least two occasions: during 66–68 and during 83–85. He became involved in minority defence programs, in the fight against social exclusion, and in programs of Excellence and Diversity in Mathematics. He devoted a large part of his life to developing teaching programs at elementary level for both school children and their teachers. He was also very aware that we are beings immersed in the crucible of history from which we find it hard to escape. This is in fact reflected at the beginning of an interesting article about the teaching of mathematics (Henkin 1995): Waves of history wash over our nation, stirring up our society and our institutions. Soon we see changes in the way that all of us do things, including our mathematics and our teaching. These changes form themselves into rivulets and streams that merge at various angles with those arising in parts of our society quite different from education, mathematics, or science. Rivers are formed, contributing powerful currents that will produce future waves of history. The Great Depression and World War II formed the background of my years of study; the Cold War and the Civil Rights Movement were the backdrop against which I began my career as a research mathematicians, and later began to involve myself with mathematics education. (Henkin 1995, p. 2) In an interview from the series entitled “The Princeton Mathematics Community in the 1930s” (PMC14, PMC19) Henkin recounts how the atmosphere of relative calm with respect to WWII changed radically towards the end of 1942, when America entered the conflict. He tells us that he came upon Mrs. Eisenhart in the street, and we learn that in their conversation she said: “We must all do our duty and get on with it.” Henkin says that very soon everybody was expressing similar opinions. He also stresses that his professor, Herman Weyl, decided not to change his work schedule and that he was positively impressed by this (PMC14): I also remember that I had a lecture by Hermann Weyl that same morning, Monday the 8th. It was 9:00. He said, “I know that all of you are very excited and upset and cannot let go of these great world events that have engulfed us.” But, he said, “I’ve learned from my experience that in the most tempestuous of times, there is a great value in giving some of your attention and your energy to your continuing work” . Therefore, he said, “I am just going to give the regular lecture now that I planned with you last week.” So he did, and I think there is something of real value in those opening remarks. Like many scientists, he felt he had to be committed and he worked for four years on the Manhattan project. As he tells us (Henkin 1996): During the period May, 1942–March, 1946 I worked as a mathematician, first on radar problems and then, beginning January 1943, on the design of a plan to separate uranium isotopes. Most of my work involved numerical analysis to obtain solutions of certain partial-differential equations. (Henkin 1996, p. 133, nt. 11)

123

Synthese

The project gathered a number of eminent scientists, including exiled Jews, many of whom joined the cause against fascism and contributed their grain of salt to the development of the bomb before the Germans. Since the experiments carried out at Los Alamos before the War it was a known fact that fission of the atom was possible, coupled with awareness of the Nazi nuclear program, it was not difficult to convince these brilliant minds, most of which where pacifists and leftists. The first reactions against the nuclear program in USA didn’t appear until the detonation of the bombs over Hiroshima and, especially, Nagasaki in August 1945. Till then very few people collaborating with the Manhattan Project had the slightest idea of the ultimate goal. In an interview (PMC14), Henkin recounts an amusing anecdote about his years at Princeton. Professor Alfred Tucker asked him to create a sort of disturbance on the last day of the academic year: “Like every great teacher he wanted some dramatic incident to imprint the course on the minds of the young students.” So Henkin started dancing around and contorting himself before the class fellows, whose eyes bulged because they were out of the know of the theatrical nature of the event and were unable to understand his lack of respect towards his teacher. He ended up by removing his waistcoat without taking off his jacket! Henkin was very fond of ballet and dancing, both ballroom and modern Nagasaki. There are other amusing anecdotes in these interviews,2 and here we shall see one that had to do with his personal dilemma about teaching: presenting the topics clearly to his students or obliging them to make an effort: That effortless way in which the ideas came made them too easy to slip away. I probably learned more densely packed material from what we called the “baby seminar”, in point set topology conducted by Arthur Stone. I learned more because he made us do all the work. In relation to that same seminar, he describes how he had to face up to professor Lefschetz, although he was fairly unworried because he defines himself as very bold: I was giving my solution to one of the problems that Arthur Stone has set to me before, and being a logician I wanted to make all the details very clear and Lefschetz became impatient. As I got into some of those details he said, “Well, that’s all obvious. Just go on toward the end.” I was a very brash young man. I said, “Professor Lefschetz, it may be obvious to you, but I have come from an environment where a proof requires us to give all the details.” And I just went ahead. 2 As a student and professor Between 1937 and 1947, Henkin began his preparation, studying at Columbia in NY and obtaining a diploma in mathematics and philosophy. Over those years he studied logic with Ernest Nagel at the Dept of Philosophy and this led him to become interested in the field to a point where he even read Russell’s Principles of Mathematics. It was 2 See PMC14 and PMC19.

123

Synthese

there that he first heard about the axiom of choice and he tells us that he was impressed by the amusing and intimate way Russell used to explain it, contrasting how easy it is to choose a shoe of each pair from an infinite collection of pairs of shoes, but how difficult it is to do so when instead we have pairs of socks. This reading led him to an incursion into the Principia Mathematica of Russell and Whitehead (1910–1913), and he became infatuated by the theory of types and by the axiom of reducibility. At Columbia, he also followed another course on logic given by Nagel, and he read an article by Quine, with a proof of completeness for propositional logic. I simply noted that the aim of the paper was to show that every tautology had a formal proof in the system of axioms presented, and I expended my utmost effort to check Quine’s reasoning that this was so, without ever reflecting on why author and reader were making this effort. This strictly limited objective also kept me from wondering how the author thought of putting the steps of the proof together; the result was that I failed to get “the idea of the proof,” the essential ingredient needed for discovery. (Henkin 1996, pp. 129–130) He also had occasion to listen to Tarski, whom the invasion of Poland had surprised while at Harvard preventing him from returning to Poland and had prevented him from returning to Poland. Tarski spoke of Gödel’s work on undecidable propositions in type theory. However, his first contact with the work of Gödel arose from a sort of reading seminar promoted by Von Neumann to comment on Gödel’s results on the consistency of the continuum hypothesis. At that time, Henkin had still not graduated, but he was the only student who seemed to be interested in these issues and prepared to invest time and energy in studying them. Upon finishing his studies at Columbia, he applied for admission to universities where logic was well established: Harvard (where Quine was), Princeton (Church) and Columbia. He was accepted at all three, but he rejected the first one because it did not offer grants and he finally opted for Princeton. It was at Princeton that Henkin followed his master’s and doctorate studies, although between both, as commented above, he worked on the famous Manhattan project, an initiative of the United States although with the collaboration of Canada and the United Kingdom. During his initial term at Princeton, he followed a logic course by Church in which both propositional and first-order calculuses were studied and normal form and completeness theorems were proved for them, and the Lö wenheim–Skolem results were analysed. The completeness proof was that of Gödel (Henkin’s, evidently, did still not exist) and the reductive nature of the proof was remarked on. This reductive nature has to do with the use of Skolem normal forms to reduce the complexity of the proof and with the elimination of quantifiers and the evaluation of the resulting propositional formula.3 During the second semester, a second-order language was studied and, in particular, Peano Arithmetic was introduced in great detail and the results of incompleteness were proved, both for arithmetic and second-order logic. To prove incompleteness, 3 See Henkin (1996, p. 132).

123

Synthese

recursive functions were introduced, although only the class of primitive recursive functions originally defined by Gö del. General recursive functions were not studied, but the role they play in the proof of certain undecidability results was mentioned. Henkin tells us that although the content of the course was not, as you see, in the least surprising, what was striking was the style of his maestro; the way he had in transmitting his conception of logic. It appears that he would make frequent halts in his discourse to clarify the idea that he was following the “logistic method”: clearly delimiting what was language and what was metalanguage; how formal language should be established in a completely effective way, and why metalanguage (English, in his case) should be limited. One can gain an idea of how by reading Church’s book Introduction to Mathematical Logic, vol I. The second volume, whose index appears in the first, was never published, although some of its chapters were circulated among his students. The Frege theory about the notions of sense and denotation4 were the topic of another subject that Henkin followed with Church during his doctorate studies. Henkin affirms that Church convincingly defended the notion that as well as formal language and that of the universe of mathematical objects where we interpret their formulae, there is a third dimension of abstract objects denominated concepts or senses. A sentence expresses a proposition but also names a truth-value. Henkin (1996) writes: Under this theory a symbolic expression functioning as a name denotes an object of the universe of discourse, and expresses some sense of that object; a sentence is construed as a name of its truth value, and the sense it expresses is called a proposition. (Henkin 1996, p. 142) The Completeness of Formal Systems is the title of the thesis that he presented at Princeton in 1947, and his director was Alonzo Church.5 In Sect. 3.2 we shall speak of this in greater detail. Between 1947 and 1957, Henkin spent two years following doctorate courses at Princeton, four teaching and investigating in Los Angeles, at the University of California; one year in Amsterdam with a Fulbright fellowship, and three years at Berkeley, also in the University of California. He valued the role of Tarski very highly as regards his own decision to set up at Berkeley. On the 30 October 1983, in a personal communication to María Manzano he wrote: I write to tell you that Alfred Tarski, who came to Berkeley in 1942 and founded our great center for the study of logic and foundations, died Wednesday night (Oct. 26), at age 82. All through this year he has been getting weaker; his wife Maria worked heroically to comfort and protect him, but finally he gave up his life… … It was he who brought me to Berkeley in 1953, so I owe much to him personally as well as scientifically. 4 Church (1951) explained what was to become his paper on that subject. 5 We strongly recommend the reading of: “Alonzo Church: His Life, His Work and Some of His Miracles”

(Manzano 1997) and “Diagonalization and Church’s Thesis: Kleene’s homework” (Alonso and Manzano 2005).

123

Synthese

From 1957, until his death Henkin devoted himself to mathematics, mainly logic and algebra. From 1953 he was at Berkeley; he was a professor from 1957 and as of 1991 he was an Emeritus Professor. From 1991 to 2006 he was at Mills College where he and Steven Givant founded the highly successful Mills Summer Mathematics Institute for undergraduate women. He spent research stays at Dartmouth College in Hanover (New Hampshire), at the Institute for Advanced Studies in Princeton, at the University of Oxford (UK), in Colorado, and at several European Universities; among them Yugoslavia, Spain and Portugal and also in France at the University of Paris VII. The story behind this is that of María Manzano, who during the academic year 1977–1978 attended his classes in algebra for students in the first years of the degree course, and of metamathematics for doctorate students. The textbook used in the algebra course was that of Birkhoff MacLane, A Survey of Modern Algebra, but we did not follow the order of the book. The topics were the usual ones in an Algebra course: Rings, Fields, Polynomials, Homomorphisms, Vector Spaces, etc. Before each class Henkin would give us a text of some 4–5 pages that summarised what was to be addressed in the class. The texts were printed in purple ink, done with the old multicopiers that we called “Vietnamese copiers” and that were so often used to (illegally) print pamphlets in our revolutionary days in Spain. Before starting the sessions, as well as the copies of the topics to be addressed he would give us a sheet explaining the tasks of the week: revision of class notes and of the corresponding sections of the book (indeed, exactly which ones) and some 8 problems to solve. Aside from returning the exercises corrected, he would give us a copy with exercises containing problems solved by him. Detailed information of everything about the course that might be of interest to us was announced a long time before strictly necessary: the dates for handing in the various tasks, the dates of our exams to be done in class with our books and notes, and his tutorial schedule. In the courses given in the first years of the degree, he was always very enthusiastic, even jovial, in class and he transmitted a feeling of confidence. His tutorials were always well attended. As mentioned above, he was extraordinarily clear in his explanations, although he himself sometimes doubted whether this was the right way of doing things. Proof of this internal debate are the following words that formed part of the summary of his course on Metamathematics. Many bright students find my lectures a little slow, and they consider my concern with the machinery of logic (as distinct from the results) as pedantic. Concerning the first of these judgments, it is valid, but since many of the students are as slowthinking as I, and the quick-thinking ones can always skip lectures and study the references, the pace as a whole is not bad—and indeed, the poorly-prepared students may find themselves struggling a bit to keep up. Concerning the second charge, however, I think it can be at least partially turned aside by adverting to pedagogical principles—which I am quite willing to explicate and discuss in office hours, or even in class if demand warrants.6

6 Henkin (1978), class notes.

123

Synthese

In the summary of the course Henkin defines metamathematics as the mathematical theory of mathematical theories, and he introduces the latter as the study of structures and their interrelations. There are three classes of structures and their interrelations that are studied in metamathematics: formal grammars, deductive calculus, and semantics (called interpreted languages). The language of sentential logic, of first-order and equational logic, many-sorted logic and higher-order logic were dealt with in a unified way in the course. In each case, we studied the relationship between the semantic notion of consequence and the syntactic notion of derivability, with proofs of the theorems of soundness and completeness. It is curious that the first-order proof of completeness that Henkin developed in class was not his own but was developed by using the reduction of Herbrand to propositional logic and the completeness of propositional logic. He wrote: “Since we use the completeness of sentential logic in our proof, we effectively reduce the completeness problem for first order logic to that of sentential logic.”7 The issue of implicit and explicit definability was addressed in detail and the Beth/Padoa theorems relating them and the interpolation theorems of Craig-Lyndon were proved (Henkin 1963a). In 1963 Henkin published the paper An Extension of the Craig-Lyndon Interpolation Theorem where we can find a different proof of completeness for first order logic. The theorems of Löwenheim–Skolem and of compactness were proved and commented. Naturally, the notions of universal algebra were introduced to relate structures; basically, substructures, homomorphisms, direct products and also ultraproducts. In particular, ultraproduct construction was used to prove compactness. Henkin did not forget classic themes such as those of the elimination of quantifiers, and of categoricity. The theory of types and Gödel’s theorem were important parts of the course; indeed, they accounted for 2/5th of the whole. The language of the theory of types introduced by Henkin is that based on identity, very similar to that of his works (Henkin 1963b, 1975), which contained a selector operator that would allow the axiom of choice to be expressed. The recursive functions, the arithmetization of formal language, the Gö delization and self-reference inevitably led to Gödel’s theorems of incompleteness. The last topic was that of general recursive functions and relations. Between 1957 and 1972, Henkin shared his work in research into mathematics with enquiries into its teaching. As from 1972, he devoted himself mainly to investigating the teaching of the subject. In fact in 1979, with a Fulbright fellowship, he spent time in Israel devoted to looking into the teaching of mathematics. He was then at the Department of Education in Science at Technion University in Haifa. On this occasion he also visited two universities in Egypt. 3 Three glances of Henkin’s work We shall constrain ourselves here to highlighting just three of the aspects of his work that seem most representative of the interests he engaged in along his productive life as an investigator and pedagogue. As seems to be evident, at the head of this volume of enquiry we must place his technique for proving completeness. We added the 7 Henkin (1978), class notes.

123

Synthese

section concerning mathematical induction because his paper devoted to the subject (Henkin 1960) was a particular source of pride for Henkin. In this paper he describe structures that he introduced to elucidate the relation between mathematical induction and recursive definitions in the theory of Peano arithmetic. Finally, we wish to devote some time to his relationship with philosophy as a way of stressing the relevance of good research in logic in that field of knowledge. Many other aspects that could have served as a basis for discussion have been left out. Perhaps as regards Henkin’s interest in the algebra of logic, the main one is Cylindric Algebras (Henkin and Tarski 1961; Henkin et al. 1971). 3.1 Mathematical induction Fruit of this emphasis on teaching is the creation of inductive models. In a personal communication he affirms that On mathematical induction, published in 1969 (Henkin 1960), was the favourite among his articles with a somewhat panoramic nature and not directed exclusively to specialists. In 1982 Leon Henkin came to Barcelona and gave two talks (Manzano 1983). The talk about inductive models was especially interesting because he told us something that would never appear in any formal article: motivation. Henkin tried to convince a mathematical colleague about the reasons that made a given argument about the existence of recursive operations completely wrong, even though at first sight it might seen convincing. Peano axiomatized the theory of natural numbers. To do so, he started out from indefinable primitive terms—in particular, those of natural number, zero, and the successor function—and by means of three axioms he synthetised the main facts. Among those axioms is that of induction, which states that any subset of natural numbers, closed by the successor operation and to which zero belongs, is precisely the set of all natural numbers. Although these axioms of the theory of natural numbers are very important, the most interesting theorems of that theory did not stem from them alone. In most of these theorems, operations of addition, multiplication, etc. are used. Peano thought that upon axiomatizing a theory it did not suffice to organize the facts by means of axiomatic laws; it was also necessary to organize the concepts, using definition laws. In particular, we can define addition recursively by means of: 1. x + 0 = x 2. x + Sy = S(x + y), for all x, y of N. However, this definition must be justified by a theorem in which the existence of a unique operation that will satisfy the previous equations must be established. A poor argument to prove this is as follows. Let us choose any x ∈ N. We define a subset G of N, placing the y ∈ N elements in G for which x + y is defined by the previous equations. It is not difficult to see that 0 ∈ G and that ∀y(y ∈ G → Sy ∈ G). Now using the induction axiom, we conclude that x + y is defined by all y ∈ N, since G = N. 3.1.1 Why is this proof wrong? This was the question that Henkin’s colleague posed him. Henkin tried to convince him that the argument was designed to establish the existence of a function

123

Synthese

f (+ in the example) and it is incorrect to assume in the course of the argument that we have such a function. Henkin made him see that in the proof only the third axiom is used and that, if correct, it would be applicable not only to models that satisfy all Peano axioms but also those that only satisfy that of induction. Henkin called these “Induction Models” and proved that in them not all recursive operations are definable: for example, exponentiation fails. Induction models turn out to have a fairly simple mathematical structure: there are standard ones—that is, isomorphic to natural numbers—but also non-standard ones. The latter also have a simple structure: either they are cycles, in particular Z modulo n, or they are what Henkin calls “spoons”; in fact, they have a handle followed by a cycle. The reason is that the induction axiom is never fulfilled alone, since it brings with it Peano’s first or second axiom. This does not mean that Peano’s axioms are redundant, as its is well known that they are formally independent; i.e., each one independent of the other two. All these aspects were addressed by Henkin in his article about mathematical induction (Henkin 1960), which from our point of view is the best paper on logic to offer students as a first reading of a “real-life” article.

3.2 His proof of the completeness theorem The theorem of completeness establishes the correspondence between deductive calculus and semantics; in particular, when soundness is assumed, it proves the equivalence between the proof-theoretic and semantic definition of logical consequence. Gödel had solved the issue positively for first-order logic and negatively for any ω-consistent recursively axiomatized logical system in which arithmetic could be embedded.8 The lambda calculus for the theory of types (Church 1940, 1941), coupled with the usual semantics over a standard hierarchy of types, was able to express arithmetic and hence could only be incomplete. Henkin showed that if the formulae were interpreted in a less rigid way, accepting other hierarchies of types that did not necessarily have to contain all the functions but did contain the definable ones, it is easily seen that all consequences of a set of hypotheses are provable in the calculus. The valid formulae with this new semantics, called general semantics, are reduced to coincide with those generated by the rules of calculus. As it is well known, Henkin’s completeness theorem rests on the proof that every consistent set of formulae has a model. The proof is essentially given in two parts: (1) The consistent set is extended to one that is maximally consistent, (2) The model that the formulae of this maximally consistent set describe is constructed. The latter is not difficult, since a maximally consistent set is a detailed description of a structure. Curiously, the model uses the formulae themselves as objects; in particular its elements are equivalence classes of formulae, the equivalence relationship being that of formal derivability. 8 We refer to the seminal papers by Gödel (1930, 1931).

123

Synthese

It is interesting to note how he discovered it.9 Church created the lambda calculus using functions as the basic concept, and he made a clear distinction between the value of a function for a given argument and the function itself. Functions and function values have proper names in lambda calculus. This language attracted Henkin very much: in particular the neatness and shortness of the formula expressing the axiom of choice. It contrasted with the case of Gö del’s calculus denominated PM that did not permit functions to be named, although of course formulae with free variables define sets and relations. Hierarchy of types The types are structured in a hierarchy that has the following as basic types: (1) D1 is a non-empty set; that of the individuals of the hierarchy, (2) D0 is the domain of truth values—since we are in binary logic, these values are reduced to T and F—and (3) The other domains are constructed from the basic types as follows: if Dα and Dβ have already been constructed, we define D(αβ) as the domain formed by all the functions from Dβ to Dα . The sets are represented by means of characteristic functions and hence D(0β) represent the power set of Dβ , formed by all the subsets of Dβ . To talk about this standard hierarchy, a formal language, named T , is introduced. Alphabet We have variables of different types, with a superindex indicating this. In the article by Church (1940), the constants N(00) and A((00)0) (for negation and conjunction) and (0(0α)) (allowing us to express quantification) are also introduced as basic components. Another interesting operator of Church’s language was ιa(0a) ; these symbols were introduced to play the role of selection operators whose interpretations should be choice functions. Expressions There are two main ways of forming expressions: (1) The simples one: Each constant or variable alone is a formula whose type is that of the index and (2) The compounds ones are of two classes: (2a) With λ we form functions. If X β is a variable and M α is an expression, then (λX β M α ) is an expression of the type (αβ). (2b) The others correspond to the assignation of value under a function: if F (αβ) and B β are expressions, F (αβ) B β is an expression of type α. Henkin (1996) says: I decided to try to see just which objects of the hierarchy of types did have names in T . ... As I struggled to see the action of functions more clearly in this way, I was struck by the realization that I have used λ-conversion, one of the formal rules of inference in Church’s deductive system for the language of the Theory T . All my efforts had been directed toward interpretations of the formal language, and now my attention was suddenly drawn to the fact that these were related to the formal deductive system for that language. (Henkin 1996, p. 150) In other words, he was trying to represent to himself the functions of the hierarchy of types that can be named by λ-expressions. To visualize this, he considered a hierarchy 9 We strongly recommend a reading of Henkin’s paper The discovery of my completeness proofs—Henkin

(1996)—on which the following exposition relies.

123

Synthese

of types whose universe of individuals D1 would be that of natural numbers, with a constant as a name for zero and another one for the successor function. In the universe D01 there were clearly objects both with and without a name, because with a countably infinite universe of individuals that of sets of individuals is uncountable, but the sets that can be named are only countable. He became involved in the recursive process of finding an object of the hierarchy of types as a denotation for each formula and the difficulties appeared with the selector ια(0α) , whose interpretation must be a choice function. However, when I tackled the problem of describing some particular choice function to serve as denotation of ι(01)(0(01)) , I was stumped. ... Could I make precise what it might mean to say that it is “intrinsically impossible” to specify any particular choice function for non-empty sets of real numbers? No, I really couldn’t. (Henkin 1996, pp. 147–148) He developed the hierarchy of the objects that have a name in the hierarchy of types and realised that in order to remove repetitions he was using the rules of lambdaconversion and that the syntax and calculus were therefore involved in the description of the semantic objects. In particular, to identify the objects named by means of M α and N α he was using calculus theorems as a criterion: in particular, that  M α = N α . He saw that using the symbol  for formal provability (or derivability) as usual, we can define for each type symbol α a domain Dα in which each sentence of the formal language acquires denotation, each functional expression denotes a function of the hierarchy and the deductively equivalent expressions denote the same object. To accomplish this, the domains are formed by classes of equivalence of formulae    Dα = M α : M α is a formula of type α where 

   M α = N α : M α = N α

Finally, the proof was completed when he realized that for the universe of the objects named by propositions (that of truth values) to be reduced to only two it would be necessary to expand the axioms until they formed a maximally consistent set, so that the number of equivalence classes induced by the relation  M α = N α would be reduced to two. Let us quote10 him again: “In particular, if M 0 is a Gödel sentence such that neither  M 0 nor ∼ M 0 , then (01 = 01 ) , (∼ 01 = 01 ) , and M 0 are three distinct elements of D0 .” He immediately realized that in this way he had formulated and proved what in his thesis would be theorem VI11 : “If S is any formally consistent set of T sentences, then there is a denumerable general model M of T for which each sentence of S is true. (Each domain Dn of M is denumerable).” 10 In Henkin (1996, p. 151). 11 In Henkin (1996, p. 141).

123

Synthese

Curiously, he obtained the proof of completeness of first-order logic later by readapting the argument found for the theory of types.12 Another interesting aspect that Henkin himself pointed out is the non-constructive nature of the proof, despite coming from a tradition as tightly bound to proofs with a constructive nature as those developed by Church.13 In the following section we will see how Henkin related the models built in this completeness proof to a nominalistic position, close to Quine’s. 3.3 Philosophy To speak of a truly philosophical contribution in the work of Henkin is undoubtedly exaggerated. The historical moment at which most of his production occurred seems to have left behind that type of mixed vocation clearly represented in figures such as Russell, Gödel, Turing or Quine. However, throughout his life Henkin tackled problems of enormous philosophical import, about which he was undoubtedly perfectly aware. The reference of the objects of logic and of mathematics is surely one that he addressed in greater detail upon accepting the terms of a debate posited by Quine and Goodman at the start of the 1950s. More will be said about this later. However, neither does he elude philosophical commitment when he analyzes the behavior of the axiom of induction in certain developments,14 or when he wonders about the non-constructive nature of certain techniques used to obtain some of his results. Another issue with an ample historical precedent is the search of a system that takes the identity relation as the sole primitive constant. Henkin studied that matter in deep in at least two of his contributions, namely, in A theory of Propositional Types and in Identity as a Logical Primitive. In the first one, a complete calculus for a logic having the lambda abstractor and equality as its only primitive constants is presented. The definition of all connectives and quantifiers using these constants, as well as the new technique of completeness he develops in this paper are extraordinary insightful. Naming every object of the hierarchy is the main part of the completeness process. The philosophical position underneath can be termed as nominalistic. A position easy to support and appropriate for a theory of types each of which is finite. In the second paper, the reverse philosophical question is posed, can we define identity using the remaining connectives and quantifiers? Along the years he devoted to his research, Henkin exhibited a subtle “nose” for checking rare forms of meaning and for referring to reality. His work on non-standard models, and above all their use to design a theorem of completeness in the theory of types, contains a considerable body of teaching relative to how language actually 12 In Completeness: from Gödel to Henkin (Manzano and Alonso 2013) readers will find a more elaborated

treatment of the historical aspects of completeness. 13 “This may seem curious, as his work in logic, and his teaching, placed great emphasis to the constructive

character of mathematical logic, while the model theory to which I contributed is filled with theorems about very large classes of mathematical structures, whose proofs often by-pass constructive methods”. In Henkin (1996, p. 127). 14 See the discussion surrounding the relation between Peano models and induction models in Henkin

(1960, Sect. 5).

123

Synthese

signifies objects in mathematical domains. The philosophical import of these issues seems indubitable. The work most directly related to philosophy is an article entitled: Some Notes on Nominalism (Henkin 1953b) which appeared in the Journal of Symbolic Logic in 1953 and to which there was to be a sequel, in 1955, in the form of a lecture (Henkin 1953c). As Henkin himself was eager to clarify, this was a reply to two papers that appeared in that journal over a short period of time; in particular in 1947. The first, “On universals” was signed by Quine and the second one, “Steps toward a constructive nominalism” by Quine and Nelson Goodman jointly. These works, including that of Henkin, are encompassed within a foundations sensitive tradition that is perhaps not as popular today. A tradition dealing with the ontological or metaphysical implications of logical investigation. The issue addressed by Henkin in his “Some notes...” revolves around the possibility of carrying out a nominalistic reading of the models of classical mathematics; a problem that had in fact troubled Quine and Goodman for several years. They proposed a new interpretation of mathematical language in terms of a narrow domain of entities, the purpose being to support a nominalistic thesis; namely, a position free of ontological commitments and so denying the existence of universals that Platonist accept. They claim that the identification of indiscernibles is compatible with their nominalistic position as they propose a method to identify objects when they differ in no respect expressible within the theory itself. Thus, the comparison is effectuated using formulas of the language that commit us only to the existence of individuals and not to abstract entities. As an example of identification of indiscernibles they posed what they called the theory of inscriptions, where the value of bound variables are concrete inscriptions. By contrast, inscriptions with the same shape are treated as equals, giving place to a new language for a theory of shapes with the following properties: “variables range over inscriptions instead of shapes, the symbol of equality is understood as asserting sameness of shape rather than identity, and a constant, instead of denoting a particular shape, becomes a schematic letter for which may be substituted the name of any inscription having that shape.”15 One of the problem such a nominalistic position must face is the interpretation of the formula ¬∃F∀G∃x∀y(F x y ↔ Gy) whose classical interpretation is that no one-one and onto function maps the totality of individuals of a domain with the class of all sets of these individuals. Cantor proved that the formula is a theorem of classical mathematics; and so it is also a theorem of second order logic and therefore should be true. For Quine and Goodman, this argument seems to show up the difficulty involved in finding a nominalist interpretation of the theory of models of standard mathematics when this is limited to countable magnitudes. Regarding this, Henkin’s position is very subtle. By establishing a similarity with the paradox of Löwenheim–Skolem, Henkin proposes a non-standard interpretation of cardinality able to resolve the situation. However, this is not conclusive and 15 Henkin (1953b, p. 19).

123

Synthese

simply allows for the possibility of following on with the nominalistic program. The construction of models suitable for second-order logic next proposed by Henkin seems to take advantage of the completeness technique Henkin previously developed for the theory of types and for first-order logic. Here we are dealing with the construction of models for the language of higher-order logic by applying an inductive construction that in successive steps adds the required entities to the basic linguistic entities. The result is a maximal consistent set of sentences that provides a nominalist model. However, the model so built depends on the enumeration chosen for the sentences of the language. The notion of logical truth is, notwithstanding, independent of the starting enumeration. The solution obtained neglects the first objection made by Quine and Goodman as regards the expression of uncountable magnitudes but it does confront the one that questions the existence of any kind of infinite magnitude. In particular, the objection would be applied to those entities that Henkin took as objects of the domain of his models, the marks that constitute new objects of the language, which he called inscriptions. Henkin openly recognises that objection cannot be sidestepped by using formal means, and hence initiated a genuinely philosophical discussion about the acceptability of certain assumptions in the domain of logic and mathematics. What is evidently important is that reference should be made to the suitability of considering, as an opportune fiction, the existence of infinite magnitudes. Thus, he states: In short, infinite collections are useful because they serve as a model to approximate finite collections. In a sense, we “make believe” that some finite set is infinite to simplify some computation connected with it. (Henkin 1953b, p. 27) References Alonso, E., & Manzano, M. (2005). Diagonalization and Church’s thesis: Kleene’s homework. History and Philosophy of Logic, 26(2), 93–113. Church, A. (1940). A formulation of the simple theory of types. The Journal of Symbolic Logic, 5, 56–68. Church, A. (1941). The calculi of lambda-conversion. Annals of mathematical studies. num. 6. Princeton, NJ: Princeton University Press. Church, A. (1951). A formulation of the logic of sense and denotation. In Structure, methods and meaning, essays in honor of Henry M. Sheffer, New York (pp. 3–24). (Revisado en NOUS: Vol. 7 (1973), pp. 24–33; Vol. 8 (1974), pp. 135–156; and, Vol. 27 (1993), pp. 141–157.) Gödel, K. (1930). The completeness of the axioms of the functional calculus of logic. In S. Feferman, J. W. Dawson, et al. (Eds.). (1986). Kurt Gödel collected works (Vols. I and II). Oxford: Oxford University Press. Gödel, K. (1931). On formally undecidable propositions of principia mathematica and related systems I. In S. Feferman, J. W. Dawson, et al. (Eds.). (1986). Kurt Gödel collected works (Vols. I and II). Oxford: Oxford University Press. Henkin, L. (1953a). Banishing the rule of substitution for functional variables. The Journal of Symbolic Logic, 18(3), 201–208. Henkin, L. (1953b). Some notes on nominalism. The Journal of Symbolic Logic, 18(1), 19–29. Henkin, L. (1953c). The nominalist interpretation of mathematical language. Bulletin de la Société Mathématique de Belgique. Henkin, L. (1960). On mathematical induction. The American Mathematical Monthly, 67(4), 323–338. Henkin, L. (1963a). An extension of the Craig-Lyndon interpolation theorem. The Journal of Symbolic Logic, 28(3), 201–216.

123

Synthese Henkin, L. (1963b). A theory of propositional types. Fundamenta Mathematicae, 52, 323–344. Henkin, L. (1975). Identity as a logical primitive. Philosophia, 5, 31–45. Henkin, L. (1978). Metamathematics. Class Notes. Course of 1978. Mimeographed notes. Henkin, L. (1995). The roles of action and of thought in mathematics education—One mathematicians’s passage. CBMS Issues in Mathematics Education, 5, 3–16. Henkin, L. (1996). The discovery of my completeness proofs. Dedicated to my teacher, Alonzo Church, in his 91st year. Bulletin of Symbolic Logic, 2(2), 2–127. Henkin, L., Monk, J. D., & Tarski, A. (1971). Cylindric algebras. Part I. Amsterdam: North-Holland. ISBN 978-0-7204-2043-2. Henkin, L., & Tarski, A. (1961). Cylindric algebras. In R. P. Dilworth (Ed.), Proceedings of symposium in pure mathematics, Vol. II: Lattice theory (pp. 83–113). Manzano, M. (1983). Conferències del professor Leon Henkin de la Universitat de California (Berkeley). In Ciència. Revista catalana de Ciè ncia y tecnologia (Vol. 24). Manzano, M. (1997). Alonzo Church: His life, his work and some of his miracles. History and Philosophy of Logic, 18, 211–232. Manzano, M., & Alonso, E. (2013). Completeness: From Gödel to Henkin. HPL (History and Philosophy of Logic). doi:10.1080/01445340.2013.816555. Russell, B. (1908). Mathematical logic as based in theory of types. In J. van Heijenoort (Ed.). (1967). From Frege to Gödel. A source book in mathematical logic,1879–1931. Cambridge: Harvard University Press. Russell, B., & Whitehead, A. (1910–1913). Principia mathematica (Vols. 1–3). Cambridge, MA: Cambridge University Press. Sanders, R. (2006). Leon Henkin, advocate for diversity in math & science, has died. Press Release. UC Berkeley News. http://www.berkeley.edu/news/media/releases/2006/11/09_henkin.shtml. The Princeton Mathematics Community in the 1930s (PMC14). http://www.princeton.edu/mudd/finding_ aids/mathoral/pmc14.htm. Accessed 30 June 2013. The Princeton Mathematics Community in the 1930s (PMC19). http://www.princeton.edu/mudd/finding_ aids/mathoral/pmc19.htm. Accessed 30 June 2013.

123