Movatterモバイル変換

No categories

Export citation   Bookmark  

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 inhigher-orderlogic.

Direct download(2 more)   Export citation   Bookmark   8 citations  

This chapter offers an opinionated introduction tohigher-order formal languages with an eye towards their applications in metaphysics. A simply relationally typedhigher-order language is introduced in four stages: starting with first-orderlogic, adding first-order predicate abstraction, generalizing tohigher-order predicate abstraction, and finally addinghigher-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 purehigher-orderlogic 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)

Direct download   Export citation   Bookmark   7 citations  

This chapter provides an overview of second-orderlogic andhigher-orderlogic generally. It provides the basic formal languages, deductive systems, and model-theoretic semantics, including a brief account of George Boolos’s interpretation of second-order languages in terms of the plural construction. It then goes into some of the arguments in favor of second-orderlogic.

No categories

Direct download(3 more)   Export citation   Bookmark   7 citations  

The purpose of this article is show that second-orderlogic, 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-orderlogic from its role in foundational studies. To wax Quinean, why should there be a sharp border separating mathematics fromlogic, especially thelogic of mathematics?

Direct download(8 more)   Export citation   Bookmark   12 citations  

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 simulatehigher-order resources in a first-order setting. More specifically, we show that any theory formulated in ahigher-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)

Direct download(3 more)   Export citation   Bookmark   1 citation  

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 α.

Direct download   Export citation   Bookmark   10 citations  

Using recent results in topos theory, two systems ofhigher-orderlogic are shown to be complete with respect to sheaf models over topological spaces- so -called "topological semantics." The first is classicalhigher-orderlogic, 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 classicallogic.

Direct download(14 more)   Export citation   Bookmark   10 citations  

Second-order languages, canonically understood, allow quantification over all sets of objects in the range of the first-order variables. In this chapter two arguments are given against the suitability of using second-order consequence as the consequence relation of axiomatic theories. According to the first argument, second-order languages are inadequate for axiomatizing set theory because of the strong set-theoretic content coded by second-order consequence. The second more general argument is directed against the determinacy of second-order consequence, (...) that is, against the assumption that this is a definite relation. Only taking a strong realist view of set theory can one maintain that it is. (shrink)

No categories

Direct download(3 more)   Export citation   Bookmark   1 citation  

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

Direct download   Export citation   Bookmark   15 citations  

Export citation   Bookmark   9 citations  

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)

Direct download   Export citation   Bookmark   5 citations  

Direct download(2 more)   Export citation   Bookmark   10 citations  

Export citation   Bookmark   1 citation  

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 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, fromhigher-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 ofhigher-orderlogic, should disavow. In other words, both presupposes that there is a unique candidate for whathigher-order claims could mean. We consider the worry that, in ahigher-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, ifHigher-Order Pluralism is correct, then there is no fixed metatheory from which to characterizehigher-order reality. (shrink)

Direct download(2 more)   Export citation   Bookmark   6 citations  

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 ofhigherorder 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)

Direct download(8 more)   Export citation   Bookmark   10 citations  

This Element is an exposition of second- andhigher-orderlogic and type theory. It begins with a presentation of the syntax and semantics of classical second-orderlogic, pointing up the contrasts with first-orderlogic. This leads to a discussion ofhigher-orderlogic 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 intuitionisticlogic. 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)

Export citation   Bookmark   1 citation  

This paper presents a new system oflogic, 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 oflogic, 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)

Direct download   Export citation   Bookmark   4 citations  

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

Export citation   Bookmark   2 citations  

We define ahigherorderlogic 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 thelogic 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 thelogic. (shrink)

Direct download(4 more)   Export citation   Bookmark  

Suppose you hold the following opinions in the philosophy oflogic. First-order predicatelogic is expressively inadequate to regiment concepts of mathematic and natural language; logicism is plausible and attractive; set theory as an adjunct tologic 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 accepthigher-orderlogic 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)

Direct download(5 more)   Export citation   Bookmark   4 citations  

Direct download   Export citation   Bookmark   12 citations  

This is the first comprehensive textbook onhigherorderlogic that is written specifically to introduce the subject matter to graduate students in philosophy. The book covers both the formal aspects ofhigher-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-extensionalhigher-order logics, making it (...) more appropriate for foundational metaphysics than other introductions to the subject from computer science, mathematics, and linguistics. A Philosophical Introduction toHigherOrder Logics assumes only that readers have a basic knowledge of first-orderlogic. 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.HigherOrder Languages III. GeneralHigher-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 tohigher-orderlogic as a grounding for addressing problems in metaphysics Introduces the basic formal tools that are needed to theorize in, and model,higherorder 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)

Direct download   Export citation   Bookmark   5 citations  

Direct download   Export citation   Bookmark  

Export citation   Bookmark  

An embedding of many-valued logics based on SIXTEEN in classicalhigher-orderlogic is presented. SIXTEEN generalizes the four-valued set of truth degrees of Dunn/Belnap’s system to a lattice of sixteen truth degrees with multiple distinct ordering relations between them. The theoretical motivation is to demonstrate that many-valued logics, like other non-classical logics, can be elegantly modeled (and even combined) as fragments of classicalhigher-orderlogic. Equally relevant are the pragmatic aspects of the presented approach: (...) interactive and automated reasoning in many-valued logics, which have broad applications in computer science, artificial intelligence, linguistics, philosophy and mathematics, become readily enabled with state of the art reasoning tools for classicalhigher-orderlogic. (shrink)

Direct download(3 more)   Export citation   Bookmark   1 citation  

Direct download(8 more)   Export citation   Bookmark   20 citations  

In this paper a proposal by Henkin of a nominalistic interpretation for second andhigher-orderlogic is developed in detail and analysed. It was proposed as a response to Quine’s claim that second andhigher-orderlogic 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 inorder 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-orderlogic. 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)

No categories

Direct download(3 more)   Export citation   Bookmark  

Many theories of rational belief give a special place tologic. 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 betweenlogic and rationality cannot be what it is standardly taken to be—ideal rationality does not require logical omniscience. (shrink)

Direct download   Export citation   Bookmark   3 citations  

Alogic is calledhigherorder if it allows for quantification overhigherorder objects, such as functions of individuals, relations between individuals, functions of functions, relations between functions, etc.Higherorderlogic 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)

Direct download   Export citation   Bookmark   18 citations  

No categories

Direct download   Export citation   Bookmark   4 citations  

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 inhigher-order necessitism. We examine the costs of this solution and compare it with the more familiar ramificationist approaches tohigher- (...) class='Hi'>orderlogic. 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)

Direct download(7 more)   Export citation   Bookmark   31 citations  

No categories

Direct download   Export citation   Bookmark   4 citations  

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 inlogic, metaphysics, the philosophy of language or the philosophy of mind. (shrink)

Direct download   Export citation   Bookmark   37 citations  

Direct download(7 more)   Export citation   Bookmark  

Direct download(2 more)   Export citation   Bookmark  

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 inhigher-order theorem proving with similar results.

Export citation   Bookmark   8 citations  

The paper contains a review and a discussion of Robert Trueman's book Properties and Propositions: The Metaphysics ofHigher-OrderLogic, Cambridge University Press, 2021, pp. xii + 227. ISBN 978-1-108-81410-2. The discussion is focused on the consistency of Truema's language-based ontology and on its value in defendinghigher-orderlogic.

Direct download(2 more)   Export citation   Bookmark  

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 inlogic 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: thathigher-orderlogic is, at worst, confused and, at best, a quirky notational alternative to standard first-orderlogic. However, Quine notwithstanding, a great deal of recent work in formal metaphysics transpires in ahigher-order logical framework in which properties and propositions fall into an infinite hierarchy of types of (at least) every finiteorder. 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 considerhigher-orderlogic 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 forlogic 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 contemporaryhigher-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 alogic of this sort in some detail, drawing especially upon work by George Bealer and related work of my own. With thelogic 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)

Direct download   Export citation   Bookmark   2 citations  

We define a generalization of the first-order cut-elimination method CERES tohigher-orderlogic. At the core of lies the computation of an set of sequents from a proof π of a sequent S. A refutation of in ahigher-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. (shrink)

Direct download(4 more)   Export citation   Bookmark   1 citation  

Thinking about misleadinghigher-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 defeasiblelogic, 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 statedlogic, toward the more unconventional view, according to which requirements are defeasible and governed by a comparatively weaklogic. When understood this way, the response is not committed to dilemmas. (shrink)

Direct download(4 more)   Export citation   Bookmark   4 citations  

The problematic features of Quine's set theories NF and ML are a result of his replacing thehigher-order predicatelogic of type theory by a first-orderlogic of membership, and can be resolved by returning to a second-orderlogic of predication with nominalized predicates as abstract singular terms. We adopt a modified Fregean position called conceptual realism in which the concepts (unsaturated cognitive structures) that predicates stand for are distinguished from the extensions (or (...) intensions) that their nominalizations denote as singular terms. We argue against Quine's view that predicate quantifiers can be given a referential interpretation only if the entities predicates stand for on such an interpretation are the same as the classes (assuming extensionality) that nominalized predicates denote as singular terms. Quine's alternative of giving predicate quantifiers only a substitutional interpretation is compared with a constructive version of conceptual realism, which with alogic of nominalized predicates is compared with Quine's description of conceptualism as a ramified theory of classes. We argue against Quine's implicit assumption that conceptualism cannot account for impredicative concept-formation and compare holistic conceptual realism with Quine's class Platonism. (shrink)

Direct download(6 more)   Export citation   Bookmark   4 citations  

Higher-OrderLogic (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. Thelogic that HOL supports and how thislogic 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)

Direct download   Export citation   Bookmark   11 citations  

In [2] we have presented sequent formulations of the modal logics S5 and S4 based on sequents ofhigher 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–orderlogic involved only sequents of level 1. Here we (...) show starting from the same sequent rules ofhigher level we can obtain sequent formulations of intuitionistic analogues of S5 and S4. We presuppose for this paper an acquaintance with [2]. (shrink)

Export citation   Bookmark  

ABSTRACT Four philosophical concerns abouthigher-orderlogic 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 ofhigher-orderlogic 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)

Direct download(5 more)   Export citation   Bookmark   1 citation  

In this book the authors reconcile two different viewpoints of the foundations of mathematics, namely mathematicallogic and category theory. In Part I, they show that typed lambda-calculi, a formulation ofhigherorderlogic, and cartesian closed categories are essentially the same. In Part II, it is demonstrated that another formulation ofhigherorderlogic is closely related to topos theory. Part III is devoted to recursive functions. Numerous applications of the close relationship (...) between traditionallogic and the algebraic language of category theory are given. The authors have included an introduction to category theory and develop the necessarylogic as required, making the book essentially self-contained. Detailed historical references are provided throughout, and each section concludes with a set of exercises. Thus it is well-suited for graduate courses and research in mathematics andlogic. Researchers in theoretical computer science, artificial intelligence and mathematical linguistics will also find this an accessible introduction to a subject of increasing application to these disciplines. (shrink)

No categories

Direct download   Export citation   Bookmark   18 citations  

We define the notion of a model ofhigher-order modallogic in an arbitrary elementary topos E. In contrast to the well-known interpretation ofhigher-orderlogic, the type of propositions is not interpreted by the subobject classifier ΩE, but rather by a suitable complete Heyting algebra H. The canonical map relating H and ΩE both serves to interpret equality and provides a modal operator on H in the form of a comonad. Examples of such (...) structures arise from surjective geometric morphisms f : F → E, where H = f∗ΩF. Thelogic differs from non-modalhigher-orderlogic in that the principles of functional and propositional extensionality are not longer valid but may be replaced by modalized versions. The usual Kripke, neighborhood, and sheaf semantics for propositional and first-order modallogic are subsumed by this notion. (shrink)

Direct download(2 more)   Export citation   Bookmark   5 citations  

First-order modallogic, 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 fullhigher-order modallogic. In this paper we present a sketch of just such ahigher-order modal (...) class='Hi'>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 wherehigher-order modal constructs have appeared. A fuller treatment of the material presented here is in preparation. (shrink)

Export citation   Bookmark  

Subverting a once widely held Quinean paradigm, there is a growing consensus among philosophers oflogic thathigher-order quantifiers (which bind variables in the syntactic position of predicates and sentences) are a perfectly legitimate and useful instrument in the logico-philosophical toolbox, while neither being reducible to nor fully explicable in terms of first-order quantifiers (which bind variables in singular term position). This article discusses the impact of this quantificational paradigm shift on metaphysics, focussing on theories of (...) properties, propositions, and identity, as well as on the metaphysics of modality. (shrink)

Direct download(3 more)   Export citation   Bookmark   23 citations  

Direct download   Export citation   Bookmark