2 papers
math.LO2021
First-order natural deduction in Agda
Louis Warren
Agda is a dependently-typed functional programming language, based on an extension of intuitionistic Martin-Löf type theory. We implement first order natural deduction in Agda. We…
math.LO2018
The Drinker Paradox and its Dual
Louis Warren, Hannes Diener, Maarten McKubre-Jordens
The Drinker Paradox is as follows. In every nonempty tavern, there is a person such that if that person is drinking, then everyone in the tavern is drinking. Formally, \[ \exists x…