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

CALCU LEMUS home page Mathesis Universalis home page Editor's Introduction Andrzej Grzegorczyk The Decidability without Mathematics (Word document). Leon Gumański (1) The Decidability of the First-Order Functional Calculus and (2) Cantor's Diagonal Method and Some Related Topics (Word document). These two contributions are treated here as a whole because of their internal connection. Item 1 was originally published in Ruch Filozoficzny, vol.57, no.3/4 (2000), item 2 contributed to a symposium (details inside the file). Witold Marciszewski On going beyond the first-order logic in testing the validity of its formulas - A case study (PDF document). To appear later: Jan Zygmunt, "Tarski's impact on decision problems". IMPORTANT LINKS 1. Stephen Wolfram: Undecidability and Intractability in Theoretical Physics www.stephenwolfram.com/publications/articles/physics/85-undecidability/2/text.html 2. Fifth Workshop on Computability and Complexity in Analysis, July 12-13, 2002, Mįlaga, Spain. "The workshop is concerned with the theory of computability and complexity over the real numbers which is built on the Turing machine model. This theory was initiated by Turing, Grzegorczyk, Lacombe, Banach and Mazur, and after a long period of slow development has seen rapid growth in recent years. Newcomers can find introductions in the books by Pour-El/Richards, Ko, and Weihrauch." 3. Curtis Brown: Symbolic Logic. Decidability. A lesson on logic containing useful discussion of decidability issues in first-order logic. Local copy.

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