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