[Agda] Questions about logic

[Jesper Cockx]

Hi Sergei,

I think the confusion comes from people misinterpreting "Agda doesn't have
the excluded middle": it means that *in general* we don't have "A or not A"
for an arbitrary type/proposition A, but there are still many specific A's
for which we can prove this fact (i.e. the *decidable* types/propositions).
So in some sense you are relying on the excluded middle for <=, but not
really since excluded middle for <= is provable (so it doesn't require any
axioms). I think it is common in intuitionistic mathematics to only talk
about the 'excluded middle' when it is used for types for which it is not
provable, for example equality of two types.

-- Jesper

On Sat, Oct 6, 2018 at 1:18 PM Sergei Meshveliani <mechvel at botik.ru> wrote:

> 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
>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20181006/ec1304df/attachment.html>