|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% (find-LATEX "2008natded-utf8.tex")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2008natded-utf8.tex" :end))
% (defun d () (interactive) (find-pdf-page "~/LATEX/2008natded-utf8.pdf"))
% (defun d () (interactive) (find-pdftools-page "~/LATEX/2008natded-utf8.pdf"))
% (defun e () (interactive) (find-LATEX "2008natded-utf8.tex"))
% (defun u () (interactive) (find-latex-upload-links "2008natded-utf8"))
% (defun v () (interactive) (find-2a '(e) '(d)) (g))
% (find-pdf-page "~/LATEX/2008natded-utf8.pdf")
% (find-sh0 "cp -v ~/LATEX/2008natded-utf8.pdf /tmp/")
% (find-sh0 "cp -v ~/LATEX/2008natded-utf8.pdf /tmp/pen/")
% file:///home/edrx/LATEX/2008natded-utf8.pdf
% file:///tmp/2008natded-utf8.pdf
% file:///tmp/pen/2008natded-utf8.pdf
% http://angg.twu.net/LATEX/2008natded-utf8.pdf
% (find-LATEX "2019.mk")
\documentclass[oneside,12pt]{article}
\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}
%
% (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")
%
%\usepackage[backend=biber,
% style=alphabetic]{biblatex} % (find-es "tex" "biber")
%\addbibresource{catsem-slides.bib} % (find-LATEX "catsem-slides.bib")
%
% (find-es "tex" "geometry")
\begin{document}
\catcode`\^^J=10
\directlua{dofile "dednat6load.lua"} % (find-LATEX "dednat6load.lua")
% (find-dednat6 "dednat6/block.lua" "TexLines")
\directlua{tf:processuntil(texlines:nlines())}
%\printbibliography
% «.prawitz-original» (to "prawitz-original")
% «.prawitz-proper-sub» (to "prawitz-proper-sub")
% «.quantifier-judgments» (to "quantifier-judgments")
% «.quantifier-diagrams» (to "quantifier-diagrams")
% «.names-for-adjunctions» (to "names-for-adjunctions")
% «.fol-quantifier-rules» (to "fol-quantifier-rules")
% «.dotted» (to "dotted")
% «.ex-intro» (to "ex-intro")
% «.ex-elim» (to "ex-elim")
% «.prawitz» (to "prawitz")
% «.prawitz-2» (to "prawitz-2")
% «.ex-elim-bad» (to "ex-elim-bad")
% «.notes-dtt» (to "notes-dtt")
%*
% (eedn4-51-bounded)
%:*&*\&*
Index of the slides:
\msk
% To update the list of slides uncomment this line:
\makelos{tmp.los}
% then rerun LaTeX on this file, and insert the contents of "tmp.los"
% below, by hand (i.e., with "insert-file"):
% (find-fline "tmp.los")
% (insert-file "tmp.los")
\tocline {Prawitz's example: original version} {2}
\tocline {Prawitz's example: proper subtrees} {3}
\tocline {Quantifiers: judgment rules} {4}
\tocline {Quantifiers: diagrammatic rules} {5}
\tocline {Dotted diagrams} {6}
\tocline {Names for some adjunctions} {7}
\tocline {Rules for the quantifiers} {8}
\tocline {Introduction of the existential} {9}
\tocline {Elimination of the existential} {10}
\tocline {A derivation from Prawitz} {11}
\tocline {A derivation from Prawitz (2)} {12}
\tocline {Wild notes about exist-elim} {13}
\tocline {Notes about DTT} {14}
\newpage
% --------------------
% «prawitz-original» (to ".prawitz-original")
% (s "Prawitz's example: original version" "prawitz-original")
\myslide {Prawitz's example: original version} {prawitz-original}
In [Prawitz], this example of a translation (from natural language)
is used to introduce Natural Deduction:
\bsk
An informal derivation of $∀x.∃y.(Pxy\&Qxy)$ from the two assumptions
(1) $∀x.∀y.Pxy$
(2) $∀x.∀y.(Pxy→Qxy)$
may run somewhat as follows:
From (1), we obtain:
(3) $∃y.Pay$
Let us therefore assume
(4) $Pab$.
From (2), we have:
(5) $Pab→Qab$
and from (4) and (5)
(6) $Qab$.
Hence, from (4) and (6), we obtain
(7) $Pab\&Qab$
and from (7) we get
(8) $∃y.(Pay\&Qay)$
Now, (8) is obtained from assumption (4), but the argument is
independent of the particular value of the parameter $b$ that
satisfies (4). In view of (3), we therefore have:
(9) (8) is independent of the assumption (4).
Because of (9), (8) depends only on (1) and (2) and thus holds on
these assumptions for any arbitrary value of $a$. Hence, the desired
result:
(10) $∀x.∃y.(Pxy\&Qxy)$.
\msk
The corresponding natural deduction is given below; the numerals refer
to steps in the informal argument above (rather than to the way the
assumptions are discharged).
%: \R2{∀x∀y(Pxy→Qxy)}
%: ------------------
%: ∀y(Pay→Qay)
%: -----------
%: \L4{Pab} \R5{Pab→Qab}
%: -------------------------
%: \L4{Pab} \R6{Qab}
%: ----------------------
%: \L1{∀x∃yPxy} \R7{Pab&Qab}
%: ------------ ----------------
%: \L3{∃yPay} \R8{∃y(Pay&Qay)}
%: --------------------------------
%: \R9{∃y(Pay&Qay)}
%: ---------------------
%: \R{10}{∀x∃y(Pxy&Qyx)}
%:
%: ^prawitz-p19-LR
%:
$$\def\N#1{\text{\tiny (#1)}}
\def\R#1#2{#2\hbox to 0pt{\;\;{\tiny (#1)}\hss}}
\def\L#1#2{\hbox to 0pt{\hss{\tiny (#1)}\;\;}#2}
\ded{prawitz-p19-LR}
$$
\newpage
% --------------------
% «prawitz-proper-sub» (to ".prawitz-proper-sub")
% (s "Prawitz's example: proper subtrees" "prawitz-proper-sub")
\myslide {Prawitz's example: proper subtrees} {prawitz-proper-sub}
We will use the same letters for free and bound variables, and
we'll often abbreviate `$Pab$' and `$Qab$' as just `$P$' and `$Q$'.
In our notation, with all discharges indicated, that tree becomes:
%: [a]^2 ∀a.∀b.P→Q
%: ----------------(∀𝐫E)
%: [b]^1 ∀b.P→Q
%: --------------(∀𝐫E)
%: [P]^1 P→Q
%: -------------
%: [P]^1 Q
%: ------------
%: [a]^2 ∀a.∃b.P P&Q
%: --------------(∀𝐫E) ------(∃𝐫I)
%: ∃b.P ∃b.P&Q
%: -----------------------(∃𝐫E);1
%: ∃b.P&Q
%: ---------(∀𝐫I);2
%: ∀a.∃b.P&Q
%:
%: ^prawitz-blaa-1
%:
$$\ded{prawitz-blaa-1}$$
Definition: a subtree of an ND derivation is {\und{improper}}
when it contains a bar that discharges hypotheses (say, ``$(∃𝐫E);1$''
above)
but it doesn't contain all of the leaves associated to that discharge
(in that case, $[P]^1$, $[P]^1$, and $[b]^1$).
% A subtree of a ND tree is {\sl improper} if
% it includes a bar with a discharge marker - say, ``4'' -,
% but it doesn't include some of the leaves marked ``4''
% in the original tree.
\msk
It is easy to attribute a meaning (a ``semantics'') for proper
subtrees in
which all the hypotheses and the conclusion have the same free
variables.
For example, this subtree,
%:
%: ∃b.Pab ∀b.Pab→Qab
%: ==================
%: ∃b.Pab&Qab
%:
%: ^prx-1
%:
$$\ded{prx-1}$$
corresponds to this inclusion between subsets of $A$:
$$\sst{b}{\text{$∃b.Pab$ \;\;and\;\; $∀b.Pab→Qab$}}$$
$$\subseteq \sst{b}{\text{$∃b.Pab\&Pqb$}}$$
But how do we attribute a semantics for proper subtrees where the sets
of free variables of the hypotheses and the conclusion are not all equal?
Even worse: how can we interpret hypotheses like `$b$' (or `$f(a)$'),
that are {\sl terms} (values for variables), instead of ``truths''?
This seems to make no sense in ``subset semantics''...
\bsk
To understand this we need to introduce other translations.
\newpage
% --------------------
% «quantifier-judgments» (to ".quantifier-judgments")
% (s "Quantifiers: judgment rules" "quantifier-judgments")
\myslide {Quantifiers: judgment rules} {quantifier-judgments}
In [Jacobs], sec.\ 4.1, the rules for the quantifiers for first-order logic
are stated in terms of ``judgments'', as below:
(his notation is very different, though -)
%:
%: [b]^2 Pa
%: :::::
%: a,b;Pa|-Qab Qab
%: ------------(∀𝐫I) ------(∀𝐫I);2
%: a;Pa|-∀b.Qab ∀b.Qab
%:
%: ^41.-FaI ^41.-FaI-nd
%:
%: Pa
%: :
%: a|-b a;Pa|-∀b.Qab b ∀b.Qab
%: -----------------(∀𝐫E) ----------(∀𝐫E)
%: a;Pa|-Qab Qab
%:
%: ^41.-FaE ^41.-FaE-nd
%:
%: b Pa
%: ::::
%: a|-b a;Pa|-Qab Qab
%: ----------------(∃𝐫I) ------(∃𝐫I)
%: a;Pa|-∃b.Qab ∃b.Qab
%:
%: ^41.-ExI ^41.-ExI-nd
%:
%: Pa [b]^1 [Qab]^1 Ra
%: : :::::::::::::::
%: a;Pa|-∃b.Qab a,b;Qab,Ra|-Sa ∃b.Qab Sa
%: ----------------------------(∃𝐫E) ------------------(∃𝐫E);1
%: a;Pa,Ra|-Sa Sa
%:
%: ^41.-ExE ^41.-ExE-nd
%:
$$\begin{array}{ccc}
\ded{41.-FaI} && \ded{41.-FaE} \\ \\
\ded{41.-ExI} && \ded{41.-ExE} \\ \\
\end{array}
$$
Each judgment of the form `$a;Pa \vdash Qa$' can be
understood as an inclusion $\sst{a}{Pa} \subseteq \sst{a}{Qa}$.
Judgments of the form $a \vdash b$ are functions $A \to B$
(or sections of a dependent projections, as we will see later).
\msk
In $(∀𝐫E)$ and $(∃𝐫I)$ there seems to be a missing `$b$' in
one of the hypotheses/conclusions; that $b$ is taken to be
the image of $a$ by $a \vdash b$.
\msk
Here's how to translate the ``judgment rules'' to Natural Deduction...
$$\begin{array}{c}
\ded{41.-FaI-nd} \qquad \ded{41.-FaE-nd} \\ \\ \\
\ded{41.-ExI-nd} \qquad \ded{41.-ExE-nd} \\ \\
\end{array}
$$
in the ND form the free variables of each subtree are not shown -
they must be inferred.
\newpage
% --------------------
% «quantifier-diagrams» (to ".quantifier-diagrams")
% (s "Quantifiers: diagrammatic rules" "quantifier-diagrams")
\myslide {Quantifiers: diagrammatic rules} {quantifier-diagrams}
Now let's draw these rules in a diagrammatic form:
$$\begin{array}{rcl}
\begin{array}{c}
\ded{41.-FaI} \\ \\
\ded{41.-FaE} \\ \\
\ded{41.-ExI} \\ \\
\ded{41.-ExE} \\ \\
\end{array}
& &
\begin{array}{c}
\ded{41.-FaI-nd} \qquad \ded{41.-FaE-nd} \\ \\ \\
\ded{41.-ExI-nd} \qquad \ded{41.-ExE-nd} \\ \\
\end{array}
\end{array}
$$
%D diagram quant-rules-dotted
%D 2Dx 100 +25 +20 +25 +20 +25 +20 +10 +15 +10
%D 2D 100 <--- aiP aeP <--- eiP eeP
%D 2D +15 <--- aib ∀E v <--- eib
%D 2D +15 aiQ ---> aiFbQ aeQ <--- aeFbQ eiQ ---> eiEbQ eeQ <--- eeEbQ
%D 2D +15 ∀I_1 <--- aeb ∃I \ eeb eeR
%D 2D +15 --> eeS
%D 2D
%D 2D +10 aiab |-> aia aeab |-> aea eiab |-> eia eeab |-> eea
%D 2D
%D (( aiP .tex= P
%D aib .tex= [b]^1
%D aiQ .tex= Q
%D aiFbQ .tex= ∀b.Q
%D aiab .tex= a,b
%D aia .tex= a
%D aiP aiQ .>
%D aib aiQ .>
%D aiQ aiFbQ .> .plabel= b ∀𝐫I_1
%D aiab aia |->
%D ))
%D (( aeP .tex= P
%D aeQ .tex= Q
%D aeFbQ .tex= ∀b.Q
%D aeb .tex= b
%D aeab .tex= a,b
%D aea .tex= a
%D aeP aeFbQ .>
%D aeFbQ aeQ .> .plabel= a ∀𝐫E
%D aeb aeQ .>
%D aeab aea |->
%D ))
%D (( eiP .tex= P
%D eib .tex= b
%D eiQ .tex= Q
%D eiEbQ .tex= ∃b.Q
%D eiab .tex= a,b
%D eia .tex= a
%D eiP eiQ .> eib eiQ .> eiQ eiEbQ .> .plabel= b ∃𝐫I
%D eiab eia |->
%D ))
%D (( eeP .tex= P
%D eeEbQ .tex= ∃b.Q
%D eeQ .tex= Q
%D eeR .tex= R
%D eeS .tex= S
%D eeb .tex= b
%D eeab .tex= a,b eea .tex= a
%D eeP eeEbQ .> eeEbQ eeQ .> .plabel= a ∃𝐫E eeQ eeS .> eeR eeS .>
%D eeEbQ eeb .> .plabel= l ∃𝐫E eeb eeS .>
%D eeab eea |->
%D ))
%D enddiagram
%D
$$\diag{quant-rules-dotted}$$
Each proposition will be draw over (the list of) is free variables. We
draw `$b$' over `$a$' for reasons that will be become clear later
(briefly: in the system with dependent types the type for $b$ will be
$B_a$, which depends on $a$).
\msk
\widemtos
Let's translate the example from [Prawitz] to diagrammatic form.
We get a DAG over $a,b \mto b \mto *$, and we can translate the
notion of ``proper subtree'' into a corresponding notion for DAGs.
\msk
A sub-DAG is ``proper'' when it is made of a subset of the vertices
and arrows of the original DAG (ignore the base $a,b \mto b \mto *$ -
think of it as being just the shadow of what's above it) such that:
\msk
$•$ If an arrow $(\aa \to \bb) ∈ D'$ then the vertices $\aa$ and $\bb$
belong to $D'$;
$•$ $D'$ has exactly one final node (its conclusion);
$•$ If $(\aa \mto \cc)$ and $(\bb \mto \cc)$ belong to $D$, and if
$(\aa \mto \cc) ∈ D'$,
then $(\bb \mto \cc) ∈ D'$;
$•$ If $D'$ contains a discharging arrow then it contains all the
associated
discharged nodes.
\newpage
% --------------------
% «dotted» (to ".dotted")
% (s "Dotted diagrams" "dotted")
\myslide {Dotted diagrams} {dotted}
%: [a]^2 ∀a.∀b.P→Q
%: ----------------(∀𝐫E)
%: [b]^1 ∀b.P→Q
%: --------------(∀𝐫E)
%: [P]^1 P→Q A
%: ------------- -[𝐫v]^3
%: [P]^1 Q a
%: ------------ -
%: [a]^2 ∀a.∃b.P P&Q A B
%: --------------(∀𝐫E) ------(∃𝐫I) -[𝐫v]^3 -[𝐫v]^1
%: ∃b.P ∃b.P&Q a b
%: -----------------------(∃𝐫E);1 ----------
%: ∃b.P&Q 𝐫W[P]
%: ---------(∀𝐫I);2 -----[𝐫v]^2
%: ∀a.∃b.P&Q P
%:
%: ^prawitz-bla-1 ^prawitz-bla-P
%:
$\ded{prawitz-bla-1} \kern-1em \ded{prawitz-bla-P}$
%D diagram prawitz-bla-diag1
%D 2Dx 100 +40 +40 +50
%D 2D 115 {b} {a}
%D 2D 100 P→Q <-- ∀b.P→Q <--- ∀a,∀b.P→Q
%D 2D /
%D 2D +20 / b [a]^2
%D 2D v
%D 2D +20 Q <-- P <---- ∃b.P <----- ∀a.∃b.P
%D 2D \ |
%D 2D \ |
%D 2D v v
%D 2D +40 P&Q --> ∃b.P&Q ---> ∀a.∃b.P&Q
%D 2D
%D 2D
%D 2D +20 a,b |----> a |--------> *
%D 2D
%D (( P→Q ∀b.P→Q ∀a,∀b.P→Q # 0 1 2
%D Q P ∃b.P ∀a.∃b.P # 3 4 5 6
%D P&Q ∃b.P&Q ∀a.∃b.P&Q # 7 8 9
%D @ 0 @ 1 <. .plabel= a ∀𝐫E
%D @ 1 @ 2 <. .plabel= a ∀𝐫E
%D @ 0 @ 3 .>
%D @ 3 @ 4 <. @ 4 @ 5 <. .plabel= b ∃𝐫E
%D @ 5 @ 6 <. .plabel= b ∀𝐫E
%D @ 3 @ 7 .> @ 4 @ 7 .>
%D @ 7 @ 8 .> .plabel= a ∃𝐫I
%D @ 8 @ 9 .> .plabel= a ∀𝐫I_2
%D ))
%D (( P→Q b <. ∃b.P b .> .plabel= l ∃𝐫E ∀b.P→Q [a]^2 <. ∃b.P [a]^2 <.
%D (( a,b a |-> a * |->
%D ))
%D enddiagram
%D
$$\diag{prawitz-bla-diag1}$$
\newpage
% --------------------
% «names-for-adjunctions» (to ".names-for-adjunctions")
% (s "Names for some adjunctions" "names-for-adjunctions")
\myslide {Names for some adjunctions} {names-for-adjunctions}
%D diagram names-for-adjunctions
%D 2Dx 100 +30 +30 +30
%D 2D 100 eq0 =====> eq1 aw0 =====> aw1
%D 2D - - - -
%D 2D | <--> | | <--> |
%D 2D v v v v
%D 2D +30 eq2 <===== eq3 aw2 <===== aw3
%D 2D - -
%D 2D | <--> |
%D 2D v v
%D 2D +30 aw4 =====> aw5
%D 2D
%D 2D +20 eq4 |----> eq5 aw6 |----> aw7
%D
%D (( eq0 .tex= P eq1 .tex= (b{=}b')&P
%D eq2 .tex= Q eq3 .tex= Q
%D @ 0 @ 1 =>
%D @ 0 @ 2 |-> @ 1 @ 3 |->
%D @ 2 @ 3 <=
%D @ 0 @ 3 harrownodes nil 20 nil |-> sl^ .plabel= a =^\fl
%D @ 0 @ 3 harrownodes nil 20 nil <-| sl_ .plabel= b =^\sh
%D ))
%D (( eq4 .tex= a,b eq5 .tex= a,b,b'
%D @ 0 @ 1 |->
%D ))
%D (( aw0 .tex= P aw1 .tex= ∃b.P
%D aw2 .tex= Q aw3 .tex= Q
%D aw4 .tex= R aw5 .tex= ∀b.R
%D @ 0 @ 1 =>
%D @ 2 @ 3 <=
%D @ 4 @ 5 =>
%D @ 0 @ 2 |-> @ 1 @ 3 |->
%D @ 2 @ 4 |-> @ 3 @ 5 |->
%D @ 0 @ 3 harrownodes nil 20 nil |-> sl^ .plabel= a ∃^\fl
%D @ 0 @ 3 harrownodes nil 20 nil <-| sl_ .plabel= b ∃^\sh
%D @ 2 @ 5 harrownodes nil 20 nil <-| sl^ .plabel= a ∀^\fl
%D @ 2 @ 5 harrownodes nil 20 nil |-> sl_ .plabel= b ∀^\sh
%D ))
%D (( aw6 .tex= a,b aw7 .tex= a
%D @ 0 @ 1 |->
%D ))
%D enddiagram
$$\diag{names-for-adjunctions}$$
\bsk
%D diagram names-for-adjunctions-2
%D 2Dx 100 +30 +30 +30 +30 +30
%D 2D 100 a,b <== a (a;a) <=== a{} P&Q <=== P
%D 2D - - - - - -
%D 2D | <-> | | <-> | | <-> |
%D 2D v v v v v v
%D 2D +30 c ==> b|->c (b;c) ===> b,c R ===> Q→R
%D 2D
%D (( a,b a c b|->c
%D @ 0 @ 1 <=
%D @ 0 @ 2 |-> @ 1 @ 3 |->
%D @ 2 @ 3 =>
%D @ 0 @ 3 harrownodes nil 20 nil <-| sl^ .plabel= a |->^\fl
%D @ 0 @ 3 harrownodes nil 20 nil |-> sl_ .plabel= b |->^\sh
%D ))
%D (( (a;a) a{} (b;c) b,c
%D @ 0 @ 1 <=
%D @ 0 @ 2 |-> @ 1 @ 3 |->
%D @ 2 @ 3 =>
%D @ 0 @ 3 harrownodes nil 20 nil <-| sl^ .plabel= a ×^\fl
%D @ 0 @ 3 harrownodes nil 20 nil |-> sl_ .plabel= b ×^\sh
%D ))
%D (( P&Q P R Q→R
%D @ 0 @ 1 <=
%D @ 0 @ 2 |-> @ 1 @ 3 |->
%D @ 2 @ 3 =>
%D @ 0 @ 3 harrownodes nil 20 nil <-| sl^ .plabel= a →^\fl
%D @ 0 @ 3 harrownodes nil 20 nil |-> sl_ .plabel= b →^\sh
%D ))
%D enddiagram
%D
$$\diag{names-for-adjunctions-2}$$
\newpage
% --------------------
% «fol-quantifier-rules» (to ".fol-quantifier-rules")
% (s "Rules for the quantifiers" "fol-quantifier-rules")
\myslide {Rules for the quantifiers} {fol-quantifier-rules}
%: a,b;P|-Q
%: ---------(∀𝐫I)
%: a;P|-∀b.Q
%:
%: ^41-FaI
%:
%: a;P|-∀b.Q
%: ---------(∀^\fl)
%: a|-b a;P|-∀b.Q a|-b a,b;P|-Q
%: ---------------(∀𝐫E) := --------------𝐫s
%: a;P|-Q a;P|-Q
%:
%: ^41-FaE ^41-FaE2
%:
%: ------------
%: a;∃b.Q|-∃b.Q
%: ------------(∃^\sh)
%: a|-b a,b;Q|-∃b.Q
%: ------------------𝐫s
%: a|-b a;P|-Q a;P|-Q a;Q|-∃b.Q
%: ----------------(∃𝐫I) := ---------------------∘
%: a;P|-∃b.Q a;P|-∃b.Q
%:
%: ^41-ExI ^41-ExI2
%:
%: a,b;Q,R|-S
%: ----------(→^\sh)
%: a,b;Q|-R→S
%: -----------(∃^\sh)
%: a;P|-∃b.Q a;∃b.Q|-R→S
%: ----------------------𝐫s
%: a;P|-∃b.Q a,b;Q,R|-S a;P|-R→S
%: ---------------------(∃𝐫E) := --------(→^\fl)
%: a;P,R|-S a;P,R|-S
%:
%: ^41-ExE ^41-ExE2
%:
$$\begin{array}{rcl}
\ded{41-FaI} & := & (∀^\sh) \\ \\
\ded{41-FaE} & := & \ded{41-FaE2} \\ \\
\ded{41-ExI} & := & \ded{41-ExI2} \\ \\
\ded{41-ExE} & := & \ded{41-ExE2} \\ \\
\end{array}
$$
\newpage
% --------------------
% «ex-intro» (to ".ex-intro")
% (s "Introduction of the existential" "ex-intro")
\myslide {Introduction of the existential} {ex-intro}
%D diagram 41-exi-cat
%D 2Dx 100 +30 +30
%D 2D 100 P
%D 2D -
%D 2D |
%D 2D v
%D 2D +30 {Q} <==== Q ==> {∃b.Q}
%D 2D - - -
%D 2D | <-| | <-| |
%D 2D v v v
%D 2D +30 {}∃b.Q <= ∃b.Q <== ∃b.Q{}
%D 2D
%D 2D +20 {}a |--> a,b |--> a{}
%D 2D
%D (( P # 0
%D {Q} Q {∃b.Q} # 1 2 3
%D {}∃b.Q ∃b.Q ∃b.Q{} # 4 5 6
%D {}a a,b a{} # 7 8 9
%D @ 0 @ 1 |-> .plabel= r a;Pa|-Qab
%D @ 0 @ 4 |-> .slide= -8pt .plabel= l a;Pa|-∃b.Qab
%D @ 1 @ 2 <= @ 2 @ 3 =>
%D @ 1 @ 4 |-> @ 2 @ 5 |-> @ 3 @ 6 |->
%D @ 4 @ 5 <= @ 5 @ 6 <=
%D @ 1 @ 5 harrownodes nil 20 nil <-|
%D @ 2 @ 6 harrownodes nil 20 nil <-| .plabel= a ∃^\sh
%D @ 7 @ 8 |-> .plabel= a a|-b @ 8 @ 9 |->
%D ))
%D enddiagram
%D
$$\diag{41-exi-cat}$$
%:
%: a;Pa
%: :
%: a|-b a;Pa|-Qab a;Qab
%: ----------------(∃𝐫I) --------
%: a;Pa|-∃b.Qab a;∃b.Qab
%:
%: ^41-ExI-sc ^41-ExI-nd
%:
$$\ded{41-ExI-sc} \qquad \ded{41-ExI-nd}$$
\newpage
% --------------------
% «ex-elim» (to ".ex-elim")
% (s "Elimination of the existential" "ex-elim")
\myslide {Elimination of the existential} {ex-elim}
%D diagram 41-ExE-cat
%D 2Dx 100 +30 +30 +30
%D 2D 100 P ====> P&R
%D 2D - -
%D 2D a;Pa|-∃b.Qab | |
%D 2D v |
%D 2D +30 Q&R <== Q ==> ∃b.Q |-> | a;Pa,Ra|-Sa
%D 2D a,b; - - - |
%D 2D Qab,Ra | |-> | |-> | |
%D 2D |-Sa v v v v
%D 2D +30 {}S => R→S <= R→S{} <=== S
%D 2D
%D 2D +20 {}a,b == a,b |--> a ====== a{}
%D 2D
%D (( P P&R # 0 1
%D Q&R Q ∃b.Q # 2 3 4
%D {}S R→S R→S{} S # 5 6 7 8
%D @ 0 @ 1 =>
%D @ 0 @ 4 |-> .plabel= l a;Pa|-∃b.Qab
%D @ 1 @ 8 |-> .plabel= r a;Pa,Ra|-Sa
%D @ 2 @ 3 <= @ 3 @ 4 =>
%D @ 2 @ 5 |-> .plabel= l a,b;Qab,Ra|-Sa
%D @ 3 @ 6 |-> @ 4 @ 7 |->
%D @ 5 @ 6 => @ 6 @ 7 <= @ 7 @ 8 <=
%D @ 2 @ 6 harrownodes nil 20 nil |-> .plabel= a →^\sh
%D @ 3 @ 7 harrownodes nil 20 nil |-> .plabel= a ∃^\fl
%D @ 0 @ 8 harrownodes 9 18 nil |-> .plabel= a →^\fl
%D ))
%D (( {}a,b a,b a a{}
%D @ 0 @ 1 = @ 1 @ 2 |-> @ 2 @ 3 =
%D ))
%D enddiagram
\bsk
%: a;Ra
%: ------
%: a;Pa [a,b;Qab]^1 a,b;Ra
%: : :::::
%: a;∃b.Qab a,b;Sa
%: ---------------------------(∃𝐫E);1
%: a;Sa
%:
%: ^41-ExE-nd
%:
%: a;Pa|-∃b.Qab a,b;Qab,Ra|-Sa
%: ---------------------(∃𝐫E)
%: a;Pa,Ra|-Sa
%:
%: ^41-ExE-sc
%:
In Natural Deduction:
$$\ded{41-ExE-nd}$$
In Sequent Calculus:
$$\ded{41-ExE-sc}$$
Categorically:
$$\diag{41-ExE-cat}$$
\newpage
% --------------------
% «prawitz» (to ".prawitz")
% (s "A derivation from Prawitz" "prawitz")
\myslide {A derivation from Prawitz} {prawitz}
Prawitz, p.19:
%: ∀x∀y(Pxy→Pyx)
%: -------------
%: ∀y(Pay→Pya)
%: -----------
%: Pab Pab→Pba
%: ---------------
%: Pab Pba
%: ------------
%: ∀x∃yPxy Pab&Pba
%: ------- -----------
%: ∃yPay ∃y(Pab&Pba)
%: ----------------------
%: ∃y(Pay&Pya)
%: -------------
%: ∀x∃y(Pxy&Pyx)
%:
%: ^prawitz-p19
%:
$$\ded{prawitz-p19}$$
%: [a]^3 ∀x∀y(Pxy→Pyx)
%: --------------------(∀𝐫E)
%: [b]^1 ∀y(Pay→Pya)
%: -------------------(∀𝐫E)
%: [Pab]^2 Pab→Pba
%: -------------------
%: [Pab]^2 Pba
%: ----------------
%: [a]^3 ∀x∃yPxy Pab&Pba
%: ----------------(∀𝐫E) -----------(∃𝐫I);1
%: ∃yPay ∃y(Pay&Pya)
%: ------------------------------(∃𝐫E);2
%: ∃y(Pay&Pya)
%: -------------(∀𝐫I);3
%: ∀x∃y(Pxy&Pyx)
%:
%: ^prawitz-p19-dnc
%:
$$\ded{prawitz-p19-dnc}$$
%: ∀x∀y(Pxy→Pyx)
%: -----------------(∀𝐫E)
%: a;∀y(Pay→Pya)
%: ---------------(∀𝐫E)
%: [a,b;Pab]^2 a,b;Pab→Pba
%: -------------------------
%: [a,b;Pab]^2 a,b;Pba
%: -----------------------------
%: ∀x∃yPxy a,b;Pab&Pba
%: -------(∀𝐫E) -------------(∃𝐫I);1
%: a;∃yPay a;∃y(Pay&Pya)
%: ------------------------------(∃𝐫E);2
%: a;∃y(Pay&Pya)
%: -------------(∀𝐫I);3
%: ∀x∃y(Pxy&Pyx)
%:
%: ^prawitz-p19-dnc2
%:
$$\ded{prawitz-p19-dnc2}$$
\newpage
% --------------------
% «prawitz-2» (to ".prawitz-2")
% (s "A derivation from Prawitz (2)" "prawitz-2")
\myslide {A derivation from Prawitz (2)} {prawitz-2}
%: ∀a.∀b.P→Q
%: -----------------(∀𝐫E)
%: a;∀b.P→Q
%: ---------------(∀𝐫E)
%: [a,b;P]^2 a,b;P→Q
%: -------------------------
%: [a,b;P]^2 a,b;Q
%: -----------------------------
%: ∀a.∃b.P a,b;P&Q
%: -------(∀𝐫E) -------------(∃𝐫I);1
%: a;∃b.P a;∃b.P&Q
%: ------------------------------(∃𝐫E);2
%: a;∃b.P&Q
%: -------------(∀𝐫I);3
%: ∀a.∃b.P&Q
%:
%: ^prawitz-p19-dnc3
%:
$$\ded{prawitz-p19-dnc3}$$
%: [a]^3 a|->(b|->(p|->q))
%: -----------------(∀𝐫E)
%: [a;b]^1 a;b|->(p|->q)
%: ---------------------(∀𝐫E)
%: [a,b;p]^2 a,b;p|->q
%: ----------------------(→𝐫E)
%: [a,b;p]^2 a,b;q
%: -------------------------(&𝐫I)
%: a|->b,q a,b;p,q
%: -------(∀𝐫E) --------(∃𝐫I);1
%: a;b,q a;b,p,q
%: -------------------------(∃𝐫E);2
%: a;b,p,q
%: ---------(∀𝐫I);3
%: a|->b,p,q
%:
%: ^prawitz-p19-dnc3b
%:
$$\ded{prawitz-p19-dnc3b}$$
%: ∀a.∀b.P→Q
%: ---------(∀𝐫E)
%: ∀a.∃b.P [a,b;P]^2 a;∀b.P→Q
%: -------(∀𝐫E) ::::::::::::::::::::::
%: a;∃b.P a;∃b.P&Q
%: ------------------------------(∃𝐫E);2
%: a;∃b.P&Q
%: -------------(∀𝐫I);3
%: ∀a.∃b.P&Q
%:
%: ^prawitz-p19-dnc4
%:
$$\ded{prawitz-p19-dnc4}$$
\newpage
% --------------------
% «ex-elim-bad» (to ".ex-elim-bad")
% (s "Wild notes about exist-elim" "ex-elim-bad")
\myslide {Wild notes about exist-elim} {ex-elim-bad}
What do I know about the $(∃𝐫E^\vee)$ rule from ND?
%D diagram ExE-foo
%D 2Dx 100 +35 +35 +40
%D 2D 100 a0 <== a1 ==> a2 ==> a3
%D 2D - - - -
%D 2D | |-> | |-> | |-> |
%D 2D v v v v
%D 2D +25 b0 ==> b1 <== b2 <== b3
%D 2D
%D 2D +20 c0 === c1 |-> c2 === c3
%D 2D
%D (( a0 .tex= P&Q a1 .tex= P a2 .tex= ∃b.P a3 .tex= (∃b.P)&Q
%D b0 .tex= R b1 .tex= Q→R b2 .tex= Q→R b3 .tex= R
%D c0 .tex= a,b c1 .tex= a,b c2 .tex= a c3 .tex= a
%D a0 a1 <= sl_ a0 a1 |-> sl^ .plabel= a π
%D a1 a2 => sl_ a1 a2 |-> sl^ .plabel= a {◻}
%D a2 a3 => sl_ a2 a3 <-| sl^ .plabel= a π
%D b0 b1 => b1 b2 <= b2 b3 <=
%D a0 b0 |-> a1 b1 |-> a2 b2 |-> a3 b3 |->
%D a0 b1 harrownodes nil 20 nil |->
%D a1 b2 harrownodes nil 20 nil |->
%D a2 b3 harrownodes nil 20 nil |->
%D c0 c1 = c1 c2 |-> c2 c3 =
%D ))
%D enddiagram
%D
$$\diag{ExE-foo}$$
\widemtos
We do have a map $P\&Q \mto (∃b.P)\&Q$:
%D diagram foo-Frob
%D 2Dx 100 +50 +30 +15
%D 2D 100 a0 ============> a2
%D 2D ^ ----> ^
%D 2D | / |
%D 2D - - Frob -
%D 2D +25 b0 ==> b1 <----| b2
%D 2D - - |--> -
%D 2D | \ |
%D 2D v ----> v
%D 2D +25 c0 <============ c2
%D 2D
%D 2D +15 a,b |------> a
%D 2D
%D (( a0 .tex= P a2 .tex= ∃b.P
%D b0 .tex= P&Q b1 .tex= ∃b.(P&Q) b2 .tex= (∃b.P)&Q
%D c0 .tex= Q c2 .tex= Q
%D a0 a2 => sl_ a0 a2 |-> sl^ .plabel= a {\co◻}
%D a0 b1 harrownodes 15 20 nil |->
%D a0 b0 <-| a2 b1 <-| a2 b2 <-|
%D b0 b1 => sl_
%D b0 b1 |-> sl^ .plabel= a {\co◻}
%D b1 b2 |-> sl^ .plabel= a {♮}
%D b1 b2 <-| sl_ .plabel= b 𝐫{Frob}
%D b0 c0 |-> b1 c2 |-> b2 c2 |->
%D c0 b1 harrownodes 15 20 nil |->
%D c0 c2 <= sl_ c0 c2 |-> sl^ .plabel= a {◻}
%D a,b a |->
%D ))
%D enddiagram
$$\cdiag{foo-Frob} \qquad \cdiag{ExE-foo2}$$
I don't know how to universalize the $R$, though...
Ah, make the adjunction arrows bidirectional,
and start with a pair of objects...
$((a,b;P);(a;Q))$
...and then?
%D diagram ExE-foo2
%D 2Dx 100 +45
%D 2D 100 a0 |-> a1
%D 2D - -
%D 2D | |-> |
%D 2D v v
%D 2D +25 b0 <== b1
%D 2D
%D 2D +20 c0 |-> c1
%D 2D
%D (( a0 .tex= P&Q a1 .tex= (∃b.P)&Q
%D b0 .tex= R b1 .tex= R
%D c0 .tex= a,b c1 .tex= a
%D a0 a1 |-> .plabel= a {\co◻;♮}
%D b0 b1 <= sl_ b0 b1 |-> sl^ .plabel= a {◻}
%D a0 b0 |-> a1 b1 |->
%D a0 b1 harrownodes nil 20 nil |->
%D c0 c1 |->
%D ))
%D enddiagram
%D
% $$\diag{ExE-foo2}$$
\newpage
% --------------------
% «notes-dtt» (to ".notes-dtt")
% (s "Notes about DTT" "notes-dtt")
\myslide {Notes about DTT} {notes-dtt}
Dependent types (or: ``dependent spaces''):
$a,b,c \vdash D$
\msk
Spaces of witnesses:
$a,b,c \vdash 𝐫W[P(a,b,c)]$
\msk
Sections:
$a \vdash b$
\msk
Substitutions:
%:
%: a|-b a,b,c|-D
%: --------------
%: a,c|-D
%:
%: ^2008may12-subst
%:
$\ded{2008may12-subst}$
\bsk
Arbitrary base maps
The category of display maps
Witnesses of equality
Vertical maps
\bsk
Ideas about display maps:
One-step projections
Generalized projections
The category with just the projections is a poset
Sections (monics, inverse to projections)
Diagonal maps
\bsk
We know how to attribute a semantics to proper trees
in propositional ND, but what about ND for (intuitionistic,
typed) first-order logic? Then each hypothesis, and the
conclusion, may have a different set of free variables -
and, worse, of the two hypotheses for the $(∀𝐫E)$ rule,
%: b(a) ∀b.P(a,b)
%: ----------------(∀𝐫E)
%: P(a,b(a))
%:
%: ^hyps-for-fae
%:
$$\ded{hyps-for-fae}$$
one is a value for a variable (as a term), the other is
is a proposition...
\bsk
Conjecture: my categorical inter-fiber semantics for ND can
be extented to a semantics for DTT.
Conjecture: in my semantics for inter-fiber ND trees, each
ND tree corresponds to a structure that can convert
sections (one for each hypothesis, and compatible somehow)
into a section corresponding to the final conclusion.
\end{document}
% __ __ _
% | \/ | __ _| | _____
% | |\/| |/ _` | |/ / _ \
% | | | | (_| | < __/
% |_| |_|\__,_|_|\_\___|
%
% <make>
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
# (find-LATEXfile "2019planar-has-1.mk")
make -f 2019.mk STEM=2008natded-utf8 veryclean
make -f 2019.mk STEM=2008natded-utf8 pdf
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
cp -v ~/LATEX/2008natded.tex /tmp/o
~/LUA/texcatcodes.lua -trans /tmp/o /tmp/o2
# (find-LATEXfile "2008natded-utf8.tex")
# (find-LATEXfile "2008comprcat.tex")
# (find-fline "~/LUA/texcatcodes.lua")
# (find-fline "/tmp/o2")
% Local Variables:
% coding: utf-8-unix
% ee-tla: "natd"
% End: