The Association for Symbolic Logic publishes analytical reviews of selected books and articles in the field of symbolic logic. The reviews were published in The Journal of Symbolic Logic from the founding of the journal in 1936 until the end of 1999. The Association moved the reviews to this bulletin, beginning in 2000.

The Reviews Section is edited by Graham Leach-Krouse (Managing Editor), Albert Atserias, Mark van Atten, Clinton Conley, Johanna Franklin, Dugald Macpherson, Antonio Montalbán, Valeria de Paiva, Christian Retoré, Marion Scheepers, and Nam Trang. Authors and publishers are requested to send, for review, copies of books to ASL, Department of Mathematics, University of Connecticut, 341 Mansfield Road, U-1009, Storrs, CT 06269-1009, USA.

The philosophical debate on impredicativity could benefit from advances in polymorphic type theory. This is the main claim of the paper, which the author substantiates by comparing the treatment of impredicativity in Frege’s (failed) proof of referentiality, in the proof of normalisability of the polymorphic type system F, and the (failed) proof of normalisability for an inconsistent version of Martin-Löf Type Theory with an impredicative universe. The discussion offers a more nuanced and illuminating view on impredicativity than Russell’s Vicious Circle Principle (VCP), which is still a main source of reference for philosophers today.

The definition of a concept or proposition is impredicative if its formulation contains a quantifier in whose range it appears. The impredicative proposition $\forall X \varphi $ might be evaluated as true iff $\varphi [T/X]$ is true for each substitution instance T. But $\forall X \varphi $ can be a substitution instance of itself, leading to circular clauses of evaluation. The failure of Frege’s proof of referentiality is attributed to such semantic ill-foundedness. However, due to the essential role that impredicativity plays in mathematics, an extensive ban, as Russell’s VCP suggests, is too radical. The question is thus: How does one (alternatively) prove that an impredicatively defined proposition is true?

An answer is suggested in the discussion of Girard’s proof of normalisability of system F. System F is a type system that contains universal types $\Pi X.\sigma $ whose terms $\Lambda X. M^{\sigma }$ have substitution instances containing types. Because of this, a reduction step $(\Lambda X. M^{\sigma })\{\tau \} \leadsto M[\tau /X]^{\sigma [\tau /X]}$ does not necessarily lead to a reduction in term complexity. Nonetheless, normalisability can be proven using the technique of reducibility candidates. A reducibility candidate $\mathcal {R}$ for a type $\tau $ is a set of normalisable terms of $\tau $ that is closed under certain properties related to the reduction procedure. Define a reducibility predicate $Comp_{\sigma [\tau /X]}[s_{X\mapsto \mathcal {R}}]$ for a type $\sigma [\tau /X]$ inductively as a set of terms of that type, where the type variable X is assigned the reducibility candidate $\mathcal {R}$ . Let M be a term of type $\Pi X. \sigma $ . Reducibility for M can then be expressed in terms of reducibility predicates:

The crucial step here is that when performing a reduction step, the variable X is replaced not by the type $\tau $ itself, but by the reducibility candidate $\mathcal {E}$ . This procedure of systematically replacing types with sets resolves the ill-foundedness of the procedure.

Pistone points out two aspects of this procedure, which can be called epistemic harmony and epistemic transcendence. Epistemic harmony is connected to the proof theoretic criterion of harmony, according to which there is neither more nor less to be inferred in the elimination of a logical connective than what is required for its introduction. In terms of reducibility candidates, fulfilment of this criterion comes down to the provable assertion that

$$ \begin{align*} \textit{Comp}_{\sigma[\tau/X]}[s](M\{\tau\}) = \textit{Comp}_{\sigma}[s_{X\mapsto \mathcal{E}}](M\{\tau\}) \end{align*} $$

which means that the set of reducibility candidates for a substitution instance $\sigma [\tau / X]$ of a universal type $\sigma $ is the same as the set of reducibility candidates corresponding to that type when used as a premise for the type abstraction operation.

Epistemic transcendence means that the definition of a reducibility candidate cannot be formulated in the system itself (with a striking parallel to formal truth definitions), as the proof of normalisability is also a proof of consistency for the system. For an extended discussion of this, see Longo, Reflections on Concrete Incompleteness, Philosophia Mathematica, vol. 11 (2011), pp. 255–280. Furthermore, the system in which the proof is formalised closely mirrors the impredicativity of the system F itself. The author calls this type of circularity “reflecting circularity”.

Epistemic transcendence is also used to distinguish Martin-Löf’s proof from Girard’s. Even though the impredicative version of Martin-Löf Type Theory is inconsistent, reducibility candidates can still be defined and their application does reduce complexity by the above procedure. Still, due to the presence of an impredicative universe, the notion of a reducibility candidate can be formalised in the system, thereby contradicting Gödel’s second incompleteness theorem. Hence, this version of reflecting circularity, unlike Girard’s, constitutes an illicit use of impredicative resources. In order to distinguish legit from illicit use, the author conjectures that Martin-Löf’s system, by contrast, is able to formalise its own proof of normalisability.

The paper raises another particularly interesting philosophical point. System F comes with a restricted type discipline according to which terms of universal types cannot be defined by taking the individual nature of possible input types into account. In other words, terms must be defined uniformly on universal types. To illustrate this idea, the author shows how definitions by case distinctions lead to the construction of a non-normalisable term. Historically, such a notion of object-independent, i.e., generic generality, has been suggested as a remedy against the problem of impredicativity in the definition of the natural numbers (cf. Carnap, The Logicist Foundations of Mathematics in: Benacerraf and Putnam (eds.), Philosophy of Mathematics, Selected Readings (1983)). This was recently reintroduced into the philosophical debate and more closely examined in Linnebo, Generality Explained, The Journal of Philosophy, vol. 119 (2022), pp. 41–52.

True to its programmatic character, the paper raises several intriguing questions. Firstly, it offers an analysis framed in proof and type theoretic terms of the semantic problem of ill-founded evaluation clauses. How do these insights transfer back to this initial problem? Second, as the author notes, the proof of reducibility reproduces much of the impredicativity of the system that it is applied to. What is the epistemic status of the proof? For example, could the neologicist appeal to the result to justify their use of impredicative resources? Finally, the relation between genericity and constructivity is worth investigating in more detail. System F is intuitionistic, but references to genericity are also used to justify impredicative comprehension for classical theories.

For someone with a primarily philosophical background, this paper is a challenging read, but for this reviewer at least, well worth the effort. Much like the technical advances it promotes and the questions it suggests, it deserves more attention from philosophers.