Logical Undecidabilities Made Easy

Article type: Research Article

Authors: Leivant, Daniel

Affiliations: Department of Computer Science, Indiana University, USA. [email protected]

Note: [] Address for correspondence: Computer Science Department, Indiana University, Bloomington, IN 47405, USA

Abstract: Referring to symbolic computing permits extremely simple proofs of undecidability for first-order logic and theories of basic structures. Using grammars we obtain a trivial proof that firstorder validity is undecidable (already for formulas with quantifier prefix ∃∃ and referring to only one unary relation and one binary function [2]). A similar proof yields Gödel's First Incompleteness Theorem for the structure of strings; undecidability for arithmetic follows by noting that addition and multiplication permit direct coding of string concatenation.

Journal: Fundamenta Informaticae, vol. 89, no. 2-3, pp. 307-312, 2008