This is the ninth part of a series developed through the Department of Philosophical Theology at the Institute of Lutheran Theology’s Christ School of Theology, exploring major results in modern logic and their significance for philosophical and systematic theology.
First-order logic achieved something remarkable. It gave modern mathematics and philosophy a formal language expressive enough to represent enormously complicated structures while retaining a collection of equally remarkable metatheoretical properties. Gödel proved it complete. Compactness tells us that if every finite subset of a first-order theory has a model, the whole theory has a model. The Löwenheim–Skolem theorems tell us that theories with infinite models ordinarily have models of different infinite sizes. Church and Turing showed that validity is not decidable, but valid first-order sentences can nevertheless be effectively enumerated through formal proof.
By this point in our series, however, we have also discovered the price paid for these virtues. First-order theories frequently fail to determine uniquely the structures about which we intended to speak. The Löwenheim–Skolem theorem guarantees that a first-order theory with an infinite model cannot, under the usual conditions, uniquely characterize an infinite structure up to isomorphism. If our theory has the intended natural numbers as a model, it will also have nonstandard models. If we hoped that sufficiently careful first-order axiomatization would force interpretation back onto the one structure we originally intended, model theory tells us otherwise.
One response is to strengthen the language.
In first-order logic our quantifiers range over individuals:
∀x Px.
We read this:
Every individual is P.
Second-order logic allows us also to quantify over properties and relations themselves. Thus we may write
∀X φ,
where X is not an individual variable but a predicate variable. Under the standard, or full, semantics for second-order logic, a one-place predicate variable ranges over all subsets of the domain, a two-place relation variable ranges over all sets of ordered pairs from the domain, and similarly for relations of higher arity. The apparently small move from quantifying only over objects to quantifying also over properties and relations produces a dramatic increase in expressive power.
The natural numbers provide the classic example.
First-order arithmetic can express induction only by means of an axiom schema. For every formula φx of the appropriate kind, there is a corresponding induction axiom. What first-order logic cannot say in a single sentence is that induction holds for every property whatsoever of natural numbers, because the variables of first-order logic do not range over properties.
Second-order logic can say exactly this:
∀X[(X0 ∧ ∀x(Xx → Xx⁺)) → ∀xXx].
The formula says:
For every property X, if 0 has X and whenever a number has X its successor also has X, then every natural number has X.
Under full second-order semantics, X ranges over every subset of the domain. The second-order Peano axioms consequently characterize the natural-number structure up to isomorphism. Unlike first-order Peano arithmetic, they have no nonstandard models when interpreted under full semantics. Similar resources permit second-order characterizations of other important mathematical structures, including the real numbers as a complete ordered field.
Here, then, is the promise of second-order logic. It can sometimes say what first-order logic cannot say, and because it can say more, it can sometimes constrain its models far more tightly.
This point deserves emphasis because it returns us to the problem raised by Löwenheim–Skolem. Suppose our concern is not merely to construct some structure satisfying a theory, but to characterize the intended structure uniquely up to isomorphism. First-order logic may frustrate that aspiration for principled reasons. Second-order logic can sometimes accomplish precisely what first-order logic cannot.
But the gain is not free.
The very features that give full second-order logic its greater expressive power cost us several of the great metatheorems that made first-order logic so attractive. There is no effective sound and complete proof calculus for full second-order validity. Compactness fails. The ordinary Löwenheim–Skolem results fail as well. Indeed, these failures are closely related to second-order logic's capacity to characterize structures such as the natural numbers and the real numbers categorically.
This is not an accidental defect in a formalism awaiting technical repair. If full second-order arithmetic categorically characterizes the natural numbers, it cannot at the same time possess the first-order combination of expressive limitations, compactness, and Löwenheim–Skolem behavior that generated nonstandard models in the first place. We have gained one thing partly because we have surrendered another.
The trade becomes clearer if we return to Gödel's completeness theorem. For first-order logic,
T ⊨ φ if and only if T ⊢ φ.
Every semantic consequence of T is captured by formal derivation. No corresponding effective proof system captures all validities of second-order logic under full semantics. In fact, the validities of full second-order logic are not recursively enumerable. There can therefore be no mechanical procedure which simply generates all and only the valid second-order formulas by means of a complete formal calculus.
At precisely this point Leon Henkin discovered something illuminating. If we weaken the semantics so that second-order variables do not range over all subsets and relations on the domain, but only over a specified collection of them, a completeness theorem can be recovered. These are now called Henkin or general models. Under Henkin semantics, second-order logic behaves in important respects like many-sorted first-order logic and regains familiar completeness and model-theoretic properties.
But once again the gain has a price. The categorical power associated with full second-order semantics is no longer generally available.
The resulting choice is philosophically fascinating. If we demand that the second-order quantifiers really range over all subsets and relations of the appropriate kind, we obtain the expressive strength responsible for categoricity, but lose an effective complete proof system and other first-order metatheoretical properties. If instead we restrict the ranges of those quantifiers sufficiently to recover a Henkin-style completeness theorem, much of the distinctive model-theoretic strength that attracted us to second-order logic disappears.
This raises an even deeper question: Where did the additional expressive power come from?
Under full semantics, when we say that X ranges over every property of objects in a domain D, the usual set-theoretical semantics understands this as quantification over the entire power set of D. But if the semantic apparatus must already determine what all the subsets of D are, then a great deal has been placed into the metalanguage before the object language begins its work. The categoricity achieved by full second-order logic therefore depends upon a very strong semantic interpretation of its quantifiers.
This is why some philosophers have questioned whether full second-order logic should be regarded simply as “logic” in the same sense as first-order logic. Others have argued that the additional expressive power is precisely what makes second-order logic indispensable. The dispute need not be settled here. What matters for our purposes is that stronger formal expressiveness may transfer some of the burden from axioms inside the formal theory to semantic assumptions governing the range of the quantifiers.
For theology, that observation should sound familiar.
Theologians regularly speak in ways that appear to quantify not merely over individuals but over properties and relations. Claims about identity offer a simple example. A Leibnizian principle can be represented as
∀x∀y[(∀X(Xx ↔ Xy)) → x = y].
This says:
For any objects x and y, if x and y have exactly the same properties, then x is identical with y.
Whatever one finally thinks about the metaphysics of properties or the adequacy of the principle, the logical point is clear. “Every property” is not ordinary first-order quantification. If the phrase is meant literally, we have crossed into second-order territory.
Such territory appears quickly in philosophical theology. Discussions of divine attributes, personal identity, Christology, the Trinity, essence, necessity, and the relation between nature and properties can require us to speak not merely about objects but about what may truly be predicated of objects. Second-order resources can therefore make explicit distinctions that a purely first-order language either cannot make or can reproduce only indirectly.
There is another theological attraction, however, that may be even more important. Throughout this series we have repeatedly distinguished a formal theory from its intended interpretation. Theology ordinarily does not mean to say merely that there is some model in which its sentences come out true. When it speaks about God, creation, incarnation, justification, or resurrection, it intends its assertions to concern a determinate reality.
This can make categoricity look enormously attractive.
Suppose a theological theory T admits a large family of non-isomorphic models. We might ask whether this plurality reflects genuine theological alternatives, harmless differences in representation, or simply the expressive weakness of the language in which T has been stated. Second-order resources may sometimes allow us to constrain the intended structure more sharply than first-order resources permit.
But nothing follows merely from the fact that we have moved to second-order logic. Second-order logic does not magically identify the intended theological structure. Nor does increased expressive power guarantee theological truth. We must still determine whether the predicates have been interpreted properly, whether the axioms say what the doctrine intends, and whether the semantic resources introduced by the formalism correspond to anything we are prepared to accept metaphysically.
Indeed, second-order logic sharpens rather than eliminates the problem of interpretation. With first-order logic, we worried that the axioms did not control their models tightly enough. With full second-order logic, we must additionally ask what licenses our claim to quantify over all the relevant properties and relations.
This yields an important lesson for model-theoretic theology. There are at least two ways in which a formal theory can fail to capture what we intend. Its language may be too weak to characterize the intended structure, or its semantics may achieve the desired characterization only because the intended structure has effectively been built into the semantic apparatus. The first danger is underdetermination; the second is concealed determination from the metalanguage.
Neither is solved by formalism alone.
Second-order logic therefore places philosophical theology before a genuine methodological choice. Sometimes the expressive poverty of first-order logic is a virtue. Its weakness makes possible completeness, compactness, and powerful general model theory. At other times that same weakness prevents us from saying what we actually want to say, particularly when we want to quantify over properties, characterize structures categorically, or distinguish intended from unintended interpretations more sharply.
The proper question is therefore not whether second-order logic is better than first-order logic. The question is what theological work we need the logic to do and what semantic price we are prepared to pay for allowing it to do that work.
Why It Matters for Theology
Second-order logic teaches theology that expressive power and formal tractability do not necessarily increase together. A stronger language can distinguish more, characterize more, and sometimes eliminate unintended models, while at the same time surrendering completeness, compactness, effective axiomatizability, and other properties available to first-order logic under its standard semantics.
That tradeoff matters whenever theology attempts formal reconstruction. If we restrict ourselves to first-order resources, we must accept limits upon what our theories can characterize. If we invoke full second-order resources, we must be explicit about the semantics that gives those resources their power and about the assumptions entering through the metalanguage.
The deepest lesson may therefore concern something we have encountered repeatedly throughout this series. Formal precision does not remove philosophical decisions; it makes their location clearer. Sometimes the decisive commitment lies in an axiom. Sometimes it lies in a rule of inference. Sometimes it lies in the structure selected as a model. And sometimes, as second-order logic shows with unusual clarity, it lies in what we have allowed our quantifiers to range over before the argument has even begun.
Theology should want that clarity.
Bibliographical Note
Leon Henkin's “Completeness in the Theory of Types,” Journal of Symbolic Logic 15 (1950): 81–91, established the completeness result associated with what are now called Henkin or general semantics. Stewart Shapiro's Foundations without Foundationalism: A Case for Second-Order Logic (Oxford University Press, 1991) provides an influential philosophical defense of second-order logic. Jouko Väänänen's work on second-order and higher-order logic gives a particularly useful account of full and general semantics, categoricity, and the failures of first-order compactness and Löwenheim–Skolem properties when full second-order semantics is adopted.
