A bounded arithmetic AID for Frege systems

Autor:	Toshiyasu Arai
Rok vydání:	2000
Předmět:	Soundness Discrete mathematics Feature (linguistics) Equational system Bounded arithmetic Logic Frege system Consistency (knowledge bases) ALOGTIME Mathematical proof Mathematics
Zdroj:	Annals of Pure and Applied Logic. 103(1-3):155-199
ISSN:	0168-0072
DOI:	10.1016/s0168-0072(99)00041-x
Popis:	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 in Buss (Ann. Pure Appl. Logic 52 (1991) 3–29). We show that AID proves the soundness of F , and conversely any Σ 0 b -theorem in AID yields boolean sentences of which F has polysize proofs. Further we define Σ 1 b -faithful interpretations between AID+Σ 0 b -CA and a quantified theory QALV of an equational system ALV in Clote (Ann. Math. Art. Intell. 6 (1992) 57–106). Hence ALV also proves the soundness of F .
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=doi_dedup___::a87a046ea463af9f9a54f4bd4936170f Zobrazit plný text záznamu Full Text from ScienceDirect