A Ramsey theorem in Boyer-Moore logic

DOI10.1007/BF00881917zbMath0836.03031MaRDI QIDQ1904403

Kenneth Kunen

Publication date: 20 December 1995

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

zbMATH Keywords

ordinalprimitive recursive arithmeticBoyer-Moore proverNqthmParis-Harrington version of Ramsey's theorem

Mathematics Subject Classification ID

First-order arithmetic and fragments (03F30) Software, source code, etc. for problems pertaining to mathematical logic and foundations (03-04)

Related Items (5)

On the metamathematics of the P vs. NP question ⋮ Informal versus formal mathematics ⋮ A formalised theorem in the partition calculus ⋮ Computer theorem proving in mathematics ⋮ Some thoughts on hypercomputation

Uses Software

• Nuprl
• NQTHM

Cites Work

• Rapidly growing Ramsey functions
• The consistency of arithmetics
• Unnamed Item
• Unnamed Item

This page was built for publication: A Ramsey theorem in Boyer-Moore logic