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)

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)

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

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.

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)

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)

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)

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)

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)

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

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)

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)

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)

We show that the loosely guarded and packed fragments of first-order logic have the finite model property. We use a construction of Herwig and Hrushovski. We point out some consequences in temporal predicate logic and algebraic logic.

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)

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)

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)

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

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)

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.

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.

Under a proper translation, the languages of propositional (and quantified relevant logic) with an absurdity constant are characterized as the fragments of first order logic preserved under (world-object) relevant directed bisimulations. Furthermore, the properties of pointed models axiomatizable by sets of propositional relevant formulas have a purely algebraic characterization. Finally, a form of the interpolation property holds for the relevant fragment of first order logic.

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)

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)

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 one-variable fragment of a first-order logic may be viewed as an “S5-like” modal logic, where the universal and existential quantifiers are replaced by box and diamond modalities, respectively. Axiomatizations of these modal logics have been obtained for special cases—notably, the modal counterparts $\mathrm {S5}$ and $\mathrm {MIPC}$ of the one-variable fragments of first-order classical logic and first-order intuitionistic logic, respectively—but a general approach, extending beyond first-order intermediate logics, (...) has been lacking. To this end, a sufficient criterion is given in this paper for the one-variable fragment of a semantically defined first-order logic—spanning families of intermediate, substructural, many-valued, and modal logics—to admit a certain natural axiomatization. More precisely, an axiomatization is obtained for the one-variable fragment of any first-order logic based on a variety of algebraic structures with a lattice reduct that has the superamalgamation property, using a generalized version of a functional representation theorem for monadic Heyting algebras due to Bezhanishvili and Harding. An alternative proof-theoretic strategy for obtaining such axiomatization results is also developed for first-order substructural logics that have a cut-free sequent calculus and admit a certain interpolation property. (shrink)

We prove a generalization of Maehara’s lemma to show that the extensions of classical and intuitionistic first-order logic with a special type of geometric axioms, called singular geometric axioms, have Craig’s interpolation property. As a corollary, we obtain a direct proof of interpolation for (classical and intuitionistic) first-order logic with identity, as well as interpolation for several mathematical theories, including the theory of equivalence relations, (strict) partial and linear orders, and various intuitionistic order (...) theories such as apartness and positive partial and linear orders. (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)

In theTractatus, 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 theTractatus, 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 theTractatuswhen 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 an earlier defense of the view that the fundamental logical properties of logical truth and logical consequence obtain or fail to obtain only relative to contexts, I focused on a variation of Kaplan’s own modal logic of indexicals. In this paper, I state a semantics and sketch a system of proof for a first-order logic of demonstratives, and sketch proofs of soundness and completeness. (I omit details for readability.) That these results obtain for the (...) class='Hi'>first-order logic of demonstratives shows that the significance of demonstratives for logic exceeds their behavior as rigid designators in counterfactual reasoning, or reasoning about alternative possibilities. Furthermore, the results in this paper help address one common objection to the view that logical truth and consequence obtain only relative to contexts. According to this objection, the view entails that logical consequence is not formal. (shrink)

We consider a new fragment of first-order logic with two variables. This logic is defined over interval structures. It constitutes unary predicates, a binary predicate and a function symbol. Considering such a fragment of first-order logic is motivated by defining a general framework for event-based interval temporal logics. In this paper, we present a sound, complete and terminating decision procedure for this logic. We show that the logic is decidable, and provide (...) a NEXPTIME complexity bound for satisfiability. This result shows that even a simple decidable fragment of first-order logic has NEXPTIME complexity. (shrink)

This book is intended, along with the computer program, to introduce the user to some of the most important concepts and tools of logic, including learning a new computer language.

We study the class of Sperner spaces, a generalized version of affine spaces, as defined in the language of pointline incidence and line parallelity. We show that, although the class of Sperner spaces is a pseudo-elementary class, it is not elementary nor even ℒ∞ω-axiomatizable. We also axiomatize the first-order theory of this class.

A classical reconstruction of Wright’s first-order logic of strict finitism is presented. Strict finitism is a constructive standpoint of mathematics that is more restrictive than intuitionism. Wright sketched the semantics of said logic in Wright (Realism, Meaning and Truth, chap 4, 2nd edition in 1993. Blackwell Publishers, Oxford, Cambridge, pp.107–75, 1982), in his strict finitistic metatheory. Yamada (J Philos Log. https://doi.org/10.1007/s10992-022-09698-w, 2023) proposed, as its classical reconstruction, a propositional logic of strict finitism under an auxiliary (...) condition that makes the logic correspond with intuitionistic propositional logic. In this paper, we extend the propositional logic to a first-order logic that does not assume the condition. We will provide a sound and complete pair of a Kripke-style semantics and a natural deduction system, and show that if the condition is imposed, then the logic exhibits natural extensions of Yamada (2023)’s results. (shrink)

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.

An algebraization of multi-signature first-order logic without terms is presented. Rather than following the traditional method of choosing a type of algebras and constructing an appropriate variety, as is done in the case of cylindric and polyadic algebras, a new categorical algebraization method is used: The substitutions of formulas of one signature for relation symbols in another are treated in the object language. This enables the automatic generation via an adjunction of an algebraic theory. The algebras of (...) this theory are then used to algebraize first-order logic. (shrink)

Inquisitive first-order logic, InqBQ, is a system which extends classical first-order logic with formulas expressing questions. From a mathematical point of view, formulas in this logic express properties of sets of relational structures. This paper makes two contributions to the study of this logic. First, we describe an Ehrenfeucht–Fraïssé game for InqBQ and show that it characterizes the distinguishing power of the logic. Second, we use the game to study cardinality (...) quantifiers in the inquisitive setting. That is, we study what statements and questions can be expressed in InqBQ about the number of individuals satisfying a given predicate. As special cases, we show that several variants of the question how many individuals satisfy α(x) are not expressible in InqBQ, both in the general case and in restriction to finite models. (shrink)