*To*: isabelle-users at cl.cam.ac.uk*Subject*: [isabelle] Boolos's Curious Inference (Speed-Up) in Isabelle/HOL*From*: Jeffrey Ketland <jeffreyketland at gmail.com>*Date*: Wed, 10 Feb 2021 02:20:49 +0000

I thought I might pass on this Isabelle/HOL formalization of Boolos’s "curious inference” to Isabelle users. In 1987, George Boolos gave an inference I, which is valid in first-order logic, but he noted that its shortest derivation, for the system he considered, is gigantc — e.g., it has at least 2^{2^{2^{…..^2}…..}}} symbols, where there are 65,536 iterations of exponentiation. The inference I is: A1: "F(x, e) = s(e)" A2: "F(e, s(y)) = s(s(F(e, y)))" A3: "F(s(x), s(y)) = F(x, F(s(x), y))" A4: "D(e)" A5: "D(x) ⟶ D(s(x))” ---------------------- Therefore: "D(F(s(s(s(s(e)))), s(s(s(s(e))))))” Though this is formalized, one might think of “e” as 1, and “s” as the successor operation, and “F” as an Ackermann-like function which grows very rapidly. Then A4 and A5 say that the set denoted by “D” is inductive. We want to prove that the number F(s(s(s(s(e)))), s(s(s(s(e))))) is in the set D. However, this number is gigantic, and the size of the required derivation in then gigantic too. Roughly, the first-order derivation has to reduce the term "F(s(s(s(s(e)))), s(s(s(s(e)))))” to a successor term (a numeral), F(s(s(s(s(e)))), s(s(s(s(e))))) = s(s(s( ….. (s (e))….))) But this is going to require a gigantic number of s’s! At least an exponential stack of 2, of height 65,536. Boolos pointed out that there is a reasonably short second-order logic derivation, which would fit in a few pages, if fully formalized. This is an example of “speed-up”, an idea first noticed by Kurt Gödel in 1936. Boolos called this a “curious inference”. [1] Boolos, G. 1987: “A Curious Inference”. Journal of Philosophical Logic. https://www.jstor.org/stable/30226368?seq=1#metadata_info_tab_contents I decided to see if I can put this into Isabelle/HOL and see if it can find the second-order derivation, so long as I used the right definitions. The main definition needed is: "N = {x. (∀Y. (induct Y ⟶ x ∈ Y))}”, where a set is called “inductive” if it contains e and is closed under s. So, N is “the intersection of all inductive sets”. The main idea of the second-order proof is to show, by a double induction, that if x and y are in N, then F(x, y) is also in N. It’s easy to show s(s(s(s(e)))) is in N. So, we conclude F(s(s(s(s(e)))), s(s(s(s(e))))) is also in N. And since it’s easy to show, by induction, that N is a subset of D, it follows that F(s(s(s(s(e)))), s(s(s(s(e))))) is in D, which is the conclusion. With some definitions and some coaxing, Isabelle finds the component derivations. I used 14 lemmas to get the final conclusion. I didn’t realise this until yesterday, but I noticed the Boolos inference has also been put into MIZAR and OMEGA in 2007, [2] Benzmüller, C. & Brown, C. 2007: “The curious inference of Boolos in MIZAR and OMEGA”, In Roman Matuszewski & Anna Zalewska (eds.), From Insight to Proof -- Festschrift in Honour of Andrzej Trybulec. The University of Bialystok, Poland. pp. 299-388 (2007) http://mizar.org/trybulec65/20.pdf Since the Isabelle/HOL proof sketch is pretty short, I thought I’d post it here. ————— theory Boolos imports Main begin text ‹Boolos's inference› locale bool_ax = fixes F :: "'a × 'a ⇒ 'a" fixes s :: "'a ⇒ 'a" fixes D :: "'a ⇒ bool" fixes e :: "'a" assumes A1: "F(x, e) = s(e)" and A2: "F(e, s(y)) = s(s(F(e, y)))" and A3: "F(s(x), s(y)) = F(x, F(s(x), y))" and A4: "D(e)" and A5: "D(x) ⟶ D(s(x))" context bool_ax begin definition (in bool_ax) induct :: "'a set ⇒ bool" where "induct X ≡ e ∈ X ∧ (∀x. (x ∈ X ⟶ s(x) ∈ X))" definition (in bool_ax) N :: "'a set" where "N = {x. (∀Y. (induct Y ⟶ x ∈ Y))}" definition (in bool_ax) P1 :: "'a ⇒ 'a ⇒ bool" where "P1 x y ≡ F(x,y) ∈ N" definition (in bool_ax) P2 :: "'a ⇒ bool" where "P2 x ≡ N ⊆ {y. P1 x y}" lemma lem1: "induct X ⟶ N ⊆ X" using N_def by auto lemma lem2: "induct N" by (simp add: N_def induct_def) lemma lem3: "induct {x. D(x)}" using A4 A5 induct_def by auto lemma lem4: "s(s(s(s(e)))) ∈ N" using induct_def lem2 by auto lemma lem5: "P1 e e" using A1 P1_def induct_def lem2 by auto lemma lem6: "P1 e x ⟶ P1 e (s(x))" using A2 P1_def induct_def lem2 by auto lemma lem7: "induct {x. P1 e x}" using induct_def lem5 lem6 by auto lemma lem8: "P1 (s(x)) e" using A1 P1_def induct_def lem2 by auto lemma lem9: "P2 e" by (simp add: P2_def lem1 lem7) lemma lem10: "P2 x ⟶ (∀y. (P1 (s(x)) y ⟶ P1 (s(x)) (s(y))))" using A3 P1_def P2_def by auto lemma lem11: "P2 x ⟶ P2 (s(x))" using P2_def induct_def lem1 lem8 lem10 by auto lemma lem12: "induct {x. P2 x}" using induct_def lem9 lem11 by auto lemma lem13: "x ∈ N ∧ y ∈ N ⟶ F(x,y) ∈ N" using N_def P1_def P2_def lem12 by auto lemma lem14: "D(F(s(s(s(s(e)))), s(s(s(s(e))))))" using N_def lem3 lem4 lem13 by auto end Best regards, Jeff Ketland ———————— Dr Jeffrey Ketland Institute of Philosophy University of Warsaw jeffreyketland at gmail.com

**Follow-Ups**:**Re: [isabelle] Boolos's Curious Inference (Speed-Up) in Isabelle/HOL***From:*Jakub Kądziołka

- Previous by Date: Re: [isabelle] Comparing Isabelle/Scala with scala-isabelle. Was: Isabelle code for getting in-memory representation (abstract syntax trees) for complete theory file (tree of loaded theories)
- Next by Date: Re: [isabelle] Boolos's Curious Inference (Speed-Up) in Isabelle/HOL
- Previous by Thread: [isabelle] 21st Midlands Graduate School in the Foundations of Computing Science: Call for Participation
- Next by Thread: Re: [isabelle] Boolos's Curious Inference (Speed-Up) in Isabelle/HOL
- Cl-isabelle-users February 2021 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list