5 papers · 1 filter
Logic and computation as combinatorics
Norihiro Yamada
The syntactic nature of logic and computation separates them from other fields of mathematics. Nevertheless, syntax has been the only way to adequately capture the dynamics of proo…
Game semantics of universes
Norihiro Yamada
This work extends the present author's computational game semantics of Martin-Löf type theory to the cumulative hierarchy of universes. This extension completes game semantics of a…
Game semantics of Martin-Löf type theory, part III: its consistency with Church's thesis
Norihiro Yamada
We prove consistency of intensional Martin-Löf type theory (MLTT) with formal Church's thesis (CT), which was open for at least fifteen years. The difficulty in proving the consist…
Sequent calculi for a unity of logic
Norihiro Yamada
We present a novel unity of logic, viz., a single sequent calculus that embodies classical, intuitionistic and linear logics. Concretely, we define classical linear logic negative…
On the Unity of Logic: a Sequential, Unpolarized Approach
Norihiro Yamada
The present work aims to give a unity of logic via standard sequential, unpolarized games. Specifically, our vision is that there must be mathematically precise concepts of linear…