% (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:
