[Agda] Questions about logic

[Silvio Frischknecht]

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

[Henning Basold]

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

Post by Silvio Frischknecht
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
https://lists.chalmers.se/mailman/listinfo/agda

[Ambrus Kaposi]

Post by Henning Basold
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?).

Here is a formalisation:
https://bitbucket.org/akaposi/tt-in-tt/src/HEAD/STT/MinimalLogic.agda

[Thorsten Altenkirch]

On 06/10/2018, 09:15, "Agda on behalf of Henning Basold" <agda-***@lists.chalmers.se<mailto:agda-***@lists.chalmers.se> on behalf of ***@basold.eu<mailto:***@basold.eu>> wrote:

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

You need to be a bit careful here.

As long as you leave out \/ and False (and also negation), then the completeness proof for propositioal logic is straightforward. However, if you include those it gets a bit more tricky and you need to exploit the decidability of propositional logic.

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

No it is not. At least not if you include \/,False,exists. Actually completeness of FOL wrt Kripke models is known to be equivalent to Markov's principle.

This can be fixed but basically Kripke models are not the right semantics for intuitionistic logic. You need something what I call Beth models, which extends Kripke models with a notion of covering of a world. While Kripke models corresponds to presheaves, Beth models correspond to sheaves.

See for example: http://www.cs.nott.ac.uk/~psztxa/talks/nbe09.pdf

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
***@lists.chalmers.se<mailto:***@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-----
_______________________________________________
Agda mailing list
***@lists.chalmers.se<mailto:***@lists.chalmers.se>
https://lists.chalmers.se/mailman/listinfo/agda




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.

[Jesper Cockx]

Hi Silvio,

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?

Agda is based on Martin-Löf type theory, which can be thought of as a
replacement for both logic and set theory of usual mathematics (since types
serve a dual role as both propositions and 'sets'). Type theory does not
rely on axioms like set theory but rather on pairs of
introduction/elimination rules, so for most tasks you do not need to add
any axioms to Agda. 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 :)

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

always terminates?

Agda is quite a large language and so hasn't been given a fully formal
semantics or a proof of termination (yet). However, there have been some
attempts at formalizing and proving correct some parts of Agda (I recently
wrote a blog post
<https://jesper.sikanda.be/posts/elaborating-dependent-copattern-matching.html>
about one of these). And of course, the basis of Agda is MLTT which has
been given many different proofs of normalization, so if you restrict
yourself to a sufficiently small fragment of Agda it may be possible to
reuse one of those.

I hope that helps!

-- Jesper

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
https://lists.chalmers.se/mailman/listinfo/agda

[Sergei Meshveliani]

Post by Jesper Cockx
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

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

[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

Post by Sergei Meshveliani

Post by Jesper Cockx
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

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

[Sergei Meshveliani]

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

Post by Jesper Cockx
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

Post by Jesper Cockx
of the excluded (not the included btw) middle or the axiom

of choice,

Post by Jesper Cockx
so you may want to postulate these. However, if you haven't

done any

Post by Jesper Cockx
intuitionistic logic before you may be surprised how far you

can get

Post by Jesper Cockx
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

Post by Jesper Cockx
On Sat, Oct 6, 2018 at 8:25 AM Silvio Frischknecht
Hello,
I am trying to learn some logic. Currently reading

"A

Post by Jesper Cockx
Mathematical Introduction to Logic" by Enderton. I

find it

Post by Jesper Cockx
hard to keep track of what can be done/assumed to be

true in

Post by Jesper Cockx
the metamathematic. I also find it hard to keep

track of all

Post by Jesper Cockx
the implicit things like models. I was wondering if

it's

Post by Jesper Cockx
possible to reproduce these results with Agda as
metamathematical system.
I found a paper that proved the completeness theorem

for

Post by Jesper Cockx
propositional logic.

https://akaposi.github.io/proplogic.pdf

Post by Jesper Cockx
Correct me if I'm wrong, but it seems like this

might be

Post by Jesper Cockx
easier than the completness theorem for first-order

logic

Post by Jesper Cockx
because it deals with finite things.
My questions are these.
1) Can Agda prove the completeness theorem of first

order

Post by Jesper Cockx
logic?
2) Can Agda prove the two incompleteness theorems?
3) Do I need some additional tools/axioms that I can

postulate

Post by Jesper Cockx
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

Post by Jesper Cockx
at some point the incompleteness theorem will kick

in. Also

Post by Jesper Cockx
popular opinion seems to suggest that the

constructivist view

Post by Jesper Cockx
can not deal with the law of included middle or the

axiom of

Post by Jesper Cockx
choice.
6) Could I theoretically rebuild the Agda syntax and

proof

Post by Jesper Cockx
that Agda always terminates?
Cheers
Silvio
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

[Peter Hancock]

Post by Silvio Frischknecht
My questions are these.
1) Can Agda prove the completeness theorem of first order logic?

I'm not 100% sure, but I think so. There is a very clever and fascinating paper by
Hugo Herbelin and Dank Ilik called
"An analysis of the constructive content of Henkin’s proof of
Gödel’s completeness theorem"
eg at https://pdfs.semanticscholar.org/62d8/86aac9b6cc466cb1c9d7f008f15d3e1e891e.pdf
I believe this has actually been carried out in Coq, with an ocaml program extracted.

But it has to be said it may not be appropriate if you just want to learn some
basic logic.

Post by Silvio Frischknecht
2) Can Agda prove the two incompleteness theorems?

I should think so. Some masochist may already have done it.
Arithmeticising the syntax will inevitably be very "sweaty".
There is I think a complete formalisation of at least the
first incompleteness theorem in some version of Isabelle.

Cheers

Peter Hancock

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

[Silvio Frischknecht]

Thanks for all the responses. It's probably going to take me some time
to digest :)

Silvio