[Agda] Ramsey theorem

[Danko Ilik]

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)

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.

Danko

-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 473 bytes
Desc: This is a digitally signed message part
Url : http://lists.chalmers.se/pipermail/agda/attachments/20140708/67b1e8a0/attachment.bin