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.

A reduction class containing formulas with one monadic predicate and one binary function symbol

1976 ◽  
Vol 41 (1) ◽  
pp. 45-49
Author(s):  
Charles E. Hughes
Keyword(s):  
Normal Form ◽  
Predicate Symbol ◽  
Conjunctive Normal Form ◽  
Function Symbol ◽  
Predicate Calculus ◽  
Binary Function ◽  
First Order ◽  
The Matrix ◽  
Reduction Class ◽  
Order Predicate Calculus

AbstractA new reduction class is presented for the satisfiability problem for well-formed formulas of the first-order predicate calculus. The members of this class are closed prenex formulas of the form ∀x∀yC. The matrix C is in conjunctive normal form and has no disjuncts with more than three literals, in fact all but one conjunct is unary. Furthermore C contains but one predicate symbol, that being unary, and one function symbol which symbol is binary.

On the reduction of the decision problem. Third paper. Pepis prefix, a single binary predicate

1950 ◽  
Vol 15 (3) ◽  
pp. 161-173 ◽  
Author(s):  
László Kalmár ◽  
János Surányi
Keyword(s):  
Decision Problem ◽  
Predicate Calculus ◽  
Existential Quantifier ◽  
First Order ◽  
Binary Predicate ◽  
Image Position ◽  
Analogous Theorem ◽  
Order Predicate Calculus ◽  
Predicate Variable

It has been proved by Pepis that any formula of the first-order predicate calculus is equivalent (in respect of being satisfiable) to another with a prefix of the formcontaining a single existential quantifier. In this paper, we shall improve this theorem in the like manner as the Ackermann and the Gödel reduction theorems have been improved in the preceding papers of the same main title. More explicitly, we shall prove theTheorem 1. To any given first-order formula it is possible to construct an equivalent one with a prefix of the form (1) and a matrix containing no other predicate variable than a single binary one.An analogous theorem, but producing a prefix of the formhas been proved in the meantime by Surányi; some modifications in the proof, suggested by Kalmár, led to the above form.

Two interpolation theorems for a predicate calculus

1971 ◽  
Vol 36 (2) ◽  
pp. 262-270
Author(s):  
Shoji Maehara ◽  
Gaisi Takeuti
Keyword(s):  
Normal Form ◽  
Completeness Theorem ◽  
Interpolation Theorem ◽  
Second Order ◽  
Predicate Calculus ◽  
Cut Elimination ◽  
First Order ◽  
Image Position ◽  
Order Predicate Calculus

A second order formula is called Π1 if, in its prenex normal form, all second order quantifiers are universal. A sequent F1, … Fm → G1 …, Gn is called Π1 if a formulais Π1If we consider only Π1 sequents, then we can easily generalize the completeness theorem for the cut-free first order predicate calculus to a cut-free Π1 predicate calculus.In this paper, we shall prove two interpolation theorems on the Π1 sequent, and show that Chang's theorem in [2] is a corollary of our theorem. This further supports our belief that any form of the interpolation theorem is a corollary of a cut-elimination theorem. We shall also show how to generalize our results for an infinitary language. Our method is proof-theoretic and an extension of a method introduced in Maehara [5]. The latter has been used frequently to prove the several forms of the interpolation theorem.

The decision problem for formulas in prenex conjunctive normal form with binary disjunctions

1970 ◽  
Vol 35 (2) ◽  
pp. 210-216 ◽  
Author(s):  
M. R. Krom
Keyword(s):  
Normal Form ◽  
Positive Solution ◽  
Decision Problem ◽  
Conjunctive Normal Form ◽  
Decision Problems ◽  
First Order ◽  
Reduction Class ◽  
Image Position ◽  
Positive Integers ◽  
Order Predicate Calculus

In [8] S. J. Maslov gives a positive solution to the decision problem for satisfiability of formulas of the formin any first-order predicate calculus without identity where h, k, m, n are positive integers, αi, βi are signed atomic formulas (atomic formulas or negations of atomic formulas), and ∧, ∨ are conjunction and disjunction symbols, respectively (cf. [6] for a related solvable class). In this paper we show that the decision problem is unsolvable for formulas that are like those considered by Maslov except that they have prefixes of the form ∀x∃y1 … ∃yk∀z. This settles the decision problems for all prefix classes of formulas for formulas that are in prenex conjunctive normal form in which all disjunctions are binary (have just two terms). In our concluding section we report results on decision problems for related classes of formulas including classes of formulas in languages with identity and we describe some special properties of formulas in which all disjunctions are binary including a property that implies that any proof of our result, that a class of formulas is a reduction class for satisfiability, is necessarily indirect. Our proof is based on an unsolvable combinatorial tag problem.

Refinements of Vaught's normal from theorem

1979 ◽  
Vol 44 (3) ◽  
pp. 289-306 ◽  
Author(s):  
Victor Harnik
Keyword(s):  
Normal Form ◽  
Boolean Combination ◽  
Form Theorem ◽  
Central Notion ◽  
The Matrix ◽  
Normal Form Theorem ◽  
Skolem Theorem ◽  
Image Position ◽  
Countable Models

The central notion of this paper is that of a (conjunctive) game-sentence, i.e., a sentence of the formwhere the indices ki, ji range over given countable sets and the matrix conjuncts are, say, open -formulas. Such game sentences were first considered, independently, by Svenonius [19], Moschovakis [13]—[15] and Vaught [20]. Other references are [1], [3]—[5], [10]—[12]. The following normal form theorem was proved by Vaught (and, in less general forms, by his predecessors).Theorem 0.1. Let L = L0(R). For every -sentence ϕ there is an L0-game sentence Θ such that ⊨′ ∃Rϕ ↔ Θ.(A word about the notations: L0(R) denotes the language obtained from L0 by adding to it the sequence R of logical symbols which do not belong to L0; “⊨′α” means that α is true in all countable models.)0.1 can be restated as follows.Theorem 0.1′. For every-sentence ϕ there is an L0-game sentence Θ such that ⊨ϕ → Θ and for any-sentence ϕ if ⊨ϕ → ϕ and L′ ⋂ L ⊆ L0, then ⊨ Θ → ϕ.(We sketch the proof of the equivalence between 0.1 and 0.1′.0.1 implies 0.1′. This is obvious once we realize that game sentences and their negations satisfy the downward Löwenheim-Skolem theorem and hence, ⊨′α is equivalent to ⊨α whenever α is a boolean combination of and game sentences.

Normalization theorems for full first order classical natural deduction

1991 ◽  
Vol 56 (1) ◽  
pp. 129-149 ◽  
Author(s):  
Gunnar Stålmarck
Keyword(s):  
Normal Form ◽  
Natural Deduction ◽  
Full System ◽  
Strong Normalization ◽  
Logical Constants ◽  
Restricted Version ◽  
First Order ◽  
Form Theorem ◽  
Normalization Theorem ◽  
Normal Form Theorem

In this paper we prove the strong normalization theorem for full first order classical N.D. (natural deduction)—full in the sense that all logical constants are taken as primitive. We also give a syntactic proof of the normal form theorem and (weak) normalization for the same system.The theorem has been stated several times, and some proofs appear in the literature. The first proof occurs in Statman [1], where full first order classical N.D. (with the elimination rules for ∨ and ∃ restricted to atomic conclusions) is embedded in a system for second order (propositional) intuitionistic N.D., for which a strong normalization theorem is proved using strongly impredicative methods.A proof of the normal form theorem and (weak) normalization theorem occurs in Seldin [1] as an extension of a proof of the same theorem for an N.D.-system for the intermediate logic called MH.The proof of the strong normalization theorem presented in this paper is obtained by proving that a certain kind of validity applies to all derivations in the system considered.The notion “validity” is adopted from Prawitz [2], where it is used to prove the strong normalization theorem for a restricted version of first order classical N.D., and is extended to cover the full system. Notions similar to “validity” have been used earlier by Tait (convertability), Girard (réducibilité) and Martin-Löf (computability).In Prawitz [2] the N.D. system is restricted in the sense that ∨ and ∃ are not treated as primitive logical constants, and hence the deductions can only be seen to be “natural” with respect to the other logical constants. To spell it out, the strong normalization theorem for the restricted version of first order classical N.D. together with the well-known results on the definability of the rules for ∨ and ∃ in the restricted system does not imply the normalization theorem for the full system.

On the reduction of the decision problem. First paper. Ackermann prefix, a single binary predicate

1939 ◽  
Vol 4 (1) ◽  
pp. 1-9 ◽  
Author(s):  
László Kalmár
Keyword(s):  
Decision Problem ◽  
Reduction Process ◽  
The Other ◽  
First Order ◽  
Other Hand ◽  
Special Cases ◽  
Binary Predicate ◽  
Ternary Variables ◽  
Order Predicate Calculus ◽  
Predicate Variable

1. Although the decision problem of the first order predicate calculus has been proved by Church to be unsolvable by any (general) recursive process, perhaps it is not superfluous to investigate the possible reductions of the general problem to simple special cases of it. Indeed, the situation after Church's discovery seems to be analogous to that in algebra after the Ruffini-Abel theorem; and investigations on the reduction of the decision problem might prepare the way for a theory in logic, analogous to that of Galois.It has been proved by Ackermann that any first order formula is equivalent to another having a prefix of the form(1) (Ex1)(x2)(Ex3)(x4)…(xm).On the other hand, I have proved that any first order formula is equivalent to some first order formula containing a single, binary, predicate variable. In the present paper, I shall show that both results can be combined; more explicitly, I shall prove theTheorem. To any given first order formula it is possible to construct an equivalent one with a prefix of the form (1) and a matrix containing no other predicate variable than a single binary one.2. Of course, this theorem cannot be proved by a mere application of the Ackermann reduction method and mine, one after the other. Indeed, Ackermann's method requires the introduction of three auxiliary predicate variables, two of them being ternary variables; on the other hand, my reduction process leads to a more complicated prefix, viz.,(2) (Ex1)…(Exm)(xm+1)(xm+2)(Exm+3)(Exm+4).

scholarly journals Implicational complexity in intuitionistic arithmetic

1981 ◽  
Vol 46 (2) ◽  
pp. 240-248 ◽  
Author(s):  
Daniel Leivant
Keyword(s):  
Normal Form ◽  
Form Theorem ◽  
Natural Measure ◽  
Normal Form Theorem ◽  
Propositional Constants ◽  
Image Position ◽  
Classical Arithmetic ◽  
Intuitionistic Arithmetic

In classical arithmetic a natural measure for the complexity of relations is provided by the number of quantifier alternations in an equivalent prenex normal form. However, the proof of the Prenex Normal Form Theorem uses the following intuitionistically invalid rules for permuting quantifiers with propositional constants.Each one of these schemas, when added to Intuitionistic (Heyting's) Arithmetic IA, generates full Classical (Peano's) Arithmetic. Schema (3) is of little interest here, since one can obtain a formula intuitionistically equivalent to A ∨ ∀xBx, which is prenex if A and B are:For the two conjuncts on the r.h.s. (1) may be successively applied, since y = 0 is decidable.We shall readily verify that there is no way of similarly going around (1) or (2). This fact calls for counting implication (though not conjunction or disjunction) in measuring in IA the complexity of arithmetic relations. The natural implicational measure for our purpose is the depth of negative nestings of implication, defined as follows. I(F): = 0 if F is atomic; I(F ∧ G) = I(F ∨ G): = max[I(F), I(G)]; I(∀xF) = I(∃xF): = I(F); I(F → G):= max[I(F) + 1, I(G)].

On the formalisation of indirect discourse

1958 ◽  
Vol 23 (4) ◽  
pp. 417-419 ◽  
Author(s):  
R. L. Goodstein
Keyword(s):  
Predicate Logic ◽  
Logical Truth ◽  
Predicate Calculus ◽  
Inference Rules ◽  
First Order ◽  
Indirect Discourse ◽  
Image Position ◽  
Order Predicate Calculus

Mr. L. J. Cohen's interesting example of a logical truth of indirect discourse appears to be capable of a simple formalisation and proof in a variant of first order predicate calculus. His example has the form:If A says that anything which B says is false, and B says that something which A says is true, then something which A says is false and something which B says is true.Let ‘A says x’ be formalised by ‘A(x)’ and let assertions of truth and falsehood be formalised as in the following table.We treat both variables x and predicates A (x) as sentences and add to the familiar axioms and inference rules of predicate logic a rule permitting the inference of A(p) from (x)A(x), where p is a closed sentence.We have to prove that from

An improved prenex normal form1

1962 ◽  
Vol 27 (3) ◽  
pp. 317-326 ◽  
Author(s):  
C. C. Chang ◽  
H. Jerome Keisler
Keyword(s):  
Positive Integer ◽  
Predicate Logic ◽  
Atomic Formula ◽  
First Order ◽  
Empty String ◽  
Image Position ◽  
First Order Predicate Logic

Let ℒ be the set of all formulas of a given first order predicate logic (with or without identity). For each positive integer n, let ℒn be the set of all formulas φ in ℒ logically equivalent to a formula of the form where Q is a (possibly empty) string of quantifiers, m is a positive integer, and each αij is either an atomic formula or the negation of an atomic formula.

Sign in / Sign up

Export Citation Format

Share Document