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)

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)

One is often said to be reasoning well when they are reasoning logically. Many attempts to say what logical reasoning is have been proposed, but one commonly proposed system is first-order classical logic. This Element will examine the basics of first-order classical logic and discuss some surrounding philosophical issues. The first half of the Element develops a language for the system, as well as a proof theory and model theory. The authors provide theorems about (...) the system they developed, such as unique readability and the Lindenbaum lemma. They also discuss the meta-theory for the system, and provide several results there, including proving soundness and completeness theorems. The second half of the Element compares first-order classical logic to other systems: classical higher order logic, intuitionistic logic, and several paraconsistent logics which reject the law of ex falso quodlibet. (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.

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)

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 paper we re-examine the semantics of classical higher-order logic with the purpose of clarifying the role of extensionality. To reach this goal, we distinguish nine classes of higher-order models with respect to various combinations of Boolean extensionality and three forms of functional extensionality. Furthermore, we develop a methodology of abstract consistency methods (by providing the necessary model existence theorems) needed to analyze completeness of (machine-oriented) higher-order calculi with respect to these (...) model classes. (shrink)

ABSTRACT This paper introduces a multi-valued variant of higher-order resolution and proves it correct and complete with respect to a variant of Henkin's general model semantics. This resolution method is parametric in the number of truth values as well as in the particular choice of the set of connectives (given by arbitrary truth tables) and even substitutional quantifiers. In the course of the completeness proof we establish a model existence theorem for this logical system. The work reported in (...) this paper provides a basis for developing higher-order mechanizations for many non-classical logics. (shrink)

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)

Classical first-order logic can be extended in two different ways to serve as a foundation for mathematics: introduce higher orders, type theory, or introduce sets. As it happens, both approaches have natural analogs for quantified modal logics, both approaches date from the 1960’s, one is not very well-known, and the other is well-known as something else. I will present the basic semantic ideas of both higher order intensional logic, and intensional set theory. Before (...) doing so, I’ll quickly sketch some necessary background material from quantified modal logic. Except for standard material concerning propositional modal logics, the paper is essentially self-contained. (shrink)

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.

The present paper is concerned with a ramified type theory (cf. (Lorenzen 1955), (Russell), (Schütte), (Weyl), e.g.,) in a cumulative version. §0 deals with reasoning in first order languages. is introduced as a first order set.

A number of authors have objected to the application of non-classical logic to problems in philosophy on the basis that these non-classical logics are usually characterised by a classical metatheory. In many cases the problem amounts to more than just a discrepancy; the very phenomena responsible for non-classicality occur in the field of semantics as much as they do elsewhere. The phenomena of higher order vagueness and the revenge liar are just two such examples. (...) The aim of this paper is to show that a large class of non-classical logics are strong enough to formulate their own model theory in a corresponding non-classical set theory. Specifically I show that adequate definitions of validity can be given for the propositional calculus in such a way that the metatheory proves, in the specified logic, that every theorem of the propositional fragment of that logic is validated. It is shown that in some cases it may fail to be a classical matter whether a given sentence is valid or not. One surprising conclusion for non-classical accounts of vagueness is drawn: there can be no axiomatic, and therefore precise, system which is determinately sound and complete. (shrink)

Second-order quantifier elimination in the context of classical logic emerged as a powerful technique in many applications, including the correspondence theory, relational databases, deductive and knowledge databases, knowledge representation, commonsense reasoning and approximate reasoning. In the current paper we first generalize the result of Nonnengart and Szałas [17] by allowing second-order variables to appear within higher-order contexts. Then we focus on a semantical analysis of conditionals, using the introduced technique and Gabbay’s semantics provided in (...) [10] and substantially using a third-order accessibility relation. The analysis is done via finding correspondences between axioms involving conditionals and properties of the underlying third-order relation. (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)

This book honors J. Michael Dunn, who was a preeminent relevance logician. Dunn's career spanned over 50 years and his research results had an impact on philosophy, mathematics and informatics. Dunn often used algebraic techniques in his research into logics such as relevance, orthomodular and substructural logics. He invented the logic R-mingle and the sequent calculus LR+; he proved crucial theorems about 2-valued first-order logic and non-classical higher-order logics - among many other results. The (...) papers in this volume touch upon topics that Dunn was concerned with. Some authors were students or colleagues of Dunn; some other authors had not met Dunn in person, but share his research interests. None of the articles published here have appeared in print before; indeed, most of the papers were written specifically for this collection. The diversity of the themes of the articles reflects the scope of Dunn's own research in logic. It will also ensure that anybody with an interest in logic - whether a student, a logician or a scholar in another field - will find reading this book a worthwhile endeavor. The editor, Katalin Bimbó was the 14th Ph.D. student of J. Michael Dunn at Indiana University in Bloomington, IN, U.S.A.; currently, she is a professor of philosophy at the University of Alberta in Canada. (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)

Starting from a generalization of the standard axioms for a monoid we present a stepwise development of various, mutually equivalent foundational axiom systems for category theory. Our axiom sets have been formalized in the Isabelle/HOL interactive proof assistant, and this formalization utilizes a semantically correct embedding of free logic in classical higher-order logic. The modeling and formal analysis of our axiom sets has been significantly supported by series of experiments with automated reasoning tools integrated with (...) Isabelle/HOL. We also address the relation of our axiom systems to alternative proposals from the literature, including an axiom set proposed by Freyd and Scedrov for which we reveal a technical issue (when encoded in free logic where free variables range over defined and undefined objects): either all operations, e.g. morphism composition, are total or their axiom system is inconsistent. The repair for this problem is quite straightforward, however. (shrink)

1. Argumentation, by considering arguments and their interactions, is a way of reasoning that has proven successful in many contexts, for instance, in multi-agent applications (Carrera & Iglesias,...

It is a commonplace remark that the identity relation, even though not expressible in a first-order language without identity with classical set-theoretic semantics, can be defined in a language without identity, as soon as we admit second-order, set-theoretically interpreted quantifiers binding predicate variables that range over all subsets of the domain. However, there are fairly simple and intuitive higher-order languages with set-theoretic semantics in which the identity relation is not definable. The point is that the (...) definability of identity in higher-order languages not only depends on what variables range over, but also is sensitive to how predication is construed. This paper is a follow-up to , where it has been proven that no actual axiomatization of Leśniewski’s Ontology determines the standard semantics for the epsilon connective. (shrink)

Most of this work is devoted to presenting aspects of proof theory that have developed out of Gentzen's work. Thus the them is "cut elimination" and transfinite induction over constructive ordinals. Smullyan's tableau systems will be used for the formalisms and some of the basic logical results as presented in Smullyan [1] will be assumed to be known (essentially only the classical completeness and consistency proofs for propositional and first order logic).

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

The content for an advanced logic course is presented, which includes the properties of first-order logic language, soundness and completeness of the first-order logic deductive system, Peano arithmetic, Gödel's incompleteness theorems, higher-order logic and its properties. As a reminder, a brief description of first-order logic is included.

A hyperintensional semantics for natural language is proposed which is agnostic about the question of whether propositions are sets of worlds or worlds are sets of propositions. Montague’s theory of intensional senses is replaced by a weaker theory, written in standard classical higher-order logic, of fine-grained senses which are in a many-to-one correspondence with intensions; Montague’s theory can then be recovered from the proposed theory by identifying the type of propositions with the type of sets of (...) worlds and adding an axiom to the effect that each world is the set of propositions which are true there. Senses are compositionally assigned to linguistic expressions by a categorial grammar with only two rule schemas, based on the implicative fragment of intuitionistic linear propositional logic, and a fully explicit grammar fragment is provided that illustrates the compositional assignment of sense to a variety of constructions, including dummy-subject constructions, infinitive complements, predicative adjectives and nominals, raising to subject, ‘tough-movement’, and quantifier scope ambiguities. Notably, the grammar and the derivations that it licenses never make reference to either worlds or to the extensions of senses. (shrink)

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.

We define the paraconsistent supra-logic Pσ by a type-shift from the booleans o of propositional logic Po to the supra-booleans σ of the propositional type logic P obtained as the propositional fragment of the transfinite type theory Q defined by Peter Andrews (North-Holland Studies in Logic 1965) as a classical foundation of mathematics. The supra-logic is in a sense a propositional logic only, but since there is an infinite number of supra-booleans and arithmetical (...) operations are available for this and other types, virtually anything can be specified. The supra-logic is a generalization of Lukasiewicz's three-valued logic, with the intermediate value duplicated many times and ordered such that none of the copies of this value imply other ones, but it differs from Lukasiewicz's many-valued logics as well as from logics based on bilattices. There are several automated theorem provers for classical higher order logic (finite type theory) and it should be possible to modify these to our needs. (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)

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 volume began as a remembrance of Alonzo Church while he was still with us and is now finally complete. It contains papers by many well-known scholars, most of whom have been directly influenced by Church's own work. Often the emphasis is on foundational issues in logic, mathematics, computation, and philosophy - as was the case with Church's contributions, now universally recognized as having been of profound fundamental significance in those areas. The volume will be of interest to logicians, (...) computer scientists, philosophers, and linguists. The contributions concern classical first-order logic, higher-order logic, non-classical theories of implication, set theories with universal sets, the logical and semantical paradoxes, the lambda-calculus, especially as it is used in computation, philosophical issues about meaning and ontology in the abstract sciences and in natural language, and much else. The material will be accessible to specialists in these areas and to advanced graduate students in the respective fields. (shrink)

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)

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)

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

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)

Modal logic is one of philosophy’s many children. As a mature adult it has moved out of the parental home and is nowadays straying far from its parent. But the ties are still there: philosophy is important to modal logic, modal logic is important for philosophy. Or, at least, this is a thesis we try to defend in this chapter. Limitations of space have ruled out any attempt at writing a survey of all the work going on (...) in our field—a book would be needed for that. Instead, we have tried to select material that is of interest in its own right or exemplifies noteworthy features in interesting ways. Here are some themes that have guided us throughout the writing: • The back-and-forth between philosophy and modal logic. There has been a good deal of give-and-take in the past. Carnap tried to use his modal logic to throw light on old philosophical questions, thereby inspiring others to continue his work and still others to criticise it. He certainly provoked Quine, who in his turn provided—and continues to provide—a healthy challenge to modal logicians. And Kripke’s and David Lewis’s philosophies are connected, in interesting ways, with their modal logic. Analytic philosophy would have been a lot different without modal logic! • The interpretation problem. The problem of providing a certain modal logic with an intuitive interpretation should not be conflated with the problem of providing a formal system with a model-theoretic semantics. An intuitively appealing model-theoretic semantics may be an important step towards solving the interpretation problem, but only a step. One may compare this situation with that in probability theory, where definitions of concepts like ‘outcome space’ and ‘random variable’ are orthogonal to questions about “interpretations” of the concept of probability. • The value of formalisation. Modal logic sets standards of precision, which are a challenge to—and sometimes a model for—philosophy. Classical philosophical questions can be sharpened and seen from a new perspective when formulated in a framework of modal logic. On the other hand, representing old questions in a formal garb has its dangers, such as simplification and distortion. • Why modal logic rather than classical (first or higher order) logic? The idioms of modal logic—today there are many!—seem better to correspond to human ways of thinking than ordinary extensional logic. (Cf. Chomsky’s conjecture that the NP + VP pattern is wired into the human brain.) In his An Essay in Modal Logic (1951) von Wright distinguished between four kinds of modalities: alethic (modes of truth: necessity, possibility and impossibility), epistemic (modes of being known: known to be true, known to be false, undecided), deontic (modes of obligation: obligatory, permitted, forbidden) and existential (modes of existence: universality, existence, emptiness). The existential modalities are not usually counted as modalities, but the other three categories are exemplified in three sections into which this chapter is divided. Section 1 is devoted to alethic modal logic and reviews some main themes at the heart of philosophical modal logic. Sections 2 and 3 deal with topics in epistemic logic and deontic logic, respectively, and are meant to illustrate two different uses that modal logic or indeed any logic can have: it may be applied to already existing (non-logical) theory, or it can be used to develop new theory. (shrink)

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?

Intuitionistic logic provides an elegant solution to the Sorites Paradox. Its acceptance has been hampered by two factors. First, the lack of an accepted semantics for languages containing vague terms has led even philosophers sympathetic to intuitionism to complain that no explanation has been given of why intuitionistic logic is the correct logic for such languages. Second, switching from classical to intuitionistic logic, while it may help with the Sorites, does not appear to offer any (...) advantages when dealing with the so-called paradoxes of higher-order vagueness. We offer a proposal that makes strides on both issues. We argue that the intuitionist’s characteristic rejection of any third alethic value alongside true and false is best elaborated by taking the normal modal system S4M to be the sentential logic of the operator ‘it is clearly the case that’. S4M opens the way to an account of higher-order vagueness which avoids the paradoxes that have been thought to infect the notion. S4M is one of the modal counterparts of the intuitionistic sentential calculus and we use this fact to explain why IPC is the correct sentential logic to use when reasoning with vague statements. We also show that our key results go through in an intuitionistic version of S4M. Finally, we deploy our analysis to reply to Timothy Williamson’s objections to intuitionistic treatments of vagueness. (shrink)

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)

Typical applications of Hintikka’s game-theoretical semantics give rise to semantic attributes—truth, falsity—expressible in the $\Sigma^{1}_{1}$-fragment of second-order logic. Actually a much more general notion of semantic attribute is motivated by strategic considerations. When identifying such a generalization, the notion of classical negation plays a crucial role. We study two languages, $L_{1}$ and $L_{2}$, in both of which two negation signs are available: $\rightharpoondown $ and $\sim$. The latter is the usual GTS negation which transposes the players’ roles, (...) while the former will be interpreted via the notion of mode. Logic $L_{1}$ extends independence-friendly logic; $\rightharpoondown $ behaves as classical negation in $L_{1}$. Logic $L_{2}$ extends $L_{1}$, and it is shown to capture the $\Sigma^{2}_{1}$-fragment of third-order logic. Consequently the classical negation remains inexpressible in $L_{2}$. (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.

So-called 'dynamic' semantic theories such as Kamp's discourse representation theory and Heim's file change semantics account for such phenomena as cross-sentential anaphora, donkey anaphora, and the novelty condition on indefinites, but compare unfavorably with Montague semantics in some important respects (clarity and simplicity of mathematical foundations, compositionality, handling of quantification and coordination). Preliminary efforts have been made by Muskens and by de Groote to revise and extend Montague semantics to cover dynamic phenomena. We present a new higher-order theory (...) of discourse semantics which improves on their accounts by incorporating a more articulated notion of context inspired by ideas due to David Lewis and to Craige Roberts. On our account, a context consists of a common ground of mutually accepted propositions together with a set of discourse referents preordered by relative salience. Employing a richer notion of contexts enables us to extend our coverage beyond pronominal anaphora to a wider range of presuppositional phenomena, such as the factivity of certain sentential-complement verbs, resolution of anaphora associated with arbitrarily complex definite descriptions, presupposition 'holes' such as negation, and the independence condition on the antecedents of conditionals. Formally, our theory is expressed within a higher-order logic with natural number type, separation-style subtyping, and dependent coproducts parameterized by the natural numbers. The system of semantic types builds on proposals due to Thomason and to Pollard in which the type of propositions (static meanings of sentential utterances) is taken as basic and worlds are constructed from propositions (rather than the other way around as in standard Montague semantics). (shrink)

This introduction to mathematical logic starts with propositional calculus and first-order logic. Topics covered include syntax, semantics, soundness, completeness, independence, normal forms, vertical paths through negation normal formulas, compactness, Smullyan's Unifying Principle, natural deduction, cut-elimination, semantic tableaux, Skolemization, Herbrand's Theorem, unification, duality, interpolation, and definability. The last three chapters of the book provide an introduction to type theory (higher-order logic). It is shown how various mathematical concepts can be formalized in this very expressive formal (...) language. This expressive notation facilitates proofs of the classical incompleteness and undecidability theorems which are very elegant and easy to understand. The discussion of semantics makes clear the important distinction between standard and nonstandard models which is so important in understanding puzzling phenomena such as the incompleteness theorems and Skolem's Paradox about countable models of set theory. Some of the numerous exercises require giving formal proofs. A computer program called ETPS which is available from the web facilitates doing and checking such exercises. Audience: This volume will be of interest to mathematicians, computer scientists, and philosophers in universities, as well as to computer scientists in industry who wish to use higher-order logic for hardware and software specification and verification. (shrink)

An ontology's theory of ontic predication has implications for the concomitant predicate logic. Remarkable in its analytic power for both ontology and logic is the here developed Particularized Predicate Logic (PPL), the logic inherent in the realist version of the doctrine of unit or individuated predicates. PPL, as axiomatized and proven consistent below, is a three-sorted impredicative intensional logic with identity, having variables ranging over individuals x, intensions R, and instances of intensions $R_{i}$ . The (...) power of PPL is illustrated by its clarification of the self-referential nature of impredicative definitions and its distinguishing between legitimate and illegitimate forms. With a wellmotivated refinement on the axiom of comprehension, PPL is, in effect, a higher-order logic without a forced stratification of predicates into types or the use of other ad hoc restrictions. The Russell-Priest characterization of the classic self-referential paradoxes is used to show how PPL diagnosis and solves these antimonies. A direct application of PPL is made to Grelling's Paradox. Also shown is how PPL can distinguish between identity and indiscernibility. (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 (which has been advanced by other authors) that identity lacks sense for elementary particles of modern physics, and the way which physicists deal with this concept; normally, they understandidentity as meaningindistinguishability (agreemment with respect to attributes). 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)

An increasing amount of contemporary philosophy of mathematics posits, and theorizes in terms of special kinds of mathematical modality. The goal of this paper is to bring recent work on higher-order metaphysics to bear on the investigation of these modalities. The main focus of the paper will be views that posit mathematical contingency or indeterminacy about statements that concern the `width' of the set theoretic universe, such as Cantor's continuum hypothesis. Within a higher-order framework I show (...) that contingency about the width of the set-theoretic universe refutes two orthodoxies concerning the structure of modal reality: the view that the broadest necessity has a logic of S5, and the "Leibniz biconditionals" stating that what is possible, in the broadest sense of possible, is what is true in some possible world. Nonetheless, I suggest that the underlying picture of modal set-theory is coherent and has attractions. (shrink)