×

zbMATH — the first resource for mathematics

Propositional proof systems, the consistency of first order theories and the complexity of computations. (English) Zbl 0696.03029
Let 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.
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
PDF BibTeX XML Cite
Full Text: DOI
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.