This chapter offers an opinionated introduction to higher-order formal languages with an eye towards their applications in metaphysics. A simply relationally typed higher-order language is introduced in four stages: starting with first-order logic, adding first-order predicate abstraction, generalizing to higher-order predicate abstraction, and finally adding higher-order quantification. It is argued that both β-conversion and Universal Instantiation are valid on the intended interpretation of this language. Given these two principles, it is then shown how we can use pure higher-order (...) class='Hi'>logic to ask, and begin to answer, metaphysical questions with non-trivial implications. In particular, while we must reject the popular idea that structural differences between sentences correspond to parallel distinctions in the logical structure of extra-linguistic reality, it may still be possible to give a purely logical characterization of objectual aboutness and related notions. (shrink)

This Element is an exposition of second- and higher-order logic and type theory. It begins with a presentation of the syntax and semantics of classical second-order logic, pointing up the contrasts with first-order logic. This leads to a discussion of higher-order logic based on the concept of a type. The second Section contains an account of the origins and nature of type theory, and its relationship to set theory. Section 3 introduces Local Set Theory, an important (...) form of type theory based on intuitionistic logic. In Section 4 number of contemporary forms of type theory are described, all of which are based on the so-called 'doctrine of propositions as types'. We conclude with an Appendix in which the semantics for Local Set Theory - based on category theory - is outlined. (shrink)

Truth predicates are widely believed to be capable of serving a certain logical or quasi-logical function. There is little consensus, however, on the exact nature of this function. We offer a series of formal results in support of the thesis that disquotational truth is a device to simulate higher-order resources in a first-order setting. More specifically, we show that any theory formulated in a higher-order language can be naturally and conservatively interpreted in a first-order theory with a disquotational truth or (...) truth-of predicate. In the first part of the paper we focus on the relation between truth and full impredicative sentential quantification. The second part is devoted to the relation between truth-of and full impredicative predicate quantification. (shrink)

The systems Kα of transfinite cumulative types up to α are extended to systems K∞α that include a natural infinitary inference rule, the so-called limit rule. For countable α a semantic completeness theorem for K∞α is proved by the method of reduction trees, and it is shown that every model of K∞α is equivalent to a cumulative hierarchy of sets. This is used to show that several axiomatic first-order set theories can be interpreted in K∞α, for suitable α.

The purpose of this article is show that second-order logic, as understood through standard semantics, is intimately bound up with set theory, or some other general theory of interpretations, structures, or whatever. Contra Quine, this does not disqualify second-order logic from its role in foundational studies. To wax Quinean, why should there be a sharp border separating mathematics from logic, especially the logic of mathematics?

Existential claims are widely held to be grounded in their true instances. However, this principle is shown to be problematic by arguments due to Kit Fine. Stephan Krämer has given an especially simple form of such an argument using propositional quantifiers. This note shows that even if a schematic principle of existential grounds for propositional quantifiers has to be restricted, this does not immediately apply to a corresponding non-schematic principle in higher-order logic.

This paper presents a new system of logic, LF, that is intended to be used as the foundation of the formalization of science. That is, deductive validity according to LF is to be used as the criterion for assessing what follows from the verdicts, hypotheses, or conjectures of any science. In work currently in progress, we argue for the unique suitability of LF for the formalization of logic, mathematics, syntax, and semantics. The present document specifies the language and (...) rules of LF, lays out some notational conventions, and states some basic technical facts about the system. (shrink)

This is the first comprehensive textbook on higher order logic that is written specifically to introduce the subject matter to graduate students in philosophy. The book covers both the formal aspects of higher-order languages -- their model theory and proof theory, the theory of λ-abstraction and its generalizations -- and their philosophical applications, especially to the topics of modality and propositional granularity. The book has a strong focus on non-extensional higher-order logics, making it more appropriate for foundational metaphysics than (...) other introductions to the subject from computer science, mathematics, and linguistics. A Philosophical Introduction to Higher Order Logics assumes only that readers have a basic knowledge of first-order logic. With an emphasis on exercises, it can be used as a textbook though is also ideal for self-study. Author Andrew Bacon organizes the book's 18 chapters around four main parts: I. Typed Language II. Higher Order Languages III. General Higher-Order Languages IV. Higher-Order Model Theory In addition, two appendices cover the Curry-Howard isomorphism and its applications for modeling propositional structure. Each chapter includes exercises that move from easier to more difficult, strategically placed throughout the chapter, and concludes with an annotated suggested reading list providing graduate students with most valuable additional resources. Key Features Is the first comprehensive introduction to higher-order logic as a grounding for addressing problems in metaphysics Introduces the basic formal tools that are needed to theorize in, and model, higher order languages Offers an abundance of: - Simple exercises throughout the book, serving as comprehension checks on basic concepts and definitions - More difficult exercises designed to facilitate long-term learning Contains annotated sections on further reading, pointing the reader to related literature, learning resources, and historical context. (shrink)

The articles in this volume represent a part of the philosophical literature on higher-order logic and the Skolem paradox. They ask the question what is second-order logic? and examine various interpretations of the Lowenheim-Skolem theorem.

In this article, we discuss a simple argument that modal metaphysics is misconceived, and responses to it. Unlike Quine's, this argument begins with the simple observation that there are different candidate interpretations of the predicate ‘could have been the case’. This is analogous to the observation that there are different candidate interpretations of the predicate ‘is a member of’. The argument then infers that the search for metaphysical necessities is misguided in much the way the ‘set-theoretic pluralist’ claims that the (...) search for the true axioms of set theory is. We show that the obvious responses to this argument fail. However, a new response has emerged that purports to prove, from higher-order logical principles, that metaphysical possibility is the broadest kind of possibility applying to propositions, and is to that extent special. We distill two lines of reasoning from the literature, and argue that their import depends on premises that any ‘modal pluralist’ should deny. Both presuppose that there is a unique typed hierarchy, which is what the modal pluralist, in the context of higher-order logic, should disavow. In other words, both presupposes that there is a unique candidate for what higher-order claims could mean. We consider the worry that, in a higher-order setting, modal pluralism faces an insuperable problem of articulation, collapses into modal monism, is vulnerable to the Russell-Myhill paradox, or even contravenes the truism that there is a unique actual world, and argue that these worries are misplaced. We also sketch the bearing of the resulting ‘Higher-Order Pluralism’ on the theory of content. One theme of the discussion is that, if Higher-Order Pluralism is correct, then there is no fixed metatheory from which to characterize higher-order reality. (shrink)

Here we investigate the classes RCA $^\uparrow_\alpha$ of representable directed cylindric algebras of dimension α introduced by Nemeti[12]. RCA $^\uparrow_\alpha$ can be seen in two different ways: first, as an algebraic counterpart of higher order logics and second, as a cylindric algebraic analogue of Quasi-Projective Relation Algebras. We will give a new, "purely cylindric algebraic" proof for the following theorems of Nemeti: (i) RCA $^\uparrow_\alpha$ is a finitely axiomatizable variety whenever α ≥ 3 is finite and (ii) one can obtain (...) a strong representation theorem for RCA $^\uparrow_\alpha$ if one chooses an appropriate (non-well-founded) set theory as foundation of mathematics. These results provide a purely cylindric algebraic solution for the Finitization Problem (in the sense of [11]) in some non-well-founded set theories. (shrink)

A logic is called higher order if it allows for quantification over higher order objects, such as functions of individuals, relations between individuals, functions of functions, relations between functions, etc. Higher order logic began with Frege, was formalized in Russell [46] and Whitehead and Russell [52] early in the previous century, and received its canonical formulation in Church [14].1 While classical type theory has since long been overshadowed by set theory as a foundation of mathematics, recent decades have (...) shown remarkable comebacks in the fields of mechanized reasoning (see, e.g., Benzm¨. (shrink)

The usage of sorts in first-order automated deduction has brought greater conciseness of representation and a considerable gain in efficiency by reducing the search spaces involved. This suggests that sort information can be employed in higher-order theorem proving with similar results.

A typical interpreted formal language has (first‐order) variables that range over a collection of objects, sometimes called a domain‐of‐discourse. The domain is what the formal language is about. A language may also contain second‐order variables that range over properties, sets, or relations on the items in the domain‐of‐discourse, or over functions from the domain to itself. For example, the sentence ‘Alexander has all the qualities of a great leader’ would naturally be rendered with a second‐order variable ranging over qualities. Similarly, (...) the sentence ‘there is a property that holds of all and only the prime numbers’ has a variable ranging over properties of natural numbers. Third‐order variables range over properties of properties, sets of sets, functions from properties to sets, etc. For example, according to some logicist accounts, the number 4 is the property shared by all properties that apply to exactly four objects in the domain. Accordingly, the number 4 is a third‐order item. Fourth‐order variables, and beyond, are characterized similarly. The phrase ‘higher‐order variable’ refers to the variables beyond first‐order. (shrink)

Suppose you hold the following opinions in the philosophy of logic. First-order predicate logic is expressively inadequate to regiment concepts of mathematic and natural language; logicism is plausible and attractive; set theory as an adjunct to logic is unnatural and ontologically extravagant; humanly usable languages are finite in lexicon and syntax; it is worth striving for a Tarskian semantics for mathematics; there are no Platonic abstract objects. Then you are probably already in cognitive distress. One way to (...) decease your unhappiness, short for embracing Platonism, is to accept higher-order logic and look, as did Arthur Prior, for a plausible way to neutralize the ontological commitment to abstract entities that this acceptance appears to entail. (shrink)

Suppose you hold the following opinions in the philosophy of logic. First-order predicate logic is expressively inadequate to regiment concepts of mathematic and natural language; logicism is plausible and attractive; set theory as an adjunct to logic is unnatural and ontologically extravagant; humanly usable languages are finite in lexicon and syntax; it is worth striving for a Tarskian semantics for mathematics; there are no Platonic abstract objects. Then you are probably already in cognitive distress. One way to (...) decease your unhappiness, short for embracing Platonism, is to accept higher-order logic and look, as did Arthur Prior, for a plausible way to neutralize the ontological commitment to abstract entities that this acceptance appears to entail. (shrink)

Using recent results in topos theory, two systems of higher-order logic are shown to be complete with respect to sheaf models over topological spaces-so-called "topological semantics". The first is classical higher-order logic, with relational quantification of finitely high type; the second system is a predicative fragment thereof with quantification over functions between types, but not over arbitrary relations. The second theorem applies to intuitionistic as well as classical logic.

In this article, a qualitative notion of subjective plausibility and its revision based on a preorder relation are implemented in higher-order logic. This notion of plausibility is used for modeling pragmatic aspects of communication on top of traditional two-dimensional semantic representations.

Using recent results in topos theory, two systems of higher-order logic are shown to be complete with respect to sheaf models over topological spaces- so -called "topological semantics." The first is classical higher-order logic, with relational quantification of finitely high type; the second system is a predicative fragment thereof with quantification over functions between types, but not over arbitrary relations. The second theorem applies to intuitionistic as well as classical logic.

We define a generalization of the first-order cut-elimination method CERES to higher-order logic. At the core of lies the computation of an set of sequents from a proof π of a sequent S. A refutation of in a higher-order resolution calculus can be used to transform cut-free parts of π into a cut-free proof of S. An example illustrates the method and shows that can produce meaningful cut-free proofs in mathematics that traditional cut-elimination methods cannot reach.

Many theories of rational belief give a special place to logic. They say that an ideally rational agent would never be uncertain about logical facts. In short: they say that ideal rationality requires "logical omniscience." Here I argue against the view that ideal rationality requires logical omniscience on the grounds that the requirement of logical omniscience can come into conflict with the requirement to proportion one’s beliefs to the evidence. I proceed in two steps. First, I rehearse an influential (...) line of argument from the "higher-order evidence" debate, which purports to show that it would be dogmatic, even for a cognitively infallible agent, to refuse to revise her beliefs about logical matters in response to evidence indicating that those beliefs are irrational. Second, I defend this "anti-dogmatism" argument against two responses put forth by Declan Smithies and David Christensen. Against Smithies’ response, I argue that it leads to irrational self-ascriptions of epistemic luck, and that it obscures the distinction between propositional and doxastic justification. Against Christensen’s response, I argue that it clashes with one of two attractive deontic principles, and that it is extensionally inadequate. Taken together, these criticisms will suggest that the connection between logic and rationality cannot be what it is standardly taken to be—ideal rationality does not require logical omniscience. (shrink)

Higher-Order Logic (HOL) is a proof development system intended for applications to both hardware and software. It is principally used in two ways: for directly proving theorems, and as theorem-proving support for application-specific verification systems. HOL is currently being applied to a wide variety of problems, including the specification and verification of critical systems. Introduction to HOL provides a coherent and self-contained description of HOL containing both a tutorial introduction and most of the material that is needed for day-to-day (...) work with the system. After a quick overview that gives a "hands-on feel" for the way HOL is used, there follows a detailed description of the ML language. The logic that HOL supports and how this logic is embedded in ML, are then described in detail. This is followed by an explanation of the theorem-proving infrastructure provided by HOL. Finally two appendices contain a subset of the reference manual, and an overview of the HOL library, including an example of an actual library documentation. (shrink)

The principle of universal instantiation plays a pivotal role both in the derivation of intensional paradoxes such as Prior’s paradox and Kaplan’s paradox and the debate between necessitism and contingentism. We outline a distinctively free logical approach to the intensional paradoxes and note how the free logical outlook allows one to distinguish two different, though allied themes in higher-order necessitism. We examine the costs of this solution and compare it with the more familiar ramificationist approaches to higher-order logic. Our (...) assessment of both approaches is largely pessimistic, and we remain reluctantly inclined to take Prior’s and Kaplan’s derivations at face value. (shrink)

Thinking about misleading higher-order evidence naturally leads to a puzzle about epistemic rationality: If one’s total evidence can be radically misleading regarding itself, then two widely-accepted requirements of rationality come into conflict, suggesting that there are rational dilemmas. This paper focuses on an often misunderstood and underexplored response to this (and similar) puzzles, the so-called conflicting-ideals view. Drawing on work from defeasible logic, I propose understanding this view as a move away from the default metaepistemological position according to which (...) rationality requirements are strict and governed by a strong, but never explicitly stated logic, toward the more unconventional view, according to which requirements are defeasible and governed by a comparatively weak logic. When understood this way, the response is not committed to dilemmas. (shrink)

We define a higher order logic which has only a notion of sort rather than a notion of type, and which permits all terms of the untyped lambda calculus and allows the use of the Y combinator in writing recursive predicates. The consistency of the logic is maintained by a distinction between use and mention, as in Gilmore's logics. We give a consistent model theory, a proof system which is sound with respect to the model theory, and a (...) cut-elimination proof for the proof system. We also give examples showing what formulas can and cannot be used in the logic. (shrink)

This book articulates and defends Fregean realism, a theory of properties based on Frege's insight that properties are not objects, but rather the satisfaction conditions of predicates. Robert Trueman argues that this approach is the key not only to dissolving a host of longstanding metaphysical puzzles, such as Bradley's Regress and the Problem of Universals, but also to understanding the relationship between states of affairs, propositions, and the truth conditions of sentences. Fregean realism, Trueman suggests, ultimately leads to a version (...) of the identity theory of truth, the theory that true propositions are identical to obtaining states of affairs. In other words, the identity theory collapses the gap between mind and world. This book will be of interest to anyone working in logic, metaphysics, the philosophy of language or the philosophy of mind. (shrink)

In this paper a proposal by Henkin of a nominalistic interpretation for second and higher-order logic is developed in detail and analysed. It was proposed as a response to Quine’s claim that second and higher-order logic not only are committed to the existence of sets, but also are committed to the existence of more sets than can ever be referred to in the language. Henkin’s interpretation is rarely cited in the debate on semantics and ontological commitments for these (...) logics, though it has many interesting ideas that are worth exploring. The detailed development will show that it employs an early strategy of using substitutional quantification in order to reduce ontological commitments. It will be argued that the perspective adopted for the predicate variables renders it a natural extension of Quine’s nominalistic interpretation for first-order logic. However, we will argue that, with respect to Quine’s nominalistic program and his notion of ontological commitment, still holds and thus Henkin’s interpretation is not nominalistic. Nevertheless, it will be seen that is addressed successfully and this provides further insights on the so-called “Skolem Paradox”. Moreover, the interpretation is ontologically parsimonious and, in this respect, it arguably fares better than a recent proposal by Bob Hale. (shrink)

W. V. Quine famously defended two theses that have fallen rather dramatically out of fashion. The first is that intensions are “creatures of darkness” that ultimately have no place in respectable philosophical circles, owing primarily to their lack of rigorous identity conditions. However, although he was thoroughly familiar with Carnap’s foundational studies in what would become known as possible world semantics, it likely wouldn’t yet have been apparent to Quine that he was fighting a losing battle against intensions, due in (...) large measure to developments stemming from Carnap’s studies and culminating in the work of Kripke, Hintikka, and Bayart. These developments undermined Quine’s crusade against intensions on two fronts. First, in the context of possible world semantics, intensions could after all be given rigorous identity conditions by defining them (in the simplest case) as functions from worlds to appropriate extensions, a fact exploited to powerful and influential effect in logic and linguistics by the likes of Kaplan, Montague, Lewis, and Cresswell. Second, the rise of possible world semantics fueled a strong resurgence of metaphysics in contemporary analytic philosophy that saw properties and propositions widely, fruitfully, and unabashedly adopted as ontological primitives in their own right. This resurgence — happily, in my view — continues into the present day. -/- For a time, at any rate, Quine experienced somewhat better success with his second thesis: that higher-order logic is, at worst, confused and, at best, a quirky notational alternative to standard first-order logic. However, Quine notwithstanding, a great deal of recent work in formal metaphysics transpires in a higher-order logical framework in which properties and propositions fall into an infinite hierarchy of types of (at least) every finite order. Initially, the most philosophically compelling reason for embracing such a framework since Russell first proposed his simple theory of types was simply that it provides a relatively natural explanation of the paradoxes. However, since the seminal work of Prior there has been a growing trend to consider higher-order logic to be the most philosophically natural framework for metaphysical inquiry, many of the contributors to this volume being among the most important and influential advocates of this view. Indeed, this is now quite arguably the dominant view among formal metaphysicians. -/- In this paper, and against the current tide, I will argue in §1 that there are still good reasons to think that Quine’s second battle is not yet lost and that the correct framework for logic is first-order and type-free — properties and propositions, logically speaking, are just individuals among others in a single domain of quantification — and that it arises naturally out of our most basic logical and semantical intuitions. The data I will draw upon are not new and are well-known to contemporary higher-order metaphysicians. However, I will try to defend my thesis in what I believe is a novel way by suggesting that these basic intuitions ground a reasonable distinction between “pure” logic and non-logical theory, and that Russell-style semantic paradoxes of truth and exemplification arise only when we move beyond the purely logical and, hence, do not of themselves provide any strong objection to a type-free conception of properties and propositions. -/- Most of my arguments in §1 are largely independent of any specific account of the nature of properties and propositions beyond their type-freedom. However, I will in addition argue that there are good reasons to take propositions, at least, to be very fine-grained. My arguments are thus bolstered significantly if it can be shown that there are in fact well-defined examples of logics that are not only type-free but which comport with such a conception of propositions. It is the purpose of §2 to lay out a logic of this sort in some detail, drawing especially upon work by George Bealer and related work of my own. With the logic in place, it will be possible to generalize the line of argument noted above regarding Russell-style paradoxes and, in §3, apply it to two propositional paradoxes — the Prior-Kaplan paradox and the Russell-Myhill paradox — that are often taken to threaten the sort of account developed here. (shrink)

In [2] we have presented sequent formulations of the modal logics S5 and S4 based on sequents of higher levels: sequents of level 1 are like ordinary sequents, sequents of level 2 have collections of sequents of level 1 on the left and right of the turnstile, etc. The rules we gave for modal constants involved sequents of level 2, whereas rules for other customary logical constants of first–order logic involved only sequents of level 1. Here we show starting (...) from the same sequent rules of higher level we can obtain sequent formulations of intuitionistic analogues of S5 and S4. We presuppose for this paper an acquaintance with [2]. (shrink)

This chapter provides an introduction to higher-order metaphysics as well as to the contributions to this volume. We discuss five topics, corresponding to the five parts of this volume, and summarize the contributions to each part. First, we motivate the usefulness of higher-order quantification in metaphysics using a number of examples, and discuss the question of how such quantifiers should be interpreted. We provide a brief introduction to the most common forms of higher-order logics used in metaphysics, and indicate a (...) number of questions which can be raised in such systems using logical vocabulary alone. Using a further example, we return to applications of higher-order logics in metaphysics. We also mention key developments in the history of higher-order logic as it pertains to metaphysics. Finally, we mention certain arguments which have been raised against the use of higher-order logic, and some ways of responding to them. (shrink)

ABSTRACT Four philosophical concerns about higher-order logic in general and the specific demands placed on it by the neo-logicist project are distinguished. The paper critically reviews recent responses to these concerns by, respectively, the late Bob Hale, Richard Kimberly Heck, and myself. It is argued that these score some successes. The main aim of the paper, however, is to argue that the most serious objection to the applications of higher-order logic required by the neo-logicist project has not been (...) properly understood. The paper concludes by outlining a strategy, prefigured in recent work of Øystein Linnebo, for meeting this objection. (shrink)

You have higher-order uncertainty iff you are uncertain of what opinions you should have. I defend three claims about it. First, the higher-order evidence debate can be helpfully reframed in terms of higher-order uncertainty. The central question becomes how your first- and higher-order opinions should relate—a precise question that can be embedded within a general, tractable framework. Second, this question is nontrivial. Rational higher-order uncertainty is pervasive, and lies at the foundations of the epistemology of disagreement. Third, the answer is (...) not obvious. The Enkratic Intuition---that your first-order opinions must “line up” with your higher-order opinions---is incorrect; epistemic akrasia can be rational. If all this is right, then it leaves us without answers---but with a clear picture of the question, and a fruitful strategy for pursuing it. (shrink)

First-order modal logic, in the usual formulations, is not suf- ficiently expressive, and as a consequence problems like Frege’s morning star/evening star puzzle arise. The introduction of predicate abstraction machinery provides a natural extension in which such difficulties can be addressed. But this machinery can also be thought of as part of a move to a full higher-order modal logic. In this paper we present a sketch of just such a higher-order modal logic: its formal semantics, and (...) a proof procedure using tableaus. Naturally the tableau rules are not complete, but they are with respect to a Henkinization of the “true” semantics. We demonstrate the use of the tableau rules by proving one of the theorems involved in G¨ odel’s ontological argument, one of the rare instances in the literature where higher-order modal constructs have appeared. A fuller treatment of the material presented here is in preparation. (shrink)