|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% (find-angg "LATEX/2019ilha-grande-slides.tex")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2019ilha-grande-slides.tex" :end))
% (defun d () (interactive) (find-pdf-page "~/LATEX/2019ilha-grande-slides.pdf"))
% (defun d () (interactive) (find-pdftools-page "~/LATEX/2019ilha-grande-slides.pdf"))
% (defun e () (interactive) (find-LATEX "2019ilha-grande-slides.tex"))
% (defun u () (interactive) (find-latex-upload-links "2019ilha-grande-slides"))
% (find-xpdfpage "~/LATEX/2019ilha-grande-slides.pdf")
% (find-sh0 "cp -v ~/LATEX/2019ilha-grande-slides.pdf /tmp/")
% (find-sh0 "cp -v ~/LATEX/2019ilha-grande-slides.pdf /tmp/pen/")
% file:///home/edrx/LATEX/2019ilha-grande-slides.pdf
% file:///tmp/2019ilha-grande-slides.pdf
% file:///tmp/pen/2019ilha-grande-slides.pdf
% http://angg.twu.net/LATEX/2019ilha-grande-slides.pdf
%
% (find-sh "make -f 2017planar-has-1.mk STEM=2019ilha-grande-slides veryclean")
% (find-TH "math-b" "2019-viipl")
% «.title-page» (to "title-page")
% «.overview» (to "overview")
% «.which-implication» (to "which-implication")
% «.goedel» (to "goedel")
% «.goedel-2» (to "goedel-2")
% «.goedel-3» (to "goedel-3")
% «.stable» (to "stable")
% «.kripke-frames» (to "kripke-frames")
% «.logic-for-children» (to "logic-for-children")
% «.LCLT» (to "LCLT")
% «.calculate-and-represent» (to "calculate-and-represent")
% «.calculate-and-represent-2» (to "calculate-and-represent-2")
% «.calculate-and-represent-3» (to "calculate-and-represent-3")
\documentclass[oneside]{book}
\usepackage[colorlinks,urlcolor=violet]{hyperref} % (find-es "tex" "hyperref")
%\usepackage[latin1]{inputenc}
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{pict2e}
\usepackage[x11names,svgnames]{xcolor} % (find-es "tex" "xcolor")
%\usepackage{color} % (find-LATEX "edrx15.sty" "colors")
%\usepackage{colorweb} % (find-es "tex" "colorweb")
%\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
\def\expr#1{\directlua{output(tostring(#1))}}
\def\eval#1{\directlua{#1}}
%
\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")
\input edrxgac2.tex % (find-LATEX "edrxgac2.tex")
\input 2017planar-has-defs.tex % (find-LATEX "2017planar-has-defs.tex")
%
% (find-angg ".emacs.papers" "latexgeom")
% (find-LATEXfile "2016-2-GA-VR.tex" "{geometry}")
% (find-latexgeomtext "total={6.5in,8.75in},")
\usepackage[paperwidth=11.5cm, paperheight=9cm,
%total={6.5in,4in},
%textwidth=4in, paperwidth=4.5in,
%textheight=5in, paperheight=4.5in,
%a4paper,
top=1.5cm, bottom=.5cm, left=1cm, right=1cm, includefoot
]{geometry}
%
\begin{document}
\catcode`\^^J=10 % (find-es "luatex" "spurious-omega")
\directlua{dofile "dednat6load.lua"} % (find-LATEX "dednat6load.lua")
% \directlua{dofile "edrxtikz.lua"} % (find-LATEX "edrxtikz.lua")
% \directlua{dofile "edrxpict.lua"} % (find-LATEX "edrxpict.lua")
% %L V.__tostring = function (v) return format("(%.3f,%.3f)", v[1], v[2]) end
%L dofile "edrxtikz.lua" -- (find-LATEX "edrxtikz.lua")
%L dofile "edrxpict.lua" -- (find-LATEX "edrxpict.lua")
\pu
\def\V{\mathbf{T}}
\def\F{\mathbf{F}}
\def\und#1#2{\underbrace{#1}_{#2}}
\def\und#1#2{\underbrace{#1}_{\text{#2}}}
\def\ug#1{\und{#1}{gen}}
\def\uf#1{\und{#1}{filt}}
\def\ue#1{\und{#1}{expr}}
\def\uC#1{\und{#1}{context}}
\def\picturedotsa(#1,#2)(#3,#4)#5{%
\vcenter{\hbox{%
\beginpicture(#1,#2)(#3,#4)%
\pictaxes%
\pictdots{#5}%
\end{picture}%
}}%
}
% «colors» (to ".colors")
% (find-LATEX "2017ebl-slides.tex" "colors")
% (find-LATEX "2017ebl-slides.tex" "colors" "\\def\\ColorGreen")
% (find-xcolorpage 39 "4.4 Colors via x11names option")
\long\def\ColorRed #1{{\color{Red1}#1}}
\long\def\ColorViolet#1{{\color{MagentaVioletLight}#1}}
\long\def\ColorGreen #1{{\color{SpringDarkHard}#1}}
\long\def\ColorGreen #1{{\color{SpringGreenDark}#1}}
\long\def\ColorGreen #1{{\color{SpringGreen4}#1}}
\long\def\ColorGray #1{{\color{GrayLight}#1}}
\long\def\ColorGray #1{{\color{black!30!white}#1}}
% «myoval» (to ".myoval")
% (find-LATEXfile "2018pict2e.tex" "\\def\\myoval")
\def\myvcenter#1{\ensuremath{\vcenter{\hbox{#1}}}}%
\def\myoval(#1,#2)(#3,#4)[#5]{%
\myvcenter{%
\begin{picture}(#1,#2)(-#3,-#4)
\put(0,0){\oval[#5](#1,#2)}
\end{picture}%
}}
\catcode`•=13 \def•{\ensuremath{\bullet}}
\def\calA{\mathcal{A}}
\def\calB{\mathcal{B}}
\def\calC{\mathcal{C}}
\def\calD{\mathcal{D}}
\def\bbG{\mathbb{G}}
\def\antitabular{\hskip-5.5pt}
\setlength{\parindent}{0em}
% _____ _ _ _
% |_ _(_) |_| | ___
% | | | | __| |/ _ \
% | | | | |_| | __/
% |_| |_|\__|_|\___|
%
% «title-page» (to ".title-page")
% (igsp 1 "title-page")
% (igs "title-page")
% (lodp 1 "title-page")
% (lod "title-page")
% (find-es "tex" "huge")
\begin{center}
\Large
{\bf
Using Planar Heyting Algebras
to develop \ColorRed{visual intuition} about
Intuitionistic Propositional Logic
}
\bsk
\normalsize
Eduardo Ochs (UFF, Brazil)
\footnotesize
\url{http://angg.twu.net/math-b.html\#2019-viipl}
% \scriptsize
%
% \url{http://www.logicauniversalis.org/wld}
%
% \url{http://www.logicauniversalis.org/wld-rio-de-janeiro}
Jornadas de Mirantão
Ilha Grande, RJ, 2019aug19
% http://www.logicauniversalis.org/wld-rio-de-janeiro
\end{center}
\newpage
\noedrxfooter
% ___ _
% / _ \__ _____ _ ____ _(_) _____ __
% | | | \ \ / / _ \ '__\ \ / / |/ _ \ \ /\ / /
% | |_| |\ V / __/ | \ V /| | __/\ V V /
% \___/ \_/ \___|_| \_/ |_|\___| \_/\_/
%
% «overview» (to ".overview")
% (igsp 2 "overview")
% (igs "overview")
{\bf How I started working on this}
Many years ago I was studying Topos Theory (mostly by myself) and
Logic (mostly with Luiz Carlos --- Proof Theory and tableaux)... I
needed to understand a bit of Intuitionistic (Propositional) Logic for
toposes, but I didn't have any intuition about it...
For example:
\newpage
% __ ___ _ _ _ _
% \ \ / / |__ (_) ___| |__ (_)_ __ ___ _ __ | |
% \ \ /\ / /| '_ \| |/ __| '_ \ | | '_ ` _ \| '_ \| |
% \ V V / | | | | | (__| | | | | | | | | | | |_) | |
% \_/\_/ |_| |_|_|\___|_| |_| |_|_| |_| |_| .__/|_|
% |_|
%
% «which-implication» (to ".which-implication")
% (igsp 3 "which-implication")
% (igs "which-implication")
{\bf Which one of these implications is false?}
And how do \ColorRed{you} remember that?
% (ph1p 11 "prop-calc-ZHA")
% (ph1 "prop-calc-ZHA")
% (ph1 "prop-calc-ZHA" "zdemorgan")
\def\HCM{\ColorGray{← \text{\ColorRed{has a countermodel}}}}
\def\HCM{\ColorGray{← \text{has a countermodel}}}
\def\THM{\ColorGray{← \text{is a theorem}}}
$$\begin{array}{ll}
(¬ ¬ P) → P & \HCM \\
(¬ ¬ P) ← P & \THM \\
¬(P ∧ Q) ← (¬ P ∨ ¬ Q) & \THM \\
¬(P ∧ Q) → (¬ P ∨ ¬ Q) & \HCM \\
¬(P ∨ Q) ← (¬ P ∧ ¬ Q) & \THM \\
¬(P ∨ Q) → (¬ P ∧ ¬ Q) & \THM \\
\end{array}
$$
One way: remember which.
Or better: remember the proofs of the ones that can be proved.
Another way: remember the countermodel.
Or better: have \ColorRed{a way to test countermodels very quickly.}
(\ColorRed{Possible} countermodels!)
\newpage
% _ _____ ____
% | | | ___/ ___|
% | | | |_ | |
% | |___| _|| |___
% |_____|_| \____|
%
% «logic-for-children» (to ".logic-for-children")
% (igsp 4 "logic-for-children")
% (igs "logic-for-children")
{\bf Logic for Children}
{\sl Fast forward many years.} I organized with a friend a workshop
called ``Logic for Children'' in the UniLog 2018 in Vichy... this is
from one of the announcements:
% See the unofficial page of the workshop:
%
% (find-TH "logic-for-children-2018")
%
% $$\text{\url{http://angg.twu.net/logic-for-children-2018.html}}$$
\msk
The ``children'' in ``logic for children'' means ``people without
mathematical maturity'', which in its turn means people who:
\begin{itemize}
\item have trouble with very abstract definitions,
\item prefer to start from particular cases (and then generalize),
\item handle diagrams better than algebraic notations,
\item like to use diagrams and analogies (...)
\end{itemize}
\newpage
{\bf Logic for Children (2)}
% \ColorGray{(Cont...)}
\ssk
If we say that categorical definitions are ``for adults'' ---
because they may be very abstract --- and that particular cases,
diagrams, and analogies are ``for children'', then our intent with
this workshop becomes easy to state. ``Children'' are willing to use
"tools for children" to do mathematics, even if they will have to
translate everything to a language ``for adults'' to make their
results dependable and publishable, and even if the bridge between
their tools ``for children'' and ``for adults'' is somewhat
defective, i.e., if the translation only works on simple cases...
\newpage
{\bf Logic for Children (3)}
\ssk
We are interested in that {\sl bridge} between maths ``for adults''
and ``for children'' in several areas. Maths "for children" are hard
to publish, even informally as notes (see {\bf this thread} in the
Categories mailing list), so often techniques are rediscovered over
and over, but kept restricted to the ``oral culture'' of the area.
Our main intents with this workshop are:
\begin{itemize}
\item to discuss (over coffe breaks!) the techniques of the
``bridge'' that we currently use in seemingly ad-hoc ways,
\item to systematize and ``mechanize'' these techniques to make
them quicker to apply,
\item to find ways to publish those techniques - in journals or
elsewhere,
\item to connect people in several areas working in related
ideas, and to create repositories of online resources.
\end{itemize}
% 1. How I discovered this
%
% 1.1. Toposes, IPL, Modal Logic, S4, Gödel translation
%
% 1.2.
% https://en.wikipedia.org/wiki/Intuitionistic_logic#Relation_to_modal_logic
% https://en.wikipedia.org/wiki/Intuitionistic_logic#Heyting_algebra_semantics
% https://en.wikipedia.org/wiki/Kripke_semantics#Semantics_of_intuitionistic_logic
\newpage
% ____ _ _
% / ___| ___ ___ __| | ___| |
% | | _ / _ \ / _ \/ _` |/ _ \ |
% | |_| | (_) | __/ (_| | __/ |
% \____|\___/ \___|\__,_|\___|_|
%
% «goedel» (to ".goedel")
% (igsp 8 "goedel")
% (igs "goedel")
{\bf The Gödel translation}
From the Wikipedia:
\msk
Let $A$ be a propositional intuitionistic formula.
A modal formula $T(A)$ is defined by induction
on the complexity of $A$:
%
$$\begin{array}{l}
T(P) = ◻P \text{\;\; for any propositional variable $P$}, \\
T(⊥) = ⊥, \\
T(A∧B) = T(A)∧T(B), \\
T(A∨B) = T(A)∨T(B), \\
T(A→B) = ◻(T(A)→T(B)), \\
\end{array}
$$
As negation is in intuitionistic logic defined by
$A→⊥$, we also have $T(¬A) = ◻¬T(A)$.
\newpage
% ____ _ _ ____
% / ___| ___ ___ __| | ___| | |___ \
% | | _ / _ \ / _ \/ _` |/ _ \ | __) |
% | |_| | (_) | __/ (_| | __/ | / __/
% \____|\___/ \___|\__,_|\___|_| |_____|
%
% «goedel-2» (to ".goedel-2")
% (igsp 9 "goedel-2")
% (igs "goedel-2")
{\bf The Gödel translation (2)}
From the Wikipedia (cont.):
\msk
$T$ is called the {\sl Gödel translation} or {\sl
Gödel--McKinsey--Tarski translation}. The translation is sometimes
presented in slightly different ways: for example, one may insert $◻$
before every subformula. All such variants are provably equivalent in
S4.
\msk
An example:
%
%UB (¬ ¬ P) → P
%UB -- --
%UB ◻P ◻P
%UB ----
%UB ◻¬◻P
%UB ------
%UB ◻¬◻¬◻P
%UB ---------------
%UB ◻((◻¬◻¬◻P)→(◻P)
%L
%L defub "notnotP"
%
\pu
$$\def\und#1#2{\underbrace{#1}_{#2}}
T(\ub{notnotP}) = ◻((◻¬◻¬◻P)→(◻P)
$$
\newpage
% «goedel-3» (to ".goedel-3")
% (igsp 10 "goedel-3")
% (igs "goedel-3")
{\bf The Gödel translation (3)}
Let $A$ be a formula in IPL.
Then $A$ is a theorem in IPL iff $T(A)$ is a theorem in S4.
$A$ is a non-theorem of IPL
$↔$ $T(A)$ has a countermodel in S4
$↔$ there is a Kripke model $(W,R,v)$ that falsifies $T(A)$
\msk
Suppose that $A$ has propositional variables $P$ and $Q$.
Suppose that we've fixed $(W,R)$.
I realized that I did not need to test all valuations ---
I could test only the valuations in which $P=◻P$ and
$Q=◻P$, i.e., the `$P$'s and `$Q$'s that are ``stable'' by $◻$...
\newpage
% «stable» (to ".stable")
% (igsp 11 "stable")
% (igs "stable")
{\bf Stable truth-values}
And I realized that I could \ColorRed{draw} the set of the stable
truth-values, and it would be a \ColorRed{finite topology} --- an
\ColorRed{order topology}... my topologies would usually be
\ColorRed{planar}, they were Heyting Algebras, and $◻P$ would be the
\ColorRed{interior} of the set $P$...
%R local house, ohouse = 2/ #1 \, 7/ !h11111 \
%R |#2 #3| | !h01111 |
%R \#4 #5/ | !h01011 !h00111 |
%R |!h01010 !h00011 !h00101|
%R | !h00010 !h00001 |
%R \ !h00000 /
%R house:tomp({def="zfHouse#1#2#3#4#5", scale="5pt", meta="s"}):addcells():output()
%R house:tomp({def="zdagHouseMicro", scale="6.8pt", meta="t"}):addbullets():addarrows():output()
%R house:tomp({def="zdagHouse", scale="20pt", meta=nil}):addbullets():addarrows():output()
%R ohouse:tomp({def="zdagOHouse", scale="28pt", meta=nil}):addcells():addarrows("w"):output()
%R ohouse:tozmp({def="zdagohouse", scale="12pt", meta="s"}):addlrs():addarrows("w"):output()
%
%R local guill, oguill = 2/ #1 #2\, 8/ !g111111 \
%R |#3 #4 | | !g101111 !g011111 |
%R \ #5 #6/ | !g001111 !g010111|
%R | !g001011 !g000111 |
%R |!g001010 !g000011 |
%R | !g000010 !g000001 |
%R \ !g000000 /
%R guill:tomp({def="zfGuill#1#2#3#4#5#6", scale="3.5pt", meta="s"}):addcells():output()
%R guill:tomp({def="zdagGuill", scale="7pt", meta="t"}):addbullets():addarrows():output()
%R guill:tomp({def="zdagGuill", scale="20pt", meta=nil}):addbullets():addarrows():output()
%R oguill:tomp({def="zdagOGuill", scale="28pt", meta=nil}):addcells():addarrows("w"):output()
%R oguill:tozmp({def="zdagoguill", scale="12pt", meta="s"}):addlrs():addarrows():output()
%
%R local w, womit, W =
%R 2/#1 #2 #3\, 2/ a \, 7/ !w11111 \
%R \ #4 #5 / | b c d | | !w11011!w10111!w01111 |
%R | e f g | | !w10011!w01011!w00111 |
%R |h i j | |!w10010 !w00011 !w00101|
%R | k l | | !w00010 !w00001 |
%R \ m / \ !w00000 /
%R w:tomp({def="zfW#1#2#3#4#5", scale="3.5pt", meta="s"}):addcells():output()
%R w:tomp({def="zfWbig#1#2#3#4#5", scale="25pt", meta=nil}):addcells():addarrows("w"):output()
%R w:tomp({def="zdagW", scale="20pt", meta=nil}):addbullets():addarrows() :output()
%R W:tomp({def="zdagOW", scale="28pt", meta=nil}):addcells():addarrowsexcept("w", "(2,4)0"):output()
%
\pu
$\resizebox{0.70\width}{!}{$
(H,\BPM(H)) = \zdagHouse
\qquad
(\Opens(H), ⊂_1) = \def\h{\zfHouse}\zdagOHouse
$}
$
\newpage
% _ __ _ _
% | |/ /_ __(_)_ __ | | _____
% | ' /| '__| | '_ \| |/ / _ \
% | . \| | | | |_) | < __/
% |_|\_\_| |_| .__/|_|\_\___|
% |_|
%
% «kripke-frames» (to ".kripke-frames")
% (igsp 12 "kripke-frames")
% (igs "kripke-frames")
{\bf Kripke frames}
A Kripke frame is a pair $(W,R)$, with $R⊆W×W$.
($W$ for ``worlds'', $R$ for ``accessibility relation'').
I will write it as $(P,A)$, for ``points'' and ``arrows''.
I pair $(P,A)$ with $A⊆P×P$ is (also) a directed graph.
Convention: $(P,A^*)$ is the transitive-reflexive closure of $(P,A)$.
A Kripke frame {\sl for S4} is a pair $(P,A^*)$.
\msk
I established some conventions to let me draw Kripke frames for S4
very compactly --- ``ahead'' would be ``down'', and the arrows would
be implicit. For example, this is my notation for a certain Kripke
frame for S4:
% (find-dn6 "zhas.lua" "MixedPicture-zset-tests")
%L X = "1.2|.3.|4.5"
%L kite = ".1.|2.3|.4.|.5."
%L house = ".1.|2.3|4.5"
%L mp = MixedPicture.new({def="dagX", meta="s", scale="5pt"}, z):zfunction(X):output()
%L mp = MixedPicture.new({def="dagKite", meta="s", scale="6pt"}, z):zfunction(kite):output()
%L mp = MixedPicture.new({def="dagHouse", meta="s", scale="6pt"}, z):zfunction(house):output()
%L mp = MixedPicture.new({def="dagKite", meta="t", scale="5pt"}, z):zfunction(kite):output()
%L mp = MixedPicture.new({def="dagHouse", meta="s", scale="6pt"}, z):zfunction(house):output()
$$\pu\dagHouse•••••$$
\newpage
% _ ____ _ _____
% | | / ___| | |_ _|
% | | | | | | | |
% | |__| |___| |___| |
% |_____\____|_____|_|
%
% «LCLT» (to ".LCLT")
% (igsp 13 "LCLT")
% (igs "LCLT")
{\bf Lambda-Calculus, Logics and Translations}
These ideas became the basis for a hands-on seminar course called
``Lambda-Calculus, Logics and Translations'' in which the students
learned many ideas from Logic, including IPL, Kripke models, S4,
Natural Deduction, in a {\sl very atypical} order...
For example:
\msk
Let $Ω$ be the set of points of a ZHA and $≤$ the default partial
order on it. The {\sl default meanings for $⊤,⊥,∧,∨,→,↔,¬$} are these
ones:
%
\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}
$\resizebox{0.80\width}{!}{$
\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∈Ω \\
\o{ne}(\ab) &:=& \o{if} \o{valid}(\a a{b+1})
\o{then} \o{ne}(\a a{b+1})
\o{else} \ab \;
\o{end} \\r
\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]
\end{array}
$}
$
$\begin{array}{rcl}
\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}(\cd) \\
\o{elseif} & \ab \o{rightof} \cd & \o{then} & \o{nw}(\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}
$
\newpage
% ____ _ _ _
% / ___|__ _| | ___ _ _| | __ _| |_ ___
% | | / _` | |/ __| | | | |/ _` | __/ _ \
% | |__| (_| | | (__| |_| | | (_| | || __/
% \____\__,_|_|\___|\__,_|_|\__,_|\__\___|
%
% «calculate-and-represent» (to ".calculate-and-represent")
% (igsp 16 "calculate-and-represent")
% (igs "calculate-and-represent")
{\bf Calculate, and represent in positional notation...}
% ...when possible.
% (Exercises! I ask the students to read sections 2--8 of ``Planar
% Heyting Algebras for Children'' and then do this...)
% (lam181p 17 "ZHAs-1")
% (lam181 "ZHAs-1")
\ssk
Read sections 2--8 of ``Planar Heyting Algebras for Children''.
% \url{http://angg.twu.net/LATEX/2017planar-has.pdf}
% (pha)
% (phap)
\msk
%L mpnew({def="foo", scale="7pt", meta="s"}, "12321L") :addlrs():output()
%L mpnew({def="qua", scale="7pt", meta="s"}, "123454321"):addlrs():output()
%L -- mp:addlrs():output()
{\pu
Let $B=\;\foo\;$ and $C=\;\qua\;\;$.
}
{\bf Exercises}
Calculate, and represent in positional notation when possible:
\newpage
% «calculate-and-represent-2» (to ".calculate-and-represent-2")
% (igsp 17 "calculate-and-represent-2")
% (igs "calculate-and-represent-2")
{\bf Calculate, and represent... (2)}
\ssk
\def\o#1{\mathop{\mathsf{#1}}}
\def\o#1{\mathbin{\mathsf{#1}}}
\def∧{\land}
\begin{tabular}{l}
a) $λlr{:}B.l$ \\
b) $λlr{:}B.r$ \\
c) $λlr{:}B.(l≤1)$ \\
d) $λlr{:}B.(r≥1)$ \\
e) $λlr{:}B.lr≤11$ \\
f) $λlr{:}B.lr∧12$ \\
g) $λlr{:}B.\o{valid}(\ang{l+1,r})$ \\
h) $λlr{:}B.lr \o{leftof} 11$ \\
i) $λlr{:}B.lr \o{leftof} 12$ \\
j) $λlr{:}B.lr \o{above} 11$ \\
k) $λlr{:}B.\o{ne}(lr)$ \\
l) $λlr{:}B.\o{nw}(lr)$ \\
\end{tabular}
\qquad
\begin{tabular}{l}
m) $20→11$ \\
n) $02→11$ \\
o) $22→11$ \\
p) $00→11$ \\
[5pt]
q) $λlr{:}B.¬lr$ \\
r) $λlr{:}B.¬¬lr$ \\
s) $λlr{:}B.(lr=¬¬lr)$ \\
[5pt]
t) $λP{:}C.(P→22)$ \\
u) $λQ{:}C.(22→Q)$ \\
\end{tabular}
\newpage
% «calculate-and-represent-3» (to ".calculate-and-represent-3")
% (igsp 18 "calculate-and-represent-3")
% (igs "calculate-and-represent-3")
{\bf Calculate, and represent... (3)}
% (ph1p 12 "HAs")
% (ph1p 13 "HAs")
% (ph1 "HAs")
% (ph1 "HAs" "we have:")
v) find $X$ such that
\quad\; $(λP{:}C.P≤X) = (λP{:}C.(P≤22)∧(P≤13)))$.
w) find $X$ such that
\quad\; $(λR{:}C.X≤R) = (λR{:}C.(22≤R)∧(13≤R)))$.
% (ph1p 13 "calculating-and")
% (ph1 "calculating-and")
% (ph1p 14 "calculating-imp")
% (ph1 "calculating-imp")
% I learned this around 1999, I think...
% It was painful.
\newpage
Let $Ω$ be the ZDAG on the left
below:
%
$$
%R local QoRai, PoQai, PnnP =
%R 1/ T \, 1/ T \, 1/ T \
%R | . . | | . . | | . |
%R | . . . | | . . . | | . . |
%R | . . . i | | . o . . | |d . n|
%R |. Q . . .| |. P . . .| | P . |
%R | . . R . | | . . Q . | \ F /
%R | . a . | | . . . |
%R | . . | | . . |
%R \ F / \ F /
%R local T = {a="(∧)", o="(∨)", i="(\\!→\\!)", n="(¬)", d="(\\!\\!¬¬\\!)",
%R T="·", F="·", T="⊤", F="⊥", }
%R PoQai:tozmp({def="PoQai", scale="12pt", meta=nil}):addcells(T):addcontour():output()
%R QoRai:tozmp({def="QoRai", scale="12pt", meta=nil}):addcells(T):addcontour():output()
%R PnnP :tozmp({def="PnnP" , scale="12pt", meta=nil}):addcells(T):addcontour():output()
%R
%R PoQai:tozmp({def="lozfive", scale="12pt", meta=nil}):addlrs():addcontour():output()
\pu
\resizebox{0.70\width}{!}{$
\lozfive \qquad \QoRai \qquad \PoQai
$}
$$
%
we will see that
a) if $Q=31$ and $R=12$ then $Q ∧_H R = 11$,
b) if $P=31$ and $Q=12$ then $P ∨_H Q = 32$,
c) if $Q=31$ and $R=12$ then $Q →_H R = 14$.
\msk
Let's see each case separately --- but, before we start, note that in
6, 7, 8, 6', 7', 8' we work part with truth values in $Ω$ and part
with standard truth values. For example, in 6, with $P=20$, we have:
%
%UB ( P ≤_H ( Q ∧_H R )) ↔ (( P ≤_H Q ) ∧ ( P ≤_H R ))
%UB -- -- -- -- -- -- --
%UB 20 31 12 20 31 20 12
%UB --------- --------- ---------
%UB 11 1 0
%UB -------------------- ----------------------------
%UB 0 0
%UB ---------------------------------------------------------
%UB 1
%L
%L defub "P<=(QaR) <-> (P<=Q a P<=R)"
$$\pu \ub{P<=(QaR) <-> (P<=Q a P<=R)}$$
%L local spec = "123454321"
%L local mpuQ = mpnew({zdef="uQ", scale="5pt", meta="s"}, spec)
%L local mpuR = mpnew({zdef="uR", scale="5pt", meta="s"}, spec)
%L local mpuQaR = mpnew({zdef="uQaR", scale="5pt", meta="s"}, spec)
%L mpuQ :zhalrf0("P -> P:below(v'31') and 1 or 0"):output()
%L mpuR :zhalrf0("P -> P:below(v'12') and 1 or 0"):output()
%L mpuQaR:zhalrf0("P -> P:below(v'11') and 1 or 0"):output()
%L
%UB ( P ≤_H Y) ↔ (( P ≤_H Q) ∧ ( P ≤_H R))
%UB -- -- --
%UB 11 31 12
%UB ---------- ---------- ----------
%UB \zha{uQaR} \zha{uQ} \zha{uR}
%UB ---------------------------
%UB \zha{uQaR}
%L
%L defub "P<=Y <-> (P<=Q a P<=R) : zhas"
%$$\pu \ub{P<=Y <-> (P<=Q a P<=R) : zhas}$$
\end{document}
% Local Variables:
% coding: utf-8-unix
% ee-tla: "igs"
% End: