[Agda] Questions about logic

[Ambrus Kaposi]

On Sat, Oct 6, 2018 at 10:15 AM Henning Basold <henning at basold.eu> wrote:

> The completeness of classical propositional logic reduces to
> completeness with respect to the Boolean algebra {0,1}. This is what
> makes the proof fairly straightforward. For intuitionistic
> propositional logic, on the other hand, requires to quantify over all
> Heyting algebras and for completeness the construction of a canonical
> model. I suppose that this could be done in Agda (anyone seen this?).
>

 Here is a formalisation:
https://bitbucket.org/akaposi/tt-in-tt/src/HEAD/STT/MinimalLogic.agda
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20181006/bd3650dd/attachment.html>