% This file: (find-LATEX "2019J-ops-valuations.tex")
%       See: (find-LATEX "2020J-ops-new.tex")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2019J-ops-valuations.tex" :end))
% (defun d () (interactive) (find-pdf-page "~/LATEX/2019J-ops-valuations.pdf"))
% (defun e () (interactive) (find-LATEX "2019J-ops-valuations.tex"))
% (defun u () (interactive) (find-latex-upload-links "2019J-ops-valuations"))
% (find-pdf-page   "~/LATEX/2019J-ops-valuations.pdf")
% (find-sh0 "cp -v  ~/LATEX/2019J-ops-valuations.pdf /tmp/")
% (find-sh0 "cp -v  ~/LATEX/2019J-ops-valuations.pdf /tmp/pen/")
%   file:///home/edrx/LATEX/2019J-ops-valuations.pdf
%               file:///tmp/2019J-ops-valuations.pdf
%           file:///tmp/pen/2019J-ops-valuations.pdf
% http://angg.twu.net/LATEX/2019J-ops-valuations.pdf
% (find-LATEX "2019.mk")

% «.valuations»				(to "valuations")

\directlua{tf_push("2019J-ops-valuations.tex")}


% __     __    _             _   _                 
% \ \   / /_ _| |_   _  __ _| |_(_) ___  _ __  ___ 
%  \ \ / / _` | | | | |/ _` | __| |/ _ \| '_ \/ __|
%   \ V / (_| | | |_| | (_| | |_| | (_) | | | \__ \
%    \_/ \__,_|_|\__,_|\__,_|\__|_|\___/|_| |_|___/
%                                                  
% «valuations»  (to ".valuations")
% (jonp 16 "valuations")
% (jov     "valuations")
% (p2lp 7 "valuations")
% (p2l    "valuations")
\section{Valuations}
\label  {valuations}

Let $H_\odot$ and $J_\odot$ be a ZHA and a J-operator on it, and let
$v_\odot$ be a function from the set $\{P,Q\}$ to $H$. By an abuse of
language $v_\odot$ will also denote the triple $(H_\odot, J_\odot,
v_\odot)$ --- and by a second abuse of language $v_\odot$ will also
denote the obvious extension of $v_\odot: \{P,Q\}→H$ to the set of all
valid expressions formed from $P$, $Q$, $·^*$, $⊤$, $⊥$, and the
connectives.

Let $i,j∈\{0,\ldots,7\}$. Then $(\oand_i,\oand_j)∈\SCube^*_\land$
means that $\oand_i ≤ \oand_j$ is a theorem, and so $v_\odot(\oand_i)
≤ v_\odot(\oand_j)$ holds; i.e.,
%
$$\SCube^*_\land
  ⊆ \setofst {(\oand_i,\oand_j)}
             {i,j∈\{0,\ldots,7\}, \; v_\odot(\oand_i) ≤ v_\odot(\oand_j)}
$$
%
and the same for:
%
$$\begin{array}{c}
  \SCube^*_\lor
  ⊆ \setofst {(\oor_i,\oor_j)}
             {i,j∈\{0,\ldots,7\}, \; v_\odot(\oor_i) ≤ v_\odot(\oor_j)}
  \\
  \SCube^*_\to
  ⊆ \setofst {(\oimp_i,\oimp_j)}
             {i,j∈\{0,\ldots,7\}, \; v_\odot(\oimp_i) ≤ v_\odot(\oimp_j)}
  \\
  \end{array}
$$

Some valuations that turn these `$⊆$'s into `$=$'. Let
%
%L mp = mpnew({def="orCube", scale="11pt"}, "12321L"):addcuts("c 21/0 0|12")
%L mp:put(v"10", "P"):put(v"20", "P*", "P^*")
%L mp:put(v"01", "Q"):put(v"02", "Q*", "Q^*")
%L mp:output()
%
%L mp = mpnew({def="andCube", scale="11pt"}, "12321"):addcuts("c 2/10 01|2")
%L mp:put(v"20", "P"):put(v"21", "P*", "P^*")
%L mp:put(v"02", "Q"):put(v"12", "Q*", "Q^*")
%L mp:output()
%
%L mp = mpnew({def="impCube", scale="11pt"}, "12R1L"):addcuts("c 2/10 01|2")
%L mp:put(v"10", "P")  -- :put(v"20", "P*", "P^*")
%L mp:put(v"01", "Q")  -- :put(v"02", "Q*", "Q^*")
%L mp:output()
%
\pu
%
$$\begin{array}{c}
  (H_∧, J_∧, v_∧) = \andCube
  \qquad
  (H_∨, J_∨, v_∨) = \orCube \\
  (H_→, J_→, v_→) = \impCube \\
  \end{array}
$$
%
then
%
$$\begin{array}{c}
  \SCube^*_\land
  = \setofst {(\oand_i,\oand_j)}
             {i,j∈\{0,\ldots,7\}, \; v_∧(\oand_i) ≤ v_∧(\oand_j)}
  \\
  \SCube^*_\lor
  = \setofst {(\oor_i,\oor_j)}
             {i,j∈\{0,\ldots,7\}, \; v_∨(\oor_i) ≤ v_∨(\oor_j)}
  \\
  \SCube^*_\to
  = \setofst {(\oimp_i,\oimp_j)}
             {i,j∈\{0,\ldots,7\}, \; v_→(\oimp_i) ≤ v_→(\oimp_j)}
  \\
  \end{array}
$$
%
or, in more elementary terms:

\newpage

{\sl A very important fact.}
For any $i$ and $j$,
%
$$\pu
  \begin{array}{rcl}
  \oand_i≤\oand_j & \text{ is a theorem iff it is true in } & \andCube \;\; , \\
  \\
  \oor_i≤\oor_j & \text{ is a theorem iff it is true in } & \orCube  \;\; , \\
  \\
  \oimp_i≤\oimp_j & \text{ is a theorem iff it is true in } & \impCube \;\; . \\
  \end{array}
$$

The very important fact, and the valuations $v_∧$, $v_∨$, $v_→$, give
us:

\begin{itemize}

\item a way to {\sl remember} which sentences of the forms
  $\oand_i≤\oand_j$, $\oor_i≤\oor_j$, $\oimp_i≤\oimp_j$ are theorems;

\item countermodels for all the sentences of these forms not in
  $\SCube_∧$, $\SCube_∨$, $\SCube_→$. For example, $\oor_7≤\oor_4$ is
  not in $\SCube_∨$; and $v_∨(\oor_7)≤v_∨(\oor_4)$, which shows that
  $\oor_7≤\oor_4$ can't be a theorem.

\end{itemize}


% (find-books "__cats/__cats.el" "bell")
% (find-books "__cats/__cats.el" "bell" "163")

{\sl An observation.} I arrived at the cubes $\ECube_∧^*$,
$\ECube_∨^*$, $\ECube_→^*$ by taking the material in the corollary 5.3
of chapter 5 in \cite{BellLST} and trying to make it fit into less
mental space (as discussed in \cite{OchsIDARCT}); after that I wanted
to be sure that each arrow that is not in the extended cubes has a
countermodel, and I found the countermodels one by one; then I
wondered if I could find a single countermodel for all non-theorems in
$\ECube_∧^*$ (and the same for $\ECube_∨^*$ and $\ECube_→^*$), and I
tried to start with a valuation that distinguished {\sl some}
equivalence classes in $\ECube_∧^*$, and change it bit by bit, getting
valuations that distinguished more equivalence classes at every step.
Eventually I arrived at $v_∧$, $v_∨$ and at $v_→$, and at the ---
surprisingly nice --- ``very important fact'' above.


% (ph2p 20 "ZHA-vals-good")
% (ph2     "ZHA-vals-good")

Note that this valuation
%
%L mp = mpnew({def="orand", scale="11pt"}, "1234321L"):addcuts("c 432/10 01|23")
%L mp:put(v"20", "P"):put(v"31", "P*", "P^*")
%L mp:put(v"02", "Q"):put(v"13", "Q*", "Q^*")
%L mp:output()
%
$$(H_{∧∨},J_{∧∨},v_{∧∨}) \;\; = \;\; \pu\orand$$
%
distinguishes all equivalence classes in $\ECube^*_∧$ and in
$\ECube^*_∨$, but not in $\ECube^*_→$... it ``thinks'' that $P→Q$ and
$P^*→Q$ are equal.

\directlua{tf_pop()}



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