[Agda] Questions about logic

[Silvio Frischknecht]

Hello,

I am trying to learn some logic. Currently reading "A Mathematical
Introduction to Logic" by Enderton. I find it hard to keep track of what
can be done/assumed to be true in the metamathematic. I also find it
hard to keep track of all the implicit things like models. I was
wondering if it's possible to reproduce these results with Agda as
metamathematical system.

I found a paper that proved the completeness theorem for propositional
logic. https://akaposi.github.io/proplogic.pdf

Correct me if I'm wrong, but it seems like this might be easier than the
completness theorem for first-order logic because it deals with finite
things.

My questions are these.

1) Can Agda prove the completeness theorem of first order logic?

2) Can Agda prove the two incompleteness theorems?

3) Do I need some additional tools/axioms that I can postulate in Agda
to do this? Like set theory axioms?

4) Is set theory replaced by Agda or is it to be defined/implemented in
Agda?

5) What exactly are the limits of what can be proved? I assume at some
point the incompleteness theorem will kick in. Also popular opinion
seems to suggest that the constructivist view can not deal with the law
of included middle or the axiom of choice.

6) Could I theoretically rebuild the Agda syntax and proof that Agda
always terminates?


Cheers


Silvio

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20181005/a537f97a/attachment.html>