A bounded arithmetic AID for Frege systems

DOI10.1016/S0168-0072(99)00041-XMaRDI QIDQ1977488zbMATH OpenFDO

Authors Toshiyasu Arai

Publication date 2 May 2001

Published in Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/math/9809205

zbMATH Keywords

bounded arithmeticALOGTIMEFrege systemalogtime inductive definitions

Mathematics Subject Classification ID

Complexity classes (hierarchies, relations among complexity classes, etc.) (68Q15) Complexity of proofs (03F20) First-order arithmetic and fragments (03F30)

Abstract: In this paper we introduce a system AID (Alogtime Inductive Definitions) of bounded arithmetic. The main feature of AID is to allow a form of inductive definitions, which was extracted from Buss' propositional consistency proof of Frege systems F. We show that AID proves the soundness of F, and conversely any Sigma^b_0-theorem in AID yields boolean sentences of which F has polysize proofs. Further we define Sigma^b_1-faithful interpretations between AID + Sigma b^_0 - CA and a quantified theory QALV of an equational system ALV in P. Clote. Hence ALV also proves the soundness of F.

Recommendations

• Bounded arithmetic in free logic
• On Rules and Parameter Free Systems in Bounded Arithmetic
• scientific article; zbMATH DE number 218509
• scientific article; zbMATH DE number 2196511
• An algebraic treatment of quantifier-free systems of arithmetic
• A note on bounded arithmetic
• Logic of Proofs for Bounded Arithmetic
• Proof complexity in algebraic systems and bounded depth Frege systems with modular counting
• On the provability logic of bounded arithmetic
• The polynomial bounds of proof complexity in Frege systems

Cites work

• scientific article; zbMATH DE number 440476 (Why is no real title available?)
• scientific article; zbMATH DE number 440478 (Why is no real title available?)
• scientific article; zbMATH DE number 4059391 (Why is no real title available?)
• scientific article; zbMATH DE number 176199 (Why is no real title available?)
• scientific article; zbMATH DE number 192916 (Why is no real title available?)
• scientific article; zbMATH DE number 3557241 (Why is no real title available?)
• scientific article; zbMATH DE number 1114018 (Why is no real title available?)
• scientific article; zbMATH DE number 1114026 (Why is no real title available?)
• scientific article; zbMATH DE number 806744 (Why is no real title available?)
• scientific article; zbMATH DE number 806747 (Why is no real title available?)
• scientific article; zbMATH DE number 806751 (Why is no real title available?)
• scientific article; zbMATH DE number 819737 (Why is no real title available?)
• Bounded arithmetic for NC, ALogTIME, L and NL
• Polynomial size proofs of the propositional pigeonhole principle
• Propositional consistency proofs
• The graph of multiplication is equivalent to counting

Cited in

(11)

• Polynomal-size Frege proofs of Bollobás' theorem on the trace of sets
• Expander construction in \(\mathsf{VNC}^1\)
• Quantified propositional calculus and a second-order theory for NC\(^{\text \textbf{1}}\)
• The equivalence of theories that characterize ALogTime
• The NP search problems of Frege and extended Frege proofs
• Equational fragments of systems for arithmetic.
• Function-algebraic characterizations of log and polylog parallel time
• scientific article; zbMATH DE number 218509 (Why is no real title available?)
• On theories of bounded arithmetic for \(\mathrm{NC}^1\)
• Expander construction in \(\mathrm{VNC}^1\)
• Tractability of cut-free Gentzen-type propositional calculus with permutation inference. II

This page was built for publication: A bounded arithmetic AID for Frege systems

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1977488)