A system of logic for partial functions under existence-dependent kleene equality

1988 ◽  
Vol 53 (3) ◽  
pp. 834-839 ◽  
Author(s):  
H. Andréka ◽  
W. Craig ◽  
I. Németi
Keyword(s):  
Practical Interest ◽  
Order Logic ◽  
First Order Logic ◽  
Basic Relation ◽  
Equational Logic ◽  
Partial Functions ◽  
First Order ◽  
Complete Set ◽  
The Subject ◽  
Relationship Of

Ordinary equational logic is a connective-free fragment of first-order logic which is concerned with total functions under the relation of ordinary equality. In [AN] (see also [AN1]) and in [Cr] it has been extended in two equivalent ways into a near-equational system of logic for partial functions. The extension given in [Cr] deals with partial functions under two relationships: a relationship of existence-dependent existence and one of existence-dependent Kleene equality. For the language that involves both relationships a set of rules was given that is complete. Those rules in the set that involve only existence-dependent existence turned out to be complete for the sublanguage that involves this relationship only. In the present paper we give a set of rules that is complete for the other sublanguage, namely the language of partial functions under existence-dependent Kleene equality.This language lacks a certain, often needed, power of expressing existence and fails, in particular, to be an extension of the language that underlies ordinary equational logic. That it possesses a fairly simple complete set of rules is therefore perhaps more of theoretical than of practical interest. The present paper is thus intended to serve as a supplement to [Cr] and, less directly, to [AN]. The subject is further rounded out, and some contrast is provided, by [Rob]. The systems of logic treated there are based on the weaker language in which partial functions are considered under the more basic relation of Kleene equality.

Relational and partial variable sets and basic predicate logic

1996 ◽  
Vol 61 (3) ◽  
pp. 843-872 ◽  
Author(s):  
Silvio Ghilardi ◽  
Giancarlo Meloni
Keyword(s):  
Predicate Logic ◽  
Order Logic ◽  
Important Case ◽  
First Order Logic ◽  
Partial Functions ◽  
First Order ◽  
Transition Functions ◽  
Independence Results

AbstractIn this paper we study the logic of relational and partial variable sets, seen as a generalization of set-valued presheaves, allowing transition functions to be arbitrary relations or arbitrary partial functions. We find that such a logic is the usual intuitionistic and co-intuitionistic first order logic without Beck and Frobenius conditions relative to quantifiers along arbitrary terms. The important case of partial variable sets is axiomatizable by means of the substitutivity schema for equality. Furthermore, completeness, incompleteness and independence results are obtained for different kinds of Beck and Frobenius conditions.

A first order logic for partial functions

1989 ◽  
pp. 47-58 ◽  
Author(s):  
Francisca Lucio-Carrasco ◽  
Antonio Gavilanes-Franco
Keyword(s):  
Order Logic ◽  
First Order Logic ◽  
Partial Functions ◽  
First Order

Properties of first-order logic

2004 ◽  
Author(s):  
Shawn Hedman
Keyword(s):  
Model Theory ◽  
Propositional Logic ◽  
Final Section ◽  
Order Logic ◽  
Countable Model ◽  
First Order Logic ◽  
First Order ◽  
Beth Definability ◽  
The Subject ◽  
Infinite Model

We show that first-order logic, like propositional logic, has both completeness and compactness. We prove a countable version of these theorems in Section 4.1. We further show that these two properties have many useful consequences for first-order logic. For example, compactness implies that if a set of first-order sentences has an infinite model, then it has arbitrarily large infinite models. To fully understand completeness, compactness, and their consequences we must understand the nature of infinite numbers. In Section 4.2, we return to our discussion of infinite numbers that we left in Section 2.5. This digression allows us to properly state and prove completeness and compactness along with the Upward and Downward Löwenhiem–Skolem theorems. These are the four central theorems of first-order logic referred to in the title of Section 4.3. We discuss consequences of these theorems in Sections 4.4–4.6. These consequences include amalgamation theorems, preservation theorems, and the Beth Definability theorem. Each of the properties studied in this chapter restrict the language of first-order logic. First-order logic is, in some sense, weak. There are many concepts that cannot be expressed in this language. For example, whereas first-order logic can express “there exist n elements” for any finite n, it cannot express “there exist countably many elements.” Any sentence having a countable model necessarily has uncountable models. As we previously mentioned, this follows from compactness. In the final section of this chapter, using graphs as an illustration, we discuss the limitations of first-order logic. Ironically, the weakness of first-order logic makes it the fruitful logic that it is. The properties discussed in this chapter, and the limitations that follow from them, make possible the subject of model theory. All formulas in this chapter are first-order unless stated otherwise. Many of the properties of first-order logic, including completeness and compactness, are consequences of the following fact: Every model has a theory and every theory has a model. Recall that a set of sentences is a “theory” if it is consistent (i.e. if we cannot derive a contradiction). “Every theory has a model” means that if a set of sentences is consistent, then it is satisfiable.

scholarly journals A first order logic for partial functions

1990 ◽  
Vol 74 (1) ◽  
pp. 37-69 ◽  
Author(s):  
Antonio Gavilanes-Franco ◽  
Francisca Lucio-Carrasco
Keyword(s):  
Order Logic ◽  
First Order Logic ◽  
Partial Functions ◽  
First Order

scholarly journals Compiling Input* FO(·) inductive definitions into tabled prolog rules for IDP3

2013 ◽  
Vol 13 (4-5) ◽  
pp. 691-704 ◽  
Author(s):  
JOACHIM JANSEN ◽  
ALBERT JORISSEN ◽  
GERDA JANSSENS
Keyword(s):  
Order Logic ◽  
Experimental Results ◽  
First Order Logic ◽  
Partial Functions ◽  
First Order ◽  
Inductive Definitions ◽  
Input Structure ◽  
Model Generator ◽  
Unit Propagation

AbstractFO(·)IDP3extends first-order logic with inductive definitions, partial functions, types and aggregates. Its model generator IDP3 first grounds the theory and then uses search to find the models. The grounder uses Lifted Unit Propagation (LUP) to reduce the size of the groundings of problem specifications in IDP3. LUP is in general very effective, but performs poorly on definitions of predicates whose two-valued interpretation can be computed from data in the input structure. To solve this problem, a preprocessing step is introduced that converts such definitions to Prolog code and usesXSBProlog to compute their interpretation. The interpretation of these predicates is then added to the input structure, their definitions are removed from the theory and further processing is done by the standard IDP3 system. Experimental results show the effectiveness of our method.

Mappings of MOF Metamodels and Algebraic Languages

2010 ◽  
pp. 78-106
Author(s):  
Liliana María Favre
Keyword(s):  
Formal Specification ◽  
Specification Language ◽  
Order Logic ◽  
First Order Logic ◽  
Algebraic Specification ◽  
Partial Functions ◽  
First Order ◽  
Simple Language ◽  
Algebraic Language ◽  
Selection Of

In this chapter we examine the relation between NEREUS and formal specification using CASL (Common Algebraic Specification Language) as a common algebraic language (Bidoit & Mosses, 2004). CASL is an expressive and simple language based on a critical selection of known constructs such as subsorts, partial functions, first-order logic, and structured and architectural specifications. A basic specification declares sorts, subsorts, operations and predicates, and gives axioms and constraints. Specifications are structured by means of specification building operators for renaming, extension and combining. Architectural specifications impose structure on implementations, whereas structured specifications only structure the text of specifications. CASL allows loose, free and generated specifications. The models of a loose specification include all those where the declared functions have the specified properties, without any restrictions on the set of values corresponding to the various sorts. In models of a generated specification, in contrast, it is required that all values can be expressed by terms formed from the specified constructors, i.e. unreachable values are prohibited. In models of free specifications, it is required that values of terms are distinct except when their equality follows from the specified axioms: the possibility of unintended coincidence between their axioms is prohibited.

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.

Sign in / Sign up

Export Citation Format

Share Document