Prenex normalization and the hierarchical classification of formulas

DOI10.1007/S00153-023-00899-XMaRDI QIDQ6128782zbMATH OpenFDO

Authors Makoto Fujiwara, Taishi Kurahashi

Publication date 16 April 2024

Published in Archive for Mathematical Logic (Search for Journal in Brave)

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

zbMATH Keywords

arithmetical hierarchyprenex normal form theoremformula classesprenex normalization

Mathematics Subject Classification ID

Classical first-order logic (03B10) Subsystems of classical logic (including intuitionistic logic) (03B20) General logic (03B99)

Abstract: Akama et al. [1] introduced a hierarchical classification of first-order formulas for a hierarchical prenex normal form theorem in semi-classical arithmetic. In this paper, we give a justification for the hierarchical classification in a general context of first-order theories. To this end, we first formalize the standard transformation procedure for prenex normalization. Then we show that the classes $mathrm{E}_k$ and $mathrm{U}_k$ introduced in [1] are exactly the classes induced by $Sigm{a}_k$ and $P{i}_k$ respectively via the transformation procedure.

Recommendations

• Prenex normal form theorems in semi-classical arithmetic
• scientific article; zbMATH DE number 2152681
• The Skolemization of prenex formulas in intermediate logics
• The Classical Model Existence Theorem in Subclassical Predicate Logics I
• scientific article; zbMATH DE number 4095435

This page was built for publication: Prenex normalization and the hierarchical classification of formulas

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