2 papers
cs.LO2026
Formalizing Representation Theorems for a Logical Framework with Rewriting
Thomas Traversié, Florian Rabe
Representation theorems for formal systems often take the form of an inductive translation that satisfies certain invariants, which are proved inductively. Theory morphisms and log…
cs.LO2026
Kuroda's Translation for Higher-Order Logic
Thomas Traversié
Kuroda's translation embeds first-order classical logic into intuitionistic logic, such that a formula and its translation are equivalent in classical logic. Recently, Brown and Ri…