<div dir="ltr">Hi Silvio,<br><div><br></div><div>> 3) Do I need some additional tools/axioms that I can postulate in
Agda to do this? Like set theory axioms?
</div><div>> 4) Is set theory replaced by Agda or is it to be
defined/implemented in Agda?
</div><div><br></div>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 :)<br><br>> 6) Could I theoretically rebuild the Agda syntax and proof that Agda always terminates?<br><br>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 <a href="https://jesper.sikanda.be/posts/elaborating-dependent-copattern-matching.html">blog post</a> 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.<br><br>I hope that helps!<br><br>-- Jesper<br><br> </div><br><div class="gmail_quote"><div dir="ltr">On Sat, Oct 6, 2018 at 8:25 AM Silvio Frischknecht <<a href="mailto:silvio.frischi@gmail.com">silvio.frischi@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div text="#000000" bgcolor="#FFFFFF">
<p>Hello,</p>
<p>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.</p>
<p>I found a paper that proved the completeness theorem for
propositional logic. <a class="m_6293560748095074532moz-txt-link-freetext" href="https://akaposi.github.io/proplogic.pdf" target="_blank">https://akaposi.github.io/proplogic.pdf</a></p>
<p>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.</p>
<p>My questions are these.<br>
</p>
<p>1) Can Agda prove the completeness theorem of first order logic?<br>
</p>
<p>2) Can Agda prove the two incompleteness theorems?</p>
<p>3) Do I need some additional tools/axioms that I can postulate in
Agda to do this? Like set theory axioms?</p>
<p>4) Is set theory replaced by Agda or is it to be
defined/implemented in Agda?<br>
</p>
<p>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.<br>
</p>
<p>6) Could I theoretically rebuild the Agda syntax and proof that
Agda always terminates?</p>
<p><br>
</p>
<p>Cheers</p>
<p><br>
</p>
<p>Silvio<br>
</p>
</div>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>