Undecidability reconsidered
Abstract
In vol. 2 of Grundlagen der Mathematik Hilbert and Bernays carry out their undecid-
ability proof of predicate logic basing it on their undecidability proof of the arithmeti-
cal systemZ00. In this paper, the latter proof is reconstructed and summarized within
a formal derivation schema. Formalizing the proof makes the presumed use of a meta
language explicit by employing formal predicates as propositional functions, with ex-
pressions as their arguments. In the final section of the paper, the proof is analyzed
critically by applying Wittgenstein’s view on meta language, which does not lead to a
questioning of the assumptions on which the proof is based but of its presumed use
of meta language. Finally, it will be argued that determining if it is the undecidability
proof or Wittgenstein’s analysis of meta language that is right depends on whether a
decision procedure for a predicate that undecidability proofs have seemingly proven
undecidable can nonetheless be defined. Thus serious attempts to define a procedure
for such a predicate should not be ruled out without studying them.