The No Counterexample Interpretation (NCI) and other proof-theoretic techniques are applied to a proof of the Infinite Ramsey Theorem. A parametric form of Ramsey's theorem is obtained, that implies the Infinite, the Finite and the Paris-Harrington versions of Ramsey's Theorem. Applications of the proof theory of fragments of PA and of Linear Logic are suggested. This work was a preliminary experiment for the implementation of the NCI in Ketonen's Proof Checker EKL.
Ramsey Interpreted: A Parametric Version of Ramsey's Theorem
BELLIN, Gianluigi
1990-01-01
Abstract
The No Counterexample Interpretation (NCI) and other proof-theoretic techniques are applied to a proof of the Infinite Ramsey Theorem. A parametric form of Ramsey's theorem is obtained, that implies the Infinite, the Finite and the Paris-Harrington versions of Ramsey's Theorem. Applications of the proof theory of fragments of PA and of Linear Logic are suggested. This work was a preliminary experiment for the implementation of the NCI in Ketonen's Proof Checker EKL.
File in questo prodotto:
| File | Dimensione | Formato | |
|---|---|---|---|
|
RamesyInterpreted.pdf
accesso aperto
Tipologia:
Documento in Post-print
Licenza:
Dominio pubblico
Dimensione
1.93 MB
Formato
Adobe PDF
|
1.93 MB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
