[Agda] Questions about logic
Sergei Meshveliani
mechvel at botik.ru
Sat Oct 6 15:30:51 CEST 2018
On Sat, 2018-10-06 at 13:42 +0200, Jesper Cockx wrote:
> 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.
This leads to a great misunderstanding among people, so that they fear
of intuitionism.
> 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).
Thank you.
Currently I think of this this way.
Computer algebra methods rely on many decidable relations.
_≡_ and _<_ are decidable on Nat and Integer.
If A has DecTotalOrder for _<_, then (List A) had DecTotalOrder order
for lexicographic extension of _<_.
If A has CommutativeRing and decidable equality _≈_, then the polynomial
domain A[x] over A has CommutativeRing and a decidable equality _=p_.
And so on. And excluded middle in Agda programs works there for these
particular relation instances.
There remains a certain esoteric area, like (may be) semi-algorithms for
real numbers. But this probably relates to very different methods.
Regards,
------
Sergei
>
> 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
>
>
More information about the Agda
mailing list