|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% (find-angg "LATEX/2008natded.tex")
% (find-dn4ex "edrx08.sty")
% (find-angg ".emacs.templates" "s2008a")
% (defun c () (interactive) (find-zsh "cd ~/LATEX/ && ~/dednat4/dednat41 2008natded.tex && latex 2008natded.tex"))
% (defun c () (interactive) (find-zsh "cd ~/LATEX/ && ~/dednat4/dednat41 2008natded.tex && pdflatex 2008natded.tex"))
% (eev "cd ~/LATEX/ && Scp 2008natded.{dvi,pdf} edrx@angg.twu.net:slow_html/LATEX/")
% (find-dvipage "~/LATEX/2008natded.dvi")
% (find-pspage "~/LATEX/2008natded.pdf")
% (find-zsh0 "cd ~/LATEX/ && dvips -D 300 -o 2008natded.ps 2008natded.dvi")
% (find-pspage "~/LATEX/2008natded.ps")
% (find-zsh0 "cd ~/LATEX/ && dvips -D 300 -o tmp.ps tmp.dvi")
% (find-pspage "~/LATEX/tmp.ps")
% «.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")
\documentclass[oneside]{book}
\usepackage[latin1]{inputenc}
\usepackage{edrx08} % (find-dn4ex "edrx08.sty")
%L process "edrx08.sty" -- (find-dn4ex "edrx08.sty")
\input edrxheadfoot.tex % (find-dn4ex "edrxheadfoot.tex")
\begin{document}
\input 2008natded.dnt
%*
% (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}
% Local Variables:
% coding: raw-text-unix
% ee-anchor-format: "«%s»"
% End: