theory "2016_ICMS_Experiments" imports Main (* Christoph Benzmüller, jointly with Dana Scott, July 2016 *) begin typedecl i (* Type for indiviuals *) consts fExistence:: "i\bool" ("E") (* Existence predicate *) abbreviation fNot:: "bool\bool" ("\<^bold>\") where "\<^bold>\\ \ \\" abbreviation fImplies:: "bool\bool\bool" (infixr "\<^bold>\" 49) where "\\<^bold>\\ \ \\\" abbreviation fForall:: "(i\bool)\bool" ("\<^bold>\") where "\<^bold>\\ \ \x. E(x)\\(x)" abbreviation fForallBinder:: "(i\bool)\bool" (binder "\<^bold>\" [8] 9) where "\<^bold>\x. \(x) \ \<^bold>\\" abbreviation fOr (infixr "\<^bold>\" 51) where "\\<^bold>\\ \ (\<^bold>\\)\<^bold>\\" abbreviation fAnd (infixr "\<^bold>\" 52) where "\\<^bold>\\ \ \<^bold>\(\<^bold>\\\<^bold>\\<^bold>\\)" abbreviation fEquiv (infixr "\<^bold>\" 50) where "\\<^bold>\\ \ (\\<^bold>\\)\<^bold>\(\\<^bold>\\)" abbreviation fExists ("\<^bold>\") where "\<^bold>\\ \ \<^bold>\(\<^bold>\(\y.\<^bold>\(\ y)))" abbreviation fExistsBinder (binder "\<^bold>\" [8]9) where "\<^bold>\x. \(x) \ \<^bold>\\" (* We now introduce the basic notions for category theory. *) consts domain:: "i\i" ("dom _" [108] 109) codomain:: "i\i" ("cod _" [110] 111) composition:: "i\i\i" (infix "\" 110) (* We now repeat our experiments from the ICMS paper and the email exchange with Freyd. These experiments studied Freyd's axiom system: Freyd's axioms for category theory A1: "\<^bold>E(x\y) \<^bold>\ ((x\) \ (\y))" A2a: "(\x)\ \ \x" A2b: "\(x\) \ x\" A3a: "(\x)\x \ x" A3b: "x\(x\) \ x" A4a: "\(x\y) \ \(x\(\y))" A4b: "(x\y)\ \ ((x\)\y)\" A5: "x\(y\z) \ (x\y)\z" We translate them here step-by-step into Scott's notation. The first thing is to reverse all x\y by y\x, to appropriately map their different order wrt. composition: A1: "\<^bold>E(y\x) \<^bold>\ ((x\) \ (\y))" A2a: "(\x)\ \ \x" A2b: "\(x\) \ x\" A3a: "x\(\x) \ x" A3b: "(x\)\x \ x" A4a: "\(y\x) \ \((\y)\x)" A4b: "(y\x)\ \ (y\(x\))\" A5: "(z\y)\x \ z\(y\x)" We rename the variables to get them in usual order: A1: "\<^bold>E(x\y) \<^bold>\ ((y\) \ (\x))" A2a: "(\x)\ \ \x" A2b: "\(x\) \ x\" A3a: "x\(\x) \ x" A3b: "(x\)\x \ x" A4a: "\(x\y) \ \((\x)\y)" A4b: "(x\y)\ \ (x\(y\))\" A5: "(x\y)\z \ x\(y\z)" We replace _\ by cod_ and \_ by dom_: A1: "\<^bold>E(x\y) \<^bold>\ ((cod y) \ (dom x))" A2a: "cod (dom x) \ dom x" A2b: "dom (cod x) \ cod x" A3a: "x\(dom x) \ x" A3b: "(cod x)\x \ x" A4a: "dom (x\y) \ dom ((dom x)\y)" A4b: "cod (x\y) \ cod (x\(cod y))" A5: "(x\y)\z \ x\(y\z)" Freyd's \ is symmetric, hence we get: We replace _\ by cod_ and \_ by dom_: A1: "\<^bold>E(x\y) \<^bold>\ ( (dom x) \ (cod y))" A2a: "cod (dom x) \ dom x" A2b: "dom (cod x) \ cod x" A3a: "x\(dom x) \ x" A3b: "(cod x)\x \ x" A4a: "dom (x\y) \ dom ((dom x)\y)" A4b: "cod (x\y) \ cod (x\(cod y))" A5: "(x\y)\z \ x\(y\z)" In an email, Dana Scott presented me his translation of Freyd's axioms in his own notation. Here is the copied text from his email (note that his versions coincides with the above): FREYD'S AXIOMS FOR A CATEGORY IN FREE LOGIC (Sott's notation) (A1) E(x o y) <==> dom(x) \ cod(y) (A2a) cod(dom(x)) \ dom(x) (A2b) dom(cod(x)) \ cod(x) (A3a) x o dom(x) \ x (A3b) cod(x) o x \ x (A4a) dom(x o y) \ dom(dom(x) o y) (A4b) cod(x o y) \ cod(x o cod(y)) (A5) x o (y o z) \ (x o y) o z *) (* My first interpretation of Freyd's equality (which is given informal in his textbook in 1.11) was "x \ y \ (E(x) \<^bold>\ E(y)) \<^bold>\ (x = y)". We denote this version of equality with "\". Freyd later told me via email that he intended Kleene equality instead; but see the experiments for Kleene equality below! *) abbreviation FreydEquality1:: "i\i\bool" (infix "\" 60) where "x \ y \ (E(x) \<^bold>\ E(y)) \<^bold>\ (x = y)" context (* Freyd_1: Freyd's axioms are consistent with "\" as equality; but note that the model generated by Nitpick identifies E with D, that is, in this model D-E is empty. *) assumes A1: "E(x\y) \<^bold>\ (dom x \ cod y)" and A2a: "cod (dom x) \ dom x" and A2b: "dom (cod x) \ cod x" and A3a: "x\(dom x) \ x" and A3b: "(cod x)\x \ x" and A4a: "dom(x\y) \ dom(dom(x)\y)" and A4b: "cod(x\y) \ cod(x\cod(y))" and A5: "x\(y\z) \ (x\y)\z" begin (* Nitpick does find a model; in this model D-E is empty. *) lemma True nitpick [satisfy, user_axioms, show_all, format = 2] oops end context (* Freyd_2: Freyd's axioms are redundant for "\" and non-empty D-E. This coincides with the results the results in our ICMS 2016 paper. *) assumes A1: "E(x\y) \<^bold>\ (dom x \ cod y)" and (* A2a: "cod (dom x) \ dom x" and *) A2b: "dom (cod x) \ cod x" and A3a: "x\(dom x) \ x" and A3b: "(cod x)\x \ x" and A4a: "dom(x\y) \ dom(dom(x)\y)" and A4b: "cod(x\y) \ cod(x\cod(y))" and A5: "x\(y\z) \ (x\y)\z" and NE: "\x. \<^bold>\(E(x))" (* Note that "\" is existence from the meta-logic, which ranges over D. *) begin lemma (*A2a*) "cod (dom x) \ dom x" by (metis A1 A2b A3b) end context (* Freyd_3: Freyd's axioms are even more redundant for "\" and non-empty D-E. This coincides with the results the results in our ICMS 2016 paper. *) assumes A1: "E(x\y) \<^bold>\ (dom x \ (cod y))" and A2a: "cod (dom x) \ dom x" and (* A2b: "dom (cod x) \ cod x" and *) A3a: "x\(dom x) \ x" and A3b: "(cod x)\x \ x" and (* A4a: "dom(x\y) \ dom(dom(x)\y)" and *) (* A4b: "cod(x\y) \ cod(x\cod(y))" and *) A5: "x\(y\z) \ (x\y)\z" and NE: "\x. \<^bold>\(E(x))" begin lemma (*A2b*) "dom (cod x) \ cod x" by (metis A1 A3a A2a) lemma (*A4a*) "dom(x\y) \ dom(dom(x)\y)" by (metis A1 A3a A2a) lemma (*A4b*) "cod(x\y) \ cod(x\cod(y))" by (metis A1 A3a A2a) end context (* Freyd_4: Freyd's axioms are inconsistent for "\" and non-empty D-E. This coincides with the results the results in our ICMS 2016 paper. *) assumes A1: "E(x\y) \<^bold>\ ((dom x) \ (cod y))" and A2a: "cod (dom x) \ dom x" and A2b: "dom (cod x) \ cod x" and A3a: "x\(dom x) \ x" and A3b: "(cod x)\x \ x" and A4a: "dom(x\y) \ dom(dom(x)\y)" and A4b: "cod(x\y) \ cod(x\cod(y))" and A5: "x\(y\z) \ (x\y)\z" and NE: "\x. \<^bold>\(E(x))" begin (* Nitpick does *not* find a model. *) lemma True nitpick [satisfy, user_axioms, show_all, format = 2] oops (* We can prove falsity. *) lemma False by (metis A1 A3a NE local.A2a) end (* Peter Freyd wrote me in an email, that he wants Kleene equality, which we denote as "\" below. Peter Freyd, email on June 15, 2016: "... To borrow your notation I would want: x \ y \ ((E x) v (E y)) => ((E x) \ (E y) \ (x = y))" Hence, We now introduce "\" and repeat the above experiments with it. *) abbreviation KleeneEquality_Freyd:: "i\i\bool" (infix "\" 60) where "x \ y \ (E x \<^bold>\ E y) \<^bold>\ (E x \<^bold>\ E y \<^bold>\ (x = y))" lemma ref: "x \ x" by simp lemma sym: "x \ y \<^bold>\ y \ x" by blast lemma tra: "(x \ y \<^bold>\ y \ z) \<^bold>\ x \ z" by blast context (* Freyd_5: Freyd's axioms are consistent for "\"; but note that the model generated by Nitpick identifies E with D, that is, in this model D-E is empty. *) assumes A1: "E(x\y) \<^bold>\ (dom x \ cod y)" and A2a: "cod (dom x) \ dom x" and A3a: "x\(dom x) \ x" and A3b: "(cod x)\x \ x" and A4a: "dom(x\y) \ dom(dom(x)\y)" and A5b: "cod(x\y) \ cod(x\cod(y))" and A5: "x\(y\z) \ (x\y)\z" begin (* nitpick does find a model *) lemma True nitpick [satisfy, user_axioms, show_all, format = 2] oops end context (* Freyd_6: Freyd's axioms are inconsistent for "\" and non-empty D-E. This seems very problematic for Freyd, doesn't it? *) assumes A1: "E(x\y) \<^bold>\ (dom x \ cod y)" and A2a: "cod (dom x) \ dom x" and A3a: "x\(dom x) \ x" and A3b: "(cod x)\x \ x" and A4a: "dom(x\y) \ dom(dom(x)\y)" and A5b: "cod(x\y) \ cod(x\cod(y))" and A5: "x\(y\z) \ (x\y)\z" and NE: "\x. \<^bold>\(E(x))" begin (* Nitpick does *not* find a model. *) lemma True nitpick [satisfy, user_axioms, show_all, format = 2] oops (* no model *) (* We can prove falsity. *) lemma False by (metis A1 A3a A2a NE) end context (* Freyd_7: Freyd's axioms are inconsistent for "\" and non-empty D-E. We present a detailed, intuitive proof. *) assumes A1: "E(x\y) \<^bold>\ (dom x \ cod y)" and A2a: "cod (dom x) \ dom x" and A3a: "x\(dom x) \ x" begin lemma Nonexistence_implies_Falsity: assumes "\x. \<^bold>\(E x)" (* We assume an undefined object, i.e. that D-E is non-empty. *) shows False (* We then prove falsity. *) proof - (* Let a be an undefined object *) obtain a where 1: "\<^bold>\(E a)" using assms by auto (* We instantiate axiom A3a with "a". *) have 2: "a\(dom a) \ a" using A3a by blast (* By unfolding the definition of "\" we get from L1 that "a\(dom a)" is not defined. This is easy to see, since if "a\(dom a)" were defined, we also had that "a" is defined, which is not the case by assumption. *) have 3: "\<^bold>\(E(a\(dom a)))" using 1 2 by blast (* We instantiate axiom A1 with "a" and "dom a". *) have 4: "E(a\(dom a)) \<^bold>\ dom a \ cod(dom a)" using A1 by blast (* We instantiate axiom A2a with "a". *) have 5: "cod(dom a) \ dom a" using A2a by blast (* We use L4 (and symmetry and transitivity of "\") to rewrite the right-hand of the equivalence L3 into into "dom a \ dom a". *) have 6: "E(a\(dom a)) \<^bold>\ dom a \ dom a" using 4 5 tra sym by blast (* By reflexivity of "\" we get that "a\(dom a)" must be defined. *) have 7: "E(a\(dom a))" using 6 ref by blast (* We have shown in L6 that "a\(dom a)" is defined, and in L2 that it is undefined. Contradiction. *) then show ?thesis using 7 3 by blast qed (* Hence: all objects must be defined in Freyd's theory (or we get inconsistency). *) lemma "\x. E(x)" using Nonexistence_implies_Falsity by auto end (* Dana Scott proposes a slightly different variant of axioms in his paper "Identity and Existence in Intuitionistic Logic (1977, published 1979)". In particular Scott distinguishes two notions of equality: (i) Kleene equality as also used by Freyd above (denoted here as "\<^bold>=\<^bold>="), and (ii) a weaker, non-reflexive notion of equality (denoted here as "\<^bold>="). Scott uses "\<^bold>=" in the axiom on existence of morphism compositions (A1 above, and S3 below) and "\<^bold>=\<^bold>=" in all other axioms. SCOTT'S AXIOMS FOR A CATEGORY IN FREE LOGIC (Scott's notation) (S1) Ex <==> Edom(x) (we actually only need right to left direction) (S2) Ex <==> Ecod(x) (we actually only need right to left direction) (S3) E(x o y) <==> dom(x) = cod(y) (S4) x o (y o z) == (x o y) o z (S5) x o dom(x) == x (S6) cod(x) o x == x *) (* Non-bold "=" is identity on the raw domain D. Bold-face "\<^bold>=" is weak, non-reflexive identity on E. Bold-face "\<^bold>=\<^bold>=" is Kleene equality. *) abbreviation eq1 (infixr "\<^bold>=" 56) where "x \<^bold>= y \ (E(x) \<^bold>\ E(y) \<^bold>\ (x = y))" abbreviation eq2 (infixr "\<^bold>=\<^bold>=" 56) where "x \<^bold>=\<^bold>= y \ ((E(x) \<^bold>\ E(y)) \<^bold>\ (x\<^bold>=y))" (* We prove some properties of "=", "\<^bold>=" and "\<^bold>=\<^bold>=" *) lemma "x \<^bold>= y \<^bold>\ ((x = y) \<^bold>\ E(x))" by simp lemma "x \<^bold>= y \<^bold>\ ((x = y) \<^bold>\ E(y))" by simp lemma "x \<^bold>=\<^bold>= y \<^bold>\ ((x \<^bold>= y) \<^bold>\ (\<^bold>\(E(x)) \<^bold>\ \<^bold>\(E(y))))" by auto (* "\<^bold>=" is an equivalence relation on E *) lemma "\<^bold>\x. (x \<^bold>= x)" by simp lemma "\<^bold>\x y. (x \<^bold>= y) \<^bold>\ (y \<^bold>= x)" by simp lemma "\<^bold>\x y z. ((x \<^bold>= y) \<^bold>\ (y \<^bold>= z)) \<^bold>\ (x \<^bold>= z)" by simp (* Reflexivity fails on D for "\<^bold>=" , i.e. "\<^bold>=" is only a partial equivalence rel on D *) lemma "(x \<^bold>= x)" nitpick [user_axioms, show_all] oops (* countermodel *) lemma "(x \<^bold>= y) \<^bold>\ (y \<^bold>= x)" by auto lemma "((x \<^bold>= y) \<^bold>\ (y \<^bold>= z)) \<^bold>\ (x \<^bold>= z)" by simp (* "\<^bold>=\<^bold>=" is an equivalence relation on E *) lemma "\<^bold>\x. (x \<^bold>=\<^bold>= x)" by simp lemma "\<^bold>\x y. (x \<^bold>=\<^bold>= y) \<^bold>\ (y \<^bold>=\<^bold>= x)" by simp lemma "\<^bold>\x y z. ((x \<^bold>=\<^bold>= y) \<^bold>\ (y \<^bold>=\<^bold>= z)) \<^bold>\ (x \<^bold>=\<^bold>= z)" by simp (* "\<^bold>=\<^bold>=" is also an equivalence relation on D, i.e. "\<^bold>=\<^bold>=" is a total equivalence rel on D *) lemma "(x \<^bold>=\<^bold>= x)" by simp lemma "(x \<^bold>=\<^bold>= y) \<^bold>\ (y \<^bold>=\<^bold>= x)" by auto lemma "((x \<^bold>=\<^bold>= y) \<^bold>\ (y \<^bold>=\<^bold>= z)) \<^bold>\ (x \<^bold>=\<^bold>= z)" by auto (* If elements of D-E are not important, then we need say nothing about them, for example: *) lemma "(\<^bold>\(E(x\y)) \<^bold>\ \<^bold>\(E(u\v))) \<^bold>\ ((x\y) \<^bold>=\<^bold>= (u\v))" by simp (* But there is no reason to assume (non-bold "=" is raw identity on D): *) lemma "(\<^bold>\(E(x\y)) \<^bold>\ \<^bold>\(E(u\v))) \<^bold>\ ((x\y) = (u\v))" nitpick [user_axioms, show_all] oops (* countermodel *) context (* Scott_1: We get consistency for Scott's axioms for "\<^bold>=" in S3. *) assumes S1: "E(dom x) \<^bold>\ E(x)" and S2: "E(cod x) \<^bold>\ E(x)" and S3: "E(x\y) \<^bold>\ (dom x \<^bold>= cod y)" and S4: "x\(y\z) \<^bold>=\<^bold>= (x\y)\z" and S5: "x\(dom x) \<^bold>=\<^bold>= x" and S6: "(cod x)\x \<^bold>=\<^bold>= x" begin (* Nitpick does find a model *) lemma True nitpick [satisfy, user_axioms, show_all, format = 2] oops end context (* Scott_2: We additionally assume that D-E is nonempty (i.e. "\x. \<^bold>\(E(x))" holds, for "\" ranging over V); we still get consistency. That is what we want! *) assumes S1: "E(dom x) \<^bold>\ E(x)" and S2: "E(cod x) \<^bold>\ E(x)" and S3: "E(x\y) \<^bold>\ (dom x \<^bold>= cod y)" and S4: "x\(y\z) \<^bold>=\<^bold>= (x\y)\z" and S5: "x\(dom x) \<^bold>=\<^bold>= x" and S6: "(cod x)\x \<^bold>=\<^bold>= x" and ex: "\x. \<^bold>\(E(x))" begin (* Nitpick does find a model *) lemma True nitpick [satisfy, user_axioms, show_all, format = 2] oops end (* Finally, we repeat the central inconsistency argument again in Freyd's original notation *) consts source:: "i\i" ("\_" [108] 109) target:: "i\i" ("_\" [110] 111) (* composition:: "i\i\i" (infix "\" 110) *) context (* Freyd_8: Freyd's axioms are inconsistent for "\" and non-empty D-E. We present a detailed, intuitive proof. *) assumes A1: "E(x\y) \<^bold>\ (x\ \ \y)" and A2a: "((\x)\) \ \x" and A2b: "\(x\) \ \x" and A3a: "(\x)\x \ x" and A3b: "x\(x\) \ x" and A4a: "\(x\y) \ \(x\(\y))" and A4b: "(x\y)\ \ ((x\)\y)\" and A5: "x\(y\z) \ (x\y)\z" begin (* Nitpick does find a model; in this model D-E is empty. *) lemma True nitpick [satisfy, user_axioms, show_all, format = 2] oops lemma Nonexistence_implies_Falsity_2: assumes "\x. \<^bold>\(E x)" (* We assume an undefined object, i.e. that D-E is non-empty. *) shows False (* We then prove falsity. *) using A1 A2a A3a assms by blast lemma Nonexistence_implies_Falsity_3: assumes "\x. \<^bold>\(E x)" (* We assume an undefined object, i.e. that D-E is non-empty. *) shows False (* We then prove falsity. *) proof - (* Let a be an undefined object *) obtain a where 1: "\<^bold>\(E a)" using assms by auto (* We instantiate axiom A3a with "a". *) have 2: "(\a)\a \ a" using A3a by blast (* By unfolding the definition of "\" we get from 1 that "(\a)\a)" is not defined. This is easy to see, since if "(\a)\a)" were defined, we also had that "a" is defined, which is not the case by assumption. *) have 3: "\<^bold>\(E((\a)\a))" using 1 2 by blast (* We instantiate axiom A1 with "(\a)" and "a". *) have 4: "E((\a)\a) \<^bold>\ (\a)\ \ \a" using A1 by blast (* We instantiate axiom A2a with "a". *) have 5: "(\a)\ \ \a" using A2a by blast (* We use 4 (and symmetry and transitivity of "\") to rewrite the right-hand of the equivalence 3 into into "\a \ \a". *) have 6: "E((\a)\a)" using 4 5 by blast (* We have "\<^bold>\(E((\a)\a))" and "\<^bold>(E((\a)\a))", hence Falsity. *) then show ?thesis using 6 3 by blast qed lemma "\x. E(x)" using Nonexistence_implies_Falsity_3 by auto lemma Nonexistence_implies_Falsity_4: assumes "\x. \<^bold>\(E x)" (* We assume an undefined object, i.e. that D-E is non-empty. *) shows False (* We then prove falsity. *) proof - (* Let a be an undefined object *) obtain a where 1: "\<^bold>\(E a)" using assms by auto (* We instantiate axiom A3a with "a". *) have 2: "(\a)\a \ a" using A3a by blast (* By unfolding the definition of "\" we get from L1 that "(\a)\a)" is not defined. This is easy to see, since if "(\a)\a)" were defined, we also had that "a" is defined, which is not the case by assumption. *) have 3: "\<^bold>\(E((\a)\a))" using 1 2 by blast (* We instantiate axiom A1 with "a" and "dom a". *) have 4: "E((\a)\a) \<^bold>\ (\a)\ \ \a" using A1 by blast (* We instantiate axiom A2a with "a". *) have 5: "(\a)\ \ \a" using A2a by blast (* We use L4 (and symmetry and transitivity of "\") to rewrite the right-hand of the equivalence L3 into into "\a \ \a". *) have 6: "E((\a)\a) \<^bold>\ \a \ \a" using 4 5 tra sym by blast (* By reflexivity of "\" we get that "a\(dom a)" must be defined. *) have 7: "E((\a)\a)" using 6 ref by blast (* We have shown in L6 that "a\(dom a)" is defined, and in L2 that it is undefined. Contradiction. *) then show ?thesis using 7 3 by blast qed end context (* Scott_in_Frey_Notation: We study Scott's axioms in Freyd's notation. *) assumes S1: "E(\x) \<^bold>\ E(x)" and S2: "E(x\) \<^bold>\ E(x)" and S3: "E(x\y) \<^bold>\ (x\ \<^bold>= \y)" and S4: "x\(y\z) \<^bold>=\<^bold>= (x\y)\z" and S5: "(\x)\x \<^bold>=\<^bold>= x" and S6: "x\(x\) \<^bold>=\<^bold>= x" begin (* Nitpick does find a model *) lemma True nitpick [satisfy, user_axioms, show_all, format = 2] oops lemma Nonexistence_implies_Falsity_1: assumes "\x. \<^bold>\(E x)" (* We assume an undefined object, i.e. that D-E is non-empty. *) shows False (* We then try to prove falsity. Nitpick finds a countermodel. *) nitpick [user_axioms, show_all, format = 2, expect = genuine] oops (* Countermodel *) lemma Another_Test: assumes "(\x. \<^bold>\(E x)) \<^bold>\ (\x. (E x))" (* We assume an undefined object, i.e. that D-E is non-empty. *) shows False (* We then try to prove falsity. Nitpick finds a countermodel. *) nitpick [user_axioms, show_all, format = 2, expect = genuine] oops (* Countermodel *) end end