[Agda] Questions about logic

[Peter Hancock]

On 05/10/2018 18:33, Silvio Frischknecht wrote:
> 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. 

> 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