Abstract
The proof of the Second Incompleteness Theorem consists essentially of proving the uniqueness and explicit definability of the sentence asserting its own unprovability. This turns out to be a rather general phenomenon: Every instance of self-reference describable in the modal logic of the standard proof predicate obeys a similar uniqueness and explicit definability law. The efficient determination of the explicit definitions of formulae satisfying a given instance of self-reference reduces to a simple algebraic problem-that of solving the corresponding fixed-point equation in the modal logic. We survey techniques for the efficient calculation of such fixed-points.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
References
C. Bernardi, The fixed-point theorem for diagonalizable algebras, Studia Logica 34 (1975), pp. 239–251.
C. Bernardi, On the equational class of diagonalizable algebras, Studia Logica 34 (1975), pp. 322–331.
C. Bernardi, The uniqueness of the fixed-point in every diagonalizable algebra, Studia Logica 35 (1976), pp. 335–343.
C. Bernardi and F. Montagna, Solution of problem 35 of H. Friedman, to appear.
G. Boolos, Friedman's 35th problem has an affirmative solution, Notices AMS 22 (1975), p. A-646.
G. Boolos, On deciding the truth of certain statements involving the notion of consistency, The Journal of Symbolic Logic 41 (1976), pp. 779–781.
D. M. Gabbay, A survey of decidability results for modal, tense and intermediate logics, in: P. Suppes, L. Henkin, A. Joja and G. C. Moisil, eds., Logic, Methodology and Philosophy of Science, IV (North-Holland, Amsterdam), 1973.
D. M. Gabbay, Investigations in Modal and Tense Logics with Applications to Problems in Philosophy and Linguistics (Reidel, Dordrecht), 1976.
K. Gödel, Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme, I, Monatshefte für Mathematik und Physik 38 (1931), pp. 173–198.
K. Gödel, Eine Interpretation des intuitionistischen Aussagenkalküls, Ergenisse eines math. Kolloq. 4 (1931/1932), pp. 39–40.
M. H. Löb, Solution of a problem of Leon Henkin, The Journal of Symbolic Logic 20 (1955), pp. 115–118.
A. Macintyre and H. Simons, Gödel's diagonalization technique and related properties of theories, Colloquium Mathematicum 28 (1973), pp. 165–180.
E. Magari, The diagonalinable algebras, Bolletino della Unione Matematica Italiana 12 (1975), pp. 117–125 (suppl. fasc. 3).
R. Montague, Syntactical treatments of modality, with corollaries on reflexion principles and finite axiomatizability, Acta Philosophica Fennica 16 (1963), pp. 153–167.
G. Sambin, Un estensione del theorema di Löb, Rendiconti del Seminario Matematico dell' Universitá di Padova 52 (1974), pp. 193–199.
G. Sambin, An effective fixed-point theorem in intuitionistic diagonaligable algebras, Studia Logica 35 (1976), pp. 345–361.
H. Simmons, Topological aspects of suitable theories, Proceedings of the Edinburgh Mathematical Society 19 (2) (1974/1975), pp. 383–391.
C. Smorynski, Consistency and related metamathematical properties, Univ. of Amsterdam, Mathematics Institute Technical Report 75-02, (1975).
C. Smorynski, The incompleteness theorems, in: K. J. Barwise, ed., Handbook of Mathematical Logic (North-Holland, Amsterdam), 1977.
C. Smorynski, Beth's theorem and self-referential sentences, in: A. Macintyre, L. Pacholski, and J. Paris, eds., Logic Colloquium'77 (North-Holland, Amsterdam).
R. M. Solovay, Provability interpretations of modal logic, Israel Journal of Mathematics 25 (1976), pp. 287–304.
Author information
Authors and Affiliations
Rights and permissions
About this article
Cite this article
Smorynski, C. Calculating self-referential statements, I: Explicit calculations. Stud Logica 38, 17–36 (1979). https://doi.org/10.1007/BF00493670
Received:
Issue Date:
DOI: https://doi.org/10.1007/BF00493670