Ketland, Jeffrey (2022) Boolos’s Curious Inference in Isabelle/HOL. Archive of Formal Proofs.

Preview

Text Boolos_Inference_Isabelle_2022.pdf Download (411kB) | Preview

Abstract

In 1987, George Boolos gave an interesting and vivid concrete example
of the considerable speed-up afforded by higher-order logic over
first-order logic. (A phenomenon first noted by Kurt Gödel in 1936.)
Boolos’s example concerned an inference I with five premises, and a
conclusion, such that the shortest derivation of the conclusion from
the premises in a standard system for first-order logic is astronomically
huge; while there exists a second-order derivation whose length
is of the order of a page or two. Boolos gave a short sketch of that
second-order derivation, which relies on the comprehension principle
of second-order logic. Here, Boolos’s inference is formalized into fourteen
lemmas, each quickly verified by the automated-theorem-proving
assistant Isabelle/HOL.

---

Export/Citation:

EndNote | BibTeX | Dublin Core | ASCII/Text Citation (Chicago) | HTML Citation | OpenURL

Social Networking:

Share |

---

Item Type:	Published Article or Volume
Creators:	Creators Email ORCID Ketland, Jeffrey jeffreyketland@gmail.com 0000-0002-5128-4387
Subjects:	Specific Sciences > Mathematics > Foundations Specific Sciences > Mathematics > Logic Specific Sciences > Computer Science
Depositing User:	Dr Jeffrey Ketland
Date Deposited:	07 Jul 2022 16:40
Last Modified:	07 Jul 2022 16:40
Item ID:	20849
Journal or Publication Title:	Archive of Formal Proofs
Official URL:	https://www.isa-afp.org/entries/Boolos_Curious_Inf...
Subjects:	Specific Sciences > Mathematics > Foundations Specific Sciences > Mathematics > Logic Specific Sciences > Computer Science
Date:	4 July 2022
URI:	https://philsci-archive.pitt.edu/id/eprint/20849

Monthly Views for the past 3 years

Monthly Downloads for the past 3 years

Plum Analytics

Actions (login required)

View Item