Mashu Noguchi

collaborators

3 papers

cs.LO2026

Mechanizing Gödel's incompleteness Theorems and Provability Logic

Shogo Saitou, Mashu Noguchi

We mechanized proof of Gödel's first and second incompleteness theorems, Solovay's arithmetical completeness theorem of \mathbf{GL}, and related results in the Lean 4 theorem prove…

math.LO2026

Embeddings of Propositional Logics into the Provability Logics $S$ and $D$

Mashu Noguchi

Just as Visser showed that the formal propositional logic $FPL$ can be embedded into Gödel-Löb provability logic $GL$ , Petrukhin proposed a propositional logic $\…

math.LO2026

Very weak subintuitionistic logics

Taishi Kurahashi, Mashu Noguchi

We introduce a new propositional logic, called very weak subintuitionistic logic $VF$ , by adapting the relational semantics of Fitting, Marek, and Truszczyński for the pur…

Mechanizing Gödel's incompleteness Theorems and Provability Logic

Embeddings of Propositional Logics into the Provability Logics S and D

Very weak subintuitionistic logics

Embeddings of Propositional Logics into the Provability Logics $S$ and $D$