[Agda] Questions about logic

[Sergei Meshveliani]

On Sat, 2018-10-06 at 11:14 +0200, Jesper Cockx wrote:
> Hi Silvio,
> [..]
> 
> Agda is based on Martin-Löf type theory, 
> [..]
> Of course, Agda is an intuitionistic logic so you do not have the law
> of the excluded (not the included btw) middle or the axiom of choice,
> so you may want to postulate these. However, if you haven't done any
> intuitionistic logic before you may be surprised how far you can get
> without them :)
> [..]


I am not a specialist in logic, but I apply Agda to programming algebra.

Let specialists correct me if I write wrong things below.

First I was surprised of how much is possible to compute and prove by
using an intuitionistic logic of Agda. Then I looked into my programs by
new and discovered that they often rely on the law of excluded middle!
But not for the general case, only for the case when a relation P is
decidable
(this is like to discover that one is writing prose).

For example, sorting algorithm for  List A  relies on a decidable
comparison _<=?_ on A, and has a branch

  case x <=? y of \ { (yes _) -> ...
                    ; (no _)  -> ... }

I think this relies on excluded middle for _<=_.
Right?

And a great part of computer algebra is done by applying excluding
middle to decidable relations.

I guess most mathematicians would think that almost nothing can be
computed or proved in languages like Agda -- because ``excluded middle
is forbidden''.
And in practice, almost all can be computed/proved there, because
excluded middle is valid for decidable relations
Do I mistake about this validity of excluded middle?

Regards,

------
Sergei

> 
> On Sat, Oct 6, 2018 at 8:25 AM Silvio Frischknecht
> <silvio.frischi at gmail.com> 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
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda