A Ramsey theorem in Boyer-Moore logic |
| |
| Authors: | Kenneth Kunen |
| |
| Affiliation: | (1) University of Wisconsin, 53706 Madison, WI, USA |
| |
| Abstract: | We use the Boyer-Moore Prover, Nqthm, to verify the Paris-Harrington version of Ramsey's theorem. The proof we verify is a modification of the one given by Ketonen and Solovay. The theorem is not provable in Peano Arithmetic, and one key step in the proof requires  0 induction.Author supported by NSF Grant DMS-9100665. |
| |
| Keywords: | Nqthm Ramsey's theorem ordinal primitive recursive arithmetic |
| 本文献已被 SpringerLink 等数据库收录！ |
|
