Abstract

Two forms of self-reference that affect complete formalizations of provability will be identified. They had been previously studied separately in works about truth and provability, and in works on non-monotonic reasoning, respectively. It will be shown that formalizing provability envolves non-monotonic reasoning as a subproblem, which implies that the two forms of self-reference need to be faced simultaneously. For this purpose, we will introduce a 3-valued provability predicate Demos, which is perfectly tolerant to both forms of self-reference. It will be shown that Demos formalizes surprisingly natural notions of provability and unprovability and that it preserves many of the intuitions underlying classical provability predicates. Furthermore, Demos can simulate autoepistemic logic as well as several forms of negation-as-failure; this is important because non-monotonic and epistemic reasoning are some of the intended applications of formalized provability. Demos will be given two complete axiomatizations: an extensional axiomatization Ax(D) (that can be obtained by iterating a monotonic operator) and a more structured axiomatization, consisting of a logic program where Demos 's implemented as a meta-interpreter.