Preservation theorem and relativization theorem for cofinal extensions

1986 ◽  
Vol 51 (4) ◽  
pp. 1022-1028
Author(s):  
Nobuyoshi Motohashi
Keyword(s):  
Predicate Logic ◽  
Predicate Symbol ◽  
First Order ◽  
Existential Sentence ◽  
Preservation Theorems ◽  
Preservation Theorem ◽  
Binary Predicate ◽  
Classical Predicate

One of the typical preservation theorems in a first order classical predicate logic with equality L is the following theorem due to J. Łoś [4] and A. Tarski [9] (also cf. [1, p. 139]).Theorem A (Łoś-Tarski). For any sentences A and B in L, the following two conditions (i) and (ii) are equivalent.(i) Every extension of any model of A is a model of B.(ii) The two sentences A ⊃ C and C ⊃ B are provable in L for some existential sentence C in L.In [2], S. Feferman obtained a similar preservation theorem for outer extensions. In the following, we assume that L has a fixed binary predicate symbol <. Then Σ-formulas are formulas in L which are constructed from atomic formulas and their negations by applying ∧ (conjunctions), ∨ (disjunctions), ∀x < y (bounded universal quantifications), and ∃ (existential quantifications). An extension of an L-structure is said to be an outer extension of if ⊨ a < b and b ϵ ∣∣ imply a ϵ ∣∣ for any elements a, b in ∣∣.Theorem B (Feferman). For any sentences A and B in L, the following two conditions (i) and (ii) are equivalent.(i) Every outer extension of any model of A is a model of B.(ii) The two sentences A ⊃ C and C ⊃ B are provable in L for some Σ-sentence C in L.

A normal form theorem for first order formulas and its application to Gaifman's splitting theorem

1984 ◽  
Vol 49 (4) ◽  
pp. 1262-1267
Author(s):  
Nobuyoshi Motohashi
Keyword(s):  
Normal Form ◽  
Predicate Symbol ◽  
Atomic Formula ◽  
Splitting Theorem ◽  
First Order ◽  
Usual Manner ◽  
Binary Predicate ◽  
Normal Form Theorem ◽  
Image Position ◽  
Order Predicate Calculus

Let L be a first order predicate calculus with equality which has a fixed binary predicate symbol <. In this paper, we shall deal with quantifiers Cx, ∀x ≦ y, ∃x ≦ y defined as follows: CxA(x) is ∀y∃x(y ≦ x ∧ A(x)), ∀x ≦ yA{x) is ∀x(x ≦ y ⊃ A(x)), and ∃x ≦ yA(x) is ∃x(x ≦ y ∧ 4(x)). The expressions x̄, ȳ, … will be used to denote sequences of variables. In particular, x̄ stands for 〈x1, …, xn〉 and ȳ stands for 〈y1,…, ym〉 for some n, m. Also ∃x̄, ∀x̄ ≦ ȳ, … will be used to denote ∃x1 ∃x2 … ∃xn, ∀x1 ≦ y1 ∀x2 ≦ y2 … ∀xn ≦ yn, …, respectively. Let X be a set of formulas in L such that X contains every atomic formula and is closed under substitution of free variables and applications of propositional connectives ¬(not), ∧(and), ∨(or). Then, ∑(X) is the set of formulas of the form ∃x̄B(x̄), where B ∈ X, and Φ(X) is the set of formulas of the form.Since X is closed under ∧, ∨, the two sets Σ(X) and Φ(X) are closed under ∧, ∨ in the following sense: for any formulas A and B in Σ(X) [Φ(X)], there are formulas in Σ(X)[ Φ(X)] which are obtained from A ∧ B and A ∨ B by bringing some quantifiers forward in the usual manner.

Undecidability of modal and intermediate first-order logics with two individual variables

1993 ◽  
Vol 58 (3) ◽  
pp. 800-823 ◽  
Author(s):  
D. M. Gabbay ◽  
V. B. Shehtman
Keyword(s):  
Modal Logic ◽  
Classical Logic ◽  
Predicate Calculus ◽  
Single Individual ◽  
First Order ◽  
Short Summary ◽  
Binary Predicate ◽  
Individual Variables ◽  
Image Position ◽  
Classical Predicate

The interest in fragments of predicate logics is motivated by the well-known fact that full classical predicate calculus is undecidable (cf. Church [1936]). So it is desirable to find decidable fragments which are in some sense “maximal”, i.e., which become undecidable if they are “slightly” extended. Or, alternatively, we can look for “minimal” undecidable fragments and try to identify the vague boundary between decidability and undecidability. A great deal of work in this area concerning mainly classical logic has been done since the thirties. We will not give a complete review of decidability and undecidability results in classical logic, referring the reader to existing monographs (cf. Suranyi [1959], Lewis [1979], and Dreben, Goldfarb [1979]). A short summary can also be found in the well-known book Church [1956]. Let us recall only several facts. Herein we will consider only logics without functional symbols, constants, and equality.(C1) The fragment of the classical logic with only monadic predicate letters is decidable (cf. Behmann [1922]).(C2) The fragment of the classical logic with a single binary predicate letter is undecidable. (This is a consequence of Gödel [1933].)(C3) The fragment of the classical logic with a single individual variable is decidable; in fact it is equivalent to Lewis S5 (cf. Wajsberg [1933]).(C4) The fragment of the classical logic with two individual variables is decidable (Segerberg [1973] contains a proof using modal logic; Scott [1962] and Mortimer [1975] give traditional proofs.)(C5) The fragment of the classical logic with three individual variables and binary predicate letters is undecidable (cf. Surańyi [1943]). In fact this paper considers formulas of the following typeφ,ψ being quantifier-free and the set of binary predicate letters which can appear in φ or ψ being fixed and finite.

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.

Some consequences of the axiom of power-set

1965 ◽  
Vol 30 (3) ◽  
pp. 293-294 ◽  
Author(s):  
Alexander Abian ◽  
Samuel Lamacchia
Keyword(s):  
Predicate Symbol ◽  
Order Theory ◽  
Finite Model ◽  
First Order ◽  
First Order Theory ◽  
Power Set ◽  
Binary Predicate ◽  
Definition Of

In this paper we prove:Theorem 1. Any finite model of the axiom of power-set also satisfies the axioms of extensionality, sum-set and choice.Clearly, it will follow from (2) below that in a finite model the axiom of power-set is satisfied if and only if every set is a power-set. Thus, Theorem 1 follows immediately from Theorem 2 below, where by a theory of sets we mean a first-order theory without identity and with only one binary predicate symbol ∈.Theorem 2. If in a theory of sets every set is a power-set and if the axiom of power-set is valid, then the axioms of extensionality, sum-set and choice are valid.The proof of Theorem 2 will follow from the lemmas which we establish below.We mean by x = y that x and y have the same elements. We denote a power-set of x by P(x) when it exists; similarly, we denote a sum-set of x by Ux.Clearly, in every theory of sets we have:(1) (x ⊂ y) ↔ (P(x) ⊂ P(y)),(2) (x = y) ↔ (P(x) = P(y)),(3) (x = y) → ((x ∈ P(z)) → (y ∈ P(z))),(4) ⋃P(x) = x.In view of (2), (3) and the definition of equality, we have:Lemma 1. If in a theory of sets every set is a power-set, then equal sets are elements of the same sets.We have also, in view of (4):Lemma 2. If in a theory of sets every set is a power-set, then every set has a sum-set.

scholarly journals On the Definitional Embeddability of the Combinatory Logic Theory into the First-Order Predicate Calculus

2015 ◽  
Vol 21 (2) ◽  
pp. 9-14
Author(s):  
В. И. Шалак
Keyword(s):  
Predicate Logic ◽  
Computability Theory ◽  
Predicate Calculus ◽  
Combinatory Logic ◽  
Applied Theory ◽  
First Order ◽  
Computable Functions ◽  
Order Predicate Calculus ◽  
Classical Predicate

In this article we prove a theorem on the definitional embeddability of the combinatory logic into the first-order predicate calculus without equality. Since all efficiently computable functions can be represented in the combinatory logic, it immediately follows that they can be represented in the first-order classical predicate logic. So far mathematicians studied the computability theory as some applied theory. From our theorem it follows that the notion of computability is purely logical. This result will be of interest not only for logicians and mathematicians but also for philosophers who study foundations of logic and its relation to mathematics.

Resolution systems and their applications I

1980 ◽  
Vol 3 (2) ◽  
pp. 235-268
Author(s):  
Ewa Orłowska
Keyword(s):  
Theorem Proving ◽  
Sufficient Conditions ◽  
Predicate Calculus ◽  
Resolution Method ◽  
First Order ◽  
Deductive Systems ◽  
Resolution System ◽  
Resolution Principle ◽  
Necessary And Sufficient ◽  
Classical Predicate

The central method employed today for theorem-proving is the resolution method introduced by J. A. Robinson in 1965 for the classical predicate calculus. Since then many improvements of the resolution method have been made. On the other hand, treatment of automated theorem-proving techniques for non-classical logics has been started, in connection with applications of these logics in computer science. In this paper a generalization of a notion of the resolution principle is introduced and discussed. A certain class of first order logics is considered and deductive systems of these logics with a resolution principle as an inference rule are investigated. The necessary and sufficient conditions for the so-called resolution completeness of such systems are given. A generalized Herbrand property for a logic is defined and its connections with the resolution-completeness are presented. A class of binary resolution systems is investigated and a kind of a normal form for derivations in such systems is given. On the ground of the methods developed the resolution system for the classical predicate calculus is described and the resolution systems for some non-classical logics are outlined. A method of program synthesis based on the resolution system for the classical predicate calculus is presented. A notion of a resolution-interpretability of a logic L in another logic L ′ is introduced. The method of resolution-interpretability consists in establishing a relation between formulas of the logic L and some sets of formulas of the logic L ′ with the intention of using the resolution system for L ′ to prove theorems of L. It is shown how the method of resolution-interpretability can be used to prove decidability of sets of unsatisfiable formulas of a given logic.

Syllogism and quantification

1962 ◽  
Vol 27 (1) ◽  
pp. 58-72 ◽  
Author(s):  
Timothy Smiley
Keyword(s):  
Predicate Logic ◽  
Modern Logic ◽  
First Order ◽  
First Order Predicate Logic

Anyone who reads Aristotle, knowing something about modern logic and nothing about its history, must ask himself why the syllogistic cannot be translated as it stands into the logic of quantification. It is now more than twenty years since the invention of the requisite framework, the logic of many-sorted quantification.In the familiar first-order predicate logic generality is expressed by means of variables and quantifiers, and each interpretation of the system is based upon the choice of some class over which the variables may range, the only restriction placed on this ‘domain of individuals’ being that it should not be empty.

Some logical and syntactical observations concerning the first-order dependent type system λP

1999 ◽  
Vol 9 (4) ◽  
pp. 335-359 ◽  
Author(s):  
HERMAN GEUVERS ◽  
ERIK BARENDSEN
Keyword(s):  
Predicate Logic ◽  
Type System ◽  
Logical Framework ◽  
First Order ◽  
Logical Derivation ◽  
Dependent Type ◽  
First Order Predicate Logic

We look at two different ways of interpreting logic in the dependent type system λP. The first is by a direct formulas-as-types interpretation à la Howard where the logical derivation rules are mapped to derivation rules in the type system. The second is by viewing λP as a Logical Framework, following Harper et al. (1987) and Harper et al. (1993). The type system is then used as the meta-language in which various logics can be coded.We give a (brief) overview of known (syntactical) results about λP. Then we discuss two issues in some more detail. The first is the completeness of the formulas-as-types embedding of minimal first-order predicate logic into λP. This is a remarkably complicated issue, a first proof of which appeared in Geuvers (1993), following ideas in Barendsen and Geuvers (1989) and Swaen (1989). The second issue is the minimality of λP as a logical framework. We will show that some of the rules are actually superfluous (even though they contribute nicely to the generality of the presentation of λP).At the same time we will attempt to provide a gentle introduction to λP and its various aspects and we will try to use little inside knowledge.

First order predicate logic

1986 ◽  
pp. 155-183
Author(s):  
Igor Aleksander ◽  
Henri Farreny ◽  
Malik Ghallab
Keyword(s):  
Predicate Logic ◽  
First Order ◽  
First Order Predicate Logic
Sign in / Sign up

Export Citation Format

Share Document