|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% (find-angg "LATEX/istanbul-handouts.tex")
% (find-angg "LATEX/istanbul-handouts.lua")
% (defun c () (interactive) (find-LATEXsh "lualatex istanbul-handouts.tex"))
% (defun c () (interactive) (find-LATEXsh "lualatex --output-format=dvi istanbul-handouts.tex"))
% (defun d () (interactive) (find-xpdfpage "~/LATEX/istanbul-handouts.pdf"))
% (defun d () (interactive) (find-xdvipage "~/LATEX/istanbul-handouts.dvi"))
% (defun e () (interactive) (find-LATEX "istanbul-handouts.tex"))
% (defun l () (interactive) (find-LATEX "istanbul-handouts.lua"))
% (find-xpdfpage "~/LATEX/istanbul-handouts.pdf")
% (find-xdvipage "~/LATEX/istanbul-handouts.dvi")
% «.mixedpicture-tests» (to "mixedpicture-tests")
% «.sandwich» (to "sandwich")
% «.J-and-connectives» (to "J-and-connectives")
% «.J-proofs» (to "J-proofs")
% «.HAs-and-CCCs» (to "HAs-and-CCCs")
% «.brute-force» (to "brute-force")
\documentclass[oneside]{book}
% (find-angg ".emacs.papers" "latexgeom")
\usepackage[a4paper, landscape, top=1cm, left=1cm]{geometry}
\usepackage[utf8]{inputenc}
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{pict2e}
\usepackage{tikz}
\usepackage{luacode}
\usepackage[colorlinks]{hyperref} % (find-es "tex" "hyperref")
% (find-dn5file "preamble6.lua" "preamble0 =")
\usepackage{proof} % For derivation trees ("%:" lines)
\input diagxy % For 2D diagrams ("%D" lines)
\xyoption{curve} % For the ".curve=" feature in 2D diagrams
\usepackage{edrx15} % (find-LATEX "edrx15.sty")
\input istanbuldefs % (find-ist "defs.tex")
\begin{document}
\catcode`\^^J=10
\directlua{dofile "dednat6load.lua"} % (find-LATEX "dednat6load.lua")
\directlua{dofile "2015logicandcats.lua"} % (find-LATEX "2015logicandcats.lua")
\directlua{dofile "istanbulall.lua"} % (find-ist "all.lua")
% NEW:
%
%L deletecomments1 = function (line)
%L return line:match"^([^%%]*)"
%L end
%L deletecomments = function (bigstr)
%L return (bigstr:gsub("([^\n]+)", deletecomments1))
%L end
% OLD:
%
% %\input edrxrepl % (find-LATEX "edrxrepl.tex")
% \catcode`\^^J=10 % (find-es "luatex" "spurious-omega")
% %\directlua{dofile "\jobname.lua"} % (find-LATEX "2015logicandcats.lua")
% \directlua{dofile "2015logicandcats.lua"}
% \directlua{dofile "istanbulall.lua"} % (find-ist "all.lua")
% \directlua{getword = getword_utf8} % (find-dn5 "dednat6.lua" "utf8")
%
% \directlua{tf = TexFile.read(tex.jobname..".tex")}
% \directlua{output = printboth}
% \directlua{output = mytexprint}
% \directlua{tf:processuntil()}
% %L output(preamble1)
% \pu
% (find-LATEX "edrx15.sty" "colors")
\edrxcolors
\def\bhbox{\bicolorhbox}
% (find-LATEX "edrx15.sty" "picture-cells")
%$$
% Hello \input /tmp/o.tex % (find-fline "/tmp/o.tex")
% \hbox{\input /tmp/o.tex } % (find-fline "/tmp/o.tex")
%\bhbox{\hbox{\input /tmp/o.tex }} % (find-fline "/tmp/o.tex")
%$$
% (find-angg ".emacs.papers" "texbook")
% (find-texbookpage (+ 12 60) "ex is the \"x-height\" of the current font")
% (find-texbooktext (+ 12 60) "ex is the \"x-height\" of the current font")
% (find-texbookpage (+ 12 151) "$\\vcenter{...}$")
% (find-texbooktext (+ 12 151) "$\\vcenter{...}$")
\def\dagHouse#1#2#3#4#5{\left(\bhbox{$\vcenter{\hbox{\unitlength=4pt%
\celllower=2.5pt%
\def\cellfont{\scriptsize}%
\begin{picture}(3,3)(-0.5,-0.5)
\put(1,2){\cell{#1}}
\put(0,1){\cell{#2}}
\put(2,1){\cell{#3}}
\put(0,0){\cell{#4}}
\put(2,0){\cell{#5}}
\end{picture}}}$}\right)}
\def\PvSTbullets{\left(\bhbox{$\vcenter{\hbox{\unitlength=3pt%
\celllower=2pt%
\def\cellfont{\scriptsize}%
\begin{picture}(8,10)(-3.5,-0.5)
\put(-1,9){\cell{\bullet}}
\put(-2,6){\cell{\bullet}}
\put(-1,7){\cell{\bullet}}
\put(0,8){\cell{\bullet}}
\put(-3,3){\cell{\bullet}}
\put(-2,4){\cell{\bullet}}
\put(-1,5){\cell{\bullet}}
\put(0,6){\cell{\bullet}}
\put(1,7){\cell{\bullet}}
\put(-2,2){\cell{\bullet}}
\put(-1,3){\cell{\bullet}}
\put(0,4){\cell{\bullet}}
\put(1,5){\cell{\bullet}}
\put(2,6){\cell{\bullet}}
\put(-1,1){\cell{\bullet}}
\put(0,2){\cell{\bullet}}
\put(1,3){\cell{\bullet}}
\put(2,4){\cell{\bullet}}
\put(3,5){\cell{\bullet}}
\put(0,0){\cell{\bullet}}
\put(1,1){\cell{\bullet}}
\put(2,2){\cell{\bullet}}
\put(3,3){\cell{\bullet}}
\put(4,4){\cell{\bullet}}
\end{picture}}}$}\right)}
\catcode`\^^O=13 \def*{\ensuremath{\bullet}}
% \catcode`*=13 \def*{\ensuremath{\bullet}}
a$\dagHouse54321 b \dagHouse***** b \PvSTbullets$c
%L drawpile = function (x, y, dy, A, B, arrow)
%L local runstr = function (str) print(str) end
%L local runstr = function (str) dxyrun(str) end
%L local runf = function (fmt, ...) runstr(format(fmt, ...)) end
%L runf "(("
%L A = split(A)
%L B = B and split(B)
%L for i=1,#A do
%L runf("node: %d,%d %s", x, y+dy*(i-1), A[i])
%L if B then runf(".tex= %s", B[i]) end
%L if not arrow then runf("place") end
%L end
%L if arrow then
%L for i=1,#A-1 do
%L runf("%s %s %s", A[i], A[i+1], arrow)
%L end
%L end
%L runf "))"
%L end
%D diagram piles0
%D 2Dx 100
%D 2D 100
%D 2D
%D 2D +20
%D 2D
%L drawpile(100, 100, -15, "L1 L2 L3 L4", "1\\_ 2\\_ 3\\_ 4\\_", "<-")
%L drawpile(120, 100, -15, "R1 R2 R3 R4", "\\_1 \\_2 \\_3 \\_4")
%D (( L1 R3 -> R2 L4 <-
%D
%D ))
%D enddiagram
%D
$$\pu a \left(\diag{piles0}\right) b$$
% «mixedpicture-tests» (to ".mixedpicture-tests")
% (find-dn5 "newrect.lua" "MixedPicture-arch-tests")
%L omp = function ()
%L print(); print("\\"..mp.lp.def..":"); print(mp)
%L output(mp:tolatex())
%L end
%L
%L -- (Pv) is *-functorial
%L z = ZHA.fromspec("1234R3L21L")
%L mp = MixedPicture.new({def="PvIsStarFunctorial"}, z)
%L mp:addcuts("c 5432/10 0|12|34")
%L mp:put(v"20", "P"):put(v"30", "P*", "P^*")
%L mp:put(v"11", "Q"):put(v"12", "Q*", "Q^*")
%L mp:put(v"03", "R"):put(v"14", "R*", "R^*")
%L omp()
%L
%L -- (&R) is *-functorial
%L z = ZHA.fromspec("1234R321")
%L mp = MixedPicture.new({def="andRIsStarFunctorial"}, z)
%L mp:addcuts("c 32/10 01|23|4")
%L mp:put(v"30", "P"):put(v"31", "P*", "P^*")
%L mp:put(v"22", "Q"):put(v"33", "Q*", "Q^*")
%L mp:put(v"04", "R"):put(v"14", "R*", "R^*")
%L omp()
%L
%L -- The (&*) cube
%L z = ZHA.fromspec("12321")
%L mp = MixedPicture.new({def="andStarCubeArchetypal"}, z)
%L mp:addcuts("c 2/10 01|2")
%L mp:put(v"20", "P"):put(v"21", "P*", "P^*")
%L mp:put(v"02", "Q"):put(v"12", "Q*", "Q^*")
%L omp()
%L
%L -- The (v*) cube
%L z = ZHA.fromspec("12321L")
%L mp = MixedPicture.new({def="orStarCubeArchetypal"}, z)
%L mp:addcuts("c 21/0 0|12")
%L mp:put(v"10", "P"):put(v"20", "P*", "P^*")
%L mp:put(v"01", "Q"):put(v"02", "Q*", "Q^*")
%L omp()
%L
%L -- The (->*) cube
%L z = ZHA.fromspec("12321")
%L mp = MixedPicture.new({def="impStarCubeArchetypal"}, z)
%L mp:addcuts("c 2/10 01|2")
%L mp:put(v"10", "P")
%L mp:put(v"00", "Q")
%L omp()
$$
\pu
\PvIsStarFunctorial
\qquad
\andRIsStarFunctorial
\qquad
\andStarCubeArchetypal
\qquad
\orStarCubeArchetypal
\qquad
\impStarCubeArchetypal
$$
%\input /tmp/o.tex % (find-fline "/tmp/o.tex")
%$$a
% \foo
% b
%$$
%$$
%{\unitlength=10pt
%\lower2\unitlength\hbox{\begin{picture}(3,5)(1.5,3)
%\put(-1,0){\line(1,1){2}}
%\put(1,2){\line(1,-1){1}}
%\put(0,-1){\line(-1,1){2}}
%\put(-2,1){\line(1,1){2}}
%\put(0,3){\line(-1,1){1}}
%\put(-1,4){\line(1,1){1}}
%\put(0,5){\line(-1,1){2}}
%\put(-2,7){\line(1,1){3}}
%\put(1,10){\line(1,-1){1}}
%\put(2,9){\line(-1,-1){2}}
%\put(0,7){\line(1,-1){4}}
%\put(4,3){\line(-1,-1){4}}
%\end{picture}
%}}
%$$
\newpage
% _ _ _
% ___ __ _ _ __ __| |_ _(_) ___| |__
% / __|/ _` | '_ \ / _` \ \ /\ / / |/ __| '_ \
% \__ \ (_| | | | | (_| |\ V V /| | (__| | | |
% |___/\__,_|_| |_|\__,_| \_/\_/ |_|\___|_| |_|
%
% «sandwich» (to ".sandwich")
{\bf The sandwich lemma}
The {\sl sandwich lemma} says that if $P≤Q≤P^*$, then $P=^*Q$:
%:
%: Q≤P^*
%: ----------Mo ----------M2
%: P≤Q Q^*≤P^{**} P^{**}=P^*
%: -------Mo ------------------------
%: P≤Q Q≤P^* P^*≤Q^* Q^*≤P^*
%: ----------Sa -----------------------
%: P^*=Q^* := P^*=Q^*
%:
%: ^sand1 ^sand2
%:
\pu
$$\ded{sand1} \qquad \ded{sand2}$$
Let's use the notation of closed interval, $[P,R]$, for the set of all
points between $P$ and $R$ (in the partial order $≤$ of the ZHA):
%
$$[P,R] := \setofst{Q∈Ω}{P≤Q≤R}$$
We saw that $Q∈[P,P^*]$ implies $P =^* Q$, which means that all points
in $[P,P^*]$ are ${}^*$-equal, and that the equivalence class $[P]^*$
contains at least the set $[P,P^*]$ -- which is never empty, because
$M1$ tells us that $P≤P^*$, so
%
$$\mat{P≤P ≤P^* \to P ∈[P,P^*], \\
P≤P^*≤P^* \to P^*∈[P,P^*]. \\
}
$$
Let's call a non-empty set of the form $[P,R]$ a {\sl lozenge}, even
though it may inherit some dents from the ambient ZHA, as here:
%
$$[11,33] = (diagram)$$
If $P_1^* = P_2^*$, then the equivalence class $[P_1]^*$ ($= [P_2]^*$)
contains the union of the lozenges $[P_1, P_1^*]$ and $[P_2, P_2^*] =
[P_2, P_1^*]$. If $42^* = 33^* = 14^* = 56$, then
%
$$\mat{
[42]^* = [33]^* = [14]^* ⊇ \\
[42,56] ∪ [33,56] ∪ [14,56] \\
}
$$
%
so each equivalence class $[P]^*$ is a union of lozenges or the form
$[\_, P^*]$; and if $[P_1]^* = \setof{P1, P_2, \ldots, P_n}$ then
$[P_1]^* = [P_1,P_1^*] ∪ [P_2,P_1^*] ∪ \ldots ∪ [P_n,P_1^*]$.
\msk
Let's go back to the example above, where $42^* = 33^* = 14^* = 56$.
We have
%
$$\begin{array}{rcl}
((42∧33)∧14)^* &=& \\
(42∧33)^*∧14^* &=& \\
(42^*∧33^*)∧14^* &=& \\
(56∧56)∧56 &=& 56, \\
\end{array}
$$
%
so $42∧33∧14$ is in the same equivalence class as 42, 33, and 14. We
have $[12, 56] ⊆ [42]^* = [33]^* = [14]^*$, which means this shape:
%
$$(diagram)$$
\newpage
(...)
%:
%:
%:
%: P_1^*=P_2^*
%: ==============
%: P_1=^*P_2 P_1^*∧P_2^*=P_1^*
%: -----------ECC∧ =================M3
%: P_1∧P_2=^*P_1 := (P_1∧P_2)^*=P_1^*
%:
%: ^Eqcand-1 ^Eqcand-2
%: ---------M1
%: P_2≤P_2^* P_2^*=P_1^*
%: ---------M1 ------------------------
%: P_1≤P_1^* P_2≤P_1^*
%: ----------- -------------------------
%: P_1=^*P_2 P_1≤P_1∨P_2 P_1∨P_2≤P_1^*
%: -------------ECC∨ --------------------------Sa
%: P_1=^*P_1∨P_2 := P_1^*=(P_1∨P_2)~*
%:
%: ^Eqcor-1 ^Eqcor-2
%:
%:
%: P^*=Q^*
%: ==========
%: P=^*Q P^*∧Q^*=P*
%: -----------ECC∧ ===========M3
%: P∧Q=^*P := (P∧Q)^*=P^*
%:
%: ^Eqcand-1 ^Eqcand-2
%: -----M1
%: Q≤Q^* Q^*=P^*
%: -----M1 ----------------
%: P≤P^* Q≤P^*
%: ----- -----------------
%: P=^*Q P≤P∨Q P∨Q≤P^*
%: -------ECC∨ ----------------Sa
%: P=^*P∨Q := P^*=(P∨Q)~*
%:
%: ^Eqcor-1 ^Eqcor-2
%:
\pu
$$\begin{array}{rcl}
\ded{Eqcand-1} &:=& \ded{Eqcand-2} \\\\
\ded{Eqcor-1} &:=& \ded{Eqcor-2} \\\\
\end{array}
$$
% $$\ded{Eqcand-1} \qquad := \qquad \ded{Eqcand-2}$$
% $$\ded{Eqcor-1} \qquad := \qquad \ded{Eqcor-2}$$
\newpage
% _
% | |
% _ | |
% | |_| |
% \___/
%
% «J-and-connectives» (to ".J-and-connectives")
% (find-istfile "1.org" "P&Q, J(P)&Q, ...")
% (find-LATEX "2008graphs.tex")
% (find-LATEX "2008graphs.tex" "LT-modalities")
% (find-853page 21 "internal-diagram")
% (find-853page 22 "and")
%L forths["="] = function () pusharrow("=") end
%L dxyren = function (li)
%L local a, b = li:match("^(.*) =+> (.*)$")
%L local A, B = split(a), split(b)
%L for i=1,#A do PP(A[i], B[i]); nodes[A[i]].tex = B[i] end
%L end
%L forths["ren"] = function () dxyren(getrestofline()) end
%D diagram test0
%D 2Dx 100 +30 +30
%D 2D 100 A1
%D 2D +25 A2 A3 A4
%D 2D +25 A5 A6 A7
%D 2D +25 A8
%D 2D
%D ren A1 ==> V_1
%D ren A2 A3 A4 ==> V_2 V_3 V_4
%D ren A5 A6 A7 ==> V_5 V_6 V_7
%D ren A8 ==> V_8
%D
%D (( A1 A2 <- A1 A3 <- A1 A4 <-
%D A2 A5 <- A2 A6 <- A3 A5 <- A3 A7 <- A4 A6 <- A4 A7 <-
%D A5 A8 <- A6 A8 <- A7 A8 <-
%D ))
%D enddiagram
%D
%D diagram test1
%D 2Dx 100 +30 +30
%D 2D 100 A1
%D 2D +25 A2 A3 A4
%D 2D +25 A5 A6 A7
%D 2D +25 A8
%D 2D
%D ren A1 ==> (P^*∧Q^*)^*
%D ren A2 A3 A4 ==> (P∧Q^*)^* P^*∧Q^* (P^*∧Q)^*
%D ren A5 A6 A7 ==> P∧Q^* (P∧Q)^* P^*∧Q
%D ren A8 ==> P∧Q
%D
%D (( A1 A2 <- A1 A3 <- A1 A4 <-
%D A2 A5 <- A2 A6 <- A3 A5 <- A3 A7 <- A4 A6 <- A4 A7 <-
%D A5 A8 <- A6 A8 <- A7 A8 <-
%D ))
%D enddiagram
%D
%D diagram test2
%D 2Dx 100 +30 +30
%D 2D 100 A1
%D 2D +25 A2 A3 A4
%D 2D +25 A5 A6 A7
%D 2D +25 A8
%D 2D
%D ren A1 ==> (P^*∧Q^*)^*
%D ren A2 A3 A4 ==> (P∧Q^*)^* P^*∧Q^* (P^*∧Q)^*
%D ren A5 A6 A7 ==> P∧Q^* (P∧Q)^* P^*∧Q
%D ren A8 ==> P∧Q
%D
%D (( A1 A2 <- A1 A3 <- A1 A4 <-
%D A2 A5 <- A2 A6 <- A3 A5 <- A3 A7 <- A4 A6 <- A4 A7 <-
%D A5 A8 <- A6 A8 <- A7 A8 <-
%D A3 A6 =
%D ))
%D enddiagram
$$\pu \diag{test0} \qquad \diag{test1} \qquad \diag{test2}$$
%D diagram LT-and-1
%D 2Dx 100 +30 +30 +30 +30 +30 +30 +30 +30 +30
%D 2D 100 P^* A7 Q^* p^* a7 q^*
%D 2D
%D 2D +25 P A3 A5 A6 Q p a3 a5 a6 q
%D 2D
%D 2D +25 A1 A2 A4 a1 a2 a4
%D 2D
%D 2D +25 A0 a0
%D 2D
%D (( A0 .tex= P∧Q a0 .tex= 11
%D A1 .tex= P∧Q^* a1 .tex= 21
%D A2 .tex= (P∧Q)^* a2 .tex= 22
%D A3 .tex= (P∧Q^*)^* a3 .tex= 22
%D A4 .tex= P^*∧Q a4 .tex= 12
%D A5 .tex= P^*∧Q^* a5 .tex= 22
%D A6 .tex= (P^*∧Q)^* a6 .tex= 22
%D A7 .tex= (P^*∧Q^*)^* a7 .tex= 22
%D
%D A0 A1 -> A0 A2 -> A1 A3 -> A2 A3 ->
%D A4 A5 -> A4 A6 -> A5 A7 -> A6 A7 ->
%D A0 A4 -> A1 A5 -> A2 A6 -> A3 A7 ->
%D
%D a0 a1 -> a0 a2 -> a1 a3 -> a2 a3 =
%D a4 a5 -> a4 a6 -> a5 a7 = a6 a7 =
%D a0 a4 -> a1 a5 -> a2 a6 = a3 a7 =
%D ))
%D (( p .tex= 31 p^* .tex= 32 q^* .tex= 23 q .tex= 13
%D P P^* -> Q Q^* ->
%D p p^* -> q q^* ->
%D ))
%D enddiagram
%D
%:
%:
%:
%: ----------M2 ----------M2
%: P^*=P^{**} Q^*=Q^{**}
%: ---------------------(∧)_1 -------------------------M3
%: P^*∧Q^*=P^{**}∧Q^{**} P^{**}∧Q^{**}=(P^*∧Q^*)^*
%: ---------------M3 -----------------------------------------------------
%: (P∧Q)^*=P^*∧Q^* P^*∧Q^*=(P^*∧Q^*)^*
%: ---------------------------------------------------
%: (P∧Q)^*=P^*∧Q^*=(P^*∧Q^*)^*
%:
%: ----------M2 ----------M2
%: P^*=P^{**} Q^*=Q^{**}
%: ---------------------(∧)_1 -------------------------M3
%: P^*∧Q^*=P^{**}∧Q^{**} P^{**}∧Q^{**}=(P^*∧Q^*)^*
%: -----------------------------------------------------
%: P^*∧Q^*=(P^*∧Q^*)^*
%:
%: ^J-and-lozenge-1
%:
%: ---------------M3 ===================
%: (P∧Q)^*=P^*∧Q^* P^*∧Q^*=(P^*∧Q^*)^*
%: ---------------------------------------
%: (P∧Q)^*=P^*∧Q^*=(P^*∧Q^*)^*
%:
%: ^J-and-lozenge-2
%:
\pu
$$\diag{LT-and-1}
\qquad
\mat{
\ded{J-and-lozenge-1} \\ \\ \\
\ded{J-and-lozenge-2} \\
}
$$
%D diagram LT-or-1
%D 2Dx 100 +30 +30 +30 +30 +30 +30 +30 +30 +30
%D 2D 100 A7 a7
%D 2D / | \
%D 2D +25 A3 A5 A6 a3 a5 a6
%D 2D | X X
%D 2D +25 A1 A2 A4 a1 a2 a4
%D 2D \ | /
%D 2D +25 P^* A0 Q^* p^* a0 q^*
%D 2D
%D 2D +25 P Q p q
%D 2D
%D (( P P^* ->
%D Q Q^* ->
%D p .tex= 10 p^* .tex= 20 ->
%D q .tex= 01 q^* .tex= 02 ->
%D ))
%D (( A0 .tex= P∨Q a0 .tex= 11
%D A1 .tex= P∨Q^* a1 .tex= 21
%D A2 .tex= (P∨Q)^* a2 .tex= 33
%D A3 .tex= (P∨Q^*)^* a3 .tex= 33
%D A4 .tex= P^*∨Q a4 .tex= 02
%D A5 .tex= P^*∨Q^* a5 .tex= 22
%D A6 .tex= (P^*∨Q)^* a6 .tex= 33
%D A7 .tex= (P^*∨Q^*)^* a7 .tex= 33
%D A0 A1 -> A0 A2 -> A1 A3 -> A2 A3 ->
%D A4 A5 -> A4 A6 -> A5 A7 -> A6 A7 ->
%D A0 A4 -> A1 A5 -> A2 A6 -> A3 A7 ->
%D
%D a0 a1 -> a0 a2 -> a1 a3 -> a2 a3 =
%D a4 a5 -> a4 a6 -> a5 a7 -> a6 a7 =
%D a0 a4 -> a1 a5 -> a2 a6 = a3 a7 =
%D ))
%D enddiagram
%D
%:
%: ------ ------
%: P≤P∨Q Q≤P∨Q
%: ------------Mo ------------Mo
%: J(P)≤J(P∨Q) J(Q)≤J(P∨Q)
%: ---------------------------
%: J(P)∨J(Q)≤J(P∨Q)
%: -----------------------Mo ----------------M2
%: J(J(P)∨J(Q))≤J(J(P∨Q)) J(J(P∨Q))=J(P∨Q)
%: --------------------------------------------
%: J(J(P)∨J(Q))≤J(P∨Q)
%:
%: ^J-or-lozenge
%:
%:
%: ------ ------
%: P≤P∨Q Q≤P∨Q
%: ------------Mo -----------Mo
%: P^*≤(P∨Q)^* Q^*≤(P∨Q)^*
%: ---------------------------
%: P^*∨Q^*≤(P∨Q)^*
%: ----------------------Mo ----------------M2
%: (P^*∨Q^*)^*≤(P∨Q)^{**} (P∨Q)^{**}=(P∨Q)^*
%: --------------------------------------------
%: (P^*∨Q^*)^*≤(P∨Q)^*
%:
%: ^J-or-lozenge
%:
\pu
$$\diag{LT-or-1}
% \qquad
\ded{J-or-lozenge}
$$
%D diagram LT-imp-1
%D 2Dx 100 +30 +30 +30 +30 +30 +30 +30
%D 2D 100 A7 A7
%D 2D
%D 2D +25 A3 A5 A6 A3 A5 A6
%D 2D
%D 2D +25 A1 A2 A4 A1 A2 A4
%D 2D
%D 2D +25 A0 A0
%D 2D
%D ((
%D A0 .tex= P^*{→}Q
%D A1 .tex= P^*{→}Q^*
%D A2 .tex= (P^*{→}Q)^*
%D A3 .tex= (P^*{→}Q^*)^*
%D A4 .tex= P{→}Q
%D A5 .tex= P{→}Q^*
%D A6 .tex= (P{→}Q)^*
%D A7 .tex= (P{→}Q^*)^*
%D A0 A1 -> A0 A2 -> A1 A3 -> A2 A3 ->
%D A4 A5 -> A4 A6 -> A5 A7 -> A6 A7 ->
%D A0 A4 -> A1 A5 -> A2 A6 -> A3 A7 ->
%D ))
%D enddiagram
%D
\pu
$$\diag{LT-imp-1}$$
% «J-proofs» (to ".J-proofs")
% (find-istfile "1.org" "P&Q, J(P)&Q, ...")
% (find-LATEX "2008graphs.tex")
% (find-LATEX "2008graphs.tex" "LT-modalities")
% (find-853page 21 "internal-diagram")
% (find-853page 22 "and")
Extras:
%: 01=_J23 45=_J67
%: --------- ---------
%: 0\_=_L2\_ \_5=_R\_7
%: --------------------
%: 05=_W27
%:
%: ^JLRW
%:
%:
%: P≤^*Q Q≤^*R
%: -------def -------def
%: P^*≤Q^* Q^*≤R^*
%: -----------(∧R)_1 -----------(P∨)_1
%: P^*∧R≤Q^*≤R P∨Q^*≤P∨R^*
%: ----------------(*)_1 -------------------(*)_1
%: (P^*∧R)^*≤(Q^*≤R)^* (P∨Q^*)^*≤(P∨R^*)^*
%: -------------------∧-cube -------------------∨-cube
%: (P∧R)^*≤(Q∧R)^* (P∨Q)^*≤(P∨R)^*
%: --------------- def ---------------def
%: P∧R≤^*Q∧R P∨Q≤^*P∨R
%:
%: ^and-R-is-star-functorial ^P-or-is-star-functorial
%:
\pu
$$\ded{JLRW}$$
$$\ded{and-R-is-star-functorial} \qquad \ded{P-or-is-star-functorial}$$
%: ----------M2 ----------M2
%: P^*=P^{**} Q^*=Q^{**}
%: ---------------------(∧)_1 -------------------------M3
%: P^*∧Q^*=P^{**}∧Q^{**} P^{**}∧Q^{**}=(P^*∧Q^*)^*
%: -----------------------------------------------------
%: P^*∧Q^*=(P^*∧Q^*)^*
%:
%: ^J-and-lozenge-1
% There the "="s get into the rule name:
% =================∧-cube
%\end{document}
\newpage
% «HAs-and-CCCs» (to ".HAs-and-CCCs")
\par Logic and Categories, or: Heyting Algebras for Children
\par Eduardo Ochs - UniLog 2015, Istanbul
\par \url{http://angg.twu.net/math-b.html#istanbul}
\msk
\par \bf{1. A comparison between HAs and Cartesian Closed Categories:}
% _ _ _ _ ____ ____ ____
% | | | | / \ ___ __ _ _ __ __| | / ___/ ___/ ___|___
% | |_| | / _ \ / __| / _` | '_ \ / _` | | | | | | | / __|
% | _ |/ ___ \\__ \ | (_| | | | | (_| | | |__| |__| |___\__ \
% |_| |_/_/ \_\___/ \__,_|_| |_|\__,_| \____\____\____|___/
%
%: HA rules:
%:
%: P∧Q≤R
%: -----π -----π' -----♯
%: Q∧R≤Q Q∧R≤R P≤Q{→}R
%:
%: ^P-pi ^P-pi' ^P-sharp
%:
%: P≤Q P≤R P≤Q{→}R
%: ---! --------\ang{,} -----♭
%: P≤⊤ P≤Q∧R P∧Q≤R
%:
%: ^P-T ^P-ang ^P-flat
%:
%:
%: -----ι -----ι'
%: P≤P∨Q Q≤P∨Q
%:
%: ^P-iota ^P-iota'
%:
%: P≤R Q≤R
%: ---¡ --------[,]
%: ⊥≤P P∨Q≤R
%:
%: ^P-F ^P-[,]
%:
%: CCC rules:
%: f:A×B→C
%: -------π --------π' -----------♯
%: π:B×C→B π':B×C→C f^♯:A→B{→}C
%:
%: ^F-pi ^F-pi' ^F-sharp
%:
%: f:A→B g:A→C g:A→B{→}C
%: ------¡ ---------------\ang{,} ---------♭
%: !:A→1 \ang{f,g}:A→B×C g^♭:A×B→C
%:
%: ^F-T ^F-ang ^F-flat
%:
%: -------ι --------ι'
%: ι:A→A+B ι':B→A+B
%:
%: ^F-iota ^F-iota'
%:
%: f:A→B g:A→C
%: ------¡ ---------------\ang{,}
%: ¡:0→A \ang{f,g}:A→B×C
%:
%: ^F-F ^F-[,]
%:
\pu
\def\BiHArules{{
\def\PT {\ded{P-T}}
\def\PPA{\ded{P-pi}}
\def\PPB{\ded{P-pi'}}
\def\PPC{\ded{P-ang}}
\def\PEA{\ded{P-sharp}}
\def\PEB{\ded{P-flat}}
\def\PF {\ded{P-F}}
\def\PCA{\ded{P-iota}}
\def\PCB{\ded{P-iota'}}
\def\PCC{\ded{P-[,]}}
\mat{ & \PPA \qquad \PPB & \PEA \\\\
\PT & \PPC & \PEB \\\\
& \PCA \qquad \PCB & \\\\
\PF & \PCC &
}
}}
\def\BiCCCrules{{
\def\PT {\ded{F-T}}
\def\PPA{\ded{F-pi}}
\def\PPB{\ded{F-pi'}}
\def\PPC{\ded{F-ang}}
\def\PEA{\ded{F-sharp}}
\def\PEB{\ded{F-flat}}
\def\PF {\ded{F-F}}
\def\PCA{\ded{F-iota}}
\def\PCB{\ded{F-iota'}}
\def\PCC{\ded{F-[,]}}
\mat{ & \PPA \qquad \PPB & \PEA \\\\
\PT & \PPC & \PEB \\\\
& \PCA \qquad \PCB & \\\\
\PF & \PCC &
}
}}
% (find-dn4 "dednat4.lua" "lplacement")
%L forths[".PLABEL="] = function ()
%L ds[1].lplacement = getword()
%L ds[1].label = getword()
%L end
%D diagram BiHAdiag
%D 2Dx 100 +15 +25 +25 +15 +25
%D 2D 100 T1 PB <- PBC -> PC EC |--> EB->C
%D 2D ^ ^ ^ ^ ^ ^
%D 2D | \ | / | |
%D 2D +25 TA PA EAxB <-| EA
%D 2D
%D 2D +15 IA CC
%D 2D ^ ^ ^ ^
%D 2D | / | \
%D 2D +25 I0 CA -> CAB <- CB
%D 2D
%D (( T1 .tex= ⊤ TA .tex= P
%D @ 0 @ 1 <-
%D ))
%D (( PB .tex= Q PBC .tex= Q∧R PC .tex= R PA .tex= P
%D @ 0 @ 1 <- @ 1 @ 2 ->
%D @ 0 @ 3 <- @ 1 @ 3 <- @ 2 @ 3 <-
%D ))
%D (( EC .tex= R EB->C .tex= Q{→}R EAxB .tex= P∧Q EA .tex= P
%D @ 0 @ 1 |->
%D @ 0 @ 2 <- @ 1 @ 3 <-
%D @ 2 @ 3 <-|
%D ))
%D (( IA .tex= P I0 .tex= ⊥
%D @ 0 @ 1 <-
%D ))
%D (( CC .tex= R CA .tex= P CAB .tex= P∨Q CB .tex= Q
%D @ 0 @ 1 <- @ 0 @ 2 <- @ 0 @ 3 <-
%D @ 1 @ 2 -> @ 2 @ 3 <-
%D ))
%D enddiagram
%D
%D diagram BiCCCdiag
%D 2Dx 100 +15 +25 +25 +15 +25
%D 2D 100 T1 PB <- PBC -> PC EC |--> EB->C
%D 2D ^ ^ ^ ^ ^ ^
%D 2D | \ | / | |
%D 2D +25 TA PA EAxB <-| EA
%D 2D
%D 2D +15 IA CC
%D 2D ^ ^ ^ ^
%D 2D | / | \
%D 2D +25 I0 CA -> CAB <- CB
%D 2D
%D (( T1 .tex= 1 TA .tex= A
%D @ 0 @ 1 <- .plabel= l !
%D ))
%D (( PB .tex= B PBC .tex= B{×}C PC .tex= C PA .tex= A
%D @ 0 @ 1 <- .plabel= a π @ 1 @ 2 -> .plabel= a π'
%D @ 0 @ 3 <- .plabel= l f @ 2 @ 3 <- .plabel= r g
%D @ 1 @ 3 <- .plabel= m <f,g>
%D ))
%D (( EC .tex= C EB->C .tex= B{→}C EAxB .tex= A{×}B EA .tex= A
%D @ 0 @ 1 |-> .plabel= a (B{→})
%D @ 0 @ 2 <- .plabel= l \sm{f\\g^♭}
%D @ 1 @ 3 <- .plabel= r \sm{f^♯\\g}
%D @ 2 @ 3 <-| .plabel= r (×B)
%D @ 0 @ 3 harrownodes nil 20 nil |-> sl^
%D @ 0 @ 3 harrownodes nil 20 nil <-| sl_
%D # @ 0 @ 2 <- .PLABEL= _(0.43) g^\flat
%D # @ 0 @ 2 <- .PLABEL= _(0.57) f
%D # @ 1 @ 3 <- .PLABEL= ^(0.43) g
%D # @ 1 @ 3 <- .PLABEL= ^(0.57) f^\sharp
%D ))
%D (( IA .tex= A I0 .tex= 0
%D @ 0 @ 1 <- .plabel= l ¡
%D ))
%D (( CC .tex= C CA .tex= A CAB .tex= A{+}B CB .tex= B
%D @ 0 @ 1 <- .plabel= l f @ 0 @ 3 <- .plabel= r g
%D @ 0 @ 2 <- .plabel= m [f,g]
%D @ 1 @ 2 -> .plabel= b ι @ 2 @ 3 <- .plabel= b ι'
%D ))
%D enddiagram
%D
\pu
\def\BiHAeqs{
\begin{array}{rl}
(id) & ∀P.(P≤P) \\
(comp) & ∀P,Q,R.(P≤Q)∧(Q≤R)→(P≤R) \\
\\
(⊤) & ∀P.(P≤⊤) \\
(⊥) & ∀P.(⊥≤P) \\
(∧) & ∀P,Q,R.(P≤Q∧R)↔(P≤Q)∧(P≤R) \\
(∨) & ∀P,Q,R.(P∨Q≤R)↔(P≤R)∧(Q≤R) \\
(→) & ∀P,Q,R.(P≤Q→R)↔(P∧Q≤R) \\
\\
(¬) & ¬P := P→⊥ \\
(↔) & P↔Q := (P→Q)∧(Q→P) \\
\end{array}
}
\def\BiCCCeqs{
\begin{array}{rl}
(id) & \id_A ∈ \Hom(A,A) \\
(comp) & (;)_{A,B,C}: \Hom(A,B)×\Hom(B,C)→\Hom(A,C) \\
\\
(⊤) & ∀A.(\Hom(A,1)≃1) \\
(⊥) & ∀A.(\Hom(0,A)≃1) \\
(∧) & ∀A,B,C.(\Hom(A,B×C)≃\Hom(A,B)×\Hom(A,C)) \\
(∨) & ∀A,B,C.(\Hom(A+B,C)≃\Hom(A,C)×\Hom(B,C)) \\
(→) & ∀A,B,C.(\Hom(A,C^B)≃\Hom(A×B,C) \\
\end{array}
}
% (find-854file "" "fdiagest")
% (find-854file "" "%D diagram yoneda-and-friends")
% (find-dn4 "experimental.lua" "BOX")
\def\ctabular#1{\begin{tabular}{c}#1\end{tabular}}
\def\ltabular#1{\begin{tabular}{c}#1\end{tabular}}
% \def\fdiagwithboxest#1#2{\ltabular{#2 \\ \fdiagwithboxes{#1}}}
\def\fdiagest#1#2{\ltabular{#2 \\ \fdiag{#1}}}
\savebox{\myboxa}{$\diag{BiHAdiag}$} \def\BiHAdiag {\usebox{\myboxa}}
\savebox{\myboxb}{$\diag{BiCCCdiag}$} \def\BiCCCdiag{\usebox{\myboxb}}
% (find-es "tex" "savebox")
$$\begin{array}{rcl}
\fbox{$\BiHAeqs$} && \fbox{$\BiCCCeqs$} \\\\
\fbox{$\BiHArules$} && \fbox{$\BiCCCrules$} \\\\
\fbox{\BiHAdiag} && \fbox{\BiCCCdiag} \\
\end{array}
$$
% _ _ __
% | |__ _ __ _ _| |_ ___ / _| ___ _ __ ___ ___
% | '_ \| '__| | | | __/ _ \ | |_ / _ \| '__/ __/ _ \
% | |_) | | | |_| | || __/ | _| (_) | | | (_| __/
% |_.__/|_| \__,_|\__\___| |_| \___/|_| \___\___|
%
% «brute-force» (to ".brute-force")
% (find-LATEX "2015logicandcats.lua" "processzrect")
\def\processzrect#1{\directlua{tf:processuntil() processzrect"#1 out"}}
\def\zr#1{\processzrect{#1}}
% NEW:
%
\end{document}
%R ra := 1/ 0 \ rb := 1/ 0 \ rc := 1/ 0 \
%R | 0 0 | | 0 0 | | 0 0 |
%R | 0 0 0 | | 0 0 0 | | 0 0 0 |
%R |0 1 0 0| |0 0 1 0| |0 0 0 0|
%R | 1 1 0 | | 0 1 1 | | 0 1 0 |
%R | 1 1 | | 1 1 | | 1 1 |
%R \ 1 / \ 1 / \ 1 /
%R
\pu
\def\ra{\mat{λP.P≤21 = \\ \zr{ra script 7pt}}}
\def\rb{\mat{λP.P≤12 = \\ \zr{rb script 7pt}}}
\def\rc{\mat{λP.P≤21∧P≤12 = \\ \zr{rc script 7pt}}}
\def\rd{\mat{λP.P≤? = \\ \zr{rc script 7pt}}}
%
% (P≤Q & R) <-> (P≤Q )&(P≤R )
% 21 12 21 12
% ----- ----- ------
% ? \ra \rb
% ------- -------------
% \rd \rc
%
%L ubs_brute_force_and = ubs [[
%L P Q 21 u R 12 u ∧ bin ? u ≤ bin \rd u ()
%L P Q 21 u ≤ bin \ra u ()
%L P R 12 u ≤ bin \rb u () ∧ bin \rc u
%L ↔ bin
%L ∀P. pre
%L ]]
%R Ra := 2/ 21 \ Rb := 1/ 0 \
%R | 21 21 | | 0 0 |
%R | 21 21 11 | | 0 0 1 |
%R |20 21 11 01| |0 0 1 1|
%R | 20 11 01 | | 0 1 1 |
%R | 10 01 | | 1 1 |
%R \ 00 / \ 1 /
%R
\pu
\def\Ra{\mat{λP.P∧21 = \\ \zr{Ra script 9pt}}}
\def\Rb{\mat{λP.(P∧21)≤12 = \\ \zr{Rb script 7pt}}}
\def\Rc{\mat{λP.P≤? = \\ \zr{Rb script 7pt}}}
%
% (P≤Q -> R) <-> (P&Q ≤ R )
% 21 12 21 12
% ------ -----
% ? \Ra
% -------- ----------
% \Rc \Rb
%
%
% P Q 21 u R 12 u → bin ? u ≤ bin \Rc u ()
% P Q 21 u ∧ bin \Ra u R 12 u ≤ bin \Rb u ()
%
%L ubs_brute_force_imp = ubs [[
%L P Q 21 u R 12 u → bin ? u ≤ bin \Rc u ()
%L P Q 21 u ∧ bin \Ra u R 12 u ≤ bin \Rb u ()
%L ↔ bin
%L ]]
\par Logic and Categories, or: Heyting Algebras for Children
\par Eduardo Ochs - UniLog 2015, Istanbul
\par \url{http://angg.twu.net/math-b.html#istanbul}
\msk
\par \bf{2. Calculating $21∧12$ and $21{→}12$ by brute force:}
\bsk
$$\Expr{ubs_brute_force_and}
\qquad
\qquad
\Expr{ubs_brute_force_imp}
$$
\end{document}
\end{document}
% Local Variables:
% coding: utf-8-unix
% ee-anchor-format: "«%s»"
% End: