Formal topologies on the set of first-order formulae

2000 ◽  
Vol 65 (3) ◽  
pp. 1183-1192 ◽  
Author(s):  
Thierry Coquand ◽  
Sara Sadocco ◽  
Giovanni Sambin ◽  
Jan M. Smith
Keyword(s):  
Order Logic ◽  
Macneille Completion ◽  
Real Numbers ◽  
Algebraic Form ◽  
Completeness Proof ◽  
First Order ◽  
Existence Property ◽  
The One ◽  
Dedekind Cuts ◽  
Formal Topology

The completeness proof for first-order logic by Rasiowa and Sikorski [13] is a simplification of Henkin's proof [7] in that it avoids the addition of infinitely many new individual constants. Instead they show that each consistent set of formulae can be extended to a maximally consistent set, satisfying the following existence property: if it contains (∃x)ϕ it also contains some substitution ϕ(y/x) of a variable y for x. In Feferman's review [5] of [13], an improvement, due to Tarski, is given by which the proof gets a simple algebraic form.Sambin [16] used the same method in the setting of formal topology [15], thereby obtaining a constructive completeness proof. This proof is elementary and can be seen as a constructive and predicative version of the one in Feferman's review. It is a typical, and simple, example where the use of formal topology gives constructive sense to the existence of a generic object, satisfying some forcing conditions; in this case an ultrafilter satisfying the existence property.In order to get a formal topology on the set of first-order formulae, Sambin used the Dedekind-MacNeille completion to define a covering relation ⊲DM. This method, by which an arbitrary poset can be extended to a complete poset, was introduced by MacNeille [9] and is a generalization of the construction of real numbers from rationals by Dedekind cuts. It is also possible to define an inductive cover, ⊲I, on the set of formulae, which can also be used to give canonical models, see Coquand and Smith [3].

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.

A probabilistic interpolation theorem

1985 ◽  
Vol 50 (3) ◽  
pp. 708-713 ◽  
Author(s):  
Douglas N. Hoover
Keyword(s):  
Interpolation Theorem ◽  
Order Logic ◽  
First Order Logic ◽  
Probability Logic ◽  
Admissible Set ◽  
First Order ◽  
Probability Spaces ◽  
Image Position ◽  
Dedekind Cuts ◽  
Exact Definition

The probability logic is a logic with a natural interpretation on probability spaces (thus, a logic whose model theory is part of probability theory rather than a system for putting probabilities on formulas of first order logic). Its exact definition and basic development are contained in the paper [3] of H. J. Keisler and the papers [1] and [2] of the author. Building on work in [2], we prove in this paper the following probabilistic interpolation theorem for .Let L be a countable relational language, and let A be a countable admissible set with ω ∈ A (in this paper some probabilistic notation will be used, but ω will always mean the least infinite ordinal). is the admissible fragment of corresponding to A. We will assume that L is a countable set in A, as is usual in practice, though all that is in fact needed for our proof is that L be a set in A which is wellordered in A.Theorem. Let ϕ(x) and ψ(x) be formulas of LAP such thatwhere ε ∈ [0, 1) is a real in A (reals may be defined in the usual way as Dedekind cuts in the rationals). Then for any real d > ε¼, there is a formula θ(x) of (L(ϕ) ∩ L(ψ))AP such thatand

Cognitive Modelling Applied to Aspects of Schizophrenia and Autonomic Computing

2011 ◽  
pp. 220-234
Author(s):  
Lee Flax
Keyword(s):  
Autonomic Computing ◽  
Signs And Symptoms ◽  
Order Logic ◽  
First Order Logic ◽  
Object Language ◽  
Cognitive Modelling ◽  
Belief Contraction ◽  
Algebraic Version ◽  
First Order ◽  
The One

We give an approach to cognitive modelling, which allows for richer expression than the one based simply on the firing of sets of neurons. The object language of the approach is first-order logic augmented by operations of an algebra, PSEN. Some operations useful for this kind of modelling are postulated: combination, comparison, and inhibition of sets of sentences. Inhibition is realised using an algebraic version of AGM belief contraction (Gärdenfors, 1988). It is shown how these operations can be realised using PSEN. Algebraic modelling using PSEN is used to give an account of an explanation of some signs and symptoms of schizophrenia due to Frith (1992) as well as a proposal for the cognitive basis of autonomic computing. A brief discussion of the computability of the operations of PSEN is also given.

On the first-order logic of terms

1973 ◽  
Vol 38 (2) ◽  
pp. 177-188
Author(s):  
Lars Svenonius
Keyword(s):  
Order Logic ◽  
First Order Logic ◽  
Identity Function ◽  
First Order ◽  
Elementary Condition ◽  
Combinatorial Function ◽  
The One ◽  
Definition Of ◽  
Image Position

By an elementary condition in the variablesx1, …, xn, we mean a conjunction of the form x1 ≤ i < j ≤ naij where each aij is one of the formulas xi = xj or xi ≠ xj. (We should add that the formula x1 = x1 should be regarded as an elementary condition in the one variable x1.)Clearly, according to this definition, some elementary conditions are inconsistent, some are consistent. For instance (in the variables x1, x2, x3) the conjunction x1 = x2 & x1 = x3 & x2 ≠ x3 is inconsistent.By an elementary combinatorial function (ex. function) we mean any function which can be given a definition of the formwhere E1(x1, …, xn), …, Ek(x1, …, xn) is an enumeration of all consistent elementary conditions in x1, …, xn, and all the numbers d1, …, dk are among 1, …, n.Examples. (1) The identity function is the only 1-ary e.c. function.(2) A useful 3-ary e.c. function will be called J. The definition is

scholarly journals On p/q-recognisable sets

2021 ◽  
Vol Volume 17, Issue 3 ◽  
Author(s):  
Victor Marsault
Keyword(s):  
Rational Number ◽  
Finite Automata ◽  
Order Relation ◽  
Order Logic ◽  
Natural Order ◽  
First Order ◽  
Finite Word ◽  
Numeration Systems ◽  
The One ◽  
Context Free

Let p/q be a rational number. Numeration in base p/q is defined by a function that evaluates each finite word over A_p={0,1,...,p-1} to some rational number. We let N_p/q denote the image of this evaluation function. In particular, N_p/q contains all nonnegative integers and the literature on base p/q usually focuses on the set of words that are evaluated to nonnegative integers; it is a rather chaotic language which is not context-free. On the contrary, we study here the subsets of (N_p/q)^d that are p/q-recognisable, i.e. realised by finite automata over (A_p)^d. First, we give a characterisation of these sets as those definable in a first-order logic, similar to the one given by the B\"uchi-Bruy\`ere Theorem for integer bases numeration systems. Second, we show that the natural order relation and the modulo-q operator are not p/q-recognisable.

Logic, sheaves, and factorization systems

1993 ◽  
Vol 58 (3) ◽  
pp. 872-893
Author(s):  
G. P. Monro
Keyword(s):  
Full Subcategory ◽  
Functional Relation ◽  
Higher Order ◽  
Order Logic ◽  
First Order Logic ◽  
Higher Order Logic ◽  
Completeness Proof ◽  
Factorization System ◽  
First Order ◽  
Functional Relations

In this paper we extend the models for the “logic of categories” to a wider class of categories than is usually considered. We consider two kinds of logic, a restricted first-order logic and the full higher-order logic of elementary topoi.The restricted first-order logic has as its only logical symbols ∧, ∃, Τ, and =. We interpret this logic in a category with finite limits equipped with a factorization system (in the sense of [4]). We require to satisfy two additional conditions: ⊆ Monos, and any pullback of an arrow in is again in . A category with a factorization system satisfying these conditions will be called an EM-category.The interpretation of the restricted logic in EM-categories is given in §1. In §2 we give an axiomatization for the logic, and in §§3 and 5 we give two completeness proofs for this axiomatization. The first completeness proof constructs an EM-category out of the logic, in the spirit of Makkai and Reyes [8], though the construction used here differs from theirs. The second uses Boolean-valued models and shows that the restricted logic is exactly the ∧, ∃-fragment of classical first-order logic (adapted to categories). Some examples of EM-categories are given in §4.The restricted logic is powerful enough to handle relations, and in §6 we assign to each EM-category a bicategory of relations Rel() and a category of “functional relations” fr. fr is shown to be a regular category, and it turns out that Rel( and Rel(fr) are biequivalent bicategories. In §7 we study complete objects in an EM-category where an object of is called complete if every functional relation into is yielded by a unique morphism into . We write c for the full subcategory of consisting of the complete objects. Complete objects have some, but not all, of the properties that sheaves have in a category of presheaves.

scholarly journals A Definability Theorem for First Order Logic

1997 ◽  
Vol 4 (3) ◽  
Author(s):  
Carsten Butz ◽  
Ieke Moerdijk
Keyword(s):  
Boolean Algebra ◽  
Topological Space ◽  
Model Theory ◽  
Order Logic ◽  
First Order Logic ◽  
Infinitary Logic ◽  
First Order ◽  
Definable Subset ◽  
Language L ◽  
The One

In this paper, we will present a definability theorem for first order logic.<br />This theorem is very easy to state, and its proof only uses elementary tools. To explain the theorem, let us first observe that if M is a model of a theory T in a language L, then, clearly, any definable subset S M (i.e., a subset S = {a | M |= phi(a)} defined by some formula phi) is invariant under all<br />automorphisms of M. The same is of course true for subsets of M" defined<br />by formulas with n free variables.<br /> Our theorem states that, if one allows Boolean valued models, the converse holds. More precisely, for any theory T we will construct a Boolean valued model M, in which precisely the T-provable formulas hold, and in which every (Boolean valued) subset which is invariant under all automorphisms of M is definable by a formula of L.<br />Our presentation is entirely selfcontained, and only requires familiarity<br />with the most elementary properties of model theory. In particular, we have added a first section in which we review the basic definitions concerning<br />Boolean valued models.<br />The Boolean algebra used in the construction of the model will be presented concretely as the algebra of closed and open subsets of a topological space X naturally associated with the theory T. The construction of this space is closely related to the one in [1]. In fact, one of the results in that paper could be interpreted as a definability theorem for infinitary logic, using topological rather than Boolean valued models.

The continuum and first-order intuitionistic logic

1992 ◽  
Vol 57 (4) ◽  
pp. 1417-1424 ◽  
Author(s):  
D. van Dalen
Keyword(s):  
Prima Facie ◽  
Order Logic ◽  
Point Of View ◽  
Ordered Sets ◽  
Practice Model ◽  
Original Proof ◽  
First Order ◽  
The One ◽  
Intuitionistic Mathematics ◽  
The Continuum

Ever since Cantor, we have known that the reals and the rationals are not isomorphic (as equality structures, i.e., sets). Logically speaking, however, they are not all that different; in first-order classical logic they are elementarily equivalent, since the theory of infinite sets is complete. The same holds for ℝ and ℚ as ordered sets; again the theory of dense linear order without end points is complete.From an intuitionistic point of view these matters are more complicated; e.g., the theory of equality of ℚ is decidable, whereas the one of ℝ patently is not. This, in a roundabout way, shows that ℚ and ℝ are not isomorphic; of course, there is no need for such a detour, as Cantor's original proof [2] is intuitionistically correct, and Brouwer's new proof [1] is another alternative intuitionistic argument.In view of the fact that ℚ and ℝ behave so strikingly differently with respect to first-order logic, one is easily tempted to look for elementary equivalences among the subsets of ℝ. Until quite recently most model theoretic investigations of intuitionistic theories made use of special (artificial) notions of “model”, e.g., Kripke models, sheaf models,…; but there is no prima facie reason why one should not practice model theory much the same way as traditional model theorists do. That is to say on the basis of a naive set theory, or, in our case, of naive intuitionistic mathematics.This paper uses the method of (k, p)-isomorphisms of Fraïssé, and it is briefly shown that one half of the Fraïssé theorem holds intuitionistically.

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.

Sign in / Sign up

Export Citation Format

Share Document