arXiv subjects

Makoto Fujiwara

Publications and source records attributed to Makoto Fujiwara.

7 recordsLinked to original sources

arXiv2025

Natural Language Translation of Formal Proofs through Informalization of Proof Steps and Recursive Summarization along Proof Structure

This paper proposes a natural language translation method for machine-verifiable formal proofs that leverages the informalization (verbalization of formal language proof steps) and summarization capabilities of LLMs. For evaluation, it was applied to formal proof data created in accordance with natural language proofs taken from an undergraduate-level textbook, and the quality of the generated natural language proofs was analyzed in comparison with the original natural language proofs. Furthermore, we will demonstrate that this method can output highly readable and accurate natural language proofs by applying it to existing formal proof library of the Lean proof assistant.

cs.CL↗

arXiv2025

Hierarchical formula classes with respect to semi-classical prenex normalization

In [10], the authors formalized the standard transformation procedure for prenex normalization of first-order formulas and showed that the classes $\mathrm{E}_k$ and $\mathrm{U}_k$ introduced in Akama et al. [1] are exactly the classes induced by $Σ_k$ and $Π_k$ respectively via the transformation procedure. In that sense, the classes $\mathrm{E}_k$ and $\mathrm{U}_k$ correspond to $Σ_k$ and $Π_k$ based on classical logic respectively. On the other hand, some transformations of the prenex normalization are not possible in constructive theories. In this paper, we introduce new classes $\mathcal{E}_k^n$ and $\mathcal{U}_k^n$ of first-order formulas with two parameters $k$ and $n$, and show that they are exactly the classes induced by $Σ_k$ and $Π_k$ respectively according to the $n$-th level semi-classical prenex normalization, which is obtained by the prenex normalization in [10] with some restriction to the introduced classes of degree $n$. In particular, the latter corresponds to possible transformations in intuitionistic arithmetic augmented with the law-of-excluded-middle schema restricted to formulas of $Σ_n$-form. In fact, if $ n\geq k$, our classes $\mathcal{E}_k^n$ and $\mathcal{U}_k^n$ are identical with the cumulative variants $\mathrm{E}^+_k$ and $\mathrm{U}^+_k$ of $\mathrm{E}_k$ and $\mathrm{U}_k$ respectively. In this sense, our classes are refinements of $\mathrm{E}^+_k$ and $\mathrm{U}^+_k$ with respect to the prenex normalization from the semi-classical perspective.

math.LO↗

arXiv2023

Prenex normalization and the hierarchical classification of formulas

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.

math.LO↗

arXiv2022

Refining the arithmetical hierarchy of classical principles

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.

math.LO↗

arXiv2022

Conservation theorems on semi-classical arithmetic

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.

math.LO↗

arXiv2020

Prenex normal form theorems in semi-classical arithmetic

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.

math.LO↗

arXiv2020

Decidable fan theorem and uniform continuity theorem with continuous moduli

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.

math.LO↗