|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% (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: