
Summary: We define the notion of the uniform reduct of a propositional proof system as the set of those bounded formulas in the language of Peano Arithmetic which have polynomial size proofs under the Paris-Wilkie-translation. With respect to the arithmetic complexity of uniform reducts, we show that uniform reducts are \(\Pi_1^0\)-hard and obviously in \(\Sigma_2^0\). We also show under certain regularity conditions that each uniform reduct is closed under bounded generalisation; that in the case the language includes a symbol for exponentiation, a uniform reduct is closed under modus ponens if and only if it already contains all true bounded formulas; and that each uniform reduct contains all true \(\Pi_1^b(\alpha)\)-formulas.
Complexity of proofs, Classical propositional logic, First-order arithmetic and fragments, uniform reduct, propositional proof system, arithmetic complexity, length of proofs, bounded arithmetic, propositional calculus, translations
Complexity of proofs, Classical propositional logic, First-order arithmetic and fragments, uniform reduct, propositional proof system, arithmetic complexity, length of proofs, bounded arithmetic, propositional calculus, translations
| selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 0 | |
| popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Average | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Average | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Average |
