No.11 (2002) On the Decidability of First-Order Logic

Introduction to this Issue

Andrzej Grzegorczyk's paper "The Decidability without Mathematics" presents a new approach to decidability. The novelty consists in an attempt to define decidability (or computability) on the basis of a formal theory of texts (as symbol strings) without any reference to mathematical entities. Grzegorczyks's enormous contribution to the theory of decidability is commonly acknowledged (as wittnessed, eg. in the note to Link 2 in the Contents of this issue), hence this new aproach, motivated by his philosophical background of "concretism" (a kind of nominalism developed by Tadeusz Kotarbiński in Poland) should be of considerable interest. The paper was accepted by the Programme Committee of Tarski's Centenary Conference (Warsaw, May 28--June 1, 2001), and this seems a sufficient substitute of refereeing procedure.

Two closely related studies by Leon Gumański, the retired professor of logic of Copernicus University in Toruń (Germ. Thorn, in Poland) have the titles "The Decidability of the First-Order Functional Calculus" and "Cantor's Diagonal Method and Some Related Topics". They are intended as a proof that the first-order predicate calculus IS decidable. Thus it opposes a fundamental and firmly established results in logic. The present Editor invited the Author to this issue not because of sharing his claim but because of hoping some advantages of a prospective polemic. The Author's technical skill, as well as the fact that in spite of publishing some earlier versions a long time ago no serious formal error has been noticed, allows to suppose that there is a result worth attention though not necessarily that one which the Author believes to have obtained. Anyway, when appearing at the Web, the study is more likely to be noticed and criticized, with possible advantages for the Author and readers.

The note by Witold Marciszewski "On going beyond the first-order logic in testing the validity of its formulas - A case study" is concerned with the formula

(x)(Ey)R(x,y) => (x) R(a,x)

as a case in which there appear infinitely many recurring loops in checking validity. Intutively, it seems to be a case of halting problem which cannot be solved with an algorithmic process. However, the formula is easily shown to be invalid through a formalized reasoning using finite domain counterexamples constructed in the language of logic and set-theory alone. The latter is necessary to define some formal properties of relations which hold in the domain in question. As set theory can be replaced by higher-order logics, such a counterexample can be regarded as purely logical, but going beyond the first-order logic. This fact is considered in the context of Gödel's idea of the increase of deductive power with proceeding to logics of higher orders.

To the top of this page