We prove that the first-order logic of CZF is intuitionistic first-order logic. To do so, we introduce a new model of transfinite computation (Set Register Machines) and combine the resulting notion of realisability with Beth semantics. On the way, we also show that the propositional admissible rules of CZF are exactly those of intuitionistic propositional logic.

This completely self-contained study, widely considered the best book in the field, is intended to serve both as an introduction to quantification theory and as ...

A sentence of first-order logic is satisfiable if it is true in some structure, and finitely satisfiable if it is true in some finite structure. The question arises as to whether there exists an algorithm for determining whether a given formula of first-order logic is satisfiable, or indeed finitely satisfiable. This question was answered negatively in 1936 by Church and Turing (for satisfiability) and in 1950 by Trakhtenbrot (for finite satisfiability).In contrast, the satisfiability and (...) finite satisfiability problems are algorithmically solvable for restricted subsets---or, as we say, fragments---of first-order logic, a fact which is today of considerable interest in Computer Science. This book provides an up-to-date survey of the principal axes of research, charting the limits of decision in first-order logic and exploring the trade-off between expressive power and complexity of reasoning. Divided into three parts, the book considers for which fragments of first-order logic there is an effective method for determining satisfiability or finite satisfiability. Furthermore, if these problems are decidable for some fragment, what is their computational complexity? Part I focusses on fragments defined by restricting the set of available formulas. Topics covered include the Aristotelian syllogistic and its relatives, the two-variable fragment, the guarded fragment, the quantifier-prefix fragments and the fluted fragment. Part II investigates logics with counting quantifiers. Starting with De Morgan's numerical generalization of the Aristotelian syllogistic, we proceed to the two-variable fragment with counting quantifiers and its guarded subfragment, explaining the applications of the latter to the problem of query answering in structured data. Part III concerns logics characterized by semantic constraints, limiting the available interpretations of certain predicates. Taking propositional modal logic and graded modal logic as our cue, we return to the satisfiability problem for two-variable first-order logic and its relatives, but this time with certain distinguished binary predicates constrained to be interpreted as equivalence relations or transitive relations. The work finishes, slightly breaching the bounds of first-order logic proper, with a chapter on logics interpreted over trees. (shrink)

This paper introduces two languages and associated logics designed to afford perspicuous representations of a range of natural language arguments involving adverbs and the like: first-order logic with basic adverbs (FOL-BA) and first-order logic with scoped adverbs (FOL-SA). The guiding logical idea is that an adverb can come between a term and the rest of the statement it is a part of, resulting in a logically stronger statement. I explain various interesting challenges that arise (...) in the attempt to implement the guiding idea, and provide solutions for some but not all of them. I conclude by outlining some directions for further research. (shrink)

What has been the historical relationship between set theory and logic? On the one hand, Zermelo and other mathematicians developed set theory as a Hilbert-style axiomatic system. On the other hand, set theory influenced logic by suggesting to Schröder, Löwenheim and others the use of infinitely long expressions. The questions of which logic was appropriate for set theory - first-order logic, second-order logic, or an infinitary logic - culminated in a vigorous (...) exchange between Zermelo and Gödel around 1930. (shrink)

From a logical point of view, Stone duality for Boolean algebras relates theories in classical propositional logic and their collections of models. The theories can be seen as presentations of Boolean algebras, and the collections of models can be topologized in such a way that the theory can be recovered from its space of models. The situation can be cast as a formal duality relating two categories of syntax and semantics, mediated by homming into a common dualizing object, in (...) this case 2.In the present work, we generalize the entire arrangement from propositional to first-order logic, using a representation result of Butz and Moerdijk. Boolean algebras are replaced by Boolean categories presented by theories in first-order logic, and spaces of models are replaced by topological groupoids of models and their isomorphisms. A duality between the resulting categories of syntax and semantics, expressed primarily in the form of a contravariant adjunction, is established by homming into a common dualizing object, now Sets, regarded once as a boolean category, and once as a groupoid equipped with an intrinsic topology.The overall framework of our investigation is provided by topos theory. Direct proofs of the main results are given, but the specialist will recognize toposophical ideas in the background. Indeed, the duality between syntax and semantics is really a manifestation of that between algebra and geometry in the two directions of the geometric morphisms that lurk behind our formal theory. Along the way, we give an elementary proof of Butz and Moerdijkʼs result in logical terms. (shrink)

‘Quantified pure existentials’ are sentences (e.g., ‘Some things do not exist’) which meet these conditions: (i) the verb EXIST is contained in, and is, apart from quantificational BE, the only full (as against auxiliary) verb in the sentence; (ii) no (other) logical predicate features in the sentence; (iii) no name or other sub-sentential referring expression features in the sentence; (iv) the sentence contains a quantifier that is not an occurrence of EXIST. Colin McGinn and Rod Girle have alleged that standard (...) first-order logic cannot adequately deal with some such existentials. The article defends the view that it can. (shrink)

This paper begins the study of first-order functions, which are a generalization of truth-functions. The concepts of truth-table and systems of truth-functions, both introduced in propositional logic by Post, are also generalized and studied in the quantificational setting. The general facts about these concepts are given in the first five sections, and constitute a “general theory” of first-order functions. The central theme of this paper is the relation of definition among notions expressed by formulas (...) of first-order logic. We emphasize that logic is not concerned only with the consequence relation among notions expressed by formulas. It also attends to the relation of definition among notions, where a notion is defined from other notions. Sections 5 and 6 deal exclusively with the relation of definition among notions expressed by formulas of first-order logic. In these sections, we study the systems of first-order functions, which are the sets of first-order functions closed under definitions. Sections 7 and 8 are concerned with the relativization of first-order functions to a class of structures. The relativization to a class of structures is a fundamental operation which is used in order to relate the theory of first-order functions with set theory and first-order model theory, a subject which we have barely scratched the surface. The apparatus developed in this paper enables us to define what is a vehicle for the foundation of classical mathematics in set theory, and, in Sect. 8, we prove that first-order logic with one binary predicate variable is not a minimal vehicle for the foundation of classical mathematics in set theory. Sections 9 and 10 introduce further operations and ideals of first-order functions. Besides some results on the influence of the arguments of a first-order function, a result about definability is proved in Sect. 10.1. It is this theorem that provides necessary and sufficient conditions for a first-order function to be in a finitely generated ideal. In Sect. 11, this result is applied to the problem of predicate definability in classes of structures, the problem with which Beth’s theorem dealt in the case of elementary classes. (shrink)

In the Tractatus, Wittgenstein advocates two major notational innovations in logic. First, identity is to be expressed by identity of the sign only, not by a sign for identity. Secondly, only one logical operator, called “N” by Wittgenstein, should be employed in the construction of compound formulas. We show that, despite claims to the contrary in the literature, both of these proposals can be realized, severally and jointly, in expressively complete systems of first-order logic. Building (...) on early work of Hintikka’s, we identify three ways in which the first notational convention can be implemented, show that two of these are compatible with the text of the Tractatus, and argue on systematic and historical grounds, adducing posthumous work of Ramsey’s, for one of these as Wittgenstein’s envisaged method. With respect to the second Tractarian proposal, we discuss how Wittgenstein distinguished between general and non-general propositions and argue that, claims to the contrary notwithstanding, an expressively adequate N-operator notation is implicit in the Tractatus when taken in its intellectual environment. We finally introduce a variety of sound and complete tableau calculi for first-order logics formulated in a Wittgensteinian notation. The first of these is based on the contemporary notion of logical truth as truth in all structures. The others take into account the Tractarian notion of logical truth as truth in all structures over one fixed universe of objects. Here the appropriate tableau rules depend on whether this universe is infinite or finite in size, and in the latter case on its exact finite cardinality. As it is obviously easy to express how propositions can be constructed by means of this operation and how propositions are not to be constructed by means of it, this must be capable of exact expression. 5.503. (shrink)

In preference aggregation a set of individuals express preferences over a set of alternatives, and these preferences have to be aggregated into a collective preference. When preferences are represented as orders, aggregation procedures are called social welfare functions. Classical results in social choice theory state that it is impossible to aggregate the preferences of a set of individuals under different natural sets of axiomatic conditions. We define a first-order language for social welfare functions and we give a complete (...) axiomatisation for this class, without having the number of individuals or alternatives specified in the language. We are able to express classical axiomatic requirements in our first-order language, giving formal axioms for three classical theorems of preference aggregation by Arrow, by Sen, and by Kirman and Sondermann. We explore to what extent such theorems can be formally derived from our axiomatisations, obtaining positive results for Sen’s Theorem and the Kirman-Sondermann Theorem. For the case of Arrow’s Theorem, which does not apply in the case of infinite societies, we have to resort to fixing the number of individuals with an additional axiom. In the long run, we hope that our approach to formalisation can serve as the basis for a fully automated proof of classical and new theorems in social choice theory. (shrink)

The main aim of this paper is to introduce first-order versions of logics of evidence and truth, together with corresponding sound and complete Kripke semantics with variable and constant domains. According to the intuitive interpretation proposed here, these logics intend to represent possibly inconsistent and incomplete information bases over time. The paper also discusses the connections between Belnap-Dunn’s and da Costa’s approaches to paraconsistency, and argues that the logics of evidence and truth combine them in a very natural (...) way. (shrink)

Classical logic has proved inadequate in various areas of computer science, artificial intelligence, mathematics, philosopy and linguistics. This is an introduction to extensions of first-order logic, based on the principle that many-sorted logic (MSL) provides a unifying framework in which to place, for example, second-order logic, type theory, modal and dynamic logics and MSL itself. The aim is two fold: only one theorem-prover is needed; proofs of the metaproperties of the different existing calculi (...) can be avoided by borrowing them from MSL. To make the book accessible to readers from different disciplines, whilst maintaining precision, the author has supplied detailed step-by-step proofs, avoiding difficult arguments, and continually motivating the material with examples. Consequently this can be used as a reference, for self-teaching or for first-year graduate courses. (shrink)

"In his introduction to this most welcome republication (and second edition) of his logic text, Heil clarifies his aim in writing and revising this book: 'I believe that anyone unfamiliar with the subject who set out to learn formal logic could do so relying solely on [this] book. That, in any case, is what I set out to create in writing An Introduction to First-Order Logic.' Heil has certainly accomplished this with perhaps the most explanatorily (...) thorough and pedagogically rich text I've personally come across. "Heil's text stands out as being remarkably careful in its presentation and illuminating in its explanations--especially given its relatively short length when compared to the average logic textbook. It hits all of the necessary material that must be covered in an introductory deductive logic course, and then some. It also takes occasional excursions into side topics, successfully whetting the reader's appetite for more advanced studies in logic. "The book is clearly written by an expert who has put in the effort for his readers, bothering at every step to see the point and then explain it clearly to his readers. Heil has found some very clever, original ways to introduce, motivate, and otherwise teach this material. The author's own special expertise and perspective--especially when it comes to tying philosophy of mind, linguistics, and philosophy of language into the lessons of logic--make for a creative and fresh take on basic logic. With its unique presentation and illuminating explanations, this book comes about as close as a text can come to imitating the learning environment of an actual classroom. Indeed, working through its presentations carefully, the reader feels as though he or she has just attended an illuminating lecture on the relevant topics!" --Jonah Schupbach, University of Utah. (shrink)

The volume includes the proceedings from the conference FOL75 -- 75 Years of First-Order Logic held at Humboldt University, Berlin, September 18 - 21, 2003 on the occasion of the anniversary of the publication of Hilbert's and Ackermann's Grundzuge der theoretischen Logik. The papers provide analyses of the historical conditions of the shaping of FOL, discuss several modern rivals to it, and show the importance of FOL for interdisciplinary research. While there is no doubt that the celebrated (...) book marks a most important step in the development of logic, the volume in hand proves the actuality of the question "Which logic is the right logic." The volume contains articles by: H. Andreka, J. X. Madarasz, I. Nemeti, A. Avron, K. Brunnler, A. Guglielmi, G. Englebretsen, W. Ewald, P. Hajek, J. Hintikka, W. Hodges, M. Kracht, R. Lanzet, H. Ben-Yami, C. Toke, S. P. Odintsov, H. Wansing, J. A. Robinson, M. Rossberg, M. Thielscher, D. E. Willard, andJ. Wole 'nski. (shrink)

We present an adaptation of continuous first order logic to unbounded metric structures. This has the advantage of being closer in spirit to C. Ward Henson's logic for Banach space structures than the unit ball approach, as well as of applying in situations where the unit ball approach does not apply. We also introduce the process of single point emph{emboundment}, allowing to bring unbounded structures back into the setting of bounded continuous first order (...) class='Hi'>logic. Together with results from cite{BenYaacov:Perturbations} regarding perturbations of bounded metric structures, we prove a Ryll-Nardzewski style characterisation of theories of Banach spaces which are separably categorical up to small perturbation of the norm. This last result is motivated by an unpublished result of Henson. (shrink)

What we call first‐order logic over fixed domain was initiated, in a certain guise, by Peirce around 1885 and championed, albeit in idiosyncratic form, by Zermelo in papers from the 1930s. We characterise such logics model‐ and proof‐theoretically and argue that they constitute exploration of a clearly circumscribed conception of domain‐dependent generality. Whereas a logic, or family of such, can be of interest for any of a variety of reasons, we suggest that one of those reasons (...) might be that said logic fosters some clarification regarding just what qualifies as a logical concept, a logical operation, or a logical law. (shrink)

If we speak of degrees of similarity, what kinds of judgment are we assuming to make sense? It will be argued that the necessary and sufficient condition for there to be degrees of similarity is that there should be a four-termed relation of comparative similarity — w resembles x at least as much as y resembles z—obeying certain constraints. Of course, nothing turns on how we use the words 'degree of similarity'. Rather, the point is to distinguish the different levels (...) of ideologicalcommitment which different kinds of judgment of similarity involve. (shrink)

Kolmogorov introduced an informal calculus of problems in an attempt to provide a classical semantics for intuitionistic logic. This was later formalised by Medvedev and Muchnik as what has come to be called the Medvedev and Muchnik lattices. However, they only formalised this for propositional logic, while Kolmogorov also discussed the universal quantifier. We extend the work of Medvedev to first-order logic, using the notion of a first-order hyperdoctrine from categorical logic, to (...) a structure which we will call the hyperdoctrine of mass problems. We study the intermediate logic that the hyperdoctrine of mass problems gives us, and we study the theories of subintervals of the hyperdoctrine of mass problems in an attempt to obtain an analogue of Skvortsova’s result that there is a factor of the Medvedev lattice characterising intuitionistic propositional logic. Finally, we consider Heyting arithmetic in the hyperdoctrine of mass problems and prove an analogue of Tennenbaum’s theorem on computable models of arithmetic. (shrink)

Introduction This is an elementary logic book designed for people who have no technical familiarity with modern logic but who have been reasoning, ...

In this paper we define computationally well-behaved versions of classical first-order logic and prove that the validity problem is decidable.

This paper shows that the logic known as Information-friendly logic (IF-logic) introduced by Jaakko Hintikka and Gabriel Sandu defines its own truth-predicate. The result is interesting given that IF logic is a much stronger logic than ordinary first-order logic and has also a well behaved notion of negation which, on its first-order subfragment, behaves like classical, contradictory negation.

This paper investigates the claim that the second-order consequence relation is intractable because of the incompleteness result for SOL. The opponents’ claim is that SOL cannot be proper logic since it does not have a complete deductive system. I argue that the lack of a completeness theorem, despite being an interesting result, cannot be held against the status of SOL as a proper logic.

We consider one aspect of the problem of specification and verification of reactive real-time systems which involve operations and constraints concerning time. Time is continuous what is motivated by specifications of hybrid systems. Our goal is to try to find a framework that is based on applied first order logic that permits to represent the verification problem directly, completely and conservatively , and that is apt to describe interesting decidable classes, maybe showing way to feasible algorithms. To (...) achieve this goal we use a first order timed logic that is an extension of a decidable theory of reals with timed functions. This logic permits, on the one hand, to rewrite directly and completely requirements and, on the other hand, to describe executions of various timed algorithms—here we consider block Gurevich abstract state machines because of their theoretical clarity and sufficient expressive power. Then we describe one decidable class of the verification problem that is based on notions reflecting finiteness properties of systems of control. These notions may be of independent interest, as, in particular, they give a way to describe a limited usage of arithmetics preserving decidability that is not covered by existing model-theoretic approaches. As an example we consider the generalized railroad crossing problem that we analyze in its entirety. (shrink)

We present the first-order logic of change, which is an extension of the propositional logic of change $\textsf {LC}\Box $ developed and axiomatized by Świętorzecka and Czermak. $\textsf {LC}\Box $ has two primitive operators: ${\mathcal {C}}$ to be read it changes whether and $\Box $ for constant unchangeability. It implements the philosophically grounded idea that with the help of the primary concept of change it is possible to define the concept of time. One of the characteristic (...) axioms for ${\mathcal {C}}$ is ${\mathcal {C}} A \to {\mathcal {C}}\neg A$ and one of the primitive rules is $\omega $-rule introducing $\Box $. It turns out that the next operator is definable in $\textsf {LC}\Box $. Logic $\textsf {LC}\Box $ with next is equivalent to certain fragment of $\textsf {LTL}$ extended by the appropriate definition of ${\mathcal {C}}$. Recently, $\textsf {LC}\Box $ has also been modified to the propositional logic of ‘branching’ changes $\textsf {BTC}$ by Łyczak and the logic of ‘parallel’ changes $\textsf {LC}\Box $ ↳ by Świętorzecka and Łyczak. Extended in an appropriate manner, $\textsf {BTC}$ is equivalent to a certain fragment of logic $\textsf {CTL}$ to which definitions of two kinds of changes have been added. Here we propose an extension of $\textsf {LC}\Box $ to first-order logic in which, again, the only primitive modal operators are ${\mathcal {C}}$ and $\Box $. We interpret our logic in the semantics of histories of changes. We give an axiomatic system $\textsf {LC}\Box Q$ for the considered logic, and we show selected theses about some relationships between ${\mathcal {C}}$, $\Box $ and $\forall $. Then we prove the completeness of $\textsf {LC}\Box Q$. Finally, we compare our logic with $\textsf {FOLT}$ and show the relation between $\textsf {LC}\Box Q$ and a certain fragment of the Kröger system $\varSigma $ to which the definition of ${\mathcal {C}}$ was added. (shrink)

What we call the Hilbert‐Bernays (HB) Theorem establishes that for any satisfiable first‐order quantificational schema S, there are expressions of elementary arithmetic that yield a true sentence of arithmetic when they are substituted for the predicate letters in S. Our goals here are, first, to explain and defend W. V. Quine's claim that the HB theorem licenses us to define the first‐order logical validity of a schema in terms of predicate substitution; second, to clarify the (...) theorem by sketching an accessible and illuminating new proof of it; and, third, to explain how Quine's substitutional definition of logical notions can be modified and extended in ways that make it more attractive to contemporary logicians. (shrink)

Basic Formal Ontology (BFO) is a top-level ontology used in hundreds of active projects in scientific and other domains. BFO has been selected to serve as top-level ontology in the Industrial Ontologies Foundry (IOF), an initiative to create a suite of ontologies to support digital manufacturing on the part of representatives from a number of branches of the advanced manufacturing industries. We here present a first draft set of axioms and definitions of an IOF upper ontology descending from BFO. (...) The axiomatization is designed to capture the meanings of terms commonly used in manufacturing and is designed to serve as starting point for the construction of the IOF ontology suite. (shrink)

In this paper we prove that $\forall \textrm{FO}$, the universal fragment of first-order logic, is superfluous in $\varSigma _2^p$ and $\varPi _2^p$. As an example, we show that this yields a syntactic proof of the $\varSigma _2^p$-completeness of value-cost satisfiability. The superfluity method is interesting since it gives a way to prove completeness of problems involving numerical data such as lengths, weights and costs and it also adds to the programme started by Immerman and Medina about the (...) syntactic approach in the study of completeness. (shrink)

Motivation and perspective for an exciting new research direction interconnecting logic, spacetime theory, relativity--including such revolutionary areas as black hole physics, relativistic computers, new cosmology--are presented in this paper. We would like to invite the logician reader to take part in this grand enterprise of the new century. Besides general perspective and motivation, we present initial results in this direction.

Starting from certain metalogical results, I argue that first-order logical truths of classical logic are a priori and necessary. Afterwards, I formulate two arguments for the idea that first-order logical truths are also analytic, namely, I first argue that there is a conceptual connection between aprioricity, necessity, and analyticity, such that aprioricity together with necessity entails analyticity; then, I argue that the structure of natural deduction systems for FOL displays the analyticity of its truths. (...) Consequently, each philosophical approach to these truths should account for this evidence, i.e., that first-order logical truths are a priori, necessary, and analytic, and it is my contention that the semantic account is a better candidate. (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)

For first order languages with no individual constants, empty structures and truth values (for sentences) in them are defined. The first order theories of the empty structures and of all structures (the empty ones included) are axiomatized with modus ponens as the only rule of inference. Compactness is proved and decidability is discussed. Furthermore, some well known theorems of model theory are reconsidered under this new situation. Finally, a word is said on other approaches to the (...) whole problem. (shrink)

The paper presents Property Theory with Curry Typing (PTCT) where the language of terms and well-formed formulæ are joined by a language of types. In addition to supporting fine-grained intensionality, the basic theory is essentially first-order, so that implementations using the theory can apply standard first-order theorem proving techniques. Some extensions to the type theory are discussed, type polymorphism, and enriching the system with sufficient number theory to account for quantifiers of proportion, such as “most.”.

The Language of First-Order Logic is a complete introduction to first-order symbolic logic, consisting of a computer program and a text. The program, an aid to learning and using symbolic notation, allows one to construct symbolic sentences and possible worlds, and verify that a sentence is well formed. The truth or falsity of a sentence can be determined by playing a deductive game with the computer.

W. V. Quine thinks logical truth can be defined in purely extensional terms, as follows: a logical truth is a true sentence that exemplifies a logical form all of whose instances are true. P. F. Strawson objects that one cannot say what it is for a particular use of a sentence to exemplify a logical form without appealing to intensional notions, and hence that Quine's efforts to define logical truth in purely extensional terms cannot succeed. Quine's reply to this criticism (...) is confused in ways that have not yet been noticed in the literature. This may seem to favour Strawson's side of the debate. In fact, however, a proper analysis of the difficulties that Quine's reply faces suggests a new way to clarify and defend the view that logical truth can be defined in purely extensional terms. (shrink)

Some authors have studied in an ad hoc fashion the inclusive logics, that is the logics which admit or include objects or sets without element. These logics have been recently brought into the limelight because of the use of arbitrary topoi for interpreting languages. (In topoi there are usually many objects without element.)The aim of the paper is to present, for some inclusive logics, an axiomatization as natural and as simple as possible. Because of the intended applications to category theory, (...) the logics studied are many-sorted and intuitionistic. (shrink)

Applying first-order logic to derive the consequences of laws that are only approximately true of empirical phenomena involves idealization of a kind that is akin to applying arithmetic to calculate the area of a rectangular surface from approximate measures of the lengths of its sides. Errors in the data, in the exactness of the lengths in one case and in the exactness of the laws in the other, are in some measure transmitted to the consequences deduced from (...) them, and the aim of a theory of idealization is to describe this process. The present paper makes a start on this in the case of applied first-order logic, and relates it to Plato's picture of a world or model of 'appearances' in which laws are only approximately true, but which to some extent resembles an ideal world or model in which they are exactly true. (shrink)