scholarly journals A Novel Categorical Approach to Semantics of Relational First-Order Logic

Symmetry ◽  
2020 ◽  
Vol 12 (10) ◽  
pp. 1584
Author(s):  
Wolfgang Schreiner ◽  
William Steingartner ◽  
Valerie Novitzká
Keyword(s):  
Term Structure ◽  
Set Theory ◽  
Order Logic ◽  
First Order Logic ◽  
Basic Logic ◽  
Categorical Approach ◽  
First Order ◽  
The Core ◽  
Deduction Rules ◽  
Categorical Semantics

We present a categorical formalization of a variant of first-order logic. Unlike other texts on this topic, the goal of this paper is to give a very transparent and self-contained account without requiring more background than basic logic and set theory. Our focus is to show how the semantics of first-order formulas can be derived from their usual deduction rules. For understanding the core ideas, it is not necessary to investigate the internal term structure of atomic formulas, thus we abstract atomic formulas to (syntactically opaque) relations; in this sense, our variant of first-order logic is “relational”. While the derived semantics is based on categorical principles (even the duality that arises from a symmetry between two ways of looking at something where there is no reason to choose one over the other), it is nevertheless “constructive” in that it describes explicit computations of the truth values of formulas. We demonstrate this by modeling the categorical semantics in the RISCAL (RISC Algorithm Language) system which allows us to validate the core propositions by automatically checking them in finite models.

Resolution in type theory

1971 ◽  
Vol 36 (3) ◽  
pp. 414-432 ◽  
Author(s):  
Peter B. Andrews
Keyword(s):  
Set Theory ◽  
Type Theory ◽  
Higher Order ◽  
Order Logic ◽  
First Order Logic ◽  
Higher Order Logic ◽  
First Order ◽  
Different Types ◽  
Axiomatic Set Theory ◽  
Order Predicate Calculus

In [8] J. A. Robinson introduced a complete refutation procedure called resolution for first order predicate calculus. Resolution is based on ideas in Herbrand's Theorem, and provides a very convenient framework in which to search for a proof of a wff believed to be a theorem. Moreover, it has proved possible to formulate many refinements of resolution which are still complete but are more efficient, at least in many contexts. However, when efficiency is a prime consideration, the restriction to first order logic is unfortunate, since many statements of mathematics (and other disciplines) can be expressed more simply and naturally in higher order logic than in first order logic. Also, the fact that in higher order logic (as in many-sorted first order logic) there is an explicit syntactic distinction between expressions which denote different types of intuitive objects is of great value where matching is involved, since one is automatically prevented from trying to make certain inappropriate matches. (One may contrast this with the situation in which mathematical statements are expressed in the symbolism of axiomatic set theory.).

scholarly journals Strong Logics of First and Second Order

2010 ◽  
Vol 16 (1) ◽  
pp. 1-36 ◽  
Author(s):  
Peter Koellner
Keyword(s):  
Set Theory ◽  
Large Cardinal ◽  
Second Order ◽  
Order Logic ◽  
First Order Logic ◽  
Close Correspondence ◽  
First Order ◽  
Second Order Logic

AbstractIn this paper we investigate strong logics of first and second order that have certain absoluteness properties. We begin with an investigation of first order logic and the strong logics ω-logic and β-logic, isolating two facets of absoluteness, namely, generic invariance and faithfulness. It turns out that absoluteness is relative in the sense that stronger background assumptions secure greater degrees of absoluteness. Our aim is to investigate the hierarchies of strong logics of first and second order that are generically invariant and faithful against the backdrop of the strongest large cardinal hypotheses. We show that there is a close correspondence between the two hierarchies and we characterize the strongest logic in each hierarchy. On the first-order side, this leads to a new presentation of Woodin's Ω-logic. On the second-order side, we compare the strongest logic with full second-order logic and argue that the comparison lends support to Quine's claim that second-order logic is really set theory in sheep's clothing.

scholarly journals Much Ado About the Many

2021 ◽  
Vol 25 (1) ◽  
Author(s):  
Jonathan Mai
Keyword(s):  
Set Theory ◽  
Formal Theory ◽  
Order Logic ◽  
First Order Logic ◽  
Plural Quantification ◽  
First Order ◽  
Order Language ◽  
The Many ◽  
Second Order Logic ◽  
Alternative Theories

English distinguishes between singular quantifiers like "a donkey" and plural quantifiers like "some donkeys". Pluralists hold that plural quantifiers range in an unusual, irreducibly plural, way over common objects, namely individuals from first-order domains and not over set-like objects. The favoured framework of pluralism is plural first-order logic, PFO, an interpreted first-order language that is capable of expressing plural quantification. Pluralists argue for their position by claiming that the standard formal theory based on PFO is both ontologically neutral and really logic. These properties are supposed to yield many important applications concerning second-order logic and set theory that alternative theories supposedly cannot deliver. I will show that there are serious reasons for rejecting at least the claim of ontological innocence. Doubt about innocence arises on account of the fact that, when properly spelled out, the PFO-semantics for plural quantifiers is committed to set-like objects. The correctness of my worries presupposes the principle that for every plurality there is a coextensive set. Pluralists might reply that this principle leads straight to paradox. However, as I will argue, the true culprit of the paradox is the assumption that every definite condition determines a plurality.

Topos-theoretic background

2018 ◽  
Author(s):  
Olivia Caramello
Keyword(s):  
Category Theory ◽  
Order Theory ◽  
Order Logic ◽  
Basic Theory ◽  
First Order Logic ◽  
Syntactic Category ◽  
First Order ◽  
Deductive Systems ◽  
First Order Theory ◽  
Categorical Semantics

This chapter provides the topos-theoretic background necessary for understanding the contents of the book; the presentation is self-contained and only assumes a basic familiarity with the language of category theory. The chapter begins by reviewing the basic theory of Grothendieck toposes, including the fundamental equivalence between geometric morphisms and flat functors. Then it presents the notion of first-order theory and the various deductive systems for fragments of first-order logic that will be considered in the course of the book, notably including that of geometric logic. Further, it discusses categorical semantics, i.e. the interpretation of first-order theories in categories possessing ‘enough’ structure. Lastly, the key concept of syntactic category of a first-order theory is reviewed; this notion will be used in Chapter 2 for constructing classifying toposes of geometric theories.

Gödel, Kurt (1906–78)

2018 ◽  
Author(s):  
John W. Dawson
Keyword(s):  
Twentieth Century ◽  
Set Theory ◽  
Continuum Hypothesis ◽  
Order Logic ◽  
First Order Logic ◽  
First Order ◽  
Mathematical Platonism ◽  
The Axiom Of Choice ◽  
Fundamental Theorems ◽  
The Continuum

The greatest logician of the twentieth century, Gödel is renowned for his advocacy of mathematical Platonism and for three fundamental theorems in logic: the completeness of first-order logic; the incompleteness of formalized arithmetic; and the consistency of the axiom of choice and the continuum hypothesis with the axioms of Zermelo–Fraenkel set theory.

scholarly journals SGGS Theorem Proving: an Exposition

10.29007/m2vf ◽  
2018 ◽  
Author(s):  
Maria Paola Bonacina ◽  
David Plaisted
Keyword(s):  
Theorem Proving ◽  
Order Logic ◽  
First Order Logic ◽  
Candidate Model ◽  
Narrative Style ◽  
First Order ◽  
The Core ◽  
Theorem Provers ◽  
Instance Generation ◽  
Main Ideas

We present in expository style the main ideas in SGGS, which stands for Semantically-Guided Goal-Sensitive theorem proving. SGGS uses sequences of constrained clauses to represent models, instance generation to go from a candidate model to the next, and resolution as well as other inferences to repair the model. SGGS is refutationally complete for first-order logic, DPLL-style model based, semantically guided, goal sensitive, and proof confluent, which appears to be a rare combination of features. In this paper we describe the core of SGGS in a narrative style, emphasizing ideas and trying to keep technicalities to a minimum, in order to advertise it to builders and users of theorem provers.

Completeness and Herbrand theorems for nominal logic

2006 ◽  
Vol 71 (1) ◽  
pp. 299-320 ◽  
Author(s):  
James Cheney
Keyword(s):  
Set Theory ◽  
Order Logic ◽  
Theory And Practice ◽  
First Order Logic ◽  
Abstract Syntax ◽  
Finite Support ◽  
First Order ◽  
Nominal Logic ◽  
Abstract Syntax Trees ◽  
Herbrand Models

AbstractNominal logic is a variant of first-order logic in which abstract syntax with names and binding is formalized in terms of two basic operations: name-swapping andfreshness. It relies on two important principles: equivariance (validity is preserved by name-swapping), and fresh name generation (“new” or fresh names can always be chosen). It is inspired by a particular class of models for abstract syntax trees involving names and binding, drawing on ideas from Fraenkel-Mostowski set theory: finite-support models in which each value can depend on only finitely many names.Although nominal logic is sound with respect to such models, it is not complete. In this paper we review nominal logic and show why finite-support models are insufficient both in theory and practice. We then identify (up to isomorphism) the class of models with respect to which nominal logic is complete: ideal-supported models in which the supports of values are elements of a proper ideal on the set of names.We also investigate an appropriate generalization of Herbrand models to nominal logic. After adjusting the syntax of nominal logic to include constants denoting names, we generalize universal theories to nominal-universal theories and prove that each such theory has an Herbrand model.

Set theory in first-order logic: Clauses for Gödel's axioms

1986 ◽  
Vol 2 (3) ◽  
pp. 287-327 ◽  
Author(s):  
Robert Boyer ◽  
Ewing Lusk ◽  
William McCune ◽  
Ross Overbeek ◽  
Mark Stickel ◽  
...  
Keyword(s):  
Set Theory ◽  
Order Logic ◽  
First Order Logic ◽  
First Order
Sign in / Sign up

Export Citation Format

Share Document