[Agda] Questions about logic

[Thorsten Altenkirch]

On 06/10/2018, 09:15, "Agda on behalf of Henning Basold" <agda-bounces at lists.chalmers.se<mailto:agda-bounces at lists.chalmers.se> on behalf of henning at basold.eu<mailto:henning at basold.eu>> wrote:

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA512

Dear Silvio,

The completeness of classical propositional logic reduces to
completeness with respect to the Boolean algebra {0,1}. This is what
makes the proof fairly straightforward. For intuitionistic
propositional logic, on the other hand, requires to quantify over all
Heyting algebras and for completeness the construction of a canonical
model. I suppose that this could be done in Agda (anyone seen this?).

You need to be a bit careful here.

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.

First-order logic is another beast though. If you ask about
intuitionistic FOL, then you have to prove completeness with respect
to Kripke-models. That again should be possible in Agda, as it is
intuitionistically valid, see [1].

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.

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.

See for example: http://www.cs.nott.ac.uk/~psztxa/talks/nbe09.pdf

Completeness for classical FOL is
much more difficult. I remember that Hugo Herbelin talked about this
at the "Programs, Structures and Computations" workshop in 2014. There
is a working draft on his homepage [2]. Implementing something like
this in Agda probably requires a lot of time though (maybe a good
master or partial PhD project (-:).

I hope this helps a bit in answering your questions.

Best,
Henning

[1] https://www.sciencedirect.com/science/article/pii/S0168007213001085
[2]
http://pauillac.inria.fr/~herbelin/articles/godel-completeness-draft16.p
df

On 05/10/18 19:33, Silvio Frischknecht 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<mailto:Agda at lists.chalmers.se>
https://lists.chalmers.se/mailman/listinfo/agda
-----BEGIN PGP SIGNATURE-----

iQIzBAEBCgAdFiEEMnUmuprSDishxVMiatBsEc2xMm4FAlu4bwQACgkQatBsEc2x
Mm6IvRAAngizOGgeobOTxOK47pB3n5XQOlcqUT7DXjjZ5w4QaVZBg0tN1dlSRXf7
ETJyUnq3XgPZF/1pGmfFusAKtFj1wbafgWyHwdf3WmzHp4A0T+j/Junl577hNQW2
b4L1oGRl1S+bzW5OdmCehYfXp5f2xfY7N+jGIIJlJ7xM8gS13wXQAA0x8VMFX5gR
X9IOdrb+KPw3Yvxs+mSyL7JKAnHA9JI/Vxnii3UhcHMQwGi4+9au5zvoeWi7iejP
PwqZh8YHgIZ3xDBvwhfXPJD5ywrEuofR/57fVfmRlUt3YR8DKWP/dBnSXlbyF/MP
Y7AUbItrNF+6zXESDoxYZuzadrkvORD8HXB+ARWMCh9xk41d/j+tV9xNuMcRCZIB
e1UtZHSqGGMMyTNma+WetZY3EibjFknVnOVird43bqZGm67bCpwaRcbMLPSvSTda
GfXtU41QfBSTNHkHqDHCDWv9zZELaXpmBhii22S5Fsh/w38ME9txOq1p6/iau1d2
kir6DvrNXYyReXwAqA2B6TzKoNHguyjBuqzovCF5krrL01wwut1dHx3YsGK6ud20
4QQFvL6dNWyB23bezFljDauAyQFd4Cl+4tzOCmtlhF0EfBro3wjH/ANovFN+0u80
hYBWts0n9yAPRJskW8LdeNAfowdvETmg8S1/PxHCbz7tn/v+qDc=
=UNc2
-----END PGP SIGNATURE-----
_______________________________________________
Agda mailing list
Agda at lists.chalmers.se<mailto:Agda at lists.chalmers.se>
https://lists.chalmers.se/mailman/listinfo/agda




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.




-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20181006/77d2e714/attachment.html>