In the context of proliferation of many logical systems in the area of mathematical logic and computer science, we present a generalization of forcing in institution-independent model theory which is used to prove two abstract results: Downward Löwenheim-Skolem Theorem and Omitting Types Theorem . We instantiate these general results to many first-order logics, which are, roughly speaking, logics whose sentences can be constructed from atomic formulas by means of Boolean connectives and classical first-order quantifiers. These include first-order logic , logic (...) of order-sorted algebras , preorder algebras , as well as their infinitary variants \ , \ , \ . In addition to the first technique for proving OTT, we develop another one, in the spirit of institution-independent model theory, which consists of borrowing the Omitting Types Property from a simpler institution across an institution comorphism. As a result we export the OTP from FOL to partial algebras and higher-order logic with Henkin semantics , and from the institution of \ to \ and \ . The second technique successfully extends the domain of application of OTT to non conventional logical systems for which the standard methods may fail. (shrink)

We define a new class of Kripke structures for the second-order λ-calculus, and investigate the soundness and completeness of some proof systems for proving inequalities as well as equations. The Kripke structures under consideration are equipped with preorders that correspond to an abstract form of reduction, and they are not necessarily extensional. A novelty of our approach is that we define these structures directly as functors A: → Preor equipped with certain natural transformations corresponding to application and abstraction . We (...) make use of an explicit construction of the exponential of functors in the Cartesian-closed category Preor, and we also define a kind of exponential ΠΦs ε T to take care of type abstraction. However, we strive for simplicity, and we only use very elementary categorical concepts. Consequently, we believe that the models described in this paper are more palatable than abstract categorical models which require much more sophisticated machinery . We obtain soundness and completeness theorems that generalize some results of Mitchell and Moggi to the second-order λ-calculus, and to sets of inequalities. (shrink)

We develop a semantics for independence logic with respect to what we will call general models. We then introduce a simpler entailment semantics for the same logic, and we reduce the validity problem in the former to the validity problem in the latter. Then we build a proof system for independence logic and prove its soundness and completeness with respect to entailment semantics.

We investigate mathematical structures that provide natural semantics for families of (quantified) non-classical logics featuring special unary connectives, known as recovery operators, that allow us to ‘recover’ the properties of classical logic in a controlled manner. These structures are known as topological Boolean algebras, which are Boolean algebras extended with additional operations subject to specific conditions of a topological nature. In this study, we focus on the paradigmatic case of negation. We demonstrate how these algebras are well-suited to provide a (...) semantics for some families of paraconsistent Logics of Formal Inconsistency and paracomplete Logics of Formal Undeterminedness. These logics feature recovery operators used to earmark propositions that behave ‘classically’ when interacting with non-classical negations. Unlike traditional semantical investigations, which are carried out in natural language (extended with mathematical shorthand), our formal meta-language is a system of higher-order logic (HOL) for which automated reasoning tools exist. In our approach, topological Boolean algebras are encoded as algebras of sets via their Stone-type representation. We use our higher-order meta-logic to define and interrelate several transformations on unary set operations, which naturally give rise to a topological cube of opposition. Additionally, our approach enables a uniform characterization of propositional, first-order and higher-order quantification, including restrictions to constant and varying domains. With this work, we aim to make a case for the utilization of automated theorem proving technology for conducting computer-supported research in non-classical logics. All the results presented in this paper have been formally verified, and in many cases obtained, using the Isabelle/HOL proof assistant. (shrink)

We present Property Theory with Curry Typing (PTCT), an intensional first-order logic for natural language semantics. PTCT permits fine-grained specifications of meaning. It also supports polymorphic types and separation types. We develop an intensional number theory within PTCT in order to represent proportional generalized quantifiers like “most.” We use the type system and our treatment of generalized quantifiers in natural language to construct a type-theoretic approach to pronominal anaphora that avoids some of the difficulties that undermine previous type-theoretic analyses of (...) this phenomenon. (shrink)

There is an extensive literature related to the algebraization of first‐order logic. But the algebraization of full second‐order logic, or Henkin‐type second‐order logic, has hardly been researched. The question arises: what kind of set algebra is the algebraic version of a Henkin‐type model of second‐order logic? The question is investigated within the framework of the theory of cylindric algebras. The answer is: a kind of cylindric‐relativized diagonal restricted set algebra. And the class of the subdirect products of these set algebras (...) is the algebraization of Henkin‐type second‐order logic. It is proved that the algebraization of a complete calculus of the Henkin‐type second‐order logic is a class of a kind of diagonal restricted cylindric algebras. Furthermore, the connection with the non‐standard enlargements of standard complete second‐order structures is investigated. (shrink)

Simple type theory is a higher-order predicate logic for reasoning about truth values, individuals, and simply typed total functions. We present in this paper a version of simple type theory, called PF*, in which functions may be partial and types may have subtypes. We define both a Henkin-style general models semantics and an axiomatic system for PF*, and we prove that the axiomatic system is complete with respect to the general models semantics. We also define a notion of an interpretation (...) of one PF* theory in another. PF* is intended as a foundation for mechanized mathematics. It is the basis for the logic of , an Interactive Mathematical Proof System developed at The MITRE Corporation. (shrink)

Simple type theory is a higher-order predicate logic for reasoning about truth values, individuals, and simply typed total functions. We present in this paper a version of simple type theory, called PF*, in which functions may be partial and types may have subtypes. We define both a Henkin-style general models semantics and an axiomatic system for PF*, and we prove that the axiomatic system is complete with respect to the general models semantics. We also define a notion of an interpretation (...) of one PF* theory in another. PF* is intended as a foundation for mechanized mathematics. It is the basis for the logic of, an Interactive Mathematical Proof System developed at The MITRE Corporation. (shrink)

First, the paper argues that Tarski's theory of language levels is best understood not only as a method for avoiding semantic paradoxes by rigidly restricting the expressive power of a language, but as a natural expression of an epistemological process of reflection which is more adequately understood as a process and not by its result. Second, it is argued that the apparent philosophical controversy between materialism and idealism dissolves whithin this process of reflection. If one has raised above the lowest (...) level, one always is a materialist as well as an idealist; however, one is so in relation to different levels. (shrink)

The criterion of naturalness represents David Lewis’s attempt to answer some of the sceptical arguments in semantics by comparing the naturalness of meaning candidates. Recently, the criterion has been challenged by a new sceptical argument. Williams argues that the criterion cannot rule out the candidates which are not permuted versions of an intended interpretation. He presents such a candidate – the arithmetical interpretation semantics by comparing the naturalness of meaning candidates. Recently, the criterion has been challenged by a new sceptical (...) argument. Williams argues that the criterion cannot rule out the candidates which are not permuted versions of an intended interpretation. He presents such a candidate – the arithmetical interpretation, and he argues that it opens up the possibility of Pythagorean worlds, i.e. the worlds similar to ours in which the arithmetical interpretation is the best candidate for a semantic theory. The aim of this paper is a) to reconsider the general conditions for the applicability of Lewis’s criterion of naturalness and b) to show that Williams’s new sceptical challenge is based on a problematic assumption that the arithmetical interpretation is independent of fundamental properties and relations. As I show, if the criterion of naturalness is applied properly, it can respond even to the new sceptical challenge. (shrink)

This paper is an investigation of the general logic of "identifications", claims such as 'To be a vixen is to be a female fox', 'To be human is to be a rational animal', and 'To be just is to help one's friends and harm one's enemies', many of which are of great importance to philosophers. I advocate understanding such claims as expressing higher-order identity, and discuss a variety of different general laws which they might be thought to obey. [New version: (...) Nov. 4th, 2016]. (shrink)

A common aim of elimination problems for languages of logic is to express the entire content of a set of formulas of the language, or a certain part of it, in a way that is more elementary or more informative. We want to bring out that as the languages for logic grew in expressive power and, at the same time, our knowledge of their expressive limitations also grew, elimination problems in logic underwent some change. For languages other than that for (...) monadic second-order logic, there remain important open problems. (shrink)

Schrödinger logics are logical systems in which the principle of identity is not true in general. The intuitive motivation for these logics is both Erwin Schrödinger's thesis that identity lacks sense for elementary particles of modern physics, and the way which physicists deal with this concept; normally, they understand identity as meaning indistinguishability . Observing that these concepts are equivalent in classical logic and mathematics, which underly the usual physical theories, we present a higher-order logical system in which these concepts (...) are systematically separated. A 'classical' semantics for the system is presented and some philosophical related questions are mentioned. One of the main characteristics of our system is that Leibniz' Principle of the Identity of Indiscernibles cannot be derived. This fact is in accordance with some authors who maintain that quantum mechanics violates this principle. Furthermore, our system may be viewed as a way of making sense some of Schrödinger's logical intuitions about the nature of elementary particles. (shrink)

The general theory of variable binding term operators is an interesting recent development in logic. It opens up a rich class of semantic and model-theoretic problems. In this paper we survey the recent literature on the topic, and offer some remarks on its significances and on its connections with other branches of mathematical logic.

In this paper we study the logic $\mathcal{L}^\lambda_{\omega\omega}$, which is first-order logic extended by quantification over functions . We give the syntax of the logic as well as the semantics in Heyting categories with exponentials. Embedding the generic model of a theory into a Grothendieck topos yields completeness of $\mathcal{L}^\lambda_{\omega\omega}$ with respect to models in Grothendieck toposes, which can be sharpened to completeness with respect to Heyting-valued models. The logic $\mathcal{L}^\lambda_{\omega\omega}$ is the strongest for which Heyting-valued completeness is known. Finally, (...) we relate the logic to locally connected geometric morphisms between toposes. (shrink)

In this paper we study the logic , which is first-order logic extended by quantification over functions (but not over relations). We give the syntax of the logic as well as the semantics in Heyting categories with exponentials. Embedding the generic model of a theory into a Grothendieck topos yields completeness of with respect to models in Grothendieck toposes, which can be sharpened to completeness with respect to Heyting-valued models. The logic is the strongest for which Heyting-valued completeness is known. (...) Finally, we relate the logic to locally connected geometric morphisms between toposes. (shrink)

Natural language semanticists have often found it useful to assume that all expressions denote sets of values. The approach is most prominent in the study of questions and prosodic focus, but also common in work on indefinites, disjunction, negative polarity, and scalar implicature. However, the most popular compositional implementation of this idea is known to face technical obstacles in the presence of object-language binding constructs, including, chiefly, lambda abstraction. The problem has been well-described on several occasions in the literature, and (...) in fact several solutions have been explored. This paper seeks to formalize the challenge of defining an indeterminate semantics for binding operators, and to formally establish the intuition that the challenge is in fact insurmountable. The primary benefit to this exercise is that it offers an abstract characterization of what it means to lift an operation from one semantic space to another, a notion which may be applied to domains having nothing to do with sets of alternatives. (shrink)

A ground-motive for this study of some historical and metaphysical implications of the diagonal lemmas of Cantor and Gödel is Cantor's insightful remark to Dedekind in 1899 that the Inbegriff alles Denkbaren (aggregate of everything thinkable) might, like some class-theoretic entities, be inkonsistent. In the essay's opening sections, I trace some recent antecedents of Cantor's observation in logical writings of Bolzano and Dedekind (more remote counterparts of his language appear in the First Critique), then attempt to relativize the notion of (...) Inkonsistenz to self-sufficient theories T which interpret themselves. In effect, I argue that Gödel's diagonal lemma suggests a sense in which metatheoretic notions of proof, well-foundeness and satisfaction are object-theoretically inkonsistent. With respect to Cantor's Inbegriff, for example, the lemma yields that any object-theoretic reconstruction of thinkability generates an antidiagonal sentence , which one can paraphrase asSelf-referential application of the assertion that. (shrink)

This paper examines the connection between model-theoretic truth and necessary truth. It is argued that though the model-theoretic truths of some standard languages are demonstrably ''''necessary'''' (in a precise sense), the widespread view of model-theoretic truth as providing a general guarantee of necessity is mistaken. Several arguments to the contrary are criticized.

We present an embedding of quantified multimodal logics into simple type theory and prove its soundness and completeness. A correspondence between QKπ models for quantified multimodal logics and Henkin models is established and exploited. Our embedding supports the application of off-the-shelf higher-order theorem provers for reasoning within and about quantified multimodal logics. Moreover, it provides a starting point for further logic embeddings and their combinations in simple type theory.

We study straightforward embeddings of propositional normal multimodal logic and propositional intuitionistic logic in simple type theory. The correctness of these embeddings is easily shown. We give examples to demonstrate that these embeddings provide an effective framework for computational investigations of various non-classical logics. We report some experiments using the higher-order automated theorem prover LEO-II.

Gabbay has gathered an enormous amount of results; some of them important and novel, others important but already known, many rather routine, however. The organization of this material shows grave defects, both in the exposition and in its logical structure. Intensional logic appears as a vast collection of (often duplicated) loosely connected results. This may be a true reflection of the present state of the subject, but it does not contribute to a better understanding of it, let alone advance it.

A semantic embedding of quantified conditional logic in classical higher-order logic is utilized for reducing cut-elimination in the former logic to existing results for the latter logic. The presented embedding approach is adaptable to a wide range of other logics, for many of which cut-elimination is still open. However, special attention has to be payed to cut-simulation, which may render cut-elimination as a pointless criterion.

We investigate several approaches to resolution based automated theoremproving in classical higher-order logic (based on Church's simply typedλ-calculus) and discuss their requirements with respect to Henkincompleteness and full extensionality. In particular we focus on Andrews' higher-order resolution (Andrews 1971), Huet's constrained resolution (Huet1972), higher-order E-resolution, and extensional higher-order resolution(Benzmüller and Kohlhase 1997). With the help of examples we illustratethe parallels and differences of the extensionality treatment of these approachesand demonstrate that extensional higher-order resolution is the sole approach thatcan completely avoid (...) additional extensionality axioms. (shrink)

We explore the view that Frege's puzzle is a source of straightforward counterexamples to Leibniz's law. Taking this seriously requires us to revise the classical logic of quantifiers and identity; we work out the options, in the context of higher-order logic. The logics we arrive at provide the resources for a straightforward semantics of attitude reports that is consistent with the Millian thesis that the meaning of a name is just the thing it stands for. We provide models to show (...) that some of these logics are non-degenerate. (shrink)

In this paper the logic of broad necessity is explored. Definitions of what it means for one modality to be broader than another are formulated, and it is proven, in the context of higher-order logic, that there is a broadest necessity, settling one of the central questions of this investigation. It is shown, moreover, that it is possible to give a reductive analysis of this necessity in extensional language. This relates more generally to a conjecture that it is not possible (...) to define intensional connectives from extensional notions. This conjecture is formulated precisely in higher-order logic, and concrete cases in which it fails are examined. The paper ends with a discussion of the logic of broad necessity. It is shown that the logic of broad necessity is a normal modal logic between S4 and Triv, and that it is consistent with a natural axiomatic system of higher-order logic that it is exactly S4. Some philosophical reasons to think that the logic of broad necessity does not include the S5 principle are given. (shrink)

This paper is the second in a two-part series in which we discuss several notions of completeness for systems of mathematical axioms, with special focus on their interrelations and historical origins in the development of the axiomatic method. We argue that, both from historical and logical points of view, higher-order logic is an appropriate framework for considering such notions, and we consider some open questions in higher-order axiomatics. In addition, we indicate how one can fruitfully extend the usual set-theoretic semantics (...) so as to shed new light on the relevant strengths and limits of higher-order logic. (shrink)

The question “what is an interpretation?” is often intertwined with the perhaps even harder question “what is a scientific theory?”. Given this proximity, we try to clarify the first question to acquire some ground for the latter. The quarrel between the syntactic and semantic conceptions of scientific theories occupied a large part of the scenario of the philosophy of science in the 20th century. For many authors, one of the two currents needed to be victorious. We endorse that such debate, (...) at least in the terms commonly expressed, can be misleading. We argue that the traditional notion of “interpretation” within the syntax/semantic debate is not the same as that of the debate concerning the interpretation of quantum mechanics. As much as the term is the same, the term “interpretation” as employed in quantum mechanics has its meaning beyond (pure) logic. Our main focus here lies on the formal aspects of the solutions to the measurement problem. There are many versions of quantum theory, many of them incompatible with each other. In order to encompass a wider variety of approaches to quantum theory, we propose a different one with an emphasis on pure formalism. This perspective has the intent of elucidating the role of each so-called “interpretation” of quantum mechanics, as well as the precise origin of the need to interpret it. (shrink)

We show that basic hybridization (adding nominals and @ operators) makes it possible to give straightforward Henkin-style completeness proofs even when the modal logic being hybridized is higher-order. The key ideas are to add nominals as expressions of type t, and to extend to arbitrary types the way we interpret $@_i$ in propositional and first-order hybrid logic. This means: interpret $@_i\alpha _a$ , where $\alpha _a$ is an expression of any type $a$ , as an expression of type $a$ that (...) rigidly returns the value that $\alpha_a$ receives at the i-world. The axiomatization and completeness proofs are generalizations of those found in propositional and first-order hybrid logic, and (as is usual inhybrid logic) we automatically obtain a wide range of completeness results for stronger logics and languages. Our approach is deliberately low-tech. We don’t, for example, make use of Montague’s intensional type s, or Fitting-style intensional models; we build, as simply as we can, hybrid logicover Henkin’s logic. (shrink)

We show that basic hybridization makes it possible to give straightforward Henkin-style completeness proofs even when the modal logic being hybridized is higher-order. The key ideas are to add nominals as expressions of type t, and to extend to arbitrary types the way we interpret \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$@_i$\end{document} in propositional and first-order hybrid logic. This means: interpret \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$@_i\alpha _a$\end{document}, where \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} (...) \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$\alpha _a$\end{document} is an expression of any type \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$a$\end{document}, as an expression of type \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$a$\end{document} that rigidly returns the value that \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$\alpha_a$\end{document} receives at the i-world. The axiomatization and completeness proofs are generalizations of those found in propositional and first-order hybrid logic, and we automatically obtain a wide range of completeness results for stronger logics and languages. Our approach is deliberately low-tech. We don’t, for example, make use of Montague’s intensional type s, or Fitting-style intensional models; we build, as simply as we can, hybrid logicover Henkin’s logic. (shrink)

While second-order quantifiers have long been known to admit nonstandard, or interpretations, first-order quantifiers (when properly viewed as predicates of predicates) also allow a kind of interpretation that does not presuppose the full power-set of that interpretationgeneral” interpretations for (unary) first-order quantifiers in a general setting, emphasizing the effects of imposing various further constraints that the interpretation is to satisfy.

This paper presents a formalization of first-order arithmetic characterizing the natural numbers as abstracta of the equinumerosity relation. The formalization turns on the interaction of a nonstandard cardinality quantifier with an abstraction operator assigning objects to predicates. The project draws its philosophical motivation from a nonreductionist conception of logicism, a deflationary view of abstraction, and an approach to formal arithmetic that emphasizes the cardinal properties of the natural numbers over the structural ones.

Henry Leonard and Karel Lambert first introduced so-called presupposition-free (or just simply: free) logics in the 1950’s in order to provide a logical framework allowing for non-denoting singular terms (be they descriptions or constants) such as “the largest prime” or “Pegasus” (see Leonard [1956] and Lambert [1960]). Of course, ever since Russell’s paradigmatic treatment of definite descriptions (Russell [1905]), philosophers have had a way to deal with such terms. A sentence such as “the..

This paper investigates the “general” semantics for first-order logic introduced to Antonelli, 637–58, 2013): a sound and complete axiom system is given, and the satisfiability problem for the general semantics is reduced to the satisfiability of formulas in the Guarded Fragment of Andréka et al. :217–274, 1998), thereby showing the former decidable. A truth-tree method is presented in the Appendix.

We take a fresh look at the logics of informational dependence and independence of Hintikka and Sandu and Väänänen, and their compositional semantics due to Hodges. We show how Hodges’ semantics can be seen as a special case of a general construction, which provides a context for a useful completeness theorem with respect to a wider class of models. We shed some new light on each aspect of the logic. We show that the natural propositional logic carried by the semantics (...) is the logic of Bunched Implications due to Pym and O’Hearn, which combines intuitionistic and multiplicative connectives. This introduces several new connectives not previously considered in logics of informational dependence, but which we show play a very natural rôle, most notably intuitionistic implication. As regards the quantifiers, we show that their interpretation in the Hodges semantics is forced, in that they are the image under the general construction of the usual Tarski semantics; this implies that they are adjoints to substitution, and hence uniquely determined. As for the dependence predicate, we show that this is definable from a simpler predicate, of constancy or dependence on nothing. This makes essential use of the intuitionistic implication. The Armstrong axioms for functional dependence are then recovered as a standard set of axioms for intuitionistic implication. We also prove a full abstraction result in the style of Hodges, in which the intuitionistic implication plays a very natural rôle. (shrink)

In the tradition of Denotational Semantics one usually lets program constructs take their denotations in reflexive domains, i.e. in domains where self-application is possible. For the bulk of programming constructs, however, working with reflexive domains is an unnecessary complication. In this paper we shall use the domains of ordinary classical type logic to provide the semantics of a simple programming language containing choice and recursion. We prove that the rule of {\em Scott Induction\/} holds in this new setting, prove soundness (...) of a Hoare calculus relative to our semantics, give a direct calculus ${\cal C}$ on programs, and prove that the denotation of any program $P$ in our semantics is equal to the union of the denotations of all those programs $L$ such that $P$ follows from $L$ in our calculus and $L$ does not contain recursion or choice. (shrink)

This three-part chapter explores a higher-order logic we call ‘Classicism’, which extends a minimal classical higher-order logic with further axioms which guarantee that provable coextensiveness is sufficient for identity. The first part presents several different ways of axiomatizing this theory and makes the case for its naturalness. The second part discusses two kinds of extensions of Classicism: some which take the view in the direction of coarseness of grain (whose endpoint is the maximally coarse-grained view that coextensiveness is sufficient for (...) identity), and some which take the view in the direction of fineness of grain (whose endpoint is the maximally fine-grained theory containing all distinctness claims compatible with Classicism). The third part introduces some techniques for constructing models of Classicism, and uses them to prove the consistency of many of the extensions of Classicism introduced in the second part. (shrink)

Plural expressions found in natural languages allow us to talk about many objects simultaneously. Plural logic — a logical system that takes plurals at face value — has seen a surge of interest in recent years. This book explores its broader significance for philosophy, logic, and linguistics. What can plural logic do for us? Are the bold claims made on its behalf correct? After introducing plural logic and its main applications, the book provides a systematic analysis of the relation between (...) this logic and other theoretical frameworks such as set theory, mereology, higher-order logic, and modal logic. The applications of plural logic rely on two assumptions, namely that this logic is ontologically innocent and has great expressive power. These assumptions are shown to be problematic. The result is a more nuanced picture of plural logic's applications than has been given thus far. Questions about the correct logic of plurals play a central role in the final chapters, where traditional plural logic is rejected in favor of a "critical" alternative. The most striking feature of this alternative is that there is no universal plurality. This leads to a novel approach to the relation between the many and the one. In particular, critical plural logic paves the way for an account of sets capable of solving the set-theoretic paradoxes. (shrink)

With material on his early philosophical views, his contributions to set theory and his work on nominalism and higher-order quantification, this book offers a uniquely expansive critical commentary on one of analytical philosophy’s great ...