[Agda] Questions about logic

[Jesper Cockx]

Hi Silvio,

> 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?

Agda is based on Martin-Löf type theory, which can be thought of as a
replacement for both logic and set theory of usual mathematics (since types
serve a dual role as both propositions and 'sets'). Type theory does not
rely on axioms like set theory but rather on pairs of
introduction/elimination rules, so for most tasks you do not need to add
any axioms to Agda. Of course, Agda is an intuitionistic logic so you do
not have the law of the excluded (not the included btw) middle or the axiom
of choice, so you may want to postulate these. However, if you haven't done
any intuitionistic logic before you may be surprised how far you can get
without them :)

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

Agda is quite a large language and so hasn't been given a fully formal
semantics or a proof of termination (yet). However, there have been some
attempts at formalizing and proving correct some parts of Agda (I recently
wrote a blog post
<https://jesper.sikanda.be/posts/elaborating-dependent-copattern-matching.html>
about one of these). And of course, the basis of Agda is MLTT which has
been given many different proofs of normalization, so if you restrict
yourself to a sufficiently small fragment of Agda it may be possible to
reuse one of those.

I hope that helps!

-- Jesper



On Sat, Oct 6, 2018 at 8:25 AM Silvio Frischknecht <silvio.frischi at gmail.com>
wrote:

> 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
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20181006/7624bc46/attachment.html>