The curious inference of Boolos in MIZAR and OMEGA
Christoph Benzmüller, Chad E. Brown · 2007
We examine Boolos’ curious inference and formalize it in a system based on set theory (Mizar) and a system based on classical higher-order logic (OMEGA). The Boolos example is interesting because while it can in principle be proven using a complete first-order calculus, it is impractical to do so. In our case study we are interested in aspects such as how natural and at what level of granularity Boolos’ short second-order proof sketch can be formalized in Mizar and OMEGA.