William Craig

Professor William Craig (November 13, 1918–January 13, 2016) was an internationally renowned logician whose name is associated with one of the key results in the field, the Craig interpolation theorem. He played an immensely important role in the development of logic at U.C. Berkeley, and he remained an active presence in the logic community until the end of his life.

Craig was born and raised in Nuremberg, Germany. There he attended grammar school and a humanistic gymnasium until the year 1937. In July of that year, he emigrated to the United States. He enrolled at Cornell University and earned a B.A. degree in 1940, with a double major in philosophy and physics. He then attended U.C. Berkeley during the period 1940–1941 on a Howison fellowship. From 1941 to 1945 he served in the U.S. Army. After the war, he spent various amounts of time at Harvard University (1946–1948), the Swiss Federal Institute of Technology (1948– 1949), Princeton University (1949–1950), and finally Harvard University again (1950–1951), where he obtained his Ph.D. in philosophy in 1951 under the supervision of the renowned philosopher Willard van Orman Quine. In the same year he became a mathematics instructor at Pennsylvania State University, and rose through the ranks, serving as an assistant professor of mathematics from 1952 to 1957, and then as an associate professor from 1957 to 1961. In 1960–1961 he spent a year on leave at U.C. Berkeley. This led to his eventual move to U.C. Berkeley as a professor of philosophy in 1961. During his long career at Berkeley, he held several important positions, serving as chair of the Philosophy Department (1963–64), as president of the Association of Symbolic Logic (1965–1967), and as president of the Pacific Division of the American Philosophical Association (1978–1979). He retired in 1989, but remained mathematically very active until the time of his death.

Craig was an extremely thoughtful and kind individual, open and helpful to all. He generously supported logic at Berkeley, and in particular he made generous donations to the U.C. Berkeley library throughout his career. He was especially helpful to students, and his teaching—which was characterized by extraordinary thoroughness, unusual care, and dedication—might be said to have been but a reflection of the man himself. Craig had five doctoral students: Charles Howard (1965), Gonzalo Reyes (1967), Michel Jean (1968), Leonard Lipner (1970), and Yutang Lin (1983); and he served as a member of the dissertation committee for countless other students. He always took these duties very seriously, and read each thesis with meticulous care.

His main contributions to logic were at the intersection of proof theory and model theory, and later in algebraic logic. His most famous articles, [4] and [5], concerned the problem of interpolation. Craig showed that for any implication proved within the framework of first-order logic, one can interpolate a formula with the same non-logical relation symbols as occur in both the hypothesis and conclusion of the implication. For example, if ϕ is a formula in which occur the relation symbols R and S, and ψ is a formula in which occur the relation symbols R and T, and if one can prove in first-order logic that ϕ implies ψ, there there is a formula ϑ in which occurs just the relation symbol R, such that one can prove in first-order logic that ϕ implies ϑ and ϑ implies ψ (see https://en.wikipedia.org/wiki/Craig_interpolation for more details). Craig used his interpolation theorem to give simple proofs of several important results in logic, including the Beth definability theorem. Stronger versions of the interpolation theorem were later discovered by Roger Lyndon [11] and Leon Henkin [9], and since then a small industry concerning interpolation results and applications has gradually arisen. In [8], Craig gave a brief account of how he was led to the discovery of his interpolation theorem.

An earlier important result appeared in [3]. In this short paper, Craig proved that every recursively enumerable theory is recursively axiomatizable. In other words, he showed that if a mechanical procedure exists for enumerating the theorems of a theory, then the theory can be axiomatized by a set of formulas for which a mechanical procedure exists to determine whether or not a given formula is one of the axioms (see https://en.wikipedia.org/wiki/Craig’s theorem for more details). This theorem is not just of mathematical interest; it has also played an important role in philosophical debates about theoretical terms in scientific theories.

In the 1970s, Craig’s interests gradually turned toward algebraic logic, a field that is concerned with the study of algebraic versions of logic, and the relationship between algebraic and logical properties. The classic example is the algebra created by Boole in [1] and [2] for the mathematical study of the systems of logic known from antiquity and the middle ages. Starting in the late 1940s, Tarski and his collaborators developed an algebraic version of first-order logic called the theory of cylindric algebras (see, e.g., [10]). The universes of the basic algebras of the theory consist of sets of infinite sequences with coordinates coming from some base set U. The fundamental operations of these algebras are algebraic analogues of operations on first-order formulas: Boolean operations of union, intersection, and complement (corresponding to the operations of forming conjunctions, disjunctions, and negations of formulas), unary cylindrification operations C_i (corresponding to the existential quantification of a variable v_i), and distinguished diagonal elements D_ij (corresponding to atomic formulas expressing equality between variables v_i and v_j). These algebras are the models for the semantic interpretations of the theory of cylindric algebras. The syntax of the theory is algebraic and equational in nature: there are variables (intended to range over the sets of sequences in the algebras), individual constant symbols (intended to denote the diagonal elements), and symbols for the basic operations; compound expressions, or terms, are built up from variables and individual constant symbols using the symbols for the operations. Assertions are expressed by means of equations between two terms. A finite system of equational schemes axiomatizes the theory.

Craig was somewhat dissatisfied with the approach of Tarski and his collaborators. He wanted to create an algebraic version of first-order logic that was closer to what he perceived as actual mathematical practice. In particular, instead of algebras of sets of infinite sequences, he wanted to study algebras of sets of finite sequences of arbitrary length. According to Craig [6], the concern of first-order logic is with certain set-theoretical operations defined on sets of finite sequences and correlated with first order formulas. To give an example of such an operation, consider a first order formula ϕ containing a binary relation symbol R, a unary relation symbol S, and a single free variable v₄, and expressing the following: there exists a v₁ such that either S does not hold for v₁, or else R does hold for the pair v₄,v₁. The domain of the correlated operation F_ϕ is the set of all pairs R, S, where R ranges over the binary relations, and S over the unary relations, on a base set U. The value of F_ϕ on such a pair is determined by

F_ϕ(R, S)= T

if and only if T is a quinary relation on U that holds for a given sequence of five elements x₀,x₁,x₂,x₃,x₄ in U just in case, for some y₁ in U, either y₁ is not in the relation S or else the pair x₄,y₁ is in the relation R. (The reason T is a quinary relation is that the free variables in ϕ all have index less than 5.) Craig then explains how to modify F_ϕ to an “equivalent” binary operation ^∧F_ϕ mapping pairs of sets of finite sequences to sets of finite sequences.

Craig [6] selects a subcollection of primitive operations on sets of finite sequences (always from the base set U), including the Boolean operations, cylindrification operations C_i (defined on sets of finite sequences), a single diagonal element D₀₁, a unary projection operation P, and a unary operation Q that is the inverse of P. Roughly speaking he shows that the set of these primitive operations generates (by means of compositions) all of the operations correlated with first-order formulas, so it suffices to consider algebras of sets of finite sequences (from U) with the selected subcollection of primitive operations. He then introduces an algebraic language with operation symbols and individual constant symbols corresponding to the primitive operations and distinguished constants he has selected, defines an effective mapping from first-order formulas to algebraic terms in the language such that two first-order formulas ϕ and ψ with the same free variables give rise to the same correlated operations ^∧F_ϕ and ^∧F_ψ (on sets of finite sequences from U) if and only if the corresponding algebraic terms define identical operations in the algebra of sets of finite sequences (from U). Finally, he gives a list of finitely many equational axiom schemata, and proves the following completeness result: an equation between terms in the algebraic language is derivable from the axioms if and only if it is true in every algebra of sets of finite sequences. Together these results show that the algebraic theory developed by Craig captures the essential content of first-order logic. The final chapters of [6] develop other algebraic theories of logic similar in spirit to the one just described, but with operations on sets of infinite sequences, not finite sequences. Craig’s book has had a significant influence on the work of many younger logicians from all over the world who are actively engaged in modal and algebraic logic.

The ideas from [6] are extended and developed in Craig’s last published work, the memoir [7]. Here, the emphasis is on partial operations of a logical nature that are defined directly on finite sequences (from some base set U), instead of on sets of such sequences. He considers partial unary operations ^*q_i, p_ij, and e_ij on finite sequences. The first of these removes the i^th coordinate of a sequence of length n if i < n, the second interchanges the i^th and (i + 1)^st coordinates of a sequence of length n if i +1 < n, and the third is the identity function on those sequences of length n for which the i^th and i^th coordinates are equal, provided i,j < n.

Taking various subcollections S of these partial operations, he forms the involuted semigroup generated by S under the operations of forming the composition of two partial operations and the inverse of a partial operation. According to Craig [7], these are the semigroups that underlie algebraic versions of first-order logic. The main task of [7] is to give axiomatic presentations for the most important of these involuted semigroups. When he died at age 97, Craig was actively engaged in a reformulation of his theory of semigroups underlying logic.

In 2007, the Philosophy Department at U.C. Berkeley and the Group in Logic and the Methodology of Science celebrated Craig’s achievements with a conference title “Interpolations” (http://sophos.berkeley.edu/interpolations/). A special issue of Synthese (https://www.jstor.org/stable/i40010659), containing the papers read at the conference and additional contributions, was published in 2008.

Craig is survived by his four children, Ruth, Walter, Sarah, and Deborah, and his two grandchildren, Caleb Maresca and Zoe Haskell-Craig, all of whom adored him.

References

1. Boole, G.: The mathematical analysis of logic—being an essay towards a calculus of deductive reasoning. MacMillan, Barclay, and MacMillan, Cambridge, 1847, 82 pp.
2. Boole, G.: An investigation of the laws of thought on which are founded the mathematical theories of logic and probabilities. MacMillan and company, Cambridge, and Walton and Maberly, London, 1854, v + iv + 424 pp.
3. Craig, W.: Axiomatizability within a system. Journal of Symbolic Logic 18 (1953), pp. 30–32.
4. Craig, W.: Linear Reasoning. A new form of the Herbrand-Gentzen theorem. Journal of Symbolic Logic 22 (1957), pp. 250–268
5. Craig, W.: Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory. Journal of Symbolic Logic 22 (1957), pp. 269–285.
6. Craig, W.: Logic in algebraic form. Three languages and theories. Studies in logic and the foundations of mathematics 72, North Holland Publishing Company, Amsterdam, 1974, viii + 204 pp.
7. Craig, W.: Semigroups underlying first-order logic. Memoirs of the American Mathematical Society 866, American Mathematical Society, Providence, RI, 2006, xvi + 263 pp.5
8. Craig, W.: The road to two theorems of logic. Synthese 164 (2008), pp. 333-339.
9. Henkin, L.: An extension of the Craig-Lyndon interpolation theorem. Journal of Symbolic Logic 28 (1963), pp. 201–216.
10. Henkin, L., Monk, J. D., and Tarski, A.: Cylindric Algebras, Part I. Studies in logic and the foundations of mathematics 64, North-Holland Publishing Company, Amsterdam, 1971, vi + 508 pp.
11. Lyndon, R.: An interpolation theorem in the predicate calculus. Pacific Journal of Mathematics 9 (1959), pp. 129–142.

STEVEN GIVANT AND PAOLO MANCOSU, WITH THE COLLABORATION OF HAJNAL ANDRÉKA AND ISTVÁN NÉMETI.