On the reduction of the decision problem

1947 ◽  
Vol 12 (3) ◽  
pp. 65-73 ◽  
Author(s):  
László Kalmár ◽  
János Surányi
Keyword(s):  
Special Form ◽  
Decision Problem ◽  
Predicate Calculus ◽  
Reduction Theorem ◽  
First Order ◽  
Title One ◽  
Order Predicate Calculus ◽  
Predicate Variable

In the first paper of the above main title, one of us has proved that any formula of the first order predicate calculus is equivalent (as to being satisfiable or not) to some binary first order formula having a prefix of the form (Ex1)(x2)(Ex3) … (xn) and containing a single predicate variable. This result is an improvement of a theorem of Ackermann stating that any first order formula is equivalent to another with a prefix of the above form but saying nothing about the number of predicate variables appearing therein. Hence the question arises if other theorems reducing the decision problem to the satisfiability question of the first order formulas with a prefix of a special form can be improved in like manner. In the present paper we shall answer this question concerning Gödel's reduction theorem stating that any first order formula is equivalent to another the prefix of which has the form

scholarly journals On a Propositional Calculus Whose Decision Problem is Recursively Unsolvable

1970 ◽  
Vol 38 ◽  
pp. 145-152
Author(s):  
Akira Nakamura
Keyword(s):  
Decision Problem ◽  
Propositional Calculus ◽  
Predicate Calculus ◽  
Reduction Theorem ◽  
List Type ◽  
First Order ◽  
Order Predicate Calculus

The purpose of this paper is to present a propositional calculus whose decision problem is recursively unsolvable. The paper is based on the following ideas: (1) Using Löwenheim-Skolem’s Theorem and Surányi’s Reduction Theorem, we will construct an infinitely many-valued propositional calculus corresponding to the first-order predicate calculus.(2) It is well known that the decision problem of the first-order predicate calculus is recursively unsolvable.(3) Thus it will be shown that the decision problem of the infinitely many-valued propositional calculus is recursively unsolvable.

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.

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

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.

Infinitary logic and admissible sets

1969 ◽  
Vol 34 (2) ◽  
pp. 226-252 ◽  
Author(s):  
Jon Barwise
Keyword(s):  
Second Order ◽  
Order Logic ◽  
Predicate Calculus ◽  
Generalized Quantifiers ◽  
Infinitary Logic ◽  
First Order ◽  
Admissible Sets ◽  
Classical Language ◽  
Second Order Logic ◽  
Order Predicate Calculus

In recent years much effort has gone into the study of languages which strengthen the classical first-order predicate calculus in various ways. This effort has been motivated by the desire to find a language which is(I) strong enough to express interesting properties not expressible by the classical language, but(II) still simple enough to yield interesting general results. Languages investigated include second-order logic, weak second-order logic, ω-logic, languages with generalized quantifiers, and infinitary logic.

Solution of a problem of Leon Henkin

1955 ◽  
Vol 20 (2) ◽  
pp. 115-118 ◽  
Author(s):  
M. H. Löb
Keyword(s):  
Number Theory ◽  
Recursive Function ◽  
Formal System ◽  
Free Variable ◽  
Formal Proof ◽  
Predicate Calculus ◽  
First Order ◽  
Free Variables ◽  
Order Predicate Calculus

If Σ is any standard formal system adequate for recursive number theory, a formula (having a certain integer q as its Gödel number) can be constructed which expresses the proposition that the formula with Gödel number q is provable in Σ. Is this formula provable or independent in Σ? [2].One approach to this problem is discussed by Kreisel in [4]. However, he still leaves open the question whether the formula (Ex)(x, a), with Gödel-number a, is provable or not. Here (x, y) is the number-theoretic predicate which expresses the proposition that x is the number of a formal proof of the formula with Gödel-number y.In this note we present a solution of the previous problem with respect to the system Zμ [3] pp. 289–294, and, more generally, with respect to any system whose set of theorems is closed under the rules of inference of the first order predicate calculus, and satisfies the subsequent five conditions, and in which the function (k, l) used below is definable.The notation and terminology is in the main that of [3] pp. 306–326, viz. if is a formula of Zμ containing no free variables, whose Gödel number is a, then ({}) stands for (Ex)(x, a) (read: the formula with Gödel number a is provable in Zμ); if is a formula of Zμ containing a free variable, y say, ({}) stands for (Ex)(x, g(y)}, where g(y) is a recursive function such that for an arbitrary numeral the value of g() is the Gödel number of the formula obtained from by substituting for y in throughout. We shall, however, depart trivially from [3] in writing (), where is an arbitrary numeral, for (Ex){x, ).

Sign in / Sign up

Export Citation Format

Share Document