scholarly journals Syntax and Semantics of the logic L_omega omega^lambda

1997 ◽  
Vol 4 (22) ◽  
Author(s):  
Carsten Butz
Keyword(s):  
Order Logic ◽  
First Order Logic ◽  
Generic Model ◽  
First Order ◽  
Geometric Morphisms

In this paper we study the logic L_omega omega^lambda , which is first order logic<br /> extended by quantification over functions (but not over relations).<br > We give the syntax of the logic, as well as the semantics in Heyting<br /> categories with exponentials. Embedding the generic model of a theory<br /> into a Grothendieck topos yields completeness of L_omega omega^lambda with respect<br /> to models in Grothendieck toposes, which can be sharpened to completeness<br />with respect to Heyting valued models. The logic L_omega omega^lambda is the<br />strongest for which Heyting valued completeness is known. Finally,<br />we relate the logic to locally connected geometric morphisms between toposes.

scholarly journals Classifying Toposes for First Order Theories

1997 ◽  
Vol 4 (20) ◽  
Author(s):  
Carsten Butz ◽  
Peter T. Johnstone
Keyword(s):  
Order Theory ◽  
Order Logic ◽  
First Order Logic ◽  
Conservative Extension ◽  
First Order ◽  
First Order Theory ◽  
Smallness Condition ◽  
Geometric Morphisms

By a classifying topos for a first-order theory T, we mean a topos<br />E such that, for any topos F, models of T in F correspond exactly to<br />open geometric morphisms F ! E. We show that not every (infinitary)<br />first-order theory has a classifying topos in this sense, but we<br />characterize those which do by an appropriate `smallness condition',<br />and we show that every Grothendieck topos arises as the classifying<br />topos of such a theory. We also show that every first-order theory<br /> has a conservative extension to one which possesses<br /> a classifying topos, and we obtain a Heyting-valued completeness<br /> theorem for infinitary first-order logic.

Definability and descent

1998 ◽  
Vol 63 (2) ◽  
pp. 372-378 ◽  
Author(s):  
David Ballard ◽  
William Boshuck
Keyword(s):  
Model Theory ◽  
Present Note ◽  
Order Logic ◽  
First Order Logic ◽  
Covering Theorem ◽  
First Order ◽  
Natural Transformations ◽  
Geometric Morphisms ◽  
Exact Categories

The present note offers a short argument for the descent theorems of Zawadowski [10] (originally [9]) and Makkai [6], which were conjectured by Pitts after the descent theorem of Joyal and Tierney [3] for open geometric morphisms of (Grothendieck) toposes. The original proofs, which involve variants of Makkai's [5] duality for first order logic, are rather involved and there has been considerable interest in locating simpler proofs. Viewed categorically, the descent theorems establish a bicategorical exactness property (conservative morphisms are effective descent) for pretop (the 2-category of small pretoposes, pretopos functors, and natural transformations), for exact (exact categories, exact functors, and natural transformations), and for bpretop* (Boolean pretoposes, pretopos functors, and natural isomorphisms). Viewed logically, they fragment into a familiar Beth/Tarski-type definability theorem and a covering theorem for certain functors on PCΔ-categories (groupoids, in the Boolean case); the latter (as the former) is a arithmetical statement about the syntax of first order logic ([6, §3])).The argument here involves special models and, independently, a continuity lemma of Makkai. The use of special models is axiomatic in that only a few properties (listed below) are needed. The continuity lemma, 9.1 of [6], is established via forcing and can be read independently of the rest of that paper. Because of its interest to both the model theorist and the category theorist, the argument is first given as straight model theory and afterwards it is briefly indicated how the descent theorems follow.

First-Order Logic Reasoning Support for the Semantic Web

2009 ◽  
Vol 19 (12) ◽  
pp. 3091-3099 ◽  
Author(s):  
Gui-Hong XU ◽  
Jian ZHANG
Keyword(s):  
Semantic Web ◽  
Order Logic ◽  
First Order Logic ◽  
First Order ◽  
Logic Reasoning

Boolean-valued structures

2018 ◽  
Author(s):  
Tim Button ◽  
Sean Walsh
Keyword(s):  
Model Theory ◽  
Order Logic ◽  
First Order Logic ◽  
Inference Rules ◽  
Mathematical Concepts ◽  
Semantic Framework ◽  
First Order ◽  
Standard Models ◽  
Boolean Valued Model ◽  
Semantic Values

Chapters 6-12 are driven by questions about the ability to pin down mathematical entities and to articulate mathematical concepts. This chapter is driven by similar questions about the ability to pin down the semantic frameworks of language. It transpires that there are not just non-standard models, but non-standard ways of doing model theory itself. In more detail: whilst we normally outline a two-valued semantics which makes sentences True or False in a model, the inference rules for first-order logic are compatible with a four-valued semantics; or a semantics with countably many values; or what-have-you. The appropriate level of generality here is that of a Boolean-valued model, which we introduce. And the plurality of possible semantic values gives rise to perhaps the ‘deepest’ level of indeterminacy questions: How can humans pin down the semantic framework for their languages? We consider three different ways for inferentialists to respond to this question.

scholarly journals Extensions in graph normal form

2020 ◽  
Author(s):  
Michał Walicki
Keyword(s):  
Normal Form ◽  
Fixed Points ◽  
Propositional Logic ◽  
Order Logic ◽  
First Order Logic ◽  
First Order ◽  
Special Cases

Abstract Graph normal form, introduced earlier for propositional logic, is shown to be a normal form also for first-order logic. It allows to view syntax of theories as digraphs, while their semantics as kernels of these digraphs. Graphs are particularly well suited for studying circularity, and we provide some general means for verifying that circular or apparently circular extensions are conservative. Traditional syntactic means of ensuring conservativity, like definitional extensions or positive occurrences guaranteeing exsitence of fixed points, emerge as special cases.

Relational Chase Procedures Interpreted as Resolution with Paramodulation1

1991 ◽  
Vol 15 (2) ◽  
pp. 123-138
Author(s):  
Joachim Biskup ◽  
Bernhard Convent
Keyword(s):  
Alternative Interpretation ◽  
Order Logic ◽  
First Order Logic ◽  
Inference Problem ◽  
First Order ◽  
Inference Problems ◽  
The One ◽  
The Relationship ◽  
Theoretical Foundations ◽  
Insight Into

In this paper the relationship between dependency theory and first-order logic is explored in order to show how relational chase procedures (i.e., algorithms to decide inference problems for dependencies) can be interpreted as clever implementations of well known refutation procedures of first-order logic with resolution and paramodulation. On the one hand this alternative interpretation provides a deeper insight into the theoretical foundations of chase procedures, whereas on the other hand it makes available an already well established theory with a great amount of known results and techniques to be used for further investigations of the inference problem for dependencies. Our presentation is a detailed and careful elaboration of an idea formerly outlined by Grant and Jacobs which up to now seems to be disregarded by the database community although it definitely deserves more attention.

scholarly journals Formula size games for modal logic and μ-calculus

2019 ◽  
Vol 29 (8) ◽  
pp. 1311-1344 ◽  
Author(s):  
Lauri T Hella ◽  
Miikka S Vilander
Keyword(s):  
Modal Logic ◽  
Optimal Strategy ◽  
Order Logic ◽  
First Order Logic ◽  
Kripke Models ◽  
First Order ◽  
Modal Operators ◽  
Crucial Difference ◽  
Definition Of ◽  
Person Game

Abstract We propose a new version of formula size game for modal logic. The game characterizes the equivalence of pointed Kripke models up to formulas of given numbers of modal operators and binary connectives. Our game is similar to the well-known Adler–Immerman game. However, due to a crucial difference in the definition of positions of the game, its winning condition is simpler, and the second player does not have a trivial optimal strategy. Thus, unlike the Adler–Immerman game, our game is a genuine two-person game. We illustrate the use of the game by proving a non-elementary succinctness gap between bisimulation invariant first-order logic $\textrm{FO}$ and (basic) modal logic $\textrm{ML}$. We also present a version of the game for the modal $\mu $-calculus $\textrm{L}_\mu $ and show that $\textrm{FO}$ is also non-elementarily more succinct than $\textrm{L}_\mu $.

Sign in / Sign up

Export Citation Format

Share Document