On the complexity of Gödel's proof predicate

Journal of Symbolic Logic 75 (1):239-254 (2010)
  Copy   BIBTEX


The undecidability of first-order logic implies that there is no computable bound on the length of shortest proofs of valid sentences of first-order logic. Some valid sentences can only have quite long proofs. How hard is it to prove such "hard" valid sentences? The polynomial time tractability of this problem would imply the fixed-parameter tractability of the parameterized problem that, given a natural number n in unary as input and a first-order sentence φ as parameter, asks whether φ has a proof of length ≤ n. As the underlying classical problem has been considered by Gödel we denote this problem by p-Gödel. We show that p-Gödel is not fixed-parameter tractable if DTIME(h O(1) ) ≠ NTIME(h O(1) ) for all time constructible and increasing functions h. Moreover we analyze the complexity of the construction problem associated with p-Gödel



    Upload a copy of this work     Papers currently archived: 80,119

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

Arithmetic Proof and Open Sentences.Neil Thompson - 2012 - Philosophy Study 2 (1):43-50.
Modal collapse in Gödel's ontological proof.Srećko Kovač - 2012 - In Miroslaw Szatkowski (ed.), Ontological Proofs Today. Frankfurt a. M., etc.: Ontos Verlag. pp. 50--323.
Some Emendations of Gödel's Ontological Proof.C. Anthony Anderson - 1990 - Faith and Philosophy 7 (3):291-303.
Questioning Gödel's Ontological Proof: Is Truth Positive?Gregor Damschen - 2011 - European Journal for Philosophy of Religion 3 (1):161-169.
The gödel paradox and Wittgenstein's reasons.Francesco Berto - 2009 - Philosophia Mathematica 17 (2):208-219.
The complexity of propositional proofs.Nathan Segerlind - 2007 - Bulletin of Symbolic Logic 13 (4):417-481.


Added to PP

35 (#348,359)

6 months
1 (#477,905)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

No citations found.

Add more citations

References found in this work

Parameterized Complexity Theory.J. Flum - 2007 - Bulletin of Symbolic Logic 13 (2):246-248.

Add more references