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

scholarly journals Formalization of Linear Space Theory in the Higher-Order Logic Proving System

2013 ◽  
Vol 2013 ◽  
pp. 1-6 ◽  
Author(s):  
Jie Zhang ◽  
Danwen Mao ◽  
Yong Guan
Keyword(s):  
Linear Space ◽  
Theorem Proving ◽  
Predicate Logic ◽  
Higher Order ◽  
Order Logic ◽  
First Order Logic ◽  
Space Theory ◽  
Higher Order Logic ◽  
First Order ◽  
Important Approach

Theorem proving is an important approach in formal verification. Higher-order logic is a form of predicate logic that is distinguished from first-order logic by additional quantifiers and stronger semantics. Higher-order logic is more expressive. This paper presents the formalization of the linear space theory in HOL4. A set of properties is characterized in HOL4. This result is used to build the underpinnings for the application of higher-order logic in a wider spectrum of engineering applications.

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

scholarly journals Model theory of monadic predicate logic with the infinity quantifier

2021 ◽  
Author(s):  
Facundo Carreiro ◽  
Alessandro Facchini ◽  
Yde Venema ◽  
Fabio Zanasi
Keyword(s):  
Model Theory ◽  
Predicate Logic ◽  
Order Logic ◽  
First Order Logic ◽  
Semantic Property ◽  
First Order ◽  
Scott Continuous ◽  
Semantic Properties

AbstractThis paper establishes model-theoretic properties of $$\texttt {M} \texttt {E} ^{\infty }$$ M E ∞ , a variation of monadic first-order logic that features the generalised quantifier $$\exists ^\infty $$ ∃ ∞ (‘there are infinitely many’). We will also prove analogous versions of these results in the simpler setting of monadic first-order logic with and without equality ($$\texttt {M} \texttt {E} $$ M E and $$\texttt {M} $$ M , respectively). For each logic $$\texttt {L} \in \{ \texttt {M} , \texttt {M} \texttt {E} , \texttt {M} \texttt {E} ^{\infty }\}$$ L ∈ { M , M E , M E ∞ } we will show the following. We provide syntactically defined fragments of $$\texttt {L} $$ L characterising four different semantic properties of $$\texttt {L} $$ L -sentences: (1) being monotone and (2) (Scott) continuous in a given set of monadic predicates; (3) having truth preserved under taking submodels or (4) being truth invariant under taking quotients. In each case, we produce an effectively defined map that translates an arbitrary sentence $$\varphi $$ φ to a sentence $$\varphi ^\mathsf{p}$$ φ p belonging to the corresponding syntactic fragment, with the property that $$\varphi $$ φ is equivalent to $$\varphi ^\mathsf{p}$$ φ p precisely when it has the associated semantic property. As a corollary of our developments, we obtain that the four semantic properties above are decidable for $$\texttt {L} $$ L -sentences.

Second- and higher-order logics

2018 ◽  
Author(s):  
Shaughan Lavine
Keyword(s):  
Predicate Logic ◽  
Higher Order ◽  
Second Order ◽  
Order Logic ◽  
First Order Logic ◽  
Third Order ◽  
First Order ◽  
Proof Systems ◽  
The Universe ◽  
Second Order Logic

In first-order predicate logic there are symbols for fixed individuals, relations and functions on a given universe of individuals and there are variables ranging over the individuals, with associated quantifiers. Second-order logic adds variables ranging over relations and functions on the universe of individuals, and associated quantifiers, which are called second-order variables and quantifiers. Sometimes one also adds symbols for fixed higher-order relations and functions among and on the relations, functions and individuals of the original universe. One can add third-order variables ranging over relations and functions among and on the relations, functions and individuals on the universe, with associated quantifiers, and so on, to yield logics of even higher order. It is usual to use proof systems for higher-order logics (that is, logics beyond first-order) that include analogues of the first-order quantifier rules for all quantifiers. An extensional n-ary relation variable in effect ranges over arbitrary sets of n-tuples of members of the universe. (Functions are omitted here for simplicity: remarks about them parallel those for relations.) If the set of sets of n-tuples of members of a universe is fully determined once the universe itself is given, then the truth-values of sentences involving second-order quantifiers are determined in a structure like the ones used for first-order logic. However, if the notion of the set of all sets of n-tuples of members of a universe is specified in terms of some theory about sets or relations, then the universe of a structure must be supplemented by specifications of the domains of the various higher-order variables. No matter what theory one adopts, there are infinitely many choices for such domains compatible with the theory over any infinite universe. This casts doubt on the apparent clarity of the notion of ‘all n-ary relations on a domain’: since the notion cannot be defined categorically in terms of the domain using any theory whatsoever, how could it be well-determined?

Provability with Finitely Many Variables

2002 ◽  
Vol 8 (3) ◽  
pp. 348-379 ◽  
Author(s):  
Robin Hirsch ◽  
Ian Hodkinson ◽  
Roger D. Maddux
Keyword(s):  
Predicate Logic ◽  
Algebraic Logic ◽  
Order Logic ◽  
First Order Logic ◽  
Alternative Semantics ◽  
Relation Symbol ◽  
First Order ◽  
Binary Predicate ◽  
Standard Set ◽  
Binary Relation Symbol

AbstractFor every finite n ≥ 4 there is a logically valid sentence φn with the following properties: φn contains only 3 variables (each of which occurs many times); φn contains exactly one nonlogical binary relation symbol (no function symbols, no constants, and no equality symbol); φn has a proof in first-order logic with equality that contains exactly n variables, but no proof containing only n − 1 variables. This result was first proved using the machinery of algebraic logic developed in several research monographs and papers. Here we replicate the result and its proof entirely within the realm of (elementary) first-order binary predicate logic with equality. We need the usual syntax, axioms, and rules of inference to show that φn has a proof with only n variables. To show that φn has no proof with only n − 1 variables we use alternative semantics in place of the usual, standard, set-theoretical semantics of first-order logic.

scholarly journals Possibility Semantics for Intuitionistic Logic

2004 ◽  
Vol 2 ◽  
Author(s):  
M. J. Cresswell
Keyword(s):  
Intuitionistic Logic ◽  
Possible Worlds ◽  
Predicate Logic ◽  
Order Logic ◽  
Semantic Interpretation ◽  
First Order Logic ◽  
First Order ◽  
Partial Indices ◽  
Closure Conditions ◽  
First Order Predicate Logic

The paper investigates interpretations of propositional and first-order logic in which validity is defined in terms of partial indices; sometimes called possibilities but here understood as non-empty subsets of a set W of possible worlds. Truth at a set of worlds is understood to be truth at every world in the set. If all subsets of W are permitted the logic so determined is classical first-order predicate logic. Restricting allowable subsets and then imposing certain closure conditions provides a modelling for intuitionistic predicate logic. The same semantic interpretation rules are used in both logics for all the operators.

scholarly journals The completeness of Heyting first-order logic

2003 ◽  
Vol 68 (3) ◽  
pp. 751-763 ◽  
Author(s):  
W. W. Tait
Keyword(s):  
Type Theory ◽  
Disjoint Union ◽  
Predicate Logic ◽  
Order Logic ◽  
First Order Logic ◽  
First Order ◽  
First Order Predicate Logic

AbstractRestricted to first-order formulas, the rules of inference in the Curry-Howard type theory are equivalent to those of first-order predicate logic as formalized by Heyting, with one exception: ∃-elimination in the Curry-Howard theory, where ∃x: A,F(x) is understood as disjoint union, are the projections, and these do not preserve first-orderedness. This note shows, however, that the Curry-Howard theory is conservative over Heyting's system.

Sign in / Sign up

Export Citation Format

Share Document