A Program to Compute G¨odel-L¨ob Fixpoints

Abstract

odel-L¨ ob computability logic. In order to make things relatively self-contained, I sketch the essential ideas of GL, and discuss the significance of its fixpoint theorem. Then I give the algorithm embodied in the program in a little more detail. It should be emphasized that nothing new is presented here — all the theory and methodology are due to others. The main interest is, in a sense, psychological. The approach taken here has been declared in the literature, more than once, to be of theoretical interest only, being too unwieldly in practice. Experimentation shows this is not so provided formulas are not too complicated. A copy of the program can be obtained by ftp from venus.gc.cuny.edu. It is in the subdirectory “/pub/fitting,” under the name “glfixpt.pro.” Log on as “anonymous” and use your full e-mail address as password. If there are difficulties with ftp, send e-mail to the author at mlflc@cunyvm.cuny.edu. The Prolog code is standard, and should run under any implementation, though minor modifications may be necessary for some systems. These modifications are described in the last section, and also in the program itself

Other Versions

No versions found

Links

PhilArchive

    This entry is not archived by us. If you are the author and have permission from the publisher, we recommend that you archive it. Many publishers automatically grant permission to authors to archive pre-prints. By uploading a copy of your work, you will enable us to better index it, making it easier to find.

    Upload a copy of this work     Papers currently archived: 102,323

External links

  • This entry has no external links. Add one.
Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

  • Only published works are available at libraries.

Similar books and articles

Nonstandard Runs And Program Verification.Laszlo Csirmaz - 1981 - Bulletin of the Section of Logic 10 (2):68-77.
Prospects for naturalizing color.Alistair Isaac - 2009 - Philosophy of Science 76 (5):902-914.
Announcements.[author unknown] - 2003 - Review of Metaphysics 56 (4):937-938.
Replacement of the “genetic program” program.Ronald J. Planer - 2014 - Biology and Philosophy 29 (1):33-53.
First-order theories for pure Prolog programs with negation.Robert F. Stärk - 1995 - Archive for Mathematical Logic 34 (2):113-144.
Hilbert's program sixty years later.Wilfried Sieg - 1988 - Journal of Symbolic Logic 53 (2):338-348.

Analytics

Added to PP
2010-12-22

Downloads
25 (#901,963)

6 months
1 (#1,839,672)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Melvin Fitting
CUNY Graduate Center

Citations of this work

Modal interpolation via nested sequents.Melvin Fitting & Roman Kuznets - 2015 - Annals of Pure and Applied Logic 166 (3):274-305.
Simple Tableaus for Simple Logics.Melvin Fitting - 2024 - Notre Dame Journal of Formal Logic 65 (3):275-309.

Add more citations

References found in this work

Solution of a problem of Leon Henkin.M. H. Löb - 1955 - Journal of Symbolic Logic 20 (2):115-118.
The modal logic of provability. The sequential approach.Giovanni Sambin & Silvio Valentini - 1982 - Journal of Philosophical Logic 11 (3):311 - 342.
Self-Reference and Modal Logic.[author unknown] - 1987 - Studia Logica 46 (4):395-398.

Add more references