[Agda] Questions about logic

[Henning Basold]

-----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?).

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]. 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 
> 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-----