Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Boolos's Curious Inference (Speed-Up) in Isabe...


view this post on Zulip Email Gateway (Feb 10 2021 at 10:10):

From: Jeffrey Ketland <jeffreyketland@gmail.com>
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@gmail.com

view this post on Zulip Email Gateway (Feb 10 2021 at 13:40):

From: Jakub Kądziołka <kuba@kadziolka.net>
You might want to consider publishing it in the AFP:
https://www.isa-afp.org/

The submission process is quite straightforward, and that way others
will be able to find your formalization much easier.

Regards,
Jakub Kądziołka


Last updated: Sep 25 2021 at 10:20 UTC