% (find-angg "LATEX/2016-2-LA-logic.tex")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2016-2-LA-logic.tex"))
% (defun d () (interactive) (find-xpdfpage "~/LATEX/2016-2-LA-logic.pdf"))
% (defun e () (interactive) (find-LATEX "2016-2-LA-logic.tex"))
% (defun u () (interactive) (find-latex-upload-links "2016-2-LA-logic"))
% (find-xpdfpage "~/LATEX/2016-2-LA-logic.pdf")
% (find-sh0 "cp -v  ~/LATEX/2016-2-LA-logic.pdf /tmp/")
% (find-sh0 "cp -v  ~/LATEX/2016-2-LA-logic.pdf /tmp/pen/")
%   file:///home/edrx/LATEX/2016-2-LA-logic.pdf
%               file:///tmp/2016-2-LA-logic.pdf
%           file:///tmp/pen/2016-2-LA-logic.pdf
% http://angg.twu.net/LATEX/2016-2-LA-logic.pdf
%
% «.classical-logic»		(to "classical-logic")
% «.3-valued-logic»		(to "3-valued-logic")
% «.tautologies»		(to "tautologies")
% «.logics-as-objects»		(to "logics-as-objects")
% «.ZHA-logic»			(to "ZHA-logic")
% «.connectives»		(to "connectives")
% «.C-H-diagram-defs»		(to "C-H-diagram-defs")
% «.C-H-diagram»		(to "C-H-diagram")
% «.HAs-and-CCCs»		(to "HAs-and-CCCs")
% «.derived-rules»		(to "derived-rules")

% (find-LATEXsh "grep lao162p 2016-2-LA-logic.tex")


\documentclass[oneside]{book}
\usepackage[colorlinks]{hyperref} % (find-es "tex" "hyperref")
%\usepackage[latin1]{inputenc}
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{tikz}
%
\usepackage{edrx15}               % (find-angg "LATEX/edrx15.sty")
\input edrxaccents.tex            % (find-angg "LATEX/edrxaccents.tex")
\input edrxchars.tex              % (find-LATEX "edrxchars.tex")
\input edrxheadfoot.tex           % (find-dn4ex "edrxheadfoot.tex")
%
\usepackage{proof}   % For derivation trees ("%:" lines)
\input diagxy        % For 2D diagrams ("%D" lines)
\xyoption{curve}     % For the ".curve=" feature in 2D diagrams
%
\begin{document}

\catcode`\^^J=10
\directlua{dednat6dir = "dednat6/"}
\directlua{dofile(dednat6dir.."dednat6.lua")}
\directlua{texfile(tex.jobname)}
\directlua{verbose()}
\directlua{output(preamble1)}
\def\expr#1{\directlua{output(tostring(#1))}}
\def\eval#1{\directlua{#1}}
\def\pu{\directlua{pu()}}

% \directlua{dofile "edrxtikz.lua"} % (find-LATEX "edrxtikz.lua")
% %L V.__tostring = function (v) return format("(%.3f,%.3f)", v[1], v[2]) end

\def\und#1#2{\underbrace{#1}_{#2}}
\def\und#1#2{\underbrace{#1}_{\textstyle #2}}
\def\subf#1{\underbrace{#1}_{}}
\def\p{\phantom{(}}

\def\cur{\operatorname{cur}}
\def\uncur{\operatorname{uncur}}
\def\app{\operatorname{app}}
\def\ren{\operatorname{ren}}

\def∧{\&}

\def\namedfunction#1#2#3#4#5{
  \begin{array}{rrcl}
    #1: & #2 & → & #3 \\
        & #4 & ↦ & #5 \\
  \end{array}
  }






%  ____                 _                _   _             _      
% |___ \    __   ____ _| |_   _  ___  __| | | | ___   __ _(_) ___ 
%   __) |___\ \ / / _` | | | | |/ _ \/ _` | | |/ _ \ / _` | |/ __|
%  / __/_____\ V / (_| | | |_| |  __/ (_| | | | (_) | (_| | | (__ 
% |_____|     \_/ \__,_|_|\__,_|\___|\__,_| |_|\___/ \__, |_|\___|
%                                                    |___/        
%
% «classical-logic» (to ".classical-logic")
% (lao162p 1 "classical-logic")

{\bf Classical logic}

\ssk

Idea:

0 means ``false''

1 means ``true''

\msk

Operations:

\ssk

$\begin{array}[t]{ccllll}
  P & Q & P∧Q   & P∨Q   & P→Q   & P↔Q   \\ \hline
  0 & 0 & 0∧0=0 & 0∨0=0 & 0→0=1 & 0↔0=1 \\
  0 & 1 & 0∧1=0 & 0∨1=1 & 0→1=1 & 0↔1=0 \\
  1 & 0 & 1∧0=0 & 1∨0=1 & 1→0=0 & 1↔0=0 \\
  1 & 1 & 1∧1=1 & 1∨1=1 & 1→1=1 & 1↔1=1 \\
  \end{array}
  %
  \qquad
  %
  \begin{array}[t]{ll}
  P & ¬P \\ \hline
  0 & ¬0=1 \\
  1 & ¬1=0 \\
  \end{array}
$

\msk

We will use a more compact form.

\ssk

If $P=1$ and $Q=0$, then

$\und{\und P 1 → \und Q 0} 0$

So:

\msk

$\begin{array}[t]{ccccccc}
  P & Q & P∧Q & P∨Q & P→Q & P↔Q \\ \hline
  0 & 0 &  0   &  0  &  1   &  1  \\
  0 & 1 &  0   &  1  &  1   &  0  \\
  1 & 0 &  0   &  1  &  0   &  0  \\
  1 & 1 &  1   &  1  &  1   &  1  \\
  \end{array}
  %
  \qquad
  %
  \begin{array}[t]{ccccccc}
  P & ¬P \\ \hline
  0 & 1 \\
  1 & 0 \\
  \end{array}
$

\msk

Constants:

$⊤ = 1$

$⊥ = 0$



\newpage

%  _____                 _                _   _             _      
% |___ /     __   ____ _| |_   _  ___  __| | | | ___   __ _(_) ___ 
%   |_ \ ____\ \ / / _` | | | | |/ _ \/ _` | | |/ _ \ / _` | |/ __|
%  ___) |_____\ V / (_| | | |_| |  __/ (_| | | | (_) | (_| | | (__ 
% |____/       \_/ \__,_|_|\__,_|\___|\__,_| |_|\___/ \__, |_|\___|
%                                                     |___/        
%
% «3-valued-logic» (to ".3-valued-logic")
% (lao162p 2 "3-valued-logic")

{\bf Our first non-classical logic}

\ssk

Idea:

00 means ``false''

11 means ``true''

01 is something intermediate between true and false

\msk

Operations:

\ssk

$\begin{array}[t]{ccccccc}
  P  & Q  & P∧Q & P∨Q & P→Q & P↔Q \\ \hline
  00 & 00 &  00 &  00  &  11  &  11  \\
  00 & 01 &  00 &  01  &  11  &  00  \\
  00 & 11 &  00 &  11  &  11  &  00  \\
  01 & 00 &  00 &  01  &  00  &  00  \\
  01 & 01 &  01 &  01  &  11  &  11  \\
  01 & 11 &  01 &  11  &  11  &  01  \\
  11 & 00 &  00 &  11  &  00  &  00  \\
  11 & 01 &  01 &  11  &  01  &  01  \\
  11 & 11 &  11 &  11  &  11  &  11  \\
  \end{array}
  %
  \qquad
  %
  \begin{array}[t]{ccccccc}
  P  & ¬P \\ \hline
  00 & 11 \\
  01 & 00 \\
  11 & 00 \\
  \end{array}
$

\msk

Constants:

$⊤ = 11$

$⊥ = 00$




\newpage

%  _____           _        _             _           
% |_   _|_ _ _   _| |_ ___ | | ___   __ _(_) ___  ___ 
%   | |/ _` | | | | __/ _ \| |/ _ \ / _` | |/ _ \/ __|
%   | | (_| | |_| | || (_) | | (_) | (_| | |  __/\__ \
%   |_|\__,_|\__,_|\__\___/|_|\___/ \__, |_|\___||___/
%                                   |___/             
%
% «tautologies» (to ".tautologies")
% (lao162p 3 "tautologies")

{\bf Tautologies}

\ssk

We can calculate the result of $¬¬P→P$

when $P=0$ (left) and

when $P=1$ (right) with:

\msk

$\und {{\und {¬ {\und {¬ \und P 0} 1}} 0} → {\und P 0}} 1
 \qquad
 \und {{\und {¬ {\und {¬ \und P 1} 0}} 1} → {\und P 1}} 1
$

\bsk

The {\it subformulas} of $¬¬P→P$ are:

\msk

$\subf{\subf{¬ \subf{¬ \subf P}} → {\subf P}}$

\bsk

If we write the result of each subformula

under its central connective we get:

\msk

\def\f#1{\framebox{1}}
 
$\begin{array}{ccccc}
 ¬ & ¬ & P & → & P \\ \hline
   &   & 0 &    & 0 \\[-7pt]
   & 1 &   &    &   \\[-7pt]
 0 &   &   &    &   \\[-7pt]
   &   &   & \f{1} &   \\
 \end{array}
 \qquad
 \begin{array}{ccccc}
 ¬ & ¬ & P & → & P \\ \hline
   &   & 1 &    & 1 \\[-7pt]
   & 0 &   &    &   \\[-7pt]
 1 &   &   &    &   \\[-7pt]
   &   &   & \f{1} &   \\
 \end{array}
$

\msk

We can write all results in the same line...

We get something more compact but harder to read,

\msk

$\begin{array}{ccccc}
 ¬ & ¬ & P & → & P \\ \hline
 0 & 1 & 0 & \f1 & 0 \\
 \end{array}
 \qquad
 \begin{array}{ccccc}
 ¬ & ¬ & P & → & P \\ \hline
 1 & 0 & 1 & \f1 & 1 \\
 \end{array}
$


\bsk

We can put each case in a single line.

Here we also add a column at the left with the values of $P$.

\msk


$\begin{array}{ccccccc}
 P & & ¬ & ¬ & P & → & P \\ \hline
 % (¬\p & (¬\p & \p\p P)) & → & P \\ \hline
 0 & & 0 & 1 & 0 & \f1 & 0 \\
 0 & & 1 & 0 & 1 & \f1 & 1 \\
 \end{array}
$





\newpage


%     _                _     _           _       
%    / \   ___    ___ | |__ (_) ___  ___| |_ ___ 
%   / _ \ / __|  / _ \| '_ \| |/ _ \/ __| __/ __|
%  / ___ \\__ \ | (_) | |_) | |  __/ (__| |_\__ \
% /_/   \_\___/  \___/|_.__// |\___|\___|\__|___/
%                         |__/                   
%
% «logics-as-objects» (to ".logics-as-objects")
% (lao162p 4 "logics-as-objects")

\def\p#1{\phantom{#1}}
\def\L{\mathsf{L}}
\def\CL{\mathsf{CL}}
\def\TL{\mathsf{L}_3}
\def\ul{_{\L}}
\def\ucl{_{\CL}}
\def\utl{_{\TL}}

\def\fo #1 #2 #3 {((#1,#2),#3)}
\def\ba #1 #2 #3 #4 {
  \foo 0 0 #1 , \\
  \foo 0 1 #2 , \\
  \foo 1 0 #3 , \\
  \foo 1 1 #4 \p, \\
}
\def\foc#1 #2 {(#1,#2)}
\def\co #1 #2 {
  \fooc 0 #1 ,\\
  \fooc 1 #2 \p,\\
}
\def\com {0,\\ 1\p,\\}
\def\cand{\ba 0 0 0 1 }
\def\cor {\ba 0 1 1 1 }
\def\cimp{\ba 1 1 0 1 }
\def\ciff{\ba 1 0 0 1 }
\def\cnot{\co 1 0 }

\def\foo#1 #2 #3 {((#1,#2),#3)}
\def\bar#1 #2 #3 #4 #5 #6 #7 #8 #9 {
  \foo 00 00 #1 , \\
  \foo 00 01 #2 , \\
  \foo 00 11 #3 ,   \\
  \foo 01 00 #4 , \\
  \foo 01 01 #5 , \\
  \foo 01 11 #6 ,   \\
  \foo 11 00 #7 , \\
  \foo 11 01 #8 , \\
  \foo 11 11 #9 \p, \\
}
\def\fooc #1 #2 {(#1,#2)}
\def\col#1 #2 #3 {
  \fooc 00 #1 ,\\
  \fooc 01 #2 ,\\
  \fooc 11 #3 \p,\\
}
\def\tom {00,\\ 01,\\ 11\p,\\}
\def\tand{\bar 00 00 00  00 01 01  00 01 11 }
\def\tor {\bar 00 01 11  01 01 11  11 11 11 }
\def\timp{\bar 11 11 11  00 11 11  00 01 11 }
\def\tiff{\bar 11 00 00  00 11 01  00 01 11 }
\def\tnot{\col 11 00 00 }



{\bf Logics as mathematical objects}

\msk

{\sl First definition.} A logic $\L$ is an 8-uple:
%
$$\begin{array}{rcl}
    \L & = & (Ω,   ⊤,   ⊥,   ∧,   ∨,   →,   ↔,   ¬) \\
       & = & (Ω\ul,⊤\ul,⊥\ul,∧\ul,∨\ul,→\ul,↔\ul,¬\ul) \\
  \end{array}
$$
\bsk

We saw two logics in the previous pages --

Classical Logic, $\CL$, and a three-valued logic, $\TL$:

\msk

$\CL = (Ω\ucl, ⊤\ucl, ⊥\ucl, ∧\ucl, ∨\ucl, →\ucl, ↔\ucl, ¬\ucl) =$

$\psm{\csm{\com}, 1, 0, \csm{\cand}, \csm{\cor}, \csm{\cimp}, \csm{\ciff}, \csm{\cnot}}$

\msk

$\TL = (Ω\utl, ⊤\utl, ⊥\utl, ∧\utl, ∨\utl, →\utl, ↔\utl, ¬\utl) =$

$\psm{\csm{\tom}, 11, 00, \csm{\tand}, \csm{\tor}, \csm{\timp}, \csm{\tiff}, \csm{\tnot}}$


\bsk

{\sl Second definition.} A logic $\L$ is {\sl given by} a 6-uple:
%
$$(Ω\ul,⊤\ul,⊥\ul,∧\ul,∨\ul,→\ul)$$

where the missing fields, $↔\ul$ and $¬\ul$, are defined from the other ones:
%
$$\begin{array}{rcl}
    P↔\ul Q & := & (P→\ul Q) ∧\ul (Q→\ul P) \\
      ¬\ul P & := & P→\ul ⊥\ul \\
  \\
       ↔\ul & := & λP,Q:Ω\ul. ((P→\ul Q) ∧\ul (Q→\ul P)) \\
       ¬\ul & := & λP:Ω\ul. (P→\ul ⊥\ul) \\
  \end{array}
$$


\bsk

We will see other definitions of a ``logic'' soon --

in them $Ω\ul$ is the set of points of a partial order $(Ω, ≤)$,

and in {\sl most} of them the constants `$⊤$', `$⊥$'

and the operations `$∧$', `$∨$' and `$→$' (and `$↔$' and `$¬$')

are induced by the order...

\newpage




%  ______   _    _      _             _      
% |__  / | | |  / \    | | ___   __ _(_) ___ 
%   / /| |_| | / _ \   | |/ _ \ / _` | |/ __|
%  / /_|  _  |/ ___ \  | | (_) | (_| | | (__ 
% /____|_| |_/_/   \_\ |_|\___/ \__, |_|\___|
%                               |___/        
%
% «ZHA-logic» (to ".ZHA-logic")
% (lao162p 5 "ZHA-logic")
% (find-planarhas 0)
% (find-planarhaspage 2 "One page intro (to the main theorem)")
% (find-planarhastext 2 "One page intro (to the main theorem)")
% (find-planarhas "one-page-intro")

{\bf Logics from partial orders}

\ssk

%R f = function (spec, def)
%R     local opts = {def=def, scale="12pt", meta="s"}
%R     local mp = mpnew(opts, spec):addlrs():addarrows("w"):output()
%R   end
%R f("1",             "zhaone")
%R f("1R",            "zhatwo")
%R f("1RL",           "zhatree")
%R f("12321L",        "zhaohouse")
%R f("12LRLRLR1",     "zhasquig")
%R f("123LLRR21",     "zhabigguill")
%R f("1234567654321", "zharect")
%R f("123RRR45R4321", "zharectcut")
%R f("123RRR43212R1", "zharectcutcut")
%R f("1234321",       "zhasixteen")
\pu

Each one of the 6 partial orders below ``is'' a logic,
%
{
%
$$\zhaone
  \quad \zhatwo
  \quad \zhatree
  \quad \zhaohouse
  \quad \zhasquig
  \quad \zhabigguill
$$
%
% $$\zharect
%   \zharectcut
%   \zharectcutcut
% $$
}

with these definitions for the constants and operations:
%
\def∧{\mathbin{\&}}
%
$$\def\o#1{\mathop{\mathsf{#1}}}
  \def\o#1{\mathbin{\mathsf{#1}}}
  \def\a#1#2{\ang{#1,#2}}
  \def\ab{\a ab}
  \def\cd{\a cd}
  \begin{array}{rcl}
  %
  \ab ≤ \cd &:=& a≤c∧b≤d \\
  \ab ≥ \cd &:=& a≥c∧b≥d \\[5pt]
  %
  \ab \o{above} \cd &:=& a≥c∧b≥d \\
  \ab \o{below} \cd &:=& a≤c∧b≤d \\
  \ab \o{leftof} \cd &:=& a≥c∧b≤d \\
  \ab \o{rightof} \cd &:=& a≤c∧b≥d \\[5pt]
  %
  \o{valid}(\ab) &:=& \ab∈Ω\ul \\
  \o{ne}(\ab) &:=& \o{if}   \o{valid}(\a a{b+1})
                   \o{then} \o{ne}(\a a{b+1})
                   \o{else} \ab \;
                   \o{end} \\
  \o{nw}(\ab) &:=& \o{if}   \o{valid}(\a {a+1}b)
                   \o{then} \o{nw}(\a {a+1}b)
                   \o{else} \ab \;
                   \o{end} \\[5pt]
  %
  \ab ∧ \cd &:=& \a{\o{min}(a,c)}{\o{min}(b,d)} \\
  \ab ∨ \cd &:=& \a{\o{max}(a,c)}{\o{max}(b,d)} \\[5pt]
  %
  \ab \to \cd &:=& \begin{array}[t]{llll}
               \o{if}     & \ab \o{below} \cd   & \o{then} & ⊤           \\
               \o{elseif} & \ab \o{leftof} \cd  & \o{then} & \o{ne}(\ab∧\cd) \\
               \o{elseif} & \ab \o{rightof} \cd & \o{then} & \o{nw}(\ab∧\cd) \\
               \o{elseif} & \ab \o{above} \cd   & \o{then} & \cd            \\
               \o{end}
               \end{array} \\[5pt]
  %
  ⊤   &:=& \o{sup}(Ω) \\
  ⊥   &:=& \a00 \\
  ¬\ab &:=& \ab→⊥ \\
  \ab↔\cd &:=& (\ab→\cd)∧ (\cd→\ab)\\
  \end{array}
$$

Exercise: calculate / represent graphically:

{
\def\o#1{\mathbin{\mathsf{#1}}}
\def\a#1#2{\ang{#1,#2}}
\def\ab{\a ab}
\def\cd{\a cd}

a) $λ\ab:Ω_{10}.\, \ab≤\a11$

b) $λ\ab:Ω_{10}.\, \ab≤\a12$

c) $λ\ab:Ω_{10}.\, \ab≥\a11$

d) $λ\ab:Ω_{10}.\, \ab \o{leftof} \a11$

e) $λ\ab:Ω_{10}.\, \ab \o{rightof} \a11$

f) $λ\ab:Ω_{10}.\, \ab \o{above} \a11$

g) $λ\ab:Ω_{10}.\, \ab \o{below} \a11$

}

\newpage



%   ____                            _   _                
%  / ___|___  _ __  _ __   ___  ___| |_(_)_   _____  ___ 
% | |   / _ \| '_ \| '_ \ / _ \/ __| __| \ \ / / _ \/ __|
% | |__| (_) | | | | | | |  __/ (__| |_| |\ V /  __/\__ \
%  \____\___/|_| |_|_| |_|\___|\___|\__|_| \_/ \___||___/
%                                                        
% «connectives» (to ".connectives")
% (lao162p 6 "connectives")

\def\LT{\mathsf{L}_{10}}
\def\LS{\mathsf{L}_{16}}
\def\ult{_{\LT}}
\def\uls{_{\LS}}

{\bf Logics from partial orders, 2: connectives}

\ssk


$$Ω\ult=\zhaohouse
  \quad
  Ω\uls=\zhasixteen
$$

$$\def\o#1{\mathop{\mathsf{#1}}}
  \def\o#1{\mathbin{\mathsf{#1}}}
  \def\a#1#2{\ang{#1,#2}}
  \def\ab{\a ab}
  \def\cd{\a cd}
  \begin{array}{rcl}
  %
  % \ab ≤ \cd &:=& a≤c∧b≤d \\
  % \ab ≥ \cd &:=& a≥c∧b≥d \\[5pt]
  %
  % \ab \o{above} \cd &:=& a≥c∧b≥d \\
  % \ab \o{below} \cd &:=& a≤c∧b≤d \\
  % \ab \o{leftof} \cd &:=& a≥c∧b≤d \\
  % \ab \o{rightof} \cd &:=& a≤c∧b≥d \\[5pt]
  %
  \o{valid}(\ab) &:=& \ab∈Ω\ul \\
  \o{ne}(\ab) &:=& \o{if}   \o{valid}(\a a{b+1})
                   \o{then} \o{ne}(\a a{b+1})
                   \o{else} \ab \;
                   \o{end} \\
  \o{nw}(\ab) &:=& \o{if}   \o{valid}(\a {a+1}b)
                   \o{then} \o{nw}(\a {a+1}b)
                   \o{else} \ab \;
                   \o{end} \\[5pt]
  %
  \ab ∧ \cd &:=& \a{\o{min}(a,c)}{\o{min}(b,d)} \\
  \ab ∨ \cd &:=& \a{\o{max}(a,c)}{\o{max}(b,d)} \\[5pt]
  %
  \ab → \cd &:=& \begin{array}[t]{llll}
               \o{if}     & \ab \o{below} \cd   & \o{then} & ⊤           \\
               \o{elseif} & \ab \o{leftof} \cd  & \o{then} & \o{ne}(\ab∧\cd) \\
               \o{elseif} & \ab \o{rightof} \cd & \o{then} & \o{nw}(\ab∧\cd) \\
               \o{elseif} & \ab \o{above} \cd   & \o{then} & \cd            \\
               \o{end}
               \end{array} \\
  %
  ⊤   &:=& \o{sup}(Ω) \\
  ⊥   &:=& \a00 \\
  ¬\ab &:=& \ab→⊥ \\
  \ab↔\cd &:=& (\ab→\cd)∧ (\cd→\ab)\\
  \end{array}
$$

Exercise: calculate / represent graphically:

{
\def\o#1{\mathbin{\mathsf{#1}}}
\def\a#1#2{\ang{#1,#2}}
\def\ab{\a ab}
\def\cd{\a cd}

\begin{tabular}{rl}
   h) & $λ\ab:Ω\ult.\, \o{ne}(\ab)$ \\
   i) & $λ\ab:Ω\ult.\, \o{nw}(\ab)$ \\
   j) & $10 ∧\ult 11$, \; $10 ∨\ult 11$, \; $20 →\ult 11$ \\
  j') & $02 ∧\ult 11$, \; $02 ∨\ult 11$, \; $02 →\ult 11$ \\
 j'') & $10 ∧\uls 11$, \; $10 ∨\uls 11$, \; $20 →\uls 11$ \\
   l) & $λP:Ω\uls.\, P→11$ \\
  l') & $λQ:Ω\uls.\, 22→Q$ \\
 l'') & $λP:Ω\uls.\, P↔12$ \\
   m) & $λP:Ω\uls.\, ¬P$ \\
   n) & $λP:Ω\uls.\, ¬¬P$ \\
   o) & $λP:Ω\uls.\, (P≤21)∧(P≤12)$ \\
  o') & $λP:Ω\uls.\, P≤(21∧12)$ \\
 o'') & $λP:Ω\uls.\, (P≤(21∧12))↔((P≤21)∧(P≤12))$ \\
   p) & $λP:Ω\uls.\, (21≤P)∧(12≤P)$ \\
  p') & $λP:Ω\uls.\, (21∨12)≤P$ \\
 p'') & $λP:Ω\uls.\, ((21∨12)≤P)↔((21≤P)∧(12≤P))$ \\
   q) & $λP:Ω\uls.\, P∧21$ \\
  q') & $λP:Ω\uls.\, (P∧21)≤12$ \\
 q'') & $λP:Ω\uls.\, P≤(21→12)$ \\
q''') & $λP:Ω\uls.\, (P≤(21→12))↔((P∧21)≤12)$
\end{tabular}


}


\newpage


%   ____      _   _       _ _                   _       __     
%  / ___|    | | | |   __| (_) __ _  __ _    __| | ___ / _|___ 
% | |   _____| |_| |  / _` | |/ _` |/ _` |  / _` |/ _ \ |_/ __|
% | |__|_____|  _  | | (_| | | (_| | (_| | | (_| |  __/  _\__ \
%  \____|    |_| |_|  \__,_|_|\__,_|\__, |  \__,_|\___|_| |___/
%                                   |___/                      
%
% «C-H-diagram-defs» (to ".C-H-diagram-defs")
% (lao162p 7 "C-H-diagram-defs")

%: HA rules:
%:  
%:                          P∧Q≤R 
%:        -----π   -----π'  -----♯
%:        Q∧R≤Q    Q∧R≤R    P≤Q{→}R 
%:                                
%:        ^P-pi    ^P-pi'   ^P-sharp
%:                                
%:        P≤Q  P≤R          P≤Q{→}R 
%:  ---!  --------\ang{,}   -----♭  
%:  P≤⊤     P≤Q∧R           P∧Q≤R 
%:  
%:  ^P-T    ^P-ang          ^P-flat
%:  
%:                   
%:        -----ι   -----ι'
%:        P≤P∨Q    Q≤P∨Q
%:  
%:        ^P-iota  ^P-iota'
%:  
%:        P≤R  Q≤R
%:  ---¡  --------[,]
%:  ⊥≤P    P∨Q≤R
%:  
%:  ^P-F   ^P-[,]
%:

%: CCC rules:
%:                                   f:A×B→C 
%:           -------π   --------π'   -----------♯
%:           π:B×C→B    π':B×C→C     f^♯:A→B{→}C 
%:                                
%:           ^F-pi      ^F-pi'       ^F-sharp                     
%:                                
%:            f:A→B  g:A→C           g:A→B{→}C 
%:  ------¡  ---------------\ang{,}  ---------♭
%:  !:A→1    \ang{f,g}:A→B×C         g^♭:A×B→C 
%:  
%:  ^F-T     ^F-ang                  ^F-flat
%:                                 
%:           -------ι  --------ι' 
%:           ι:A→A+B   ι':B→A+B   
%:                                 
%:           ^F-iota   ^F-iota'
%:                                 
%:            f:A→C  g:B→C         
%:  ------¡  ---------------[,]
%:  ¡:0→A    [f,g]:A+B→C      
%:  
%:  ^F-F     ^F-[,]
%:  

\pu

\def\BiHArules{{
\def\PT {\ded{P-T}}
\def\PPA{\ded{P-pi}}
\def\PPB{\ded{P-pi'}}
\def\PPC{\ded{P-ang}}
\def\PEA{\ded{P-sharp}}
\def\PEB{\ded{P-flat}}
\def\PF {\ded{P-F}}
\def\PCA{\ded{P-iota}}
\def\PCB{\ded{P-iota'}}
\def\PCC{\ded{P-[,]}}
\mat{     & \PPA \qquad \PPB & \PEA \\\\
      \PT &       \PPC       & \PEB \\\\
          & \PCA \qquad \PCB &      \\\\
      \PF &       \PCC       &
}
}}

\def\BiCCCrules{{
\def\PT {\ded{F-T}}
\def\PPA{\ded{F-pi}}
\def\PPB{\ded{F-pi'}}
\def\PPC{\ded{F-ang}}
\def\PEA{\ded{F-sharp}}
\def\PEB{\ded{F-flat}}
\def\PF {\ded{F-F}}
\def\PCA{\ded{F-iota}}
\def\PCB{\ded{F-iota'}}
\def\PCC{\ded{F-[,]}}
\mat{     & \PPA \qquad \PPB & \PEA \\\\
      \PT &       \PPC       & \PEB \\\\
          & \PCA \qquad \PCB &      \\\\
      \PF &       \PCC       &
}
}}


% (find-dn4 "dednat4.lua" "lplacement")
%L forths[".PLABEL="] = function ()
%L     ds[1].lplacement = getword()
%L     ds[1].label = getword()
%L   end


%D diagram BiHAdiag
%D 2Dx     100  +15   +25    +25  +15     +25
%D 2D  100 T1   PB <- PBC -> PC   EC |--> EB->C 
%D 2D	   ^       ^   ^   ^      ^       ^     
%D 2D	   |        \  |  /       |       |     
%D 2D  +25 TA         PA         EAxB <-| EA    
%D 2D	                                        
%D 2D  +15 IA         CC			       
%D 2D	   ^        ^  ^  ^		       
%D 2D	   |       /   |   \		       
%D 2D  +25 I0   CA -> CAB <- CB                 
%D 2D
%D (( T1 .tex= ⊤ TA .tex= P				       
%D    @ 0 @ 1 <-					       
%D ))
%D (( PB .tex= Q PBC .tex= Q∧R PC .tex= R PA .tex= P       
%D    @ 0 @ 1 <- @ 1 @ 2 ->				       
%D    @ 0 @ 3 <- @ 1 @ 3 <- @ 2 @ 3 <-			       
%D ))
%D (( EC .tex= R EB->C .tex= Q{→}R EAxB .tex= P∧Q EA .tex= P 
%D    @ 0 @ 1 |->					       
%D    @ 0 @ 2 <-  @ 1 @ 3 <-			       
%D    @ 2 @ 3 <-|					       
%D ))
%D (( IA .tex= P I0 .tex= ⊥				       
%D    @ 0 @ 1 <-					       
%D ))
%D (( CC .tex= R CA .tex= P CAB .tex= P∨Q CB .tex= Q       
%D    @ 0 @ 1 <- @ 0 @ 2 <- @ 0 @ 3 <-			       
%D    @ 1 @ 2 -> @ 2 @ 3 <-                                  
%D ))
%D enddiagram
%D

%D diagram BiCCCdiag
%D 2Dx     100  +15   +25    +25  +15     +25
%D 2D  100 T1   PB <- PBC -> PC   EC |--> EB->C 
%D 2D	   ^       ^   ^   ^      ^       ^     
%D 2D	   |        \  |  /       |       |     
%D 2D  +25 TA         PA         EAxB <-| EA    
%D 2D	                                        
%D 2D  +15 IA         CC			       
%D 2D	   ^        ^  ^  ^		       
%D 2D	   |       /   |   \		       
%D 2D  +25 I0   CA -> CAB <- CB                 
%D 2D
%D (( T1 .tex= 1 TA .tex= A				       
%D    @ 0 @ 1 <- .plabel= l !				       
%D ))
%D (( PB .tex= B PBC   .tex= B{×}C   PC   .tex= C   PA .tex= A       
%D    @ 0 @ 1 <- .plabel= a π  @ 1 @ 2 -> .plabel= a π'
%D    @ 0 @ 3 <- .plabel= l f  @ 2 @ 3 <- .plabel= r g
%D    @ 1 @ 3 <- .plabel= m \ang{f,g}
%D ))
%D (( EC .tex= C EB->C .tex= B{→}C EAxB .tex= A{×}B EA .tex= A 
%D    @ 0 @ 1 |-> .plabel= a (B{→})
%D    @ 0 @ 2 <-  .plabel= l \sm{f\\g^♭} 
%D    @ 1 @ 3 <-  .plabel= r \sm{f^♯\\g} 
%D    @ 2 @ 3 <-| .plabel= r (×B) 
%D    @ 0 @ 3 harrownodes nil 20 nil |-> sl^
%D    @ 0 @ 3 harrownodes nil 20 nil <-| sl_
%D #  @ 0 @ 2 <-  .PLABEL= _(0.43) g^\flat
%D #  @ 0 @ 2 <-  .PLABEL= _(0.57) f
%D #  @ 1 @ 3 <-  .PLABEL= ^(0.43) g
%D #  @ 1 @ 3 <-  .PLABEL= ^(0.57) f^\sharp
%D ))
%D (( IA .tex= A I0 .tex= 0				       
%D    @ 0 @ 1 <- .plabel= l ¡					       
%D ))
%D (( CC .tex= C CA .tex= A CAB .tex= A{+}B CB .tex= B       
%D    @ 0 @ 1 <- .plabel= l f @ 0 @ 3 <- .plabel= r g
%D    @ 0 @ 2 <- .plabel= m [f,g]
%D    @ 1 @ 2 -> .plabel= b ι @ 2 @ 3 <-  .plabel= b ι'
%D ))
%D enddiagram
%D

\pu

\def\BiHAeqs{
\begin{array}{rl}
(id)   & ∀P.(P≤P)                    \\
(comp) & ∀P,Q,R.(P≤Q)∧(Q≤R)→(P≤R)    \\
                                     \\
(⊤)    & ∀P.(P≤⊤)                    \\
(⊥)    & ∀P.(⊥≤P)                    \\
(∧)    & ∀P,Q,R.(P≤Q∧R)↔(P≤Q)∧(P≤R)  \\
(∨)    & ∀P,Q,R.(P∨Q≤R)↔(P≤R)∧(Q≤R)  \\
(→)    & ∀P,Q,R.(P≤Q→R)↔(P∧Q≤R)      \\
                                     \\
(¬)    & ¬P := P→⊥                   \\
(↔)    & P↔Q := (P→Q)∧(Q→P)          \\
\end{array}
}

\def\BiCCCeqs{
\begin{array}{rl}
(id)   & \id_A ∈ \Hom(A,A)                  \\
(comp) & (;)_{A,B,C}: \Hom(A,B)×\Hom(B,C)→\Hom(A,C) \\
                                     \\
(⊤)    & ∀A.(\Hom(A,1)≃1)            \\
(⊥)    & ∀A.(\Hom(0,A)≃1)            \\
(∧)    & ∀A,B,C.(\Hom(A,B×C)≃\Hom(A,B)×\Hom(A,C)) \\
(∨)    & ∀A,B,C.(\Hom(A+B,C)≃\Hom(A,C)×\Hom(B,C)) \\
(→)    & ∀A,B,C.(\Hom(A,C^B)≃\Hom(A×B,C)      \\
\end{array}
}


% (find-854file "" "fdiagest")
% (find-854file "" "%D diagram yoneda-and-friends")
% (find-dn4 "experimental.lua" "BOX")
\def\ctabular#1{\begin{tabular}{c}#1\end{tabular}}
\def\ltabular#1{\begin{tabular}{c}#1\end{tabular}}
% \def\fdiagwithboxest#1#2{\ltabular{#2 \\ \fdiagwithboxes{#1}}}
\def\fdiagest#1#2{\ltabular{#2 \\ \fdiag{#1}}}

\savebox{\myboxa}{$\diag{BiHAdiag}$}   \def\BiHAdiag {\usebox{\myboxa}}
\savebox{\myboxb}{$\diag{BiCCCdiag}$}  \def\BiCCCdiag{\usebox{\myboxb}}

% (find-es "tex" "savebox")

%   ____      _   _       _ _                                 
%  / ___|    | | | |   __| (_) __ _  __ _ _ __ __ _ _ __ ___  
% | |   _____| |_| |  / _` | |/ _` |/ _` | '__/ _` | '_ ` _ \ 
% | |__|_____|  _  | | (_| | | (_| | (_| | | | (_| | | | | | |
%  \____|    |_| |_|  \__,_|_|\__,_|\__, |_|  \__,_|_| |_| |_|
%                                   |___/                     
%
% «C-H-diagram» (to ".C-H-diagram")
% (lao162p 7 "C-H-diagram")

{\setlength{\parindent}{0em}

{\bf Curry Howard as a big diagram}

\ssk

The diagram below shows the connection between logic and $λ$-calculus.

We are now ready to understand the rules $(∧)$, $(∨)$, $(→)$ in the top left box.

\bsk

\noindent\hbox to \textwidth{\hss
\resizebox{1.5\textwidth}{!}{
$\begin{array}{rcl}
    \fbox{$\BiHAeqs$}    && \fbox{$\BiCCCeqs$}  \\\\
    \fbox{$\BiHArules$}  && \fbox{$\BiCCCrules$} \\\\
    \fbox{\BiHAdiag}     && \fbox{\BiCCCdiag}   \\
  \end{array}
$%
}%
\hss}

}

\newpage



%  ____            _               _ 
% |  _ \  ___ _ __(_)_   _____  __| |
% | | | |/ _ \ '__| \ \ / / _ \/ _` |
% | |_| |  __/ |  | |\ V /  __/ (_| |
% |____/ \___|_|  |_| \_/ \___|\__,_|
%                                    
% «derived-rules» (to ".derived-rules")
% (lao162p 8 "derived-rules")

{\bf Some derived rules}

\def\flip{\mathsf{flip}}
\def\MP{\mathsf{MP}}

%:
%:                      ------         ----      
%:                      A∧C≤A  A≤B   A∧C≤C  C≤D    
%:                      ------------   ------------
%:  A≤B  C≤D              A∧C≤B         A∧C≤D      
%:  ---------(∧)   :=     ---------------------    
%:  A∧C≤B∧D                     A∧C≤B∧D            
%:
%:   ^xandL                        ^xandR
%:  
%:                      ------         ----      
%:                      A∨C≥A  A≥B   A∨C≥C  C≥D    
%:                      ------------   ------------
%:  A≥B  C≥D              A∨C≥B         A∨C≥D      
%:  ---------(∨)   :=     ---------------------    
%:  A∨C≥B∨D                     A∨C≥B∨D            
%:
%:   ^xorL                        ^xorR
%:  
%:                            ------    ------
%:                            A∧B≤B    A∧B≤A
%:  ---------\flip_{∧}  :=    ----------------
%:  A∧B≤B∧A                     A∧B≤B∧A
%:
%:   ^flipandL                    ^flipandR
%:                                              ---------
%:                                              Q→R≤Q→R 
%:                       ------------------   --------------
%:                       Q∧(Q→R)≤(Q→R)∧Q    (Q→R)∧Q≤R
%:  -----------\MP_0 :=  -------------------------------
%:  Q∧(Q→R)≤R                   Q∧(Q→R)≤R
%:
%:    ^MP0L                         ^MP0R
%:
%:                          P≤Q  P≤Q→R
%:                          ------------    ----------\MP_0
%:  P≤Q  P≤Q→R             P≤Q∧(Q→R)    Q∧(Q→R)≤R
%:  ------------\MP  :=     --------------------------
%:      P≤R                         P≤R
%:
%:      ^MPL                         ^MPR
%:
%:
%:                    ------------
%:                    A∧(A→⊥)≤⊥
%:  ------(¬¬)  :=    --------------
%:  A≤¬¬A             A≤(A→⊥)→⊥
%:
%:
$$\pu
  \begin{array}{rcl}
  \ded{xandL}    &:=& \ded{xandR}    \\{}\\
  \ded{xorL}     &:=& \ded{xorR}     \\\\
  \ded{flipandL} &:=& \ded{flipandR} \\\\
  \ded{MP0L}     &:=& \ded{MP0R}     \\\\
  \ded{MPL}      &:=& \ded{MPR}      \\\\
  \end{array}
$$

Exercises:

a) Name all the rules used in the right column above.

b) Visualize $(∧)$ in $\L_{5×5}$ with $A=31$, $B=42$, $C=13$, $D=24$.

c) Visualize $(∨)$ in $\L_{5×5}$ with $A=42$, $B=31$, $C=24$, $D=13$.

d) Visualize $\MP_0$ in $\L_{3×3}$ with $Q=21$, $R=12$.

e) Visualize $\MP$ in $\L_{3×3}$ with $Q=21$, $R=12$, $P=01$.

f) Visualize $(¬¬)$ in $\LT$ with $A=10$.




\end{document}

% Local Variables:
% coding: utf-8-unix
% ee-anchor-format:     "«%s»"
% End:
