The Mathematics Genealogy project is a huge database of mathematicians, where and when they got their degrees, and who their advisors were.  (There’s also a wiki-based Philosophy Genealogy.)  Nice pastime when the polar vortex keeps you from leaving the house: find famous people in your academic family tree.

If you’re in the Mathematics Genealogy, you can use Geneagrapher by David Alber to produce a graphical genealogy.  It’s pretty amazing. Here is mine (click for full size):

TIL: Mersenne and Copernicus are in that tree.

# CfP: Hilbert’s Epsilon and Tau in Logic, Informatics and Linguistics

Dates: June 10-12, 2015
Location: Montpellier, France

This workshop aims at promoting work on Hilbert’s epsilon calculus in a number of relevant fields ranging from Philosophy and Mathematics to Linguistics and Informatics. The Epsilon and Tau operators were introduced by David Hilbert, inspired by Russell’s Iota operator for definite descriptions, as binding operators that form terms from formulae. One of their main features is that substitution with Epsilon and Tau terms expresses quantification. This leads to a calculus which is a strict and conservative extension of First Order Predicate Logic. The calculus was developed for studying first order logic in view of the program of providing a rigorous foundation of mathematics via syntactic consistency proofs. The first relevant outcomes that certainly deserve a mention are the two “Epsilon Theorems” (similar to quantifiers elimination), the first correct proof of Herbrand’s theorem or the use of the Epsilon operator in Bourbaki’s Éléments de Mathématique. Nowadays the interest in the Epsilon substitution method has spread in a variety of fields: Mathematics, Logic, Philosophy, History of Mathematics, Linguistic, Type Theory, Computer science, Category Theory and others.

## Submission

The workshop welcomes submissions of up to 4 (but not less than 2) pages. Usual spacing, font and margin should be used (single-spaced, 11pt or larger, and 1 inch margin on A4 or letter size paper). Abstracts should be submitted by April 1st, 2015 as pdf files through the EasyChair conference system ( https://easychair.org/conferences/?conf=epsilon2015). An indicative list of themes that are of particular interest to the conference are (non-exhaustive):

• History of Logic
• Philosophy
• Proof theoryModel theory
• Category theory
• Type theory
• Quantification in Natural language
• Noun-Phrases Semantics
• Proof Assistants (e.g. Coq, Isabelle, … )
• Other subnectors (e.g. Russell’s iota, μ-operator, … )
Abstracts will be reviewed by members of the program committee, and, where appropriate, outside reviewers. The organizers will be responsible for making decisions partly in consultation with the program committee. Notifications will be made by May 1st, 2015.  Selected papers from the workshop will appear as a special volume in Journal of Logics and their Applications

## Important dates

May 1, 2015: Notification of acceptance
June 10-12, 2015: Workshop

## Invited speakers

Claus-Peter Wirth (University of Saarland): The descriptive operators iota, tau and epsilon – on their origin, partial and complete specification, model-theoretic semantics, practical applicability (with the support of the Hilbert Bernays Project (sponsored by IFCoLog)).

Vito Michele Abrusci (University of Roma Tre): Hilbert’s tau and epsilon in proof theory.

Hartley Slater (University of Western Australia): Linguistic and philosophical ramifications of the epsilon calculus.

## Program Committee

Daisuke Bekki (Ochanomizu University)
Stergios Chatzikyriakidis (LIRMM-CNRS & University of Montpellier)
Francis Corblin  (University of Paris-Sorbonne & Institut Jean Nicod CNRS)
Michael Gabbay (University of Cambridge)
Makoto Kanazawa (National Institute of Informatics of Tokyo)
Ruth Kempson (King’s College, London)
Alda Mari (CNRS Institut Jean Nicod & ENS & EHESS)
Georg Moser (University of Innsbruck)
Bruno Woltzenlogel Paleo (Vienna University of Technology)
Michel Parigot (CNRS-PPS & University of Paris Diderot 7)
Fabio Pasquali (University of Aix-Marseille & I2M CNRS)
Christian Retoré (University of Montpellier & LIRMM-CNRS)\
Mark Steedman
(University of Edimburgh)
Richard Zach (University of Calgary)

## Organizers / workshop co-chairs

Stergios Chatzikyriakidis, LIRMM-CNRS, University of Montpellier
Fabio Pasquali, University of Marseille
Christian Retoré, University of Montpellier & LIRMM-CNRS

Host: I2M-CNRS and University of Montpellier

# In Memoriam: Grigori Mints

Grigori (“Grisha”) Mints died unexpectedly at Stanford on May 29, 2014. Born on June 7, 1939 in what is now St. Petersburg, Russia, Mints studied at the then Leningrad State University, obtaining a Masters degree in mathematics in 1961 with a thesis on proof search in classical predicate logic, a Ph.D. in 1965 with the thesis On Predicate and Operator Variants for Building Theories of Constructive Mathematics , and a D.Sc. in 1990 with Proof Transformations and Synthesis of Programs. From 1961 to 1979, Mints was a researcher at the Leningrad Branch of the Steklov Mathematics Institute. In 1980 he was appointed to a research position at the Institute of Cybernetics in Tallinn, Estonia. In 1991 he became a professor of philosophy and, by courtesy, of mathematics and computer science at Stanford University. Mints was elected to the Estonian Academy of Sciences in 2008 and to the American Academy of Arts and Sciences in 2010.

Mints’ research spanned several areas, with many interconnections. The grand unifying theme in his oeuvre was proof theory and constructivism, but entangled with this came a lifelong interest in computational logic as well as special attention for two specific areas: intuitionistic logic and modal logic.

Mints was trained in the Russian school of constructive mathematics of Markov and of his teacher Nikolai Shanin. In this paradigm, all mathematical objects should be defined in a finite language, and every proof of existence should provide an algorithm, where properties of the algorithm are to be proved by constructive principles including Markov’s schema. In tandem with this foundational view concerning mathematics, Shanin’s group at Steklov also worked on practical automated reasoning, with an emphasis on generating natural proofs, where ‘natural’ included making sense from the perspective of a human agent. This mixture of proof theory and computation led to inventions such as the inverse method, a style of analyzing provability similar to resolution, developed in 1964 by Sergei Maslov, a close friend of Mints.

Combining proof theory and computation naturally leads to a study of intuitionistic logic, and the most significant results of Mints’ first period concern this interface. They include an extension of Herbrand’s theorem to intuitionistic predicate logic (1962), and a proof of the undecidability of intuitionistic predicate logic with a single unary predicate (1965, a classical paper joint with Maslov and Orevkov). Some of these results are still under active investigation. Mints’ paper of 1968 on decidability of a certain fragment of the Gentzen system LJ introduced what is now called the “Mints hierarchy” of intuitionistic first-order formulas. Complexity properties of Mints classes are still under investigation (e.g., in recent works by Schubert, Urzyczyn, et al.), since they are important to understanding constructive type-theoretic proof assistants such as Coq. Also noteworthy is Mints’ proof in 1974 that familiar procedures for extracting programs from existence proofs in intuitionistic arithmetic produce equivalent algorithms.

In subsequent years, Mints turned to the study of relationships between proof theory and category theory. He used proof-theoretic methods to simplify proofs in category theory and to prove new theorems. Three key papers appeared in 19771980 in Russian (English translations in G. Mints, Selected Papers in Proof Theory, Bibliopolis and North-Holland, 1992). In particular, Mints gave a clear exposition of Lambek’s results connecting Cartesian closed categories and intuitionistic logic using a novel technique of encoding proofs as explicit proof-terms, an idea that has entered categorical logic itself, and that reemerged in modern manifestations such as Artemov’s justification logic. Important results obtained by Mints with this style of analysis include normalization and coherence theorems.

Mints retained his fundamental proof-theoretic interests throughout, witness his longstanding work on Hilbert’s epsilon calculus to subsystems of analysis right through his Stanford period.

During his stay in Estonia, Mints was actively involved with automated deduction. While in Tallinn, he studied the mathematical principles behind the program synthesizer PRIZ, designed by a group at the Institute of Cybernetics led by Enn Tyugu. Mints came up with an example that PRIZ could not handle, leading to an improvement of the algorithm for which Mints established completeness (1982, joint with Tyugu).

This applied work was based on Mints’ earlier research in proof theory for intuitionistic logic. But he also proved a large number of pure results in the area of intuitionism. These include his proof of Novikov’s hypothesis that a Tarski-style translation from Heyting arithmetic to modal arithmetic is faithful (1978). This result fits in an important line of system embeddings, whose later highlights include Flagg and Friedman (1984). Another long-standing interest of Mints in this area were interpolation theorems. An error in the interpolation proof by Lopez-Escobar for intuitionistic first-order logic with constant domains was found by him in 1983, and a recent joint paper with Olkhovikov and Urquhart (2012) finally produced a concrete and instructive counter-example. Mints’ book A Short Introduction to Intuitionistic Logic (2000) is a delightful introduction to the field with many original perspectives.

A natural step leads from intuitionism to modal logic. Mints was the first logician in the Soviet Union to work in modal logic, an exotic area in the 1960s. His first papers (1968-1969) addressed proof theory and decidability of first-order modal logics: in particular, he gave a cut-free sequent calculus for first-order S5 with equality. He also independently introduced the standard translation from modal to classical formulas, one of the main tools in contemporary modal logic. In 1974 he wrote an overview of modal logic in the period 1965-1973 including some of his own results (later transformed into the book A Short Introduction to Modal Logic, 1992).

In the 2000s, Mints proposed a study of basic laws of topology and of dynamical systems over these in a modal language. His results from this period include new proofs (some with Ting Zhang) of the completeness of S4 for the open unit interval and for Cantor space, and for the completeness of the basic dynamic topological logic S4C in Cantor space. Much of this work was collected in a chapter in the Handbook of Spatial Logics (2007), written by Mints and his collaborator Phil Kremer, which put this research program on the map. Recent new directions in his work included work on cut-elimination in fragments of the modal mu-calculus (2012).

Looking back at Mints’ work one sees a unity of themes and style that connected logic, mathematics, and computer science in many innovative ways. In addition he had a unique charm, formed by Russian and later on also by American culture, and a generous and encouraging intellectual attitude that exerted a strong positive influence on his colleagues, from America to Russia, and on successive generations of students until this very period. Many people owe him great ideas that set them on their paths, which he gave unstintingly, as well as help at crucial stages in their career.

# Previously Unknown Turing Manuscript Going to Auction

You may have heard that a notebook by Alan Turing, which he left to Robin Gandy, is going to auction in April. Bonham’s, the auction house, has kindly permitted me to share the auction catalog.

22795_turing

The notebook apparently dates from around 1944. The mathematical content is divided into two parts, one on Peano’s axioms (judging from the few samples in the catalog, in what looks like Principia notation), the other on “notation,” specifically variables.  He quotes from Weyl’s 1939 book Classical Groups, where Weyl introduces polynomials as “a formal expression $$f(x) = \sum_{i=0}^n \alpha_i x^i$$ involving the ‘indeterminate’ (or variable) $$x$$ whose coefficients $$\alpha_i$$ are numbers in a field $$k$$.” Turing writes:

The idea of of an “indeterminate” is distinctly subtle, I would almost say too subtle. It is not (at any rate as van der Waerden sees it) the same as a variable. Polynomials in an indeterminate $$x$$, $$f_1(x)$$ and $$f_2(x)$$, would not be considered identical if $$f_1(x) = f_2(x)$$ all $$x$$ in $$k$$, but the coefficients differed. They are in effect the array of coefficients, with rules for multiplication and addition suggested by their form.

I am inclined to the view that this is too subtle and makes an inconvenient definition. I prefer the indeterminate $$k$$ [possibly should be $$x$$?] be just the variable.

Turing’s worry is clear enough. If the $$x$$ in the polynomial is a variable, then the polynomial is determined by its values for all variables, essentially, as a function on $$k$$. But identity conditions for polynomials are more fine grained.  I’m not sure, though, why he thinks this is “too subtle” or why he prefers “the indeterminate be just the variable.” Anyway, it is subtle, and I don’t know if logicians (or algebraists for that matter) by that time commonly made the distinction clearly.  When did people start talking about free algebras on generators $${x, \dots}$$?

The other detail from the manuscript included in the catalog concerns Leibniz’s $$dy/dx$$ notation.  Here, too, he seems to be concerned essentially with the role the symbol “$x$” plays in mathematical notation: is it a variable, so that this notation, as he puts it, has “laid down a relation  between $$x$$ and $$y$$” (i.e., between their values), and that a polynomial is just a special kind of specification of a function? Or are they indeterminate symbols, and polynomials are certain sequences involving these variables?  In other words, do the variables belong to the mathematical metalanguage used to describe mathematical objects, or are they symbols in a formal object language?

Frustrating that we don’t have more to look at!  If you have a few mil lying around and are going to buy this, please share with the poor scholars.

# Carnap (and Goodman and Quine) and Linguistics (Guest post by Darin Flynn)

(This is a guest post by my linguistics colleague Darin Flynn)

I was intrigued by your last post—that Carnap (apparently) gave serious consideration to suggestions by Gödel and Behmann that he use “semantics” rather than “syntax” in the title of his 1934 book. The story we’re told in linguistics is that Carnap learned to love semantics (e.g. 1939, 1942, 1947/1956) only after logicians (notably Tarski) showed it to be competitive with logical syntax, but his goal in the early 30s was precisely to develop a formal theory of language (though not of natural language) based on syntax rather than semantics—not just because the latter had a less reputable scientific status at the time, but also because Carnap considered only the first part of the familiar linguistic form/meaning dichotomy to be properly formal:

“A theory, a rule, a definition, or the like is to be called formal when no reference is made in it either to the meaning of the symbols (for example, the words) or to the sense of the expressions (e.g. the sentences), but simply and solely to the kinds and order of the symbols from which the expressions are constructed.” (p. 1)

Some of America’s most important theoretical linguists—notably Leonard Bloomfield, Zellig Harris and Noam Chomsky—believed linguistics to be about form rather than meaning, so were impressed by Carnap’s semantics-free theorizing, and by his first example, “Pirots karulize elatically” (p. 2). The latter demonstrated that a sentence could be analyzed as well-formed phonologically, morphologically and syntactically in the absence of meaning. Carnap also used this pseudo-sentence to illustrate “logical syntax” (e.g. deduction): “A is a Pirot” ∴ “A karulizes elatically”. Crucially, “neither the meaning of the words nor the sense of these three sentences need be known” (p. 3).

Chomsky was suspicious of Carnap’s “syntactically” defined logical deductions (semantics in sheep’s clothing?), but was otherwise (like his former mentor, Harris) a careful and appreciative reader of Carnap, and of Goodman’s and Quine’s takes on Carnap. As Heitner (2005) describes in “An odd couple: Chomsky and Quine on reducing the phoneme”:

“Chomsky’s early philosophical interaction with Nelson Goodman (1906–1998) and Morton White (b. 1917)—two prominent figures within analytic philosophy of language deeply suspicious of an uncritical reliance on “meaning” in philosophy—with whom he took graduate classes with as an undergraduate is no doubt also relevant. After all, it was Goodman who recommended Chomsky for a Junior Fellowship in the Society of Fellows at Harvard where Chomsky would come into close contact with an elite Harvard philosophical circle revolving around Goodman and Quine… Chomsky recalls how “studying at Penn with Zellig Harris and Nelson Goodman was a highly stimulating experience”; a “remarkable opportunity” where he spent “a good deal of time in courses, seminars, discussions, primarily with philosophers at Harvard—Quine, Austin (who was visiting Harvard then), White, and others… a very lively and stimulating period in the Cambridge area for a student with my particular interests” (p. 17). … [I]n addition to these interpersonal relations, others have also detected a significant line of intellectual descent connecting Chomsky to Quine through the influence of Goodman, and through Goodman and Quine, to the philosophical heritage of Rudolph [sic] Carnap (1891–1970)—one of the leading positivist figures of the Vienna Circle of Logical Empiricism. For while Otero (1994, vol. II) reports that among non-American philosophers, it was only Rudolf Carnap whom Chomsky read as a student (p. 3), Tomalin (2002, 2003) has more recently provided valuable research documenting the distinctive Carnapian aspirations and “constructive nominalist” methodology adopted throughout Chomsky’s early formulations of generative grammar as reflected in The Logical Structure of Linguistic Theory (1955/1975) and his first published paper “Systems of Syntactic Analysis” (1953). According to Tomalin, Chomsky’s early commitment to constructing formal systems of syntactic analysis independent of semantic information is traceable to the empiricist methodology of Carnap and the meta-mathematical efforts of Goodman and Quine to devise a formal system for mathematics without appeal to abstract objects (2003, p. 1236). (See Newmeyer (1996, p. 15) for similar considerations.) In fact, in “Logical Syntax and Semantics, Their linguistic relevance” Chomsky (1955a, p. 36) favorably references Quine’s (1953) extremely influential critiques of meaning, and even explicitly defends Quine’s anti-mentalistic philosophy in The Logical Structure of Linguistic Theory.” (p. 2-3)

For instance, compare Carnap’s quotation above with Chomsky’s in The Logical Structure of Linguistic Theory (the title of which may plausibly be construed as a mashup of Carnap’s The Logical Structure of the World & The Logical Syntax of Language): “In the strict sense of the word, an argument, a characterization, a theory, etc. is ‘formal’ if it deals with form as opposed to meaning, that is, if it deals solely with the shape and arrangement of symbols” (1955/1975, p. 83). Compare, too, Chomsky’s “Colorless green ideas sleep furiously” with Carnap’s pseudo-sentence. According to Tomalin (2006), these are examples among many of Carnap’s influence on Chomsky and on his former mentor, Harris. Another notable example: “the transformations developed by Harris and Chomsky were related to the transformation rules presented in (the English translation of) Carnap LST” (p. 168).

Tomalin’s research on the philosophical and historical background of transformational generative grammar is fascinating—particularly his original attention to Carnap, and Goodman’s modifications. For critical reviews, see especially Scholz & Pullum (2007) “Tracking the origins of transformational generative grammar” and Seuren (2009) “Concerning the roots of transformational generative grammar” [sorry, this one’s paywalled 🙁 -RZ].

# Carnap on “Syntax” vs “Semantics”

Carnap’s Logical Syntax of Language actually deals with semantic notions such as “analytic.”  Why, then, didn’t he call it “semantics”?

When the project was still in its early stages, Carnap sent a manuscript entitled “Metalogik” to Heinrich Behmann.  Behmann objected to the title and suggested as alternatives first “Logic of Language” and then “Semantics.” Carnap replied:

I like the term “semantics”; Gödel also suggested it.  Neurath, on the other hand, thinks it is unappealing and pedantic; he suggests “syntax.” In order to avoid confusion with syntax in philology, one would probably have to often call it “logical syntax.”

Der Terminus “Semantik” sagt mir zu; auch Gödel schlug ihn gleichzeitig vor. Neurath aber findet ihn unsymphatisch und gelehrtenhaft; er schlägt “Syntax” vor. Zur Vermeidung der Verwechslung mit der philologischen S. müsste man dann wohl häufig “logische Syntax” sagen.

(Carnap to Behmann, April 17, 1932)