[Agda] Ramsey theorem

[Sergei Meshveliani]

On Tue, 2014-07-08 at 08:42 +0200, Danko Ilik wrote:
> Hi,
> 
> If you are looking at Kruskal's Theorem, or its special case Higman's
> Lemma, the following two papers are comprehensive studies, including
> Nash-Williams' argument:
> 
> - Jean H. Gallier: What’s so special about Kruskal’s theorem and the
> ordinal \Gamma_0 A survey of some results in proof theory. Annals of
> Pure and Applied Logic 53 (1991) 199-260
> 
> - Wim Veldman: An intuitionistic proof of Kruskal’s theorem. Arch. Math.
> Logic 43, 215–264 (2004)
> 


Thank you very much, Danko.

In Gallier's paper I see the proof for Higman's lemma that does not use
Ramsey's theorem. So that Higman's lemma can, probably, be considered as
`simplest/basic' in the considered field. 
I am going to look into this.


> Concerning formalization in Agda, and developing a constructive version
> of a classical argument, you should know that the classical proofs not
> only use classical logic but also a choice axiom. One might get away
> with a restricted version of Law of Excluded Middle, to purely
> existential formulas, but a choice axiom will be needed. I am not sure
> whether the type theory of Agda is strong enough to formalize the
> argument. It does prove Choice, but not in presence of (restricted) LEM.
> If not, that would nevertheless not mean that the proof can not be made
> constructively.
> 
> One sufficient form of choice axiom is the Open Induction Principle.
> This I believe is constructive for Cantor Space, but I would not know
> how to prove it in Agda. Assuming it as an axiom might give you a nice
> way to prove Kruskal or Higman.

See the  .ps  file on the Web for 
    "A proof of Higman's lemma by structural induction"
    by Coquand & Fridlender

I expect that it is proved in Coq, and need to see what it will be with
Agda.

Regards,

------
Sergei