<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; font-family: Calibri, sans-serif; font-size: 14px; color: rgb(0, 0, 0);">
<div>On 06/10/2018, 09:15, "Agda on behalf of Henning Basold" <<a href="mailto:agda-bounces@lists.chalmers.se">agda-bounces@lists.chalmers.se</a> on behalf of
<a href="mailto:henning@basold.eu">henning@basold.eu</a>> wrote:</div>
<div><br>
</div>
<blockquote id="MAC_OUTLOOK_ATTRIBUTION_BLOCKQUOTE" style="BORDER-LEFT: #b5c4df 5 solid; PADDING:0 0 0 5; MARGIN:0 0 0 5;">
<blockquote style="margin:0 0 0 40px; border:none; padding:0px;">
<div>-----BEGIN PGP SIGNED MESSAGE-----</div>
<div>Hash: SHA512</div>
<div><br>
</div>
<div>Dear Silvio,</div>
<div><br>
</div>
<div>The completeness of classical propositional logic reduces to</div>
<div>completeness with respect to the Boolean algebra {0,1}. This is what</div>
<div>makes the proof fairly straightforward. For intuitionistic</div>
<div>propositional logic, on the other hand, requires to quantify over all</div>
<div>Heyting algebras and for completeness the construction of a canonical</div>
<div>model. I suppose that this could be done in Agda (anyone seen this?).</div>
</blockquote>
</blockquote>
<blockquote style="margin:0 0 0 40px; border:none; padding:0px;">
<div><br>
</div>
</blockquote>
<div>
<div style="font-family: Consolas, monospace; font-size: 12px;">You need to be a bit careful here.</div>
<div style="font-family: Consolas, monospace; font-size: 12px;"><br>
</div>
<div style="font-family: Consolas, monospace; font-size: 12px;">As long as you leave out \/ and False (and also negation), then the completeness proof for propositioal logic is straightforward. However, if you include those it gets a bit more tricky and you
need to exploit the decidability of propositional logic.</div>
<div style="font-family: Consolas, monospace; font-size: 12px;"><br>
</div>
</div>
<blockquote id="MAC_OUTLOOK_ATTRIBUTION_BLOCKQUOTE" style="BORDER-LEFT: #b5c4df 5 solid; PADDING:0 0 0 5; MARGIN:0 0 0 5;">
<blockquote style="margin:0 0 0 40px; border:none; padding:0px;">
<div>First-order logic is another beast though. If you ask about</div>
<div>intuitionistic FOL, then you have to prove completeness with respect</div>
<div>to Kripke-models. That again should be possible in Agda, as it is</div>
<div>intuitionistically valid, see [1]. </div>
</blockquote>
</blockquote>
<div><br>
</div>
<div>No it is not. At least not if you include \/,False,exists. Actually completeness of FOL wrt Kripke models is known to be equivalent to Markov's principle.</div>
<div><br>
</div>
<div>This can be fixed but basically Kripke models are not the right semantics for intuitionistic logic. You need something what I call Beth models, which extends Kripke models with a notion of covering of a world. While Kripke models corresponds to presheaves,
Beth models correspond to sheaves.</div>
<div><br>
</div>
<div>See for example: http://www.cs.nott.ac.uk/~psztxa/talks/nbe09.pdf</div>
<div><br>
</div>
<blockquote id="MAC_OUTLOOK_ATTRIBUTION_BLOCKQUOTE" style="BORDER-LEFT: #b5c4df 5 solid; PADDING:0 0 0 5; MARGIN:0 0 0 5;">
<blockquote style="margin:0 0 0 40px; border:none; padding:0px;">
<div>Completeness for classical FOL is</div>
<div>much more difficult. I remember that Hugo Herbelin talked about this</div>
<div>at the "Programs, Structures and Computations" workshop in 2014. There</div>
<div>is a working draft on his homepage [2]. Implementing something like</div>
<div>this in Agda probably requires a lot of time though (maybe a good</div>
<div>master or partial PhD project (-:).</div>
<div><br>
</div>
</blockquote>
<div>I hope this helps a bit in answering your questions.</div>
<div><br>
</div>
<div>Best,</div>
<div>Henning</div>
<div><br>
</div>
<div>[1] <a href="https://www.sciencedirect.com/science/article/pii/S0168007213001085">
https://www.sciencedirect.com/science/article/pii/S0168007213001085</a></div>
<div>[2]</div>
<div><a href="http://pauillac.inria.fr/~herbelin/articles/godel-completeness-draft16.p">http://pauillac.inria.fr/~herbelin/articles/godel-completeness-draft16.p</a></div>
<div>df</div>
<div><br>
</div>
<div>On 05/10/18 19:33, Silvio Frischknecht wrote:</div>
<blockquote id="MAC_OUTLOOK_ATTRIBUTION_BLOCKQUOTE" style="BORDER-LEFT: #b5c4df 5 solid; PADDING:0 0 0 5; MARGIN:0 0 0 5;">
<div>Hello,</div>
<div></div>
<div>I am trying to learn some logic. Currently reading "A Mathematical </div>
<div>Introduction to Logic" by Enderton. I find it hard to keep track of</div>
<div>what can be done/assumed to be true in the metamathematic. I also</div>
<div>find it hard to keep track of all the implicit things like models.</div>
<div>I was wondering if it's possible to reproduce these results with</div>
<div>Agda as metamathematical system.</div>
<div></div>
<div>I found a paper that proved the completeness theorem for</div>
<div>propositional logic. <a href="https://akaposi.github.io/proplogic.pdf">https://akaposi.github.io/proplogic.pdf</a></div>
<div></div>
<div>Correct me if I'm wrong, but it seems like this might be easier</div>
<div>than the completness theorem for first-order logic because it deals</div>
<div>with finite things.</div>
<div></div>
<div>My questions are these.</div>
<div></div>
<div>1) Can Agda prove the completeness theorem of first order logic?</div>
<div></div>
<div>2) Can Agda prove the two incompleteness theorems?</div>
<div></div>
<div>3) Do I need some additional tools/axioms that I can postulate in</div>
<div>Agda to do this? Like set theory axioms?</div>
<div></div>
<div>4) Is set theory replaced by Agda or is it to be</div>
<div>defined/implemented in Agda?</div>
<div></div>
<div>5) What exactly are the limits of what can be proved? I assume at</div>
<div>some point the incompleteness theorem will kick in. Also popular</div>
<div>opinion seems to suggest that the constructivist view can not deal</div>
<div>with the law of included middle or the axiom of choice.</div>
<div></div>
<div>6) Could I theoretically rebuild the Agda syntax and proof that</div>
<div>Agda always terminates?</div>
<div></div>
<div></div>
<div>Cheers</div>
<div></div>
<div></div>
<div>Silvio</div>
<div></div>
<div></div>
<div></div>
<div></div>
<div>_______________________________________________ Agda mailing list </div>
<div><a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a> </div>
<div><a href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a></div>
<div></div>
</blockquote>
<div>-----BEGIN PGP SIGNATURE-----</div>
<div><br>
</div>
<div>iQIzBAEBCgAdFiEEMnUmuprSDishxVMiatBsEc2xMm4FAlu4bwQACgkQatBsEc2x</div>
<div>Mm6IvRAAngizOGgeobOTxOK47pB3n5XQOlcqUT7DXjjZ5w4QaVZBg0tN1dlSRXf7</div>
<div>ETJyUnq3XgPZF/1pGmfFusAKtFj1wbafgWyHwdf3WmzHp4A0T+j/Junl577hNQW2</div>
<div>b4L1oGRl1S+bzW5OdmCehYfXp5f2xfY7N+jGIIJlJ7xM8gS13wXQAA0x8VMFX5gR</div>
<div>X9IOdrb+KPw3Yvxs+mSyL7JKAnHA9JI/Vxnii3UhcHMQwGi4+9au5zvoeWi7iejP</div>
<div>PwqZh8YHgIZ3xDBvwhfXPJD5ywrEuofR/57fVfmRlUt3YR8DKWP/dBnSXlbyF/MP</div>
<div>Y7AUbItrNF+6zXESDoxYZuzadrkvORD8HXB+ARWMCh9xk41d/j+tV9xNuMcRCZIB</div>
<div>e1UtZHSqGGMMyTNma+WetZY3EibjFknVnOVird43bqZGm67bCpwaRcbMLPSvSTda</div>
<div>GfXtU41QfBSTNHkHqDHCDWv9zZELaXpmBhii22S5Fsh/w38ME9txOq1p6/iau1d2</div>
<div>kir6DvrNXYyReXwAqA2B6TzKoNHguyjBuqzovCF5krrL01wwut1dHx3YsGK6ud20</div>
<div>4QQFvL6dNWyB23bezFljDauAyQFd4Cl+4tzOCmtlhF0EfBro3wjH/ANovFN+0u80</div>
<div>hYBWts0n9yAPRJskW8LdeNAfowdvETmg8S1/PxHCbz7tn/v+qDc=</div>
<div>=UNc2</div>
<div>-----END PGP SIGNATURE-----</div>
<div>_______________________________________________</div>
<div>Agda mailing list</div>
<div><a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a></div>
<div><a href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a></div>
<div><br>
</div>
</blockquote>
<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>