<html>
<head>
<meta http-equiv="content-type" content="text/html; charset=utf-8">
</head>
<body 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="moz-txt-link-freetext" href="https://akaposi.github.io/proplogic.pdf">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>
</body>
</html>