-
Prenex normalization and the hierarchical classification of formulas
Authors:
Makoto Fujiwara,
Taishi Kurahashi
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 cla…
▽ More
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 $Σ_k$ and $Π_k$ respectively via the transformation procedure in any first-order theory.
△ Less
Submitted 13 November, 2023; v1 submitted 23 February, 2023;
originally announced February 2023.
-
Conservation theorems on semi-classical arithmetic
Authors:
Makoto Fujiwara,
Taishi Kurahashi
Abstract:
We systematically study conservation theorems on theories of semi-classical arithmetic, which lie in-between classical arithmetic $\mathsf{PA}$ and intuitionistic arithmetic $\mathsf{HA}$. Using a generalized negative translation, we first provide a new structured proof of the fact that $\mathsf{PA}$ is $Π_{k+2}$-conservative over $\mathsf{HA} + Σ_k\text{-}\mathrm{LEM}$ where…
▽ More
We systematically study conservation theorems on theories of semi-classical arithmetic, which lie in-between classical arithmetic $\mathsf{PA}$ and intuitionistic arithmetic $\mathsf{HA}$. Using a generalized negative translation, we first provide a new structured proof of the fact that $\mathsf{PA}$ is $Π_{k+2}$-conservative over $\mathsf{HA} + Σ_k\text{-}\mathrm{LEM}$ where $Σ_k\text{-}\mathrm{LEM}$ is the axiom scheme of the law-of-excluded-middle restricted to formulas in $Σ_k$. In addition, we show that this conservation theorem is optimal in the sense that for any semi-classical arithmetic $T$, if $\mathsf{PA}$ is $Π_{k+2}$-conservative over $T$, then $T$ proves $Σ_k\text{-}\mathrm{LEM}$. In the same manner, we also characterize conservation theorems for other well-studied classes of formulas by fragments of classical axioms or rules. This reveals the entire structure of conservation theorems with respect to the arithmetical hierarchy of classical principles.
△ Less
Submitted 13 March, 2022; v1 submitted 23 July, 2021;
originally announced July 2021.
-
Refining the arithmetical hierarchy of classical principles
Authors:
Makoto Fujiwara,
Taishi Kurahashi
Abstract:
We refine the arithmetical hierarchy of various classical principles by finely investigating the derivability relations between these principles over Heyting arithmetic. We mainly investigate some restricted versions of the law of excluded middle, de Morgan's law, the double negation elimination, the collection principle and the constant domain axiom.
We refine the arithmetical hierarchy of various classical principles by finely investigating the derivability relations between these principles over Heyting arithmetic. We mainly investigate some restricted versions of the law of excluded middle, de Morgan's law, the double negation elimination, the collection principle and the constant domain axiom.
△ Less
Submitted 27 April, 2022; v1 submitted 22 October, 2020;
originally announced October 2020.
-
Prenex normal form theorems in semi-classical arithmetic
Authors:
Makoto Fujiwara,
Taishi Kurahashi
Abstract:
Akama et al. systematically studied an arithmetical hierarchy of the law of excluded middle and related principles in the context of first-order arithmetic. In that paper, they first provide a prenex normal form theorem as a justification of their semi-classical principles restricted to prenex formulas. However, there are some errors in their proof. In this paper, we provide a simple counterexampl…
▽ More
Akama et al. systematically studied an arithmetical hierarchy of the law of excluded middle and related principles in the context of first-order arithmetic. In that paper, they first provide a prenex normal form theorem as a justification of their semi-classical principles restricted to prenex formulas. However, there are some errors in their proof. In this paper, we provide a simple counterexample of their prenex normal form theorem, then modify it in an appropriate way. In addition, we characterize several prenex normal form theorems with respect to semi-classical arithmetic.
△ Less
Submitted 7 September, 2020;
originally announced September 2020.
-
Decidable fan theorem and uniform continuity theorem with continuous moduli
Authors:
Makoto Fujiwara,
Tatsuji Kawai
Abstract:
The uniform continuity theorem (UCT) states that every pointwise continuous real-valued function on the unit interval is uniformly continuous. In constructive mathematics, UCT is stronger than the decidable fan theorem (DFT); however, Loeb [Ann. Pure Appl. Logic, 132(1):51-66, 2005] has shown that the two principles become equivalent with a suitable coding of "continuous functions" as type-one obj…
▽ More
The uniform continuity theorem (UCT) states that every pointwise continuous real-valued function on the unit interval is uniformly continuous. In constructive mathematics, UCT is stronger than the decidable fan theorem (DFT); however, Loeb [Ann. Pure Appl. Logic, 132(1):51-66, 2005] has shown that the two principles become equivalent with a suitable coding of "continuous functions" as type-one objects. The question remains whether DFT can be characterised by a weaker version of UCT using a natural subclass of pointwise continuous functions without such a coding. We show that when "pointwise continuous" is replaced with "having a continuous modulus", UCT becomes equivalent to DFT. We also show that this weakening of UCT is equivalent to a similar principle for real-valued functions on the Cantor space $\{0,1\}^{\mathbb{N}}$. These results extend Berger's characterisation of DFT by the similar principle for functions from $\{0,1\}^{\mathbb{N}}$ to $\mathbb{N}$, and unifies these characterisations of DFT in terms of functions having continuous moduli. Furthermore, we directly show that the continuous real-valued functions on the unit interval having continuous moduli are exactly those functions which admit the coding of "continuous functions" due to Loeb. Our result allows us to interpret her work in the usual context of mathematics.
△ Less
Submitted 16 April, 2020; v1 submitted 5 December, 2019;
originally announced December 2019.
-
Finite type invariants of words and Arnold's invariants
Authors:
M. Fujiwara
Abstract:
We define a new finite type invariant for stably homeomorphic class of curves on compact oriented surfaces without boundaries and extend to a regular homotopy invariant for spherical curves.
We define a new finite type invariant for stably homeomorphic class of curves on compact oriented surfaces without boundaries and extend to a regular homotopy invariant for spherical curves.
△ Less
Submitted 27 August, 2008;
originally announced August 2008.
