László Kalmár. On the reduction of the decision problem. First paper. Ackermann prefix, a single binary predicate. The journal of symbolic logic, Bd. 4 (1939), S. 1–9.

1939 ◽  
Vol 4 (3) ◽  
pp. 127-128
Author(s):  
Th. Skolem
Keyword(s):  
Decision Problem ◽  
Symbolic Logic ◽  
Binary Predicate

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

Closing the Circle: An Analysis of Emil Post's Early Work

2006 ◽  
Vol 12 (2) ◽  
pp. 267-289 ◽  
Author(s):  
Liesbeth de Mol
Keyword(s):  
Mathematical Logic ◽  
Decision Problem ◽  
Symbolic Logic ◽  
Negative Solution ◽  
Kurt Gödel ◽  
Historical Fact

AbstractIn 1931 Kurt Gödel published his incompleteness results, and some years later Church and Turing showed that the decision problem for certain systems of symbolic logic has a negative solution. However, already in 1921 the young logician Emil Post worked on similar problems which resulted in what he called an “anticipation” of these results. For several reasons though he did not submit these results to a journal until 1941. This failure ‘to be the first’, did not discourage him: his contributions to mathematical logic and its foundations should not be underestimated. It is the purpose of this article to show that an interest in the early work of Emil Post should be motivated not only by this historical fact, but also by the fact that Post's approach and method differs substantially from those offered by Gödel, Turing and Church. In this paper it will be shown how this method evolved in his early work and how it finally led him to his results.

A Boolean derivation of the Moore-Osgood theorem

1946 ◽  
Vol 11 (3) ◽  
pp. 65-70 ◽  
Author(s):  
Archie Blake
Keyword(s):  
Decision Problem ◽  
Fundamental Problem ◽  
Symbolic Logic ◽  
Logical Function ◽  
Consistent System ◽  
First Order ◽  
Methods Of Calculation ◽  
Truth Value ◽  
Function Calculus ◽  
Logical Calculi

A fundamental problem of symbolic logic is to define logical calculi sufficient to comprise important parts of mathematics, and to develop systematic methods of calculation therein.The possibility of progress in this direction has been severely limited by Gödel's proof that a consistent system sufficient to comprise arithmetic must contain propositions whose truth-value cannot be decided within the system, and by Church's extension of Gödel's method to the result that even in the first order logical function calculus the general decision problem cannot be solved.

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.

Sign in / Sign up

Export Citation Format

Share Document