[Agda] Questions about logic

[Thorsten Altenkirch]

Hi Silvio,

you already got some interesting replies. Let me add my 10p:

My questions are these.

1) Can Agda prove the completeness theorem of first order logic?

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.

2) Can Agda prove the two incompleteness theorems?

That shouldn't be a problem. That is actually a nice project.

3) Do I need some additional tools/axioms that I can postulate in Agda to do this? Like set theory axioms?

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.

For more background on HoTT see the HoTT book
https://homotopytypetheory.org/book/
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.

4) Is set theory replaced by Agda or is it to be defined/implemented in Agda?

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.

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.

Yes, any interesting formal system is always incomplete – in particular you cannot show the consistency of any type theory (e.g. Agda) in itself.

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.

6) Could I theoretically rebuild the Agda syntax and proof that Agda always terminates?

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.

Thorsten



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/645d5938/attachment.html>