scientific article; zbMATH DE number 1149459

DOI10.5486/PMD.1997.1841MaRDI QIDQ4386982zbMATH OpenFDO

Authors Albert G. Dragalin

Publication date 6 May 1998

Full work available at URL https://doi.org/10.5486/PMD.1997.1841

zbMATH Keywords

\(\omega\)-ruleconstructible setscut eliminationdefinable sets of natural numberssecond order arithmeticsequent calculus

Mathematics Subject Classification ID

Inner models, including constructibility, ordinal definability, and core models (03E45) Cut-elimination and normal-form theorems (03F05) Second- and higher-order arithmetic and fragments (03F35)

Review text

This paper is a revised English version of an article which originally appeared in Russian [cf. Set theory and topology, No. 1, Interuniv. Work. Collect., Izhevsk 1977, 27-36 (1977; Zbl 0483.03038)]. The author introduces a sequent calculus for second order arithmetic with \(\omega\)-rule, where second order variables range over definable sets of natural numbers. Formally, this means that the sequent calculus has an infinitary rule which allows to infer \(\forall X A(X)\) whenever \(A(T)\) is derivable for each closed second order term \(T\). The main result is a non-constructive cut-elimination theorem for the calculus (whence consistency); the proof adapts Takahashi's method of completing semivaluations and uses the constructibility axiom, \(V=L\), in order to get a sound interpretation of the infinitary inference rule for universal set quantification. The paper is neatly written. It would be interesting to know if there are applications of the main theorem to other branches to mathematical logic.

Recommendations

• An extension of the omega-rule
• scientific article; zbMATH DE number 4123723
• scientific article; zbMATH DE number 4066873
• Further applications of ultra-conservative ω-rules
• scientific article; zbMATH DE number 1187191

This page was built for publication:

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