Propositional proof systems, the consistency of first order theories and the complexity of computations.

*(English)*Zbl 0696.03029Let S be a finitely axiomatized theory. The authors consider the sequence \(Con_ S(\underline n)\), where \(Con_ S(\underline n)\) denotes the statement that there is no proof of contradiction in S whose length is \(\leq n\). They formulate nine statements, e.g. the following ones:

(1) There exists a finitely axiomatized fragment T of true arithmetic such that for every finitely axiomatized consistent theory S, there exists a polynomial p such that, for every \(n\in {\mathbb{N}}\), there is a proof of \(Con_ S(\underline n)\) in T, whose length is \(\leq p(n).\)

(6) There exists a finitely axiomatized fragment T of true arithmetic such that, for every finitely axiomatized consistent theory S, there exists a deterministic Turing machine M and a polynomial p such that for any given n, M constructs a proof of \(Con_ S(\underline n)\) in T, in time \(\leq p(n).\)

Then it is proved that statements (1)-(5) and (6)-(9) are equivalent, respectively. The problem arises whether (1)-(9) are true or not. This problem is discussed in the last part of the paper.

(1) There exists a finitely axiomatized fragment T of true arithmetic such that for every finitely axiomatized consistent theory S, there exists a polynomial p such that, for every \(n\in {\mathbb{N}}\), there is a proof of \(Con_ S(\underline n)\) in T, whose length is \(\leq p(n).\)

(6) There exists a finitely axiomatized fragment T of true arithmetic such that, for every finitely axiomatized consistent theory S, there exists a deterministic Turing machine M and a polynomial p such that for any given n, M constructs a proof of \(Con_ S(\underline n)\) in T, in time \(\leq p(n).\)

Then it is proved that statements (1)-(5) and (6)-(9) are equivalent, respectively. The problem arises whether (1)-(9) are true or not. This problem is discussed in the last part of the paper.

Reviewer: N.Both

##### MSC:

03F20 | Complexity of proofs |

03D10 | Turing machines and related notions |

03D15 | Complexity of computation (including implicit computational complexity) |

03B05 | Classical propositional logic |

03B10 | Classical first-order logic |

03F30 | First-order arithmetic and fragments |

##### Keywords:

finitely axiomatized fragment of true arithmetic; finitely axiomatized theory; Turing machine
PDF
BibTeX
XML
Cite

\textit{J. Krajíček} and \textit{P. Pudlák}, J. Symb. Log. 54, No. 3, 1063--1079 (1989; Zbl 0696.03029)

Full Text:
DOI

**OpenURL**

##### References:

[1] | Proceedings of the seventh annual ACM symposium on the theory of computing pp 83– (1975) |

[2] | The relative efficiency of propositional proof systems 44 pp 36– (1979) · Zbl 0408.03044 |

[3] | DOI: 10.1137/0204037 · Zbl 0323.68033 |

[4] | Relativization, readabilities and the exponential hierarchy (1980) |

[5] | Subsystems of arithmetic and complexity theory (1987) |

[6] | The complexity of computing (1976) |

[7] | DOI: 10.1090/conm/065/891256 |

[8] | Logic Colloquium ’84 pp 165– (1986) |

[9] | DOI: 10.1016/0168-0072(87)90066-2 · Zbl 0647.03046 |

[10] | Problemy Peredači Informacii 9 pp 115– (1973) |

[11] | Methods in mathematical logic (proceedings, Caracas, 1983) 1130 pp 317– (1985) |

[12] | Zeitschrift für Mathematische Logik und Grundlagen der Mathematik |

[13] | DOI: 10.1016/0304-3975(85)90144-6 · Zbl 0586.03010 |

[14] | On the consistency, completeness and correctness problems (1979) |

[15] | Bounded arithmetic (1986) |

This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.