<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
</head>
<body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; color: rgb(0, 0, 0); font-size: 14px; font-family: Calibri, sans-serif;">
<div>Hi Silvio,</div>
<div><br>
</div>
<div>you already got some interesting replies. Let me add my 10p:</div>
<div><br>
</div>
<span id="OLK_SRC_BODY_SECTION">
<div style="font-family:Calibri; font-size:11pt; text-align:left; color:black; BORDER-BOTTOM: medium none; BORDER-LEFT: medium none; PADDING-BOTTOM: 0in; PADDING-LEFT: 0in; PADDING-RIGHT: 0in; BORDER-TOP: #b5c4df 1pt solid; BORDER-RIGHT: medium none; PADDING-TOP: 3pt">
<span style="font-family: Calibri, sans-serif; font-size: 14px;">My questions are these.</span></div>
<div>
<div text="#000000" bgcolor="#FFFFFF">
<p>1) Can Agda prove the completeness theorem of first order logic?</p>
</div>
</div>
</span>
<div>You mean the completeness wrt to the classical notion of model due to Goedel? This uses classical logic hence in this form it is not provable in an intuitionistic system. You can give another definition of a model of classical logic and then it should
be provable. This is related to my comments about the completeness if intuitionistic first order logic. Many people think that intuitionistic logic is complete wrt Kripke models but this again needs classical logic. It can be fixed by correcting the notion
of model and then you can restrict to those models where excluded middle holds and I think completenss is then provable. I think Helmut Schwichtenberg has looked at this but I don't know of a formalisation.</div>
<span id="OLK_SRC_BODY_SECTION">
<div>
<div text="#000000" bgcolor="#FFFFFF">
<p>2) Can Agda prove the two incompleteness theorems?</p>
</div>
</div>
</span>
<div>That shouldn't be a problem. That is actually a nice project.</div>
<span id="OLK_SRC_BODY_SECTION">
<div>
<div text="#000000" bgcolor="#FFFFFF">
<p>3) Do I need some additional tools/axioms that I can postulate in Agda to do this? Like set theory axioms?</p>
</div>
</div>
</span>
<div>If you want to formalize the classical proof due to Gentzen, you need the axiom of choice which can be formulated in Type Theory. I am now thinking of HoTT which currently isn't matched by Agda's type theory but I hope that will change in the future. Instead
of adding assumptions corresponding to set theoretic axioms it makes more sense to add the principles of HoTT as postulates, e.g. the univalence axiom and the existsnece of certain higher inductive types. </div>
<div><br>
</div>
<div>For more background on HoTT see the HoTT book</div>
<div><a href="https://homotopytypetheory.org/book">https://homotopytypetheory.org/book</a>/</div>
<div>Time has moved on a bit since the book was written and there is now an implementation of HoTT in for of cubical type theory and there is some work in progress to add this to Agda.</div>
<span id="OLK_SRC_BODY_SECTION">
<div>
<div text="#000000" bgcolor="#FFFFFF">
<p>4) Is set theory replaced by Agda or is it to be defined/implemented in Agda?</p>
</div>
</div>
</span>
<div>Ok Agda is only an implementation of type theory and as indicated above it needs a bit of catching up to do. But yes, type theory replaces set theory and it has a number of advantages. In particular it is actually it allows us to hide details of implementations
while in set theory you can always see the encodings (e.g. how natural numbers are represented). As a payoff you can add the above mentioned univalence axioms, in a nutshell isomorphic sets are equal.</div>
<span id="OLK_SRC_BODY_SECTION">
<div>
<div text="#000000" bgcolor="#FFFFFF">
<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.</p>
</div>
</div>
</span>
<div>Yes, any interesting formal system is always incomplete – in particular you cannot show the consistency of any type theory (e.g. Agda) in itself.</div>
<div><br>
</div>
<div>The lack of excluded middle and the axiom of choice are not bugs but features. You can actually say that a predicate is decidable (I.e. excluded middle holds for it) and you can run your functions on a computer.</div>
<span id="OLK_SRC_BODY_SECTION">
<div text="#000000" bgcolor="#FFFFFF">
<p>6) Could I theoretically rebuild the Agda syntax and proof that Agda always terminates?</p>
<p>Yes, you just need a version of Agda that is stronger then the one you want to verify. E.g. you can just add additional universes.</p>
</div>
</span>
<div>Thorsten</div>
<PRE>
This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment.
Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored
where permitted by law.
</PRE></body>
</html>