Logical Undecidabilities Made Easy

• Autorzy: Leivan D.
• Języki publikacji: EN

Abstrakty

EN

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.

Słowa kluczowe

EN

grammars; first-order logic

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2008
• Tom: Vol. 89, nr 2-3
• Strony: 307--312
• Opis fizyczny: bibliogr. 3 poz.

Twórcy

autor

Leivan D.

• Computer Science Department, Indiana University, Bloomington, IN 47405, USA,

Bibliografia

• [1] Egon Börger, Erich Grädel, and Yuri Gurevich. The classical decision problem. Springer, Berlin, 1997.
• [2] Yuri Gurevich. The decision problem for the logic of predicates and operations. Algebra i Logika, 8:284-308, 1969. English translation: Algebra and Logic 8 (1969), 160-174.
• [3] Willard V. Quine. Concatenation as a basis for arithmetic. Journal of Symbolic Logic, 11:105-114, 1946.