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\