|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% (find-LATEX "2020hyp.tex")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2020hyp.tex" :end))
% (defun d () (interactive) (find-pdf-page "~/LATEX/2020hyp.pdf"))
% (defun d () (interactive) (find-pdftools-page "~/LATEX/2020hyp.pdf"))
% (defun e () (interactive) (find-LATEX "2020hyp.tex"))
% (defun u () (interactive) (find-latex-upload-links "2020hyp"))
% (defun v0 () (interactive) (find-2a '(e) '(d)))
% (defun v () (interactive) (find-2a '(e) '(d)) (g))
% (find-pdf-page "~/LATEX/2020hyp.pdf")
% (find-sh0 "cp -v ~/LATEX/2020hyp.pdf /tmp/")
% (find-sh0 "cp -v ~/LATEX/2020hyp.pdf /tmp/pen/")
% file:///home/edrx/LATEX/2020hyp.pdf
% file:///tmp/2020hyp.pdf
% file:///tmp/pen/2020hyp.pdf
% http://angg.twu.net/LATEX/2020hyp.pdf
% http://angg.twu.net/LATEX/2020hyp.pdf#page=14
% (find-LATEX "2019.mk")
% «.defs» (to "defs")
% «.limp-2020» (to "limp-2020")
% «.myenumerate» (to "myenumerate")
% «.title-page» (to "title-page")
% «.sources» (to "sources")
% «.bcc-seely-lccc» (to "bcc-seely-lccc")
% «.equahyp-p5» (to "equahyp-p5")
% «.preservation-of-imp» (to "preservation-of-imp")
%
% «.introduction» (to "introduction")
% «.hyp-ND-rules» (to "hyp-ND-rules")
% «.why-hyperdoctrines» (to "why-hyperdoctrines")
% «.why-hyperdoctrines-2» (to "why-hyperdoctrines-2")
% «.quants-for-children» (to "quants-for-children")
% «.or-elim» (to "or-elim")
% «.quants-for-children-2» (to "quants-for-children-2")
% «.dummett» (to "dummett")
% «.we-can-use-to» (to "we-can-use-to")
% «.judgments» (to "judgments")
% «.judgments-cat» (to "judgments-cat")
% «.arrows» (to "arrows")
% «.pred» (to "pred")
% «.predicates-over» (to "predicates-over")
% «.predicates-over-2» (to "predicates-over-2")
% «.plc» (to "plc")
\documentclass[oneside]{book}
\usepackage[colorlinks,citecolor=DarkRed,urlcolor=DarkRed]{hyperref} % (find-es "tex" "hyperref")
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{pict2e}
\usepackage[x11names,svgnames]{xcolor} % (find-es "tex" "xcolor")
%\usepackage{colorweb} % (find-es "tex" "colorweb")
%\usepackage{tikz}
%\usepackage{kpfonts} % (find-es "tex" "mathfrak-kpfonts")
\usepackage{MnSymbol} % (find-es "tex" "lhookdownarrow")
%
% (find-dn6 "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 edrxaccents.tex % (find-LATEX "edrxaccents.tex")
\input edrxchars.tex % (find-LATEX "edrxchars.tex")
\input edrxheadfoot.tex % (find-LATEX "edrxheadfoot.tex")
%\input edrxgac2.tex % (find-LATEX "edrxgac2.tex")
%
%\input edrx17defs.tex % (find-LATEX "edrx17defs.tex")
%\input 2017planar-has-defs.tex % (find-LATEX "2017planar-has-defs.tex")
%
% (find-es "tex" "geometry")
% (find-latexgeomtext "total={6.5in,8.75in},")
\usepackage[paperwidth=11.5cm, paperheight=9.5cm,
%total={6.5in,4in},
%textwidth=4in, paperwidth=4.5in,
%textheight=5in, paperheight=4.5in,
%a4paper,
top=1.5cm, bottom=.5cm, left=1cm, right=1cm, includefoot
]{geometry}
%
\usepackage[backend=biber,
style=alphabetic]{biblatex} % (find-es "tex" "biber")
\addbibresource{catsem-u.bib} % (find-LATEX "catsem-u.bib")
%
% See: (find-es "tex" "limp-abx")
\DeclareFontFamily{U}{matha}{\hyphenchar\font45}
\DeclareFontShape{U}{matha}{m}{n}{
<5> <6> <7> <8> <9> <10> gen * matha
<10.95> matha10 <12> <14.4> <17.28> <20.74> <24.88> matha12
}{}
\DeclareSymbolFont{matha}{U}{matha}{m}{n}
\DeclareMathSymbol{\thinsubset}{3}{matha}{"80}
\DeclareMathSymbol{\thinsupset}{3}{matha}{"81}
\def\limp{\thinsupset}
%
\begin{document}
\catcode`\^^J=10
\directlua{dofile "dednat6load.lua"} % (find-LATEX "dednat6load.lua")
%L dofile "edrxtikz.lua" -- (find-LATEX "edrxtikz.lua")
%L dofile "edrxpict.lua" -- (find-LATEX "edrxpict.lua")
\pu
% ____ __
% | _ \ ___ / _|___
% | | | |/ _ \ |_/ __|
% | |_| | __/ _\__ \
% |____/ \___|_| |___/
%
% «defs» (to ".defs")
\def\dnito{\lhookdownarrow}
\def\Ords{\mathsf{Ords}}
\def\psmi #1#2{ \psm {#1 \\ \dnito \\ #2}}
\def\pmati #1#2{ \pmat{#1 \\ \dnito \\ #2}}
\def\pmatin#1#2#3{\pmat{#1 \\ \dnito & #3 \\ #2}}
\def \matin#1#2#3{ \mat{#1 \\ \dnito & #3 \\ #2}}
\long\def\ColorRed #1{{\color{Red1}#1}}
\long\def\ColorViolet#1{{\color{MagentaVioletLight}#1}}
\long\def\ColorViolet#1{{\color{Violet!50!black}#1}}
\long\def\ColorGreen #1{{\color{SpringDarkHard}#1}}
\long\def\ColorGreen #1{{\color{SpringGreenDark}#1}}
\long\def\ColorGreen #1{{\color{SpringGreen4}#1}}
\long\def\ColorGray #1{{\color{GrayLight}#1}}
\long\def\ColorGray #1{{\color{black!30!white}#1}}
% «limp-2020» (to ".limp-2020")
% Logical implication, as a thin \supset - version 2020feb20
% (find-es "tex" "limp-abx")
% (find-es "tex" "thin_supset")
% (find-es "tex" "pict2e")
% (find-es "tex" "begin-picture" "(XSIZE,YSIZE)(XORG,YORG)")
%
%\def\limpbody{%
% \begin{picture}%(4,2)
% (5.1,2.5)(-0.5,-0.25)
% \Line(0,0)(3,0)
% \Line(0,2)(3,2)
% \put(3,1){\arc[-90,90]{1}}
% \end{picture}%
% }
%\def\limp{%
% \mathrel{\vcenter{\hbox{%
% \unitlength=2pt%
% \linethickness{0.4pt}%
% \limpbody%
% }}}}
\catcode`✀=13 \def✀{\limp}
\catcode`⊸=13 \def⊸{\limp}
% Test:
% $R {\limp}
% S \limp
% T \supset
% U \bhbox{$\supset$}
% V \bhbox{$\limp$}
% W
% $
\setlength{\parindent}{0pt}
% «myenumerate» (to ".myenumerate")
% (find-LATEX "2020list-test.tex")
\newcounter{mycounter}
\long\def\myenumerate#1{%
\begin{list}{\arabic{mycounter}.}%
{\usecounter{mycounter}
\setlength\topsep{0pt}
\setlength\parsep{0pt}
\setlength\itemsep{0pt}
}
#1
\end{list}
}
% _____ _ _ _
% |_ _(_) |_| | ___ _ __ __ _ __ _ ___
% | | | | __| |/ _ \ | '_ \ / _` |/ _` |/ _ \
% | | | | |_| | __/ | |_) | (_| | (_| | __/
% |_| |_|\__|_|\___| | .__/ \__,_|\__, |\___|
% |_| |___/
%
% «title-page» (to ".title-page")
Notes on Hyperdoctrines
\newpage
\noedrxfooter
{\bf Dummett's notation for Natural Deduction: $∃-$}
In \cite{Dummett}, p.89, he writes ND trees as $H_1,\ldots,H_n:C$...
%
%: Γ:∃x\,A(x) Δ,A(y):C
%: ---------------------∃-
%: Γ,Δ:C
%:
%: ^Dummett-0
%:
%: \vec{P}:∃x\,Q(x) \vec{R},Q(y):S
%: ---------------------------------
%: \vec{P},\vec{R}:S
%:
%: ^Dummett-1
%:
%: P_1,P_2:∃x\,Q(x) R_1,R_2,Q(y):S α β
%: -------------------------------- ----
%: P_1,P_2,R_1,R_2:S γ
%:
%: ^Dummett-2 ^Dummett-3
%:
%: P_1 P_2 R_1 R_2 [Q(y)]^1
%: ::::::::α ::::::::::::::::::β
%: ∃x\,Q(x) S P_1 P_2 R_1 R_2
%: -------------------1 ::::::::::::::::::γ
%: S S
%:
%: ^Dummett-4 ^Dummett-5
%:
\pu
$$\scalebox{0.8}{$
\begin{array}{l}
\begin{array}{lll}
\ded{Dummett-0} \\ \\
\ded{Dummett-1} \\ \\
\ded{Dummett-2} & & \ded{Dummett-3} \\
\end{array}
\\
\\
\\
\begin{array}{ccc}
\ded{Dummett-4} &\Longrightarrow & \ded{Dummett-5} \\
\end{array} \\
\end{array}
$}
$$
\newpage
{\bf A weaker rule: $∃-$}
%:
%: Γ:∃x\,A(x) Δ,A(y):C
%: ---------------------∃-
%: Γ,Δ:C
%:
%: ^DumWeak-0
%:
%: Γ:∃x\,A(x) A(y):C
%: -------------------∃--
%: Γ:C
%:
%: ^DumWeak-1
%:
%: A(y):C
%: ----------------∃---
%: ∃x\,A(x):C
%:
%: ^DumWeak--1
%:
%: P_1,P_2:∃x\,Q(x) R_1,R_2,Q(y):S
%: ---------------------------------
%: P_1,P_2,R_1,R_2:S
%:
%: ^DumWeak-2
%:
%: R_1,R_2,Q(y):S
%: --------------
%: R_1,Q(y):R_2⊸S
%: ----------------
%: P_1,P_2:∃x\,Q(x) Q(y):R_1⊸(R_2⊸S)
%: -----------------------------------∃--
%: P_1,P_2:R_1⊸(R_2⊸S)
%: -------------------
%: P_1,P_2,R_1:R_2⊸S
%: -----------------
%: P_1,P_2,R_1,R_2:S
%:
%: ^DumWeak-3
%:
%: R_1,R_2,Q(y):S
%: --------------
%: R_1,Q(y):R_2⊸S
%: ----------------
%: Q(y):R_1⊸(R_2⊸S)
%: --------------------∃---
%: P_1,P_2:∃x\,Q(x) ∃x\,Q(x):R_1⊸(R_2⊸S)
%: -------------------------------------𝐬{Cut}
%: P_1,P_2:R_1⊸(R_2⊸S)
%: -------------------
%: P_1,P_2,R_1:R_2⊸S
%: -----------------
%: P_1,P_2,R_1,R_2:S
%:
%: ^DumWeak--3
%:
\pu
\bsk
$\scalebox{0.8}{$
\begin{array}{l}
\ded{DumWeak-0} \\ \\
\ded{DumWeak-1} \\ \\
\ded{DumWeak-2} \\ \\
\ded{DumWeak-3} \\
\end{array}
$}
$
\newpage
{\bf A rule that is even weaker: $∃---$}
\bsk
$\scalebox{0.8}{$
\begin{array}{l}
\ded{DumWeak-0} \\ \\
\phantom{mmmmm}
\ded{DumWeak--1} \\ \\
\ded{DumWeak-2} \\ \\
\ded{DumWeak--3} \\
\end{array}
$}
$
\newpage
{\bf A rule that is even weaker: $∃---$ (2)}
%:
%: [R_1]^2 [R_2]^1 [Q(y)]^3
%: ::::::::::::::::::::::::::β
%: S
%: -----1
%: P_1 P_2 R_2⊸S
%: ::::::::α ----------2
%: ∃x\,Q(x) R_1⊸(R_2⊸S)
%: ----------------------------3
%: R_1 R_1⊸(R_2⊸S)
%: ---------------------------
%: R_2 R_2⊸S
%: ---------------------
%: S
%:
%: ^DumWeak--3-ND
%:
\pu
\msk
$\scalebox{0.7}{$
\begin{array}{ccc}
\cded{DumWeak--3} && \cded{Dummett-3} \\ \\ \\
\cded{DumWeak--3-ND} && \cded{Dummett-5} \\
\end{array}
$}
$
\newpage
% ____
% / ___| ___ _ _ _ __ ___ ___ ___
% \___ \ / _ \| | | | '__/ __/ _ \/ __|
% ___) | (_) | |_| | | | (_| __/\__ \
% |____/ \___/ \__,_|_| \___\___||___/
%
% «sources» (to ".sources")
{\bf Sources}
% https://ncatlab.org/nlab/show/Grothendieck+fibration#references
\cite{SeelyBeck},
\cite{SeelyLCCC},
\cite{SeelyPLC}
% (find-books "__cats/__cats.el" "seely-hyp")
% (find-books "__cats/__cats.el" "seely-lccc")
% (find-books "__cats/__cats.el" "seely-plc")
\cite{LawvereAdjFo},
\cite{LawvereEqHyp}
% (find-books "__cats/__cats.el" "lawvere-adjfo")
% (find-lawvereadjfopage 11 "A hyperdoctrine shall consist of")
% (find-lawvereadjfotext 11 "A hyperdoctrine shall consist of")
% (find-books "__cats/__cats.el" "lawvere-equahyp")
\cite{PareSchumacher}
% (find-books "__cats/__cats.el" "pare-schumacher")
\cite{Gray66}
% (find-books "__cats/__cats.el" "gray")
\cite{Jacobs}
% (find-books "__cats/__cats.el" "jacobs")
\cite{BarrWellsCTCS}
% (find-books "__cats/__cats.el" "barr-wells-ctcs")
% (find-books "__cats/__cats.el" "grothendieck-sga1")
% (find-books "__cats/__cats.el" "grothendieck-sga1" "VI. Categories fibrees")
\newpage
% ____ _ _ ____ ____ ____
% / ___| ___ ___| |_ _| | / ___/ ___/ ___|
% \___ \ / _ \/ _ \ | | | | | | | | | | |
% ___) | __/ __/ | |_| | |__| |__| |__| |___
% |____/ \___|\___|_|\__, |_____\____\____\____|
% |___/
%
% «bcc-seely-lccc» (to ".bcc-seely-lccc")
% (hypp 7 "bcc-seely-lccc")
% (hyp "bcc-seely-lccc")
% (find-books "__cats/__cats.el" "seely-lccc")
% (find-seelylcccpage (+ -32 37) "(iv) P satisfies the Beck condition:")
% (find-seelylccctext (+ -32 37) "(iv) P satisfies the Beck condition:")
% (find-TH "dednat6" "a-big-example")
% (find-dednat6 "tug-slides.tex" "BCC")
{\bf BCC in the SeelyLCCC paper}
\def\BCCL{\mathsf{BCCL}}
%D diagram BCC-Seely-LCCC-1
%D 2Dx 100 +45 +55 +45
%D 2D 100 B0 <====================== B1
%D 2D -\\ -\\
%D 2D | \\ | \\
%D 2D v \\ v \\
%D 2D +20 B2 <\\> B2' ============== B3 \\
%D 2D /\ \/ /\ \/
%D 2D +15 \\ B4 \\ B5
%D 2D \\ - \\ -
%D 2D \\ | \\|
%D 2D \\v \v
%D 2D +20 B6 <===================== B7
%D 2D
%D 2D +10 A0 |---------------------> A1
%D 2D |-> |->
%D 2D +35 A2 |--------------------> A3
%D 2D
%D ((
%D B0 .tex= h^*φ B1 .tex= φ
%D B2 .tex= k^*f^*Σ_gφ B3 .tex= g^*Σ_gφ
%D B2' .tex= h^*g^*Σ_gφ
%D B4 .tex= Σ_kh^*φ B5 .tex= Σ_gφ
%D B6 .tex= f^*Σ_gφ B7 .tex= Σ_gφ
%D B0 B1 <-| B0 B2 -> B0 B2' -> B1 B3 -> B2 B2' <-> B2' B3 <-|
%D B0 B4 |-> B1 B5 |->
%D B2 B6 <-| B3 B7 <-|
%D B6 B7 <-| B5 B7 -> .plabel= r \id
%D B4 B6 -> sl_ .plabel= l ♮ B4 B6 <- sl^ .plabel= r \BCCL
%D B0 B2' midpoint B1 B3 midpoint harrownodes nil 20 nil <-|
%D B0 B2 midpoint B4 B6 midpoint dharrownodes nil 20 nil |->
%D B1 B3 midpoint B5 B7 midpoint dharrownodes nil 20 nil <-|
%D ))
%D (( A0 .tex= D A1 .tex= C A2 .tex= A A3 .tex= B
%D A0 A1 -> .plabel= b h
%D A0 A2 -> .plabel= l k
%D A1 A3 -> .plabel= r g
%D A2 A3 -> .plabel= a f
%D A0 relplace 20 7 \pbsymbol{7}
%D ))
%D enddiagram
%
$$\pu
\diag{BCC-Seely-LCCC-1}
$$
\newpage
{\bf BCC in the SeelyLCCC paper (2)}
%D diagram BCC-Seely-LCCC-my
%D 2Dx 100 +45 +55 +45
%D 2D 100 B0 <====================== B1
%D 2D -\\ -\\
%D 2D | \\ | \\
%D 2D v \\ v \\
%D 2D +20 B2 <\\> B2' ============== B3 \\
%D 2D /\ \/ /\ \/
%D 2D +15 \\ B4 \\ B5
%D 2D \\ - \\ -
%D 2D \\ | \\|
%D 2D \\v \v
%D 2D +20 B6 <===================== B7
%D 2D
%D 2D +10 A0 |---------------------> A1
%D 2D |-> |->
%D 2D +35 A2 |--------------------> A3
%D 2D
%D ((
%D B0 .tex= h^*φ B1 .tex= φ
%D B2 .tex= k^*f^*Σ_gφ B3 .tex= g^*Σ_gφ
%D B2' .tex= h^*g^*Σ_gφ
%D B4 .tex= Σ_kh^*φ B5 .tex= Σ_gφ
%D B6 .tex= f^*Σ_gφ B7 .tex= Σ_gφ
%D
%D B0 .tex= \bsm{x\\b,a,c} B1 .tex= \bsm{x\\b,c}
%D B2 .tex= \bsm{c,x\\b,a,c} B3 .tex= \bsm{c,x\\b,c}
%D B2' .tex= \bsm{c,x\\b,a,c}
%D B4 .tex= \bsm{c,x\\b,a} B5 .tex= \bsm{c,x\\b}
%D B6 .tex= \bsm{c,x\\b,a} B7 .tex= \bsm{c,x\\b}
%D
%D B0 B1 <-| B0 B2 -> B0 B2' -> B1 B3 -> B2 B2' <-> B2' B3 <-|
%D B0 B4 |-> B1 B5 |->
%D B2 B6 <-| B3 B7 <-|
%D B6 B7 <-| B5 B7 -> .plabel= r \id
%D B4 B6 -> sl_ .plabel= l ♮ B4 B6 <- sl^ .plabel= r \BCCL
%D B0 B2' midpoint B1 B3 midpoint harrownodes nil 20 nil <-|
%D B0 B2 midpoint B4 B6 midpoint dharrownodes nil 20 nil |->
%D B1 B3 midpoint B5 B7 midpoint dharrownodes nil 20 nil <-|
%D ))
%D (( A0 .tex= D A1 .tex= C A2 .tex= A A3 .tex= B
%D A0 .tex= [b,a,c] A1 .tex= [b,c] A2 .tex= [b,a] A3 .tex= [b]
%D A0 A1 -> .plabel= b h
%D A0 A2 -> .plabel= l k
%D A1 A3 -> .plabel= r g
%D A2 A3 -> .plabel= a f
%D A0 relplace 20 7 \pbsymbol{7}
%D ))
%D enddiagram
%
$$\pu
\scalebox{0.9}{$
\diag{BCC-Seely-LCCC-my}
$}
$$
\newpage
{\bf BCC in the SeelyLCCC paper (2)}
% (nmop 2 "components")
% (nmo "components")
%:
%: φ
%: ----
%: Σ_gφ
%: -------------
%: \id:Σ_gφ→Σ_gφ φ
%: ----------------- ------------- ----
%: η=\id^♯:φ→g^*Σ_gφ h^*g^*≅k^*f^* Σ_gφ
%: -------------------- -----------------------
%: h^*η:h^*φ→h^*g^*Σ_gφ α:h^*g^*Σ_gφ→k^*f^*Σ_gφ
%: -----------------------------------------------
%: α∘h^*η:h^*φ→k^*f^*Σ_gφ
%: ----------------------------
%: ♮=(α∘h^*η)^♭:Σ_kh^*φ→f^*Σ_gφ
%:
%: ^BCC-Seely-LCCC-1
%:
$$\pu
\ded{BCC-Seely-LCCC-1}
$$
\newpage
% _____ _ _
% | ____|__ _ _ _ __ _| | | |_ _ _ __
% | _| / _` | | | |/ _` | |_| | | | | '_ \
% | |__| (_| | |_| | (_| | _ | |_| | |_) |
% |_____\__, |\__,_|\__,_|_| |_|\__, | .__/
% |_| |___/|_|
%
% «equahyp-p5» (to ".equahyp-p5")
% (hypp 10 "equahyp-p5")
% (hyp "equahyp-p5")
% (leqp 1 "reflexivity")
% (leq "reflexivity")
% (find-books "__cats/__cats.el" "lawvere-equahyp")
% (find-lawvereequahyppage 5 "reflexivity")
% (find-lawvereequahyptext 5 "reflexivity")
{\bf Lawvere EquaHyp, p.5}
%D diagram ??
%D 2Dx 100 +35 +20 +10
%D 2D 100 A0 A1 A1= A1R
%D 2D
%D 2D +25 A2 A3
%D 2D
%D 2D +15 B0 B1
%D 2D
%D ren A0 A1 A1= A1R ==> 1_X 1_XΣ(Xδ) = Θ_X
%D ren A2 A3 ==> (Xδ)·Θ_X Θ_X
%D ren B0 B1 ==> X X×X
%D
%D (( A0 A1 |-> A1= place A1R place
%D A0 A2 -> .plabel= l \text{refl}
%D A1 A3 -> .plabel= r \id
%D A0 A3 harrownodes nil 20 nil <-|
%D A2 A3 <-|
%D B0 B1 -> .plabel= a Xδ
%D ))
%D enddiagram
%D
$$\pu
\diag{??}
$$
\newpage
% «preservation-of-imp» (to ".preservation-of-imp")
% (hypp 11 "preservation-of-imp")
% (hyp "preservation-of-imp")
{\bf Preservation of `implies'}
% (find-LATEX "2008hyp-utf8.tex" "pres-of-imp")
\bsk
%D diagram pres-imp-1
%D 2Dx 100 +60 +55 +60
%D 2D 100 B0 <-> B0' <============== B1
%D 2D -/\ -/\
%D 2D | \\ | \\
%D 2D v \\ v \\
%D 2D +20 B2 <\\==================== B3 \\
%D 2D \\ \\ \\ \\
%D 2D +25 \\ B4 <===================== B5
%D 2D \\ - \\ -
%D 2D \\ | \\|
%D 2D \/v Vv
%D 2D +20 B6 B7
%D 2D
%D 2D +0 b0 |---------------------> b1
%D 2D |-> |->
%D 2D +35 b2 |--------------------> b3
%D 2D
%D ((
%D B0 .tex= f^*(P{→}Q)∧f^*P B0' .tex= f^*((P{→}Q)∧P) B1 .tex= (P{→}Q)∧P
%D B2 .tex= f^*Q B3 .tex= Q
%D B4 .tex= f^*(P{→}Q) B5 .tex= P{→}Q
%D B6 .tex= f^*P→f^*Q B7 .tex= P{→}Q
%D B0 B0' <->
%D B0' B1 <-| B0 B2 -> B0' B2 -> B1 B3 -> B2 B3 <-|
%D B0 B4 <-| B2 B6 |->
%D B1 B5 <-| B3 B7 |->
%D B4 B5 <-| B5 B7 -> .plabel= r \id
%D B4 B6 -> sl_ .plabel= l ♮ B4 B6 <- sl^ .plabel= r 𝐬P→
%D B0' B2 midpoint B1 B3 midpoint harrownodes nil 20 nil <-|
%D B0 B2 midpoint B4 B6 midpoint dharrownodes nil 20 nil |->
%D B1 B3 midpoint B5 B7 midpoint dharrownodes nil 20 nil <-|
%D ))
%D (( b0 b2 midpoint .TeX= A b1 b3 midpoint .TeX= B -> .plabel= a f
%D ))
%D enddiagram
%
$\pu
\scalebox{0.85}{$
\diag{pres-imp-1}
$}
$
% (find-lawvereequahyppage 6 "PROPOSITION (SUBSTITUTIVITY OF EQUALITY)")
% (find-lawvereequahyptext 6 "PROPOSITION (SUBSTITUTIVITY OF EQUALITY)")
%: ---------------
%: (P{→}Q)→(P{→}Q)
%: ---------------
%: (P{→}Q)∧P→Q
%: ------------------------------ -------------------
%: f^*(P{→}Q)∧f^*P↔f^*((P{→}Q)∧P) f^*((P{→}Q)∧P)→f^*Q
%: ----------------------------------------------------
%: f^*(P{→}Q)∧f^*P→f^*Q
%: ------------------------
%: ♮:f^*(P{→}Q)→(f^*P→f^*Q)
%:
%: ^pres-imp-1
%:
$$\pu
\ded{pres-imp-1}
$$
%:
%:
%: ----- ------- --------
%: ⊤∧P→P π∘Δ=\id π'∘Δ=\id
%: ------- ---------- -----------
%: ⊤→(P→P) Δ^*π^*≅\id Δ^*π'^*≅\id
%: ----------------------------------
%: ⊤→(Δ^*π^*P→Δ^*π'^*P) 𝐬P→
%: ----------------------------------------
%: ⊤→Δ^*(π^*P→π'^*P)
%: -----------------
%: Σ_Δ⊤→(π^*P→π'^*P)
%:
%: ^pres-imp-2
%:
$$\pu
\ded{pres-imp-2}
$$
\newpage
% ___ _ _ _ _
% |_ _|_ __ | |_ _ __ ___ __| |_ _ ___| |_(_) ___ _ __
% | || '_ \| __| '__/ _ \ / _` | | | |/ __| __| |/ _ \| '_ \
% | || | | | |_| | | (_) | (_| | |_| | (__| |_| | (_) | | | |
% |___|_| |_|\__|_| \___/ \__,_|\__,_|\___|\__|_|\___/|_| |_|
%
% «introduction» (to ".introduction")
% (hypp 13 "introduction")
% (hyp "introduction")
{\bf Introduction}
One of the main ideas that I tried to develop in my PhD thesis a
looong time ago was that {\sl constructions in Category Theory can be
expressed in a language that looks like Natural Deduction}. That
language turned out to be {\sl very} difficult to formalize, but it
gave rise to several spin-offs, most of them related to translating
between languages... basically, between:
\ssk
\myenumerate{
\item the internal language of a topos
\item the language of the categorical constructions in a topos
\item the internal language of the ``archetypal'' topos, $\Set$
\item the language of the categorical constructions in a hyperdoctrine
\item the languages in Bart Jacobs's book
\ssk
\item the language of a general case (``for adults'')
\item the language of a particular case (``for children'')
}
\newpage
% _ _ _ _ ____ _
% | | | |_ _ _ __ | \ | | _ \ _ __ _ _| | ___ ___
% | |_| | | | | '_ \ | \| | | | | | '__| | | | |/ _ \/ __|
% | _ | |_| | |_) | | |\ | |_| | | | | |_| | | __/\__ \
% |_| |_|\__, | .__/ |_| \_|____/ |_| \__,_|_|\___||___/
% |___/|_|
%
% «hyp-ND-rules» (to ".hyp-ND-rules")
% (hypp 7 "hyp-ND-rules")
% (hyp "hyp-ND-rules")
% See: (hyp8p 37 "hyp-subst-quant-refl")
% (hyp8 "hyp-subst-quant-refl")
{\bf hyp-ND-rules}
%
%D diagram hyp-ND-rules-fa-ex
%D 2Dx 100 +50 +50 +40 +40 +30
%D 2D 100 A0 A1 B0 B1
%D 2D
%D 2D +25 A2 A3 B2 B3
%D 2D
%D 2D +15 A4 A5 B4 B5
%D 2D
%D 2D +20 C0 C1 C2 D0 D1
%D 2D
%D 2D +25 C3 C4 C5 D2 D3
%D 2D
%D 2D +15 C6 C7 C8 D4 D5
%D 2D
%D ren A4 A5 ==> A{×}B A
%D ren B4 B5 ==> A{×}B A
%D ren C6 C7 C8 ==> A A{×}B A
%D ren D4 D5 ==> A{×}B A
%D
%D ren A0 A1 ==> P(a,b) ∃b⠆B.P(a,b)
%D ren A2 A3 ==> ∃b⠆B.P(a,b) ∃b⠆B.P(a,b)
%D
%D ren B0 B1 ==> P(a,b) ∃b⠆B.P(a,b)
%D ren B2 B3 ==> Q(a) Q(a)
%D
%D ren C0 C1 C2 ==> ∀b⠆B.R(a,b) ∀b⠆B.R(a,b) ∀b⠆B.R(a,b)
%D ren C3 C4 C5 ==> R(a,f(a)) R(a,b) ∀b⠆B.R(a,b)
%D
%D ren D0 D1 ==> Q(a) Q(a)
%D ren D2 D3 ==> R(a,b) ∀b⠆B.R(a,b)
%D
%D (( A0 A1 A2 A3 A4 A5
%D @ 0 @ 1 |->
%D @ 0 @ 2 -> .plabel= l (∃Icat)
%D @ 1 @ 3 -> .plabel= r \id
%D @ 0 @ 3 harrownodes nil 20 nil <-|
%D @ 2 @ 3 <-|
%D @ 4 @ 5 -> .plabel= a π
%D ))
%D (( B0 B1 B2 B3 B4 B5
%D @ 0 @ 1 |->
%D @ 0 @ 2 ->
%D @ 1 @ 3 ->
%D @ 0 @ 3 harrownodes nil 20 nil |-> sl__ .plabel= a (∃Ecat)
%D @ 2 @ 3 <-|
%D @ 4 @ 5 -> .plabel= a π
%D ))
%D (( C0 C1 C2 C3 C4 C5 C6 C7 C8
%D @ 0 @ 1 <-| @ 1 @ 2 <-|
%D @ 0 @ 3 -> .plabel= l (∀Ecat)
%D @ 1 @ 4 ->
%D @ 2 @ 5 -> .plabel= r \id
%D @ 0 @ 4 harrownodes nil 20 nil <-|
%D @ 1 @ 5 harrownodes nil 20 nil <-|
%D @ 3 @ 4 <-|
%D @ 4 @ 5 |->
%D @ 6 @ 7 -> .plabel= a \ang{\id,f}
%D @ 7 @ 8 -> .plabel= a π
%D ))
%D (( D0 D1 D2 D3 D4 D5
%D @ 0 @ 1 <-|
%D @ 0 @ 2 ->
%D @ 1 @ 3 ->
%D @ 0 @ 3 harrownodes nil 20 nil |-> sl__ .plabel= a (∀Icat)
%D @ 2 @ 3 |->
%D @ 4 @ 5 -> .plabel= a π
%D ))
%D enddiagram
%D
$$\pu
\scalebox{0.8}{$
\diag{hyp-ND-rules-fa-ex}
$}
$$
\newpage
{\bf hyp-ND-rules: equality}
%
%D diagram hyp-ND-rules-eq
%D 2Dx 100 +35 +35 +45
%D 2D 100 A0 A1 B0 B1
%D 2D
%D 2D +25 A2 A3 B2 B3
%D 2D
%D 2D +15 A4 A5 B4 B5
%D 2D
%D ren A4 A5 ==> A A{×}A
%D ren B4 B5 ==> A A{×}A
%D
%D ren A0 A1 ==> ⊤ a{=}a'
%D ren A2 A3 ==> a{=}a a{=}a'
%D
%D ren B0 B1 ==> P(a,a) a{=}a'∧P(a,a)
%D ren B2 B3 ==> P(a,a) P(a,a')
%D
%D (( A0 A1 A2 A3 A4 A5
%D @ 0 @ 1 |->
%D @ 0 @ 2 -> .plabel= l (=Icat)
%D @ 1 @ 3 -> .plabel= r \id
%D @ 0 @ 3 harrownodes nil 20 nil <-|
%D @ 2 @ 3 <-|
%D @ 4 @ 5 -> .plabel= a Δ
%D ))
%D (( B0 B1 B2 B3 B4 B5
%D @ 0 @ 1 |->
%D @ 0 @ 2 -> .plabel= l \id
%D @ 1 @ 3 -> .plabel= r (=Ecat)
%D @ 0 @ 3 harrownodes nil 20 nil |->
%D @ 2 @ 3 <-|
%D @ 4 @ 5 -> .plabel= a Δ
%D ))
%D enddiagram
%D
$$\pu
\diag{hyp-ND-rules-eq}
$$
\newpage
% __ ___ _
% \ \ / / |__ _ _ | |__ _ _ _ __ ___
% \ \ /\ / /| '_ \| | | | | '_ \| | | | '_ \/ __|
% \ V V / | | | | |_| | | | | | |_| | |_) \__ \
% \_/\_/ |_| |_|\__, | |_| |_|\__, | .__/|___/
% |___/ |___/|_|
%
% «why-hyperdoctrines» (to ".why-hyperdoctrines")
% (hypp 3 "why-hyperdoctrines")
% (hyp "why-hyperdoctrines")
{\bf Why hyperdoctrines?}
A hyperdoctrine is a category in which we can
interpret first-order logic (``FOL'').
($↑$ Both Sequent Calculus and Natural Deduction!)
\msk
Hyperdoctrines are hard to define (many axioms!)
Toposes are easy to define (5 axioms!)
Every topos is a hyperdoctrine (hard to prove!)
We can interpret FOL in a topos (hard!)
We can interpret FOL in a hyperdoctrine (easy!)
\msk
Hyperdoctrines are more ``modular'' than toposes
(in the sense of \cite{Jacobs}, pages 8--11).
I have some technical and personal reasons for not
liking toposes very much --- see \cite{OchsIDARCT}, sections 12, 19,
20.
% (find-books "__cats/__cats.el" "jacobs")
\newpage
% __ ___ _ ____
% \ \ / / |__ _ _ | |__ _ _ _ __ ___ |___ \
% \ \ /\ / /| '_ \| | | | | '_ \| | | | '_ \/ __| __) |
% \ V V / | | | | |_| | | | | | |_| | |_) \__ \ / __/
% \_/\_/ |_| |_|\__, | |_| |_|\__, | .__/|___/ |_____|
% |___/ |___/|_|
%
% «why-hyperdoctrines-2» (to ".why-hyperdoctrines-2")
% (hypp 4 "why-hyperdoctrines-2")
% (hyp "why-hyperdoctrines-2")
{\bf Why hyperdoctrines? (2)}
The fibration $\Cod: \Set^\dnito → \Set$ is an
archetypal hyperdoctrine.
\msk
We can use hyperdoctrines to learn Natural Deduction!
Two of the quantifier rules in Natural Deduction
have restrictions that are very technical, and that
only made sense to me when I understood their
categorical versions!!! Or, more precisely, these adjunctions:
%
$$∃ ⊣ π^* ⊣ ∀$$
What made me understand them was the concrete example
in the next page...
\newpage
% ___ _ __ _ _
% / _ \ _ _ __ _ _ __ | |_ ___ / _| ___ _ __ ___| |__ (_)
% | | | | | | |/ _` | '_ \| __/ __| | |_ / _ \| '__| / __| '_ \| |
% | |_| | |_| | (_| | | | | |_\__ \ | _| (_) | | | (__| | | | |
% \__\_\\__,_|\__,_|_| |_|\__|___/ |_| \___/|_| \___|_| |_|_|
%
% «quants-for-children» (to ".quants-for-children")
% (hypp 18 "quants-for-children")
% (hyp "quants-for-children")
{\bf Quantifiers as adjoints, for children}
\def\Lpred#1{#1}
\def\Rpred#1{#1}
\def\Lmat#1#2{\sm{#1\\#2}}
\def\Rmat#1{\sm{#1}}
A concrete example with
% $A=\{0,1,2,3,4\}$, $B=\{0,1\}$,
$X=\{0,1,2,3,4\}$, $Y=\{0,1\}$,
$P = \Lmat{00001}{00011}$, $Q = \Rmat{00111}$, $R = \Lmat{01111}{11111}$:
\msk
% (find-idarctpage 17 "13. Hyperdoctrines")
% (find-idarcttext 17 "13. Hyperdoctrines")
%D diagram quants-as-adjs-1
%D 2Dx 100 +45 +40 +45
%D 2D 100 A0 A1 B0 B1
%D 2D
%D 2D +25 A2 A3 B2 B3
%D 2D
%D 2D +25 A4 A5 B4 B5
%D 2D
%D 2D +20 A6 A7 B6 B7
%D 2D
%D ren A0 A1 ==> \Lpred{P(a,b)} \Rpred{∃b⠆B.P(a,b)}
%D ren A2 A3 ==> \Lpred{Q(a)} \Rpred{Q(a)}
%D ren A4 A5 ==> \Lpred{R(a,b)} \Rpred{∀b⠆B.R(a,b)}
%D ren A6 A7 ==> A{×}B A
%D
%D ren A0 A1 ==> \Lpred{P(x,y)} \Rpred{∃y⠆Y.P(x,y)}
%D ren A2 A3 ==> \Lpred{Q(x)} \Rpred{Q(x)}
%D ren A4 A5 ==> \Lpred{R(x,y)} \Rpred{∀y⠆Y.R(x,y)}
%D ren A6 A7 ==> X{×}Y X
%D
%D ren B0 B1 ==> \Lmat{00001}{00011} \Rmat{00011}
%D ren B2 B3 ==> \Lmat{00111}{00111} \Rmat{00111}
%D ren B4 B5 ==> \Lmat{01111}{11111} \Rmat{01111}
%D ren B6 B7 ==> A{×}B A
%D ren B6 B7 ==> X{×}Y X
%D ren B6 B7 ==> \Lmat{•••••}{•••••} \Rmat{•••••}
%D
%D (( A0 A1 A2 A3 A4 A5
%D @ 0 @ 1 |-> .plabel= a ∃
%D @ 0 @ 2 -> @ 1 @ 3 -> @ 0 @ 3 harrownodes nil 20 nil <->
%D @ 2 @ 3 <-| .plabel= a π^*
%D @ 2 @ 4 -> @ 3 @ 5 -> @ 2 @ 5 harrownodes nil 20 nil <->
%D @ 4 @ 5 |-> .plabel= a ∀
%D ))
%D (( # A6 A7 -> sl^^ .plabel= a ∃
%D # A6 A7 <- .plabel= m π
%D # A6 A7 -> sl__ .plabel= b ∀
%D A6 A7 -> .plabel= a π
%D ))
%D
%D (( B0 B1 B2 B3 B4 B5
%D @ 0 @ 1 |-> .plabel= a ∃
%D @ 0 @ 2 -> @ 1 @ 3 -> @ 0 @ 3 harrownodes nil 20 nil <->
%D @ 2 @ 3 <-| .plabel= a π^*
%D @ 2 @ 4 -> @ 3 @ 5 -> @ 2 @ 5 harrownodes nil 20 nil <->
%D @ 4 @ 5 |-> .plabel= a ∀
%D ))
%D (( # B6 B7 -> sl^^ .plabel= a ∃
%D # B6 B7 <- .plabel= m π
%D # B6 B7 -> sl__ .plabel= b ∀
%D B6 B7 -> .plabel= a π
%D ))
%D enddiagram
%D
$$\pu
\diag{quants-as-adjs-1}
$$
\newpage
% ___ _____ _ _
% / _ \ _ __ | ____| (_)_ __ ___
% | | | | '__|____| _| | | | '_ ` _ \
% | |_| | | |_____| |___| | | | | | | |
% \___/|_| |_____|_|_|_| |_| |_|
%
% «or-elim» (to ".or-elim")
{\bf Cheap and expensive or-elimination}
One of the rules of ND that people find harder to understand
is `$∨E$', that can come in several forms...
The expensive form can have undischarged hypotheses.
The cheap form discharges the only hypothesis.
%:
%:
%: [P]^1 R [Q]^1 R
%: ::::::::α :::::::::β
%: P{∨}Q S S
%: ------------------------
%: S
%:
%: ^or-E-exp-1
%:
\pu
$$\ded{or-E-exp-1}$$
\newpage
% ___ _ __ _ _ ____
% / _ \ _ _ __ _ _ __ | |_ ___ / _| ___ _ __ ___| |__ (_) |___ \
% | | | | | | |/ _` | '_ \| __/ __| | |_ / _ \| '__| / __| '_ \| | __) |
% | |_| | |_| | (_| | | | | |_\__ \ | _| (_) | | | (__| | | | | / __/
% \__\_\\__,_|\__,_|_| |_|\__|___/ |_| \___/|_| \___|_| |_|_| |_____|
%
% «quants-for-children-2» (to ".quants-for-children-2")
{\bf Quantifiers as adjoints, for children (2)}
$
%\picturedotsadef{b3} (0,0)(4,5){ 2,0 3,1 4,2 1,1 2,2 3,3 0,2 1,3 2,4 1,5 }\quad
% \picturedotsa(0,0)(4,5){ 2,0 3,1 4,2 1,1 2,2 3,3 0,2 1,3 2,4 1,5 }\quad
b
$
$
% \picturedotsadef{b4} (0,0)(5,1){ 0,0 1,1 2,0 4,0 }\quad
a
$
\newpage
% _
% / \ _ __ _ __ _____ _____
% / _ \ | '__| '__/ _ \ \ /\ / / __|
% / ___ \| | | | | (_) \ V V /\__ \
% /_/ \_\_| |_| \___/ \_/\_/ |___/
%
% «arrows» (to ".arrows")
{\bf Arrows}
$$\scalebox{3.0}{$
\begin{array}{cl}
A \monicto B & \text{monic} \\
A \ito B & \text{inclusion} \\
\end{array}
$}
$$
\newpage
% ____ _
% | _ \ _ __ ___ __| |
% | |_) | '__/ _ \/ _` |
% | __/| | | __/ (_| |
% |_| |_| \___|\__,_|
%
% «pred» (to ".pred")
% (hypp 6 "pred")
% (hyp "pred")
{\bf A category of ``predicates''}
I will use `$\ito$' to denote inclusion maps in $\Set$.
The category $\Set^\dnito$ has:
inclusions as its objects, and
commutative squares as its morphisms.
A morphism $\psm{A \\ \dnito \\ B} \diagxyto/->/^{(f,g)} \psm{C \\ \dnito \\ D}$ in $\Set^\dnito$
is a commutative square
%
%D diagram pred-c-s
%D 2Dx 100 +25
%D 2D 100 A C
%D 2D
%D 2D +25 B D
%D 2D
%D
%D (( A C -> .plabel= a f
%D B D -> .plabel= a g
%D A B `-> C D `->
%D
%D ))
%D enddiagram
%D
$\pu
\diag{pred-c-s}
$
%
in $\Set$.
\msk
The codomain functor $\Cod: \Set^\dnito → \Set$ works like this:
\msk
$\Cod ( \psm{A \\ \dnito \\ B} ) = B$,
\;
$\Cod \left( \psm{A \\ \dnito \\ B} \diagxyto/->/^{(f,g)} \psm{C \\ \dnito \\ D} \right)
\; = \; (B \diagxyto/->/^g D)$.
\newpage
% ____ _ _ _
% | _ \ _ __ ___ __| (_) ___ __ _| |_ ___ ___ _____ _____ _ __
% | |_) | '__/ _ \/ _` | |/ __/ _` | __/ _ \/ __| / _ \ \ / / _ \ '__|
% | __/| | | __/ (_| | | (_| (_| | || __/\__ \ | (_) \ V / __/ |
% |_| |_| \___|\__,_|_|\___\__,_|\__\___||___/ \___/ \_/ \___|_|
%
% «predicates-over» (to ".predicates-over")
% (hypp 7 "predicates-over")
% (hyp "predicates-over")
{\bf Predicates over a set}
I will draw the functor $\Cod: \Set^\dnito \to \Set$ as going downwards:
%D diagram pred-over-1
%D 2Dx 100 +25 +35
%D 2D 100 E P --> Q
%D 2D | - -
%D 2D | | |
%D 2D v v v
%D 2D +30 B CodP --> CodQ
%D 2D
%D ren E B ==> \Set^\dnito \Set
%D ren P Q CodP CodQ ==> \psmi{A}{B} \psmi{C}{D} B D
%D
%D (( E B -> .plabel= l \Cod
%D P Q -> .plabel= a (f,g)
%D P CodP |->
%D Q CodQ |->
%D CodP CodQ -> .plabel= a g
%D ))
%D enddiagram
%D
$$\pu
\diag{pred-over-1}
$$
I will usually omit the downward `$↦$'s:
%D diagram pred-over-2
%D 2Dx 100 +25 +35
%D 2D 100 E P --> Q
%D 2D | - -
%D 2D | | |
%D 2D v v v
%D 2D +30 B CodP --> CodQ
%D 2D
%D ren E B ==> \Set^\dnito \Set
%D ren P Q CodP CodQ ==> \psmi{A}{B} \psmi{C}{D} B D
%D
%D (( E B -> .plabel= l \Cod
%D P Q -> .plabel= a (f,g)
%D # P CodP |->
%D # Q CodQ |->
%D CodP CodQ -> .plabel= a g
%D ))
%D enddiagram
%D
$$\pu
\diag{pred-over-2}
$$
\newpage
{\bf Some standard terminology}
\ssk
(See \cite{Jacobs}, p.26, for the full definition!)
$p: \bbE → \bbB$ is a fibration (the general case),
$\Cod: \Set^\dnito→\Set$ is a fibration (our archetypal case),
%
%D diagram pred-over-3
%D 2Dx 100 +25 +35 +60
%D 2D 100 E P --> Q \labela
%D 2D | - -
%D 2D +12 | | | \labelb
%D 2D v v v
%D 2D +12 B CodP --> CodQ \labelc
%D 2D
%D ren E B ==> \Set^\dnito \Set
%D ren P Q CodP CodQ ==> \psmi{A}{B} \psmi{C}{D} B D
%D
%D (( E B -> .plabel= l \Cod
%D P Q -> .plabel= a (f,g)
%D # P CodP |->
%D # Q CodQ |->
%D CodP CodQ -> .plabel= a g
%D
%D \labela place
%D \labelb place
%D \labelc place
%D ))
%D enddiagram
%D
$$\pu
\def\labela{\text{$←$ Entire category}}
\def\labelb{\text{$←$ Projection functor}}
\def\labelc{\text{$←$ Base category}}
\diag{pred-over-3}
$$
$\psmi{A}{B}$ is an object ``over'' $B$,
$\psmi{A}{B} \diagxyto/->/<200>^{(f,g)} \psmi{C}{D}$ is a morphism
``over'' $B \ton{g} D$.
$\Cod^{-1}(B)$ is the \ColorRed{fiber} over $B$ (a category!)
\newpage
% ____ _ _
% | _ \ _ _ _ __ ___ _ __ ___ ___| |_| |_
% | | | | | | | '_ ` _ \| '_ ` _ \ / _ \ __| __|
% | |_| | |_| | | | | | | | | | | | __/ |_| |_
% |____/ \__,_|_| |_| |_|_| |_| |_|\___|\__|\__|
%
% «dummett» (to ".dummett")
% (hypp 3 "dummett")
% (hyp "dummett")
% (find-books "__logic/__logic.el" "dummett")
% (find-dummetteipage (+ 14 88) "4.1. Natural Deduction")
% (find-dummetteipage (+ 14 89) "logical rules")
{\bf Dummett}
The rules for the quantifiers in ND, from \cite{Dummett}, p.89:
%:
%: Γ:A(y) Γ:∀x\,A(x)
%: ----------∀+ ----------∀-
%: Γ:∀x\,A(x) Γ:A(t)
%:
%: ^Dum-Fa+ ^Dum-Fa-
%:
%:
%: Γ:A(y) Γ:∃x\,A(x) Δ,A(y):C
%: ----------∃+ ---------------------∃-
%: Γ:∃x\,A(x) Γ,Δ:C
%:
%: ^Dum-Ex+ ^Dum-Ex-
%:
%:
\pu
$$\scalebox{0.8}{$
\begin{array}{ccl}
\ded{Dum-Fa+} && \ded{Dum-Fa-} \\ \\
\ded{Dum-Ex+} && \ded{Dum-Ex-} \\
\end{array}
$}
$$
\msk
Let's specialize and change notation a bit...
%:
%: P(x)⊢Q(x,y) P(x)⊢∀y⠆Y.Q(x,y)
%: ----------------∀+ ----------------∀-
%: P(x)⊢∀y⠆Y.Q(x,y) P(x)⊢Q(x,f(x))
%:
%: ^Dum-Fa+.my ^Dum-Fa-.my
%:
%:
%: P(x)⊢Q(x,f(x)) P(x)⊢∃y⠆Y.Q(x,y) R(x),Q(x,f(x))⊢S(x)
%: -------------∃+ --------------------------------------∃-
%: P(x)⊢∃y⠆Y.Q(x,y) P(x),R(x)⊢S(x)
%:
%: ^Dum-Ex+.my ^Dum-Ex-.my
%:
%:
%:
\pu
$$\scalebox{0.7}{$
\begin{array}{ccl}
\ded{Dum-Fa+.my} && \ded{Dum-Fa-.my} \\ \\
\ded{Dum-Ex+.my} && \ded{Dum-Ex-.my} \\
\end{array}
$}
$$
\newpage
% {\bf Dummett (as ND)}
{\bf The rule $∃-$ in Natural Deduction}
Let's convert the hardest rule, $∃-$, to ND...
$$\ded{Dum-Ex-.my}$$
%
% (find-es "tex" "proof")
% (find-es "tex" "proof" "\\DeduceSym")
% (find-tlfile "texmf-dist/tex/latex/lkproof/proof.sty" "\\DeduceSym")
%
%:
%: P(x) \hspace{35pt}R(x) [Q(x,f(x))]^1
%: :::::::::::α :::::::::::::::::::::::::::::β
%: ∃y⠆Y.Q(x,y) \hspace{-40pt} S(x)
%: ----------------------------------∃-;1
%: S(x)
%:
%: ^Ex-ND-1
%:
%:
%:
%: P(x) R(x)
%: :::::::::::γ
%: S(x)
%:
%: ^Ex-ND-2
%:
%:
It becomes:
\pu
$$\ded{Ex-ND-1}
\Longrightarrow
\quad
\ded{Ex-ND-2}
$$
where:
%
$$\begin{array}{rcl}
α &=& P(x)⊢∃y⠆Y.Q(x,y) \\
β &=& R(x),Q(x,f(x))⊢S(x) \\
γ &=& P(x),R(x)⊢S(x) \\
\end{array}
$$
\newpage
{\bf A variant of the rule $∃-$}
Let's look at a simpler rule, called `$∃--$'.
%:
%: [Q(x,f(x))]^1
%: :::::::::::::δ
%: ∃y⠆Y.Q(x,y) S'(x) ∃y⠆Y.Q(x,y)
%: -----------------------∃--;1 :::::::::::ε
%: S'(x) S'(x)
%:
%: ^Ex-ND-3 ^Ex-ND-4
%:
%: Q(x,f(x))⊢S'(x)
%: ----------------∃--
%: ∃y⠆Y.Q(x,y)⊢S'(x)
%:
%: ^Ex-ND-5
%:
\pu
$$\scalebox{0.9}{$
\begin{array}{c}
\ded{Ex-ND-1}
\Longrightarrow
\quad
\ded{Ex-ND-2}
\\
\\
\ded{Ex-ND-3}
\quad
\Longrightarrow
\quad
\ded{Ex-ND-4}
\\
\\
\\
\ded{Ex-ND-5}
\end{array}
$}
$$
\newpage
{\bf The rules $∃-$ and $∃--$ are ``equivalent'' (1)}
%: R(x),Q(x,f(x))⊢S(x)
%: ===================
%: Q(x,f(x))⊢R(x)⊸S(x)
%: -------------------∃--
%: P(x)⊢∃y⠆Y.Q(x,y) ∃y⠆Y.Q(x,y)⊢R(x)⊸S(x)
%: --------------------------------------\text{Cut}
%: P(x)⊢R(x)⊸S(x)
%: ==============
%: P(x),R(x)⊢S(x)
%:
%: ^Dum-trans-1
%:
%: P(x)⊢∃y⠆Y.Q(x,y) Q(x,f(x))⊢S(x)
%: ---------------------------------∃-
%: P(x)⊢S(x)
%:
%: ^Dum-trans-2
%:
%: -----------------------
%: ∃y⠆Y.Q(x,y)⊢∃y⠆Y.Q(x,y) Q(x,f(x))⊢S'(x)
%: ----------------------------------------∃-
%: ∃y⠆Y.Q(x,y)⊢S'(x)
%:
%: ^Dum-trans-3
%:
\pu
$$\begin{array}{c}
\ded{Ex-ND-5} \\
\\
\ded{Dum-Ex-.my} \\
\\
\ded{Dum-trans-1} \\
\end{array}
$$
\newpage
{\bf The rules $∃-$ and $∃--$ are ``equivalent'' (2)}
making $Δ:=\{\}$ instead of $Δ:=\{R(x)\}$,
and after that $P(x):=∃y⠆Y.Q(x,y)$ and $S(x):=S'(x)$,
%
$$\scalebox{0.9}{$
\begin{array}{c}
\ded{Ex-ND-5} \\
\\
\ded{Dum-Ex-.my} \\
\\
\ded{Dum-trans-2} \\
\\
\ded{Dum-trans-3} \\
\end{array}
$}
$$
% (find-books "__logic/__logic.el" "prawitz")
% (find-prawitzpage (+ -4 20) "Restriction on the (Ex E)-rule")
% (find-books "__logic/__logic.el" "negri-vonplato")
% (find-negrivpspfpage (+ 19 64) "Quantifiers in natural deduction")
% (find-negrivpspftext (+ 19 64) "Quantifiers in natural deduction")
% (find-books "__logic/__logic.el" "gentzen")
% (find-gentzenpaperspage (+ 7 79) "The three examples of" "5 1" "as NJ-derivations")
% (find-gentzenpaperstext (+ 7 79) "The three examples of" "5 1" "as NJ-derivations")
\newpage
{\bf Predicates, visually}
% (lodp 11 "propositions-3")
% (lod "propositions-3")
\newpage
% __ __ _
% \ \ / /__ ___ __ _ _ __ _ _ ___ ___ | |_ ___
% \ \ /\ / / _ \ / __/ _` | '_ \ | | | / __|/ _ \ | __/ _ \
% \ V V / __/ | (_| (_| | | | | | |_| \__ \ __/ | || (_) |
% \_/\_/ \___| \___\__,_|_| |_| \__,_|___/\___| \__\___/
%
% «we-can-use-to» (to ".we-can-use-to")
{\bf We can use hyperdoctrines to understand:}
\msk
1. the rules for $∃$ in ND
2. some notations in \cite{Jacobs}
3. the internal language of a topos
4. polymorphism (as in Haskell; advanced)
\msk
We will do (1) and (2) in these notes.
\newpage
% _ _ _
% | |_ _ __| | __ _ _ __ ___ ___ _ __ | |_ ___
% _ | | | | |/ _` |/ _` | '_ ` _ \ / _ \ '_ \| __/ __|
% | |_| | |_| | (_| | (_| | | | | | | __/ | | | |_\__ \
% \___/ \__,_|\__,_|\__, |_| |_| |_|\___|_| |_|\__|___/
% |___/
%
% «judgments» (to ".judgments")
{\bf Judgments (for children)}
\ssk
We will interpret $a:A,b:B,P(a,b)⊢Q(a,b)$ as:
for every choice of $a∈A$,
for every choice of $b∈B$,
if $P(a,b)$ is true
then $Q(a,b)$ is true.
\msk
...or, equivalently, as:
$\setofst{(a,b)∈A×B}{P(a,b)} ⊆
\setofst{(a,b)∈A×B}{Q(a,b)}.
$
\bsk
For variants of this and lots of fun (yeah!), see:
\url{http://angg.twu.net/LATEX/2019notes-types.pdf}
(slides 14-16).
% (ntyp 14 "set-comprehensions")
% (nty "set-comprehensions")
\newpage
% _ _ _ _
% | |_ _ __| | __ _ _ __ ___ ___ _ __ | |_ ___ ___ __ _| |_
% _ | | | | |/ _` |/ _` | '_ ` _ \ / _ \ '_ \| __/ __| / __/ _` | __|
% | |_| | |_| | (_| | (_| | | | | | | __/ | | | |_\__ \ | (_| (_| | |_
% \___/ \__,_|\__,_|\__, |_| |_| |_|\___|_| |_|\__|___/ \___\__,_|\__|
% |___/
%
% «judgments-cat» (to ".judgments-cat")
% (hypp 5 "judgments-cat")
% (hyp "judgments-cat")
{\bf Judgments (for children, but categorically)}
\ssk
So $a:A,P(a)⊢Q(a)$ means
$\setofst{a∈A}{P(a)} ⊆
\setofst{a∈A}{Q(a)},
$
and this is true if and only if
we have arrows `$\diagxyto/-->/<250>$' in:
%
%D diagram j-f-c-c-1
%D 2Dx 100 +30 +30
%D 2D 100 A B
%D 2D
%D 2D +40 C
%D 2D
%D ren A B C ==> \setofst{a{∈}A}{P(a)} \setofst{a{∈}A}{Q(a)} A
%D
%D (( A B --> A C `-> B C `->
%D
%D ))
%D enddiagram
%D
%D diagram j-f-c-c-2
%D 2Dx 100 +30 +30
%D 2D 100 A B
%D 2D
%D 2D +40 C D
%D 2D
%D ren A B C D ==> \setofst{a{∈}A}{P(a)} \setofst{a{∈}A}{Q(a)} A A
%D
%D (( A B --> A C `-> B D `-> C D -> .plabel= a \id
%D
%D ))
%D enddiagram
%D
$$\pu
\scalebox{0.8}{$
\diag{j-f-c-c-1}
\qquad
\diag{j-f-c-c-2}
$}
$$
When these arrows exist they are unique.
\newpage
% ____ _ ____
% | _ \ _ __ ___ __| |___ _____ _____ _ __ |___ \
% | |_) | '__/ _ \/ _` / __| / _ \ \ / / _ \ '__| __) |
% | __/| | | __/ (_| \__ \ | (_) \ V / __/ | / __/
% |_| |_| \___|\__,_|___/ \___/ \_/ \___|_| |_____|
%
% «predicates-over-2» (to ".predicates-over-2")
% (hypp 8 "predicates-over-2")
% (hyp "predicates-over-2")
{\bf Predicates over a set (2)}
I will say that $\psmi{A}{B}$ is an object ``over'' $B$, and that
$\psmi{A}{B} \diagxyto/->/<200>^{(f,g)} \psmi{C}{D}$ is a morphism
``over'' $B \ton{g} D$.
\msk
Some standard terminology: in our particular case,
$\Cod: \Set^\dnito→\Set$ is a \ColorRed{fibration}.
$\Cod$ is the \ColorRed{projection functor}.
$\Set^\dnito$ is the \ColorRed{total category} (or the \ColorRed{entire category}).
$\Set$ is the \ColorRed{base category}.
\msk
General case (see \cite{Jacobs}, p.26, for the full definition):
$p: \bbE → \bbB$ is a \ColorRed{fibration}.
$p$ is the \ColorRed{projection functor}.
$\bbE$ is the \ColorRed{total category} (or the \ColorRed{entire category}).
$\bbB$ is the \ColorRed{base category}.
\newpage
For the general case and a formal definition see \cite{Jacobs},
page 26; he uses the notation $p: \bbE → \bbB$...
$$
\mat{ {\Set^\dnito} \\
↓ & {\hspace{-15pt}\Cod} \\
{\Set} \\
}
$$
\def\Codfibrationbody#1{
{\Set^\dnito} \\
{↓} & {\hspace{#1}\Cod} \\
{\Set} \\
}
\def\pfibrationbody#1{
{\bbE} \\
{↓} & {\hspace{#1}p} \\
{\Set} \\
}
$$\pmat{
hi \\
\Set^\dnito \\
\phantom{\Cod} \; ↓ \; \Cod \\
\Set \\
}
$$
$$\pmat{\pfibrationbody{-15pt}}$$
$$\def\b#1{\hspace{#1}}
%
\begin{array}{ccccccl}
\Set^\dnito & && \bbE & & \text{(entire category)} \\
↓ & \b{-15pt}\Cod && ↓ & \b{-12pt} p & \text{(projection functor)} \\
\Set & && \bbB & & \text{(base category)} \\
\end{array}
$$
\msk
% (find-jacobspage (+ 19 26) "p: E -> B")
The functor $\pmat{\Set^\dnito \\ ↓ & \hspace{-15pt} \Cod \\ \Set}$ is a \ColorRed{fibration}.
General case: $\pmat{\bbE \\ ↓ & \hspace{-10pt} p \\ \bbB}$
% (find-books "__cats/__cats.el" "jacobs")
The \ColorRed{fiber over} an object $B$ of the \ColorRed{base
category}
Some shorthands:
$$\pmati{\setofst{a∈A}{}}{}$$
and I will use this notation
I will draw
\newpage
% ____ _ ____
% | _ \| | / ___|
% | |_) | | | |
% | __/| |__| |___
% |_| |_____\____|
%
% «plc» (to ".plc")
% (hypp 38 "plc")
% (hyp "plc")
% (find-books "__cats/__cats.el" "seely")
% (find-seelyplcpage (+ -967 972) "1.1.2. Operators")
% (find-seelyplctext (+ -967 972) "1.1.2. Operators")
{\bf PL (1)}
$$\begin{array}[t]{rcccc}
1 &:& \Ords \\
Ω &:& \Ords \\
A &:& \Ords \\
B &:& \Ords \\
A{×}B &:& \Ords \\
A{→}Ω &:& \Ords \\
\end{array}
%
\qquad
%
\begin{array}[t]{rcccc}
⊤ &:& Ω &:& \Ords \\
ρ &:& Ω &:& \Ords \\
σ &:& Ω &:& \Ords \\
τ &:& Ω &:& \Ords \\
σ{∧}τ &:& Ω &:& \Ords \\
σ{⊸}τ &:& Ω &:& \Ords \\
β &:& B &:& \Ords \\
σ[τ/β] &:& Ω &:& \Ords \\
Σβ{∈}B·ρ &:& Ω &:& \Ords \\
Πβ{∈}B·τ &:& Ω &:& \Ords \\
\end{array}
$$
\newpage
{\bf PL (1) in another notation}
$$\begin{array}[t]{rcccc}
1 &:& Θ \\
Ω &:& Θ \\
A &:& Θ \\
B &:& Θ \\
A{×}B &:& Θ \\
A{→}Ω &:& Θ \\
\end{array}
%
\qquad
%
\begin{array}[t]{rcccc}
⊤ &:& Ω &:& Θ \\
P &:& Ω &:& Θ \\
Q &:& Ω &:& Θ \\
R &:& Ω &:& Θ \\
P{∧}Q &:& Ω &:& Θ \\
P{⊸}Q &:& Ω &:& Θ \\
b &:& B &:& Θ \\
P[b:=f(a)] &:& Ω &:& Θ \\
∃b{∈}B.P &:& Ω &:& Θ \\
∀b{∈}B.R &:& Ω &:& Θ \\
\end{array}
$$
\newpage
{\bf PL (2)}
% (find-seelyplcpage (+ -967 972) "1.1.2. Operators")
% (find-seelyplctext (+ -967 972) "1.1.2. Operators")
$$
\begin{array}[t]{rcrccccccc}
* &:& ⊤ &:& Ω &:& \Ords && ({⊤}I) \\[5pt]
%
a &:& σ &:& Ω &:& \Ords \\
b &:& τ &:& Ω &:& \Ords \\
c &:& σ{∧}τ &:& Ω &:& \Ords \\
〈a,b〉 &:& σ{∧}τ &:& Ω &:& \Ords && ({∧}I) \\
π_1c &:& σ &:& Ω &:& \Ords && ({∧}E) \\
π_2c &:& τ &:& Ω &:& \Ords && ({∧}E) \\[5pt]
%
a &:& σ &:& Ω &:& \Ords \\
b &:& τ &:& Ω &:& \Ords \\
f &:& σ{⊸}τ &:& Ω &:& \Ords \\
fa &:& τ &:& Ω &:& \Ords && ({⊸}E) \\
λx{∈}σ·b &:& σ{⊸}τ &:& Ω &:& \Ords && ({⊸}I) \\
\end{array}
$$
\newpage
{\bf PL (2) in another notation}
% (find-seelyplcpage (+ -967 972) "1.1.2. Operators")
% (find-seelyplctext (+ -967 972) "1.1.2. Operators")
$$
\begin{array}[t]{rcrccccccc}
* &:& ⊤ &:& Ω &:& Θ && ({⊤}I) \\[5pt]
%
p &:& P &:& Ω &:& Θ \\
q &:& Q &:& Ω &:& Θ \\
s &:& P{∧}Q &:& Ω &:& Θ \\
(p,q) &:& P{∧}Q &:& Ω &:& Θ && ({∧}I) \\
π_1s &:& P &:& Ω &:& Θ && ({∧}E) \\
π_2s &:& Q &:& Ω &:& Θ && ({∧}E) \\[5pt]
%
p &:& P &:& Ω &:& Θ \\
q &:& Q &:& Ω &:& Θ \\
f &:& P{⊸}Q &:& Ω &:& Θ \\
fp &:& Q &:& Ω &:& Θ && ({⊸}E) \\
λp{:}P.q &:& P{⊸}Q &:& Ω &:& Θ && ({⊸}I) \\
\end{array}
$$
\newpage
{\bf PL (3)}
% (find-seelyplcpage (+ -967 972) "1.1.2. Operators")
% (find-seelyplctext (+ -967 972) "1.1.2. Operators")
$$
\begin{array}[t]{rcrcccccl}
& & α &:& A &:& \Ords && (\text{indet}) \\
& & σ &:& Ω &:& \Ords \\
& & τ &:& A &:& \Ords \\
b &:& σ[τ/α] &:& Ω &:& \Ords \\
I(b) &:& Σα{∈}A·σ &:& Ω &:& \Ords && (ΣI) \\
I_{Σα·σ,τ}(b) &:& Σα{∈}A·σ &:& Ω &:& \Ords && (ΣI) \\[5pt]
%
a &:& σ{⊸}ρ &:& Ω &:& \Ords \\
& & α &:& A &:& \Ords && (\text{indet n.f.}) \\
𝐛Vα{∈}A·a &:& (Σα{∈}A·σ){⊸}ρ &:& Ω &:& \Ords && (ΣE) \\
\end{array}
$$
\newpage
{\bf PL (3) in another notation}
% (find-seelyplcpage (+ -967 972) "1.1.2. Operators")
% (find-seelyplctext (+ -967 972) "1.1.2. Operators")
$$
\begin{array}[t]{rcrcccccl}
& & b &:& B &:& Θ && (\text{indet}) \\
& & P(a,b) &:& Ω &:& Θ \\
& & f(a) &:& B &:& Θ \\
p &:& P(a,f(a)) &:& Ω &:& Θ \\
I(p) &:& ∃b⠆B.P(a,b) &:& Ω &:& Θ && (ΣI) \\
I_{Σα·σ,τ}(b) &:& ∃b⠆B.P(a,b) &:& Ω &:& Θ && (ΣI) \\[5pt]
%
a &:& P(a,b){⊸}Q(a) &:& Ω &:& Θ \\
& & b &:& B &:& Θ && (\text{indet n.f.}) \\
𝐛Vα{∈}A·a &:& (∃b⠆B.P(a,b)){⊸}Q(a) &:& Ω &:& Θ && (ΣE) \\
\end{array}
$$
\newpage
{\bf PL (4)}
% (find-seelyplcpage (+ -967 972) "1.1.2. Operators")
% (find-seelyplctext (+ -967 972) "1.1.2. Operators")
$$
\begin{array}[t]{rcrccccccc}
a &:& σ &:& Ω &:& \Ords \\
& & α &:& A &:& \Ords && (\text{indet n.f.}) \\
Λα{∈}A·a &:& Πα{∈}A·σ &:& Ω &:& \Ords && (ΠI) \\[5pt]
%
τ &:& α &:& A &:& \Ords \\
a &:& Πα{∈}A·σ &:& Ω &:& \Ords \\
a\{τ\} &:& σ[τ/α] &:& A &:& \Ords && (ΠE) \\
\end{array}
$$
\newpage
{\bf PL (4) in another notation}
% (find-seelyplcpage (+ -967 972) "1.1.2. Operators")
% (find-seelyplctext (+ -967 972) "1.1.2. Operators")
% (fooi "\\Ords" "Θ")
$$
\begin{array}[t]{rcrccccccc}
r &:& R(a,b) &:& Ω &:& Θ \\
& & b &:& B &:& Θ && (\text{indet n.f.}) \\
Λr &:& ∀b⠆B.R(a,b) &:& Ω &:& Θ && (ΠI) \\[5pt]
%
& & f(a) &:& B &:& Θ \\
g &:& ∀b⠆B.R(a,b) &:& Ω &:& Θ \\
g(f(a)) &:& R(a,f(a)) &:& Ω &:& Θ && (ΠE) \\
\end{array}
$$
\newpage
\def\Vpred#1#2{\cmat{#2 \\ #1}}
\def\vpred#1#2{\csm {#2 \\ #1}}
\def\hpred#1#2{\setofst{#1}{#2}}
quants-my-1:
%D diagram quants-my-1
%D 2Dx 100 +50 +50
%D 2D 100 A0 A1
%D 2D
%D 2D +30 A2 A3
%D 2D
%D 2D +30 A4 A5
%D 2D
%D 2D +20 B0 B1 B2
%D 2D
%D ren A0 A1 ==> \vpred{(a,b){∈}A{×}B}{P(a,b)} \vpred{a{∈}A}{∃b{∈}B.P(a,b)}
%D ren A2 A3 ==> \vpred{(a,b){∈}A{×}B}{Q(a)} \vpred{a{∈}A}{Q(a)}
%D ren A4 A5 ==> \vpred{(a,b){∈}A{×}B}{R(a,b)} \vpred{a{∈}A}{∀b{∈}B.R(a,b)}
%D ren B0 B1 B2 ==> A{×}B A Ω
%D
%D (( A0 A1 |->
%D A0 A2 ->
%D A1 A3 ->
%D A0 A3 harrownodes nil 20 nil <->
%D A2 A3 <-|
%D A2 A4 ->
%D A3 A5 ->
%D A2 A5 harrownodes nil 20 nil <->
%D A4 A5 |->
%D
%D B0 B1 -> .plabel= a π
%D B1 B2 -> .plabel= a χiQ
%D B0 B2 -> .slide= -10pt .plabel= m χiP
%D B0 B2 -> .slide= -15pt .plabel= b χiR
%D ))
%D enddiagram
%D
$$\pu
\diag{quants-my-1}
$$
\newpage
quants-my-2:
%D diagram quants-my-2
%D 2Dx 100 +30 +30
%D 2D 100 A0 A1
%D 2D
%D 2D +25 A2 A3
%D 2D
%D 2D +25 A4 A5
%D 2D
%D 2D +20 B0 B1 B2
%D 2D
%D ren A0 A1 ==> P ∃_πP
%D ren A2 A3 ==> π^*Q Q
%D ren A4 A5 ==> Q ∀_πQ
%D ren B0 B1 B2 ==> A{×}B A Ω
%D
%D (( A0 A1 |->
%D A0 A2 ->
%D A1 A3 ->
%D A0 A3 harrownodes nil 20 nil <->
%D A2 A3 <-|
%D A2 A4 ->
%D A3 A5 ->
%D A2 A5 harrownodes nil 20 nil <->
%D A4 A5 |->
%D
%D B0 B1 -> .plabel= a π
%D B1 B2 -> .plabel= a χiQ
%D B0 B2 -> .slide= -10pt .plabel= m χiP
%D B0 B2 -> .slide= -15pt .plabel= b χiR
%D ))
%D enddiagram
%D
$$\pu
\diag{quants-my-2}
$$
\newpage
quants-seely-1:
%D diagram quants-seely-1
%D 2Dx 100 +30 +30
%D 2D 100 A0 A1
%D 2D
%D 2D +25 A2 A3
%D 2D
%D 2D +25 A4 A5
%D 2D
%D 2D +20 B0 B1 B2
%D 2D
%D ren A0 A1 ==> ρ Σβ{∈}B·ρ
%D ren A2 A3 ==> π^*σ σ
%D ren A4 A5 ==> τ Πβ{∈}B·τ
%D ren B0 B1 B2 ==> A{×}B A Ω
%D
%D (( A0 A1 |->
%D A0 A2 ->
%D A1 A3 ->
%D A0 A3 harrownodes nil 20 nil <->
%D A2 A3 <-|
%D A2 A4 ->
%D A3 A5 ->
%D A2 A5 harrownodes nil 20 nil <->
%D A4 A5 |->
%D
%D B0 B1 -> .plabel= a π
%D B1 B2 -> .plabel= a σ
%D B0 B2 -> .slide= -10pt .plabel= m ρ
%D B0 B2 -> .slide= -15pt .plabel= b τ
%D ))
%D enddiagram
%D
$$\pu
\diag{quants-seely-1}
$$
\newpage
{\bf The rules for `$∃$' in Natural Deduction}
The rules are easier to understand and visualize
if we use bounded quantifiers and finite sets...
Bounded: $∃y⠆Y.P(x,y)$
Unbounded: $∃y.P(x,y)$
Finite sets: $X=\{1,2,3,4,5,6\}$, $Y=\{0,1,2\}$
% (find-books "__logic/__logic.el" "prawitz")
% (find-prawitzpage (+ -4 19) "The corresponding natural deduction is given below")
$\pmat{A \\ \dnito \\ B \\}
\psm {A \\ \dnito \\ B \\}
\Set^\dnito
$
$\mathsf{Cod}: \Set^\dnito \to \Set$
$\cmat{P(a) \\ a∈A} := \pmat {\setofst{a∈A}{P(a)} \\ \dnito \\ A \\}$
% (find-books "__cats/__cats.el" "jacobs")
% (find-jacobspage (+ 19 11) "Pred")
% (find-jacobspage (+ 19 27) "cartesian lifting")
% (find-jacobspage (+ 19 19) "1. Introduction to fibred category theory")
% (find-jacobspage (+ 19 19) "simple slice categories")
% (find-jacobspage (+ 19 20) "1.1. Fibrations")
% (find-jacobspage (+ 19 22) "Sets^\\to")
% (find-jacobspage (+ 19 23) "cod: Sets^\\to -> Sets")
I learned hyperdoctrines
\end{document}
% __ __ _
% | \/ | __ _| | _____
% | |\/| |/ _` | |/ / _ \
% | | | | (_| | < __/
% |_| |_|\__,_|_|\_\___|
%
% «make» (to ".make")
% (find-LATEX "2019ilha-grande-poster-a4.tex")
% (find-LATEX "2019ilha-grande-poster-a4.tex" "write-poster-body")
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
# (find-LATEXfile "2019planar-has-1.mk")
make -f 2019.mk STEM=2020hyp veryclean
make -f 2019.mk STEM=2020hyp pdf
# (hypp)
# (hypp 25)
% Local Variables:
% coding: utf-8-unix
% ee-tla: "hyp"
% End: