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 等数据库收录! |
|