% (find-angg "LATEX/2019derived-rules.tex")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2019derived-rules.tex" :end))
% (defun d () (interactive) (find-pdf-page "~/LATEX/2019derived-rules.pdf"))
% (defun d () (interactive) (find-pdftools-page "~/LATEX/2019derived-rules.pdf"))
% (defun b () (interactive) (find-zsh "bibtex 2019derived-rules; makeindex 2019derived-rules"))
% (defun e () (interactive) (find-LATEX "2019derived-rules.tex"))
% (defun u () (interactive) (find-latex-upload-links "2019derived-rules"))
% (find-xpdfpage "~/LATEX/2019derived-rules.pdf")
% (find-sh0 "cp -v  ~/LATEX/2019derived-rules.pdf /tmp/")
% (find-sh0 "cp -v  ~/LATEX/2019derived-rules.pdf /tmp/pen/")
%   file:///home/edrx/LATEX/2019derived-rules.pdf
%               file:///tmp/2019derived-rules.pdf
%           file:///tmp/pen/2019derived-rules.pdf
% http://angg.twu.net/LATEX/2019derived-rules.pdf
\documentclass[oneside]{article}
\usepackage[colorlinks]{hyperref} % (find-es "tex" "hyperref")
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{pict2e}
\usepackage[x11names,svgnames]{xcolor} % (find-es "tex" "xcolor")
%\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")
\input 2017planar-has-defs.tex    % (find-LATEX "2017planar-has-defs.tex")
%
\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




%  _                _        _         _   _    _        
% | |    ___   __ _(_) ___  (_)_ __   | | | |  / \   ___ 
% | |   / _ \ / _` | |/ __| | | '_ \  | |_| | / _ \ / __|
% | |__| (_) | (_| | | (__  | | | | | |  _  |/ ___ \\__ \
% |_____\___/ \__, |_|\___| |_|_| |_| |_| |_/_/   \_\___/
%             |___/                                      
%
% «logic-in-HAs» (to ".logic-in-HAs")
% (ph1p 14 "logic-in-HAs")

\section{Logic in a Heyting Algebra}
\label  {logic-in-HAs}

In sec.\ref{HAs} we saw a set of conditions --- called 1 to 8' ---
that characterize the ``Heyting-Algebra-ness'' of a PC-structure. It
is easy to see that Heyting-Algebra-ness, or ``HA-ness'', is
equivalent to this set of conditions:
%
$$
  \fbox{$
  \begin{array}{ll%
                rrcccc%
                cc}
  1) && ∀P.     &     (P≤P) & &       & &                   && (\id)   \\
     && ∀P,Q,R. &     (P≤R) &←& (P≤Q) &∧& (Q≤R)             && (\comp) \\[5pt]
  2) && ∀P.     &     (P≤⊤) & &       & &                   && (⊤_1)   \\
  3) && ∀Q.     &     (⊥≤Q) & &       & &                   && (⊥_1)   \\[10pt]
  6) && ∀P,Q,R. &   (P≤Q∧R) &→& (P≤Q) & &                   && (∧_1)   \\
     && ∀P,Q,R. &   (P≤Q∧R) &→&       & & (P≤R)             && (∧_2)   \\
     && ∀P,Q,R. &   (P≤Q∧R) &←& (P≤Q) &∧& (P≤R)             && (∧_3)   \\[5pt]
  7) && ∀P,Q,R. &   (P∨Q≤R) &→& (P≤R) & &                   && (∨_1)   \\
     && ∀P,Q,R. &   (P∨Q≤R) &→&       & & (Q≤R)             && (∨_2)   \\
     && ∀P,Q,R. &   (P∨Q≤R) &←& (P≤R) &∧& (Q≤R)             && (∨_3)   \\[5pt]
  8) && ∀P,Q,R. & (P≤Q{→}R) &→& \multicolumn{3}{l}{(P∧Q≤R)} && (→_1)   \\
     && ∀P,Q,R. & (P≤Q{→}R) &←& \multicolumn{3}{l}{(P∧Q≤R)} && (→_2)   \\
  \end{array}
  $}
$$
%
We omitted the conditions 4 and 5, that defined `$↔$' and `$¬$' in
terms of the other operators. The last column of the table gives a
name to each of these new conditions.

These new conditions let us put (some) proofs about HAs in tree form,
as we shall see soon.

\def\t{\text}

\msk

Let us introduce two new notations. The first one,
$$(\t{expr})\subst{v_1 := \t{repl}_1 \\ v_2 := \t{repl}_2}$$ indicates
simultaneous substitution of all (free) occurrences of the variables
$v_1$ and $v_2$ in expr by the replacements $\t{repl}_1$ and
$\t{repl}_2$. For example,
%
$$((x+y)·z) \subst{ 
    x:=a+y \\
    y:=b+z \\
    z:=c+x \\
  }
  \;\;=\;\;
  ((a+y)+(b+z))·(c+x).
$$

The second is a way to write `$→$'s as horizontal bars. In
%:
%:                                           L   M
%:                                    -\ee   -----\zeta
%:  A  B  C     E  F     H            K        N         O
%:  -------\aa  ----\bb  -\gg  -\dd   --------------------\eta
%:     D         G       I     J               P
%:
%:     ^t1       ^t2     ^t3   ^t4             ^t5
%:
$$\pu
  \ded{t1} \qquad \ded{t2} \qquad \ded{t3} \qquad \ded{t4} \qquad \ded{t5}
$$
%
the trees mean:
%
\begin{itemize}
\item if $A$, $B$, $C$ are true then $D$ is true (by $\aa$),

\item if $E$, $F$, are true then $G$ is true (by $\bb$),

\item if $H$ is true then $I$ is true (by $\gg$),

\item $J$ is true (by $\dd$, with no hypotheses),

\item $K$ is true (by $\ee$); if $L$ and $M$ then $N$ (by $\zeta$);
  if $K$, $N$, $O$, then $P$ (by $\eta$); combining all this we get a
  way to prove that if $L$, $M$, $O$, then $P$,
\end{itemize}
%
where $\aa, \bb, \gg, \dd, \ee, \zeta, \eta$ are usually names
of rules.

\msk

The implications in the table in the beginning of this section can be
rewritten as ``tree rules'' as:
%:
%:             P≤Q  Q≤R
%:   ----\id   ---------\comp    -----⊤_1    -----⊥_1
%:   P≤P         P≤R            P≤⊤        ⊥≤Q
%:
%:    ^id         ^comp           ^T1       ^B1
%:
%:   P≤Q∧R      P≤Q∧R      P≤Q  P≤R
%:   ------∧_1  ------∧_2  -----------∧_3
%:    P≤Q        P≤R         P≤Q∧R
%:
%:    ^and1      ^and2        ^and3
%:
%:   P∨Q≤R      P∨Q≤R      P≤R  Q≤R
%:   ------∨_1  ------∨_2  -----------∨_3
%:    P≤R        Q≤R         P∨Q≤R
%:
%:    ^or1       ^or2         ^or3
%:
%:
%:    P≤Q{→}R         P∧Q≤R
%:    ---------→_1   ---------→_2
%:    P∧Q≤R          P≤Q{→}R
%:
%:     ^imp1           ^imp2
%:
{
\pu
$$\ded{id} \qquad \ded{comp} \qquad \ded{T1} \qquad \ded{B1}$$

$$\ded{and1} \qquad \ded{and2} \qquad \ded{and3}$$

$$\ded{or1} \qquad \ded{or2} \qquad \ded{or3}$$

$$\ded{imp1} \qquad \ded{imp2}$$

}

\msk

Note that the `$∀P,Q,R∈Ω$'s are left implicit in the tree rules, which
means that {\sl every substitution instance of the tree rules hold};
sometimes --- but rarely --- we will indicate the substitution
explicitly, like this,
%:
%:    P≤Q{→}R         P∧Q≤R
%:    ---------→_1   ---------→_2
%:    P∧Q≤R          P≤Q{→}R
%:
%:     ^imp1           ^imp2
%:
%:    P∧(P{→}⊥)≤⊥
%:   ------------------→_2\su
%:   P≤((P{→}⊥){→}⊥)
%:
%:     ^foo
%:
$$\pu
  \def\su{\bsm{Q:=P{→}⊥ \\ R:=⊥}}
  %
  \begin{array}{rcl}
    \left(\cded{imp2}\right) \su &\squigto& {\def\su{} \cded{foo}} \\\\
    (→_2)\su  &\squigto& \cded{foo} \\
  \end{array}
$$
%
Usually we will only say `$→_2$' instead of `$→_2\bsm{Q:=P{→}⊥
  \\ R:=⊥}$' at the right of a bar, and the task of discovering which
substitution has been used is left to the reader.

\msk

The tree rules can be composed in a nice visual way. For example,
this tree --- let's call it $({∧}{∧})$,
%:
%:  ---------\id               ---------\id
%:  P∧Q≤P∧Q                    P∧Q≤P∧Q
%:  ---------∧_1               ---------∧_2
%:   P∧Q≤P         P≤R          P∧Q≤Q       Q≤S
%:   ------------------\comp    ------------------\comp
%:      P∧Q≤R                        P∧Q≤S
%:      ------------------------------------∧_3
%:                    P∧Q≤R∧S
%:
%:                     ^foo
%:
$$\pu
  \ded{foo}
$$
%
``is'' a proof for:
%
%$$∀P,Q,R,S∈Ω.\; (P ≤_H R)∧(Q ≤_H S) → ((P ∧_H Q) ≤_H (R ∧_H S)).$$
%
$$∀P,Q,R,S∈Ω.\; (P ≤ R)∧(Q ≤ S) → ((P ∧ Q) ≤ (R ∧ S)).$$

We can perform substitutions on trees, and the notation will be the
same as for tree rules: for example, $({∧}{∧}) \subst{S:=P∧Q}$.




%  ____            _               _              _           
% |  _ \  ___ _ __(_)_   _____  __| |  _ __ _   _| | ___  ___ 
% | | | |/ _ \ '__| \ \ / / _ \/ _` | | '__| | | | |/ _ \/ __|
% | |_| |  __/ |  | |\ V /  __/ (_| | | |  | |_| | |  __/\__ \
% |____/ \___|_|  |_| \_/ \___|\__,_| |_|   \__,_|_|\___||___/
%                                                             
\subsection{Derived rules}

\def\Hs{\{H_1, \ldots, H_n\}}

Let be $𝐬{HAT}$ the set of ``Heyting Algebra rules in tree form'' from
the last section:
%
$$𝐬{HAT} = \{(\id), \ldots, (→_2)\}.$$

Let's see a way to treat $𝐬{HAT}$ as a deductive system.

If $𝐬S$ is a set of tree rules, we will write:

\begin{itemize}

\item $𝐬{Trees}(𝐬S)$ for the set of all trees whose bars are all
  substituion instances of rules in $𝐬S$,

\item $𝐬{Trees}(𝐬S, \Hs)$ for the set of all trees in $𝐬{Trees}(𝐬S)$
  whose hypotheses are contained in the set $\{H_1, \ldots, H_n\}$,
  and

\item $𝐬{Trees}(𝐬S, \Hs, C)$ for the set of trees in $𝐬{Trees}(𝐬S,
  \Hs)$ having $C$ as their conclusion.

\end{itemize}

When the set $𝐬S$ is clear from the context, we write
%:
%:  H_1  \ldots  H_n
%:  ================
%:       C
%:
%:       ^fooC
%:
$$\pu
  \ded{fooC}
$$
%
to mean: {\sl we know} a tree in $𝐬{Trees}(𝐬S, \Hs, C)$, and this is
an abbreviation for it. I like to think of the double bar as the
bellows of a closed accordion: we can see the keys at both sides, but
not the drawings painted on the folded part of the pleated cloth.

The notation that defines a {\sl derived rule} is ``\textsl{newrule
  $:=$ expansion}'', where \textsl{expansion} is a tree in
$𝐬{Trees}(𝐬S, \Hs, C)$ and \textsl{newrule} is a bar with hypotheses
$H_1, \ldots, H_n$ and conclusion $C$, written with a single bar with
a (new) rule name, instead of with a double bar. For example, this is
a version of Modus Ponens for Heyting Algebras:
%:
%:                                          ---------\id    
%:                        P≤Q{→}R  P≤Q      Q{→}R≤Q{→}R     
%:                        ------------∧_3   ----------→_1
%:  P≤Q  P≤Q{→}R          P≤(Q{→}R){∧}Q    (Q{→}R){∧}Q≤R
%:  ------------\MP  :=   --------------------------\comp
%:      P≤R                         P≤R
%:
%:      ^MPL                         ^MPR
%:
\pu
$$\ded{MPL} \quad := \quad \ded{MPR}$$

After the definition of a derived rule --- say, ``$D_1 := E_1$'' ---
the set of allowed tree rules that is implicit from the context is
increased, with $D_1$ being added to it; when we define another
derived rule, $D_2 := E_2$, its expansion $E_2$ can have bars that are
substitution instances of $D_1$. After adding more derived rules, $D_3
:= E_3$, $\ldots$, $D_n := E_n$, we can use all the new rules $D_1,
\ldots, D_n$ in our trees --- and we have a way to remove all the
derived rules from our trees! Take a tree $T∈𝐬{Trees}(𝐬S∪\{D_1,
\ldots, D_n\})$; replace each substitution instance of $D_n$ in it by
its expansion, then replace every substitution instance of $D_{n-1}$
in the new tree by its expansion, and so on; after replacing all
substitution instances of $D_1$ we get a tree in $𝐬{Trees}(𝐬S)$, with
the same hypotheses and the same conclusion as the original $T$.

We want to add these other derived rules:
%:
%:                   -------\id
%:                   Q∧R≤Q∧R
%:   ------∧E_1 :=   -------∧_1
%:   Q∧R≤Q           Q∧R≤Q
%:
%:   ^and4a           ^and4b
%:
%:
%:                   ---------\id
%:                   Q∧R≤Q∧R
%:   ------∧E_2  :=  ---------∧_2
%:   Q∧R≤R           Q∧R≤R
%:
%:   ^and5a           ^and5b
%:
%:                   ---------\id
%:                   P∨Q≤P∨Q
%:   ------∨I_1  :=  ---------∨_1
%:   P≤P∨Q           P≤P∨Q
%:
%:   ^or4a            ^or4b
%:
%:                   ---------\id
%:                   P∨Q≤P∨Q
%:   ------∨I_2  :=  ---------∨_2
%:   Q≤P∨Q           Q≤P∨Q
%:
%:   ^or5a            ^or5b
%:
%:  
%:                        P∧R≤S     Q∧R≤S 
%:                        -----→_2  -----→_2 
%:                        P≤R→S     Q≤R→S 
%:                        ---------------∨_3 
%:  P∧R≤S  Q∧R≤S            P∨Q≤R→S    
%:  ------------∨E   :=     ---------→_1  
%:    (P∨Q)∧R≤R             (P∨Q)∧R≤R  
%:
%:       ^orE1               ^orE2
%:

\pu
$$\begin{array}{rcl}
  \ded{and4a} &:=& \ded{and4b}    \\\\
  \ded{and5a} &:=& \ded{and5b}    \\\\
  \ded{or4a}  &:=& \ded{or4b}     \\\\
  \ded{or5a}  &:=& \ded{or5b}     \\\\
  \ded{orE1}  &:=& \ded{orE2}     \\\\
  \end{array}
$$



%  _   _       _                   _       _          _ 
% | \ | | __ _| |_ _   _ _ __ __ _| |   __| | ___  __| |
% |  \| |/ _` | __| | | | '__/ _` | |  / _` |/ _ \/ _` |
% | |\  | (_| | |_| |_| | | | (_| | | | (_| |  __/ (_| |
% |_| \_|\__,_|\__|\__,_|_|  \__,_|_|  \__,_|\___|\__,_|
%                                                       

\subsection{Natural deduction}

The system $𝐬{HAT}$ with all the derived rules of the last section
added to it will be called $𝐬{HAND}$:
%
$$𝐬{HAND} = \{(\id), \ldots, (→_2), (\MP), \ldots, (∨E))\}$$

Trees in Natural Deduction for IPL can be translated into $𝐬{HAND}$ by
a method that we will sketch below. Note that this section is not
self-contained --- it should be regarded as an introduction to
\cite{NegriVonPlato}.

\msk

This is an example of a tree in Natural Deduction:
%
% (ntyp 46 "ND-3")
% (nty     "ND-3")
%
%:   [P]^1  P{→}Q       [P]^1  P{→}R   
%:   ------------(→E)   ------------(→E)
%:         Q                 R
%:         -------------------(∧I)
%:             Q{∧}R
%:          -----------(→I);1
%:          P{→}(Q{∧}R)
%:
%:          ^ND-1
%:
\pu
$$\ded{ND-1}$$
%
The ``;1'' in its last bar means: below this point the hypotheses
marked with `$[\,·\,]^1$' are ``discharged'' from the list of
hypotheses. Each subtree of a ND tree with undischarged hypotheses
$H_1, \ldots, H_n$ and conclusion $C$ will be interpreted as {\sl
  some} tree in $𝐬{HAND}$ with no hypotheses and conclusion
$H_1∧\ldots∧H_n≤C$ --- there are usually several possible choices. So:
%:
%:   P  P{→}Q
%:   --------   ==>   -----------\MP
%:      Q             P∧(P{→}Q)≤Q
%:
%:      ^a1            ^a2
%:
%:   P  P{→}R    
%:   --------   ==>   -----------\MP
%:      R             P∧(P{→}R)≤R
%:
%:      ^b1            ^b2
%:
%:   Q   R          
%:   -----      ==>   -----------\id
%:   Q{∧}R            Q{∧}R≤Q{∧}R
%:
%:     ^c1             ^c2
%:
%:   P  P{→}Q       P  P{→}R   
%:   --------       --------    
%:      Q              R          
%:      ----------------           ==>  =========================
%:             Q{∧}R                    ((P{→}R)∧(P{→}Q))∧P≤Q{∧}R
%:
%:              ^d1                       ^d2
%:
%:   [P]^1  P{→}Q       [P]^1  P{→}R   
%:   ------------       ------------    
%:         Q                 R
%:         -------------------            =========================
%:             Q{∧}R                      ((P{→}R)∧(P{→}Q))∧P≤Q{∧}R
%:          -----------(→I);1      ==>    -------------------------→_2
%:          P{→}(Q{∧}R)                   (P{→}R)∧(P{→}Q)≤P{→}Q{∧}R
%:
%:          ^e1                            ^e2
%:
\pu
$$\def\becomes{\Longrightarrow}
  \begin{array}{rcl}
  \ded{a1} &\becomes& \ded{a2} \\ \\
  \ded{b1} &\becomes& \ded{b2} \\ \\
  \ded{c1} &\becomes& \ded{c2} \\ \\
  \ded{d1} &\becomes& \ded{d2} \\ \\
  \ded{e1} &\becomes& \ded{e2} \\
  \end{array}
$$

The ND rules that are difficult to understand and difficult to
translate are the ones that involve discharges: `$(→I)$', that appears
above, and `$(∨E)$':
%:        
%:        [P]^1  R     [Q]^1  R
%:        ::::::::T_1  ::::::::T_2      =====T_1  =====T_2
%:   P∨Q      S           S             P∧R≤S     Q∧R≤S
%:   ----------------------(∨E)         ---------------∨E
%:              S                          (P∨Q)∧R≤S
%:
%:              ^oE1                        ^oE2
%:
\pu
$$\def\becomes{\Longrightarrow}
  \begin{array}{rcl}
  \ded{oE1} &\becomes& \ded{oE2} \\
  \end{array}
$$
%
Note that the derived rule $∨E$ is used to combine the translations of
the subtrees $T_1$ and $T_2$ into a translation of the whole ND tree.

My suggestion for the readers that are seeing this for the first time
is: start by translating the ND tree below to a tree in $𝐬{HAND}$, and
then to a tree in $𝐬{HAT}$; then read the relevant parts of
\cite{NegriVonPlato} to see how they would do that translation.
%

% (find-books "__logic/__logic.el" "negri-vonplato")
% (find-books "__logic/__logic.el" "van_dalen")
% (find-xpdfpage "~/LATEX/2017distributivity.pdf")
% (find-LATEXfile "2017distributivity.tex" "fails in some way")
%:            
%:                         (P∨Q)∧R                (P∨Q)∧R   
%:                         -------(∧E_2)          -------(∧E_2)  
%:                  [P]^1    R             [Q]^1     R       
%:                  ----------(∧I)         -----------(∧I)       
%:  (P∨Q)∧R            P∧R                    Q∧R       
%:  -------(∧E_1)   ------------(∨I_1)   -----------(∨I_2)
%:    P∨Q           (P∧R)∨(Q∧R)          (P∧R)∨(Q∧R)  
%:    ----------------------------------------------(∨E);1
%:          (P∧R)∨(Q∧R)
%:  
%:          ^distr-weird-1
%:  
$$\pu
  \ded{distr-weird-1}
$$















\end{document}

% Local Variables:
% coding: utf-8-unix
% ee-tla: "dru"
% End:
