% (find-LATEX "2020bell-lst.tex")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2020bell-lst.tex" :end))
% (defun D () (interactive) (find-pdf-page      "~/LATEX/2020bell-lst.pdf"))
% (defun d () (interactive) (find-pdftools-page "~/LATEX/2020bell-lst.pdf"))
% (defun e () (interactive) (find-LATEX "2020bell-lst.tex"))
% (defun u () (interactive) (find-latex-upload-links "2020bell-lst"))
% (defun v () (interactive) (find-2a '(e) '(d)) (g))
% (find-pdf-page   "~/LATEX/2020bell-lst.pdf")
% (find-sh0 "cp -v  ~/LATEX/2020bell-lst.pdf /tmp/")
% (find-sh0 "cp -v  ~/LATEX/2020bell-lst.pdf /tmp/pen/")
%   file:///home/edrx/LATEX/2020bell-lst.pdf
%               file:///tmp/2020bell-lst.pdf
%           file:///tmp/pen/2020bell-lst.pdf
% http://angg.twu.net/LATEX/2020bell-lst.pdf
% (find-LATEX "2019.mk")

% «.3._local_set_theory»	(to "3._local_set_theory")
% «.3.8._elim-ex-unique»	(to "3.8._elim-ex-unique")
% «.5._from_logic_to_sheaves»	(to "5._from_logic_to_sheaves")
% «.5.1.»			(to "5.1.")
% «.5.1.(1)_my_proof»		(to "5.1.(1)_my_proof")

\documentclass[oneside,12pt]{article}
\usepackage[colorlinks,citecolor=DarkRed,urlcolor=DarkRed]{hyperref} % (find-es "tex" "hyperref")
\usepackage{indentfirst}
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{pict2e}
\usepackage[x11names,svgnames]{xcolor} % (find-es "tex" "xcolor")
%\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
%
\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")
%
%\usepackage[backend=biber,
%   style=alphabetic]{biblatex}            % (find-es "tex" "biber")
%\addbibresource{catsem-slides.bib}        % (find-LATEX "catsem-slides.bib")
%
% (find-es "tex" "geometry")
\begin{document}

\catcode`\^^J=10
\directlua{dofile "dednat6load.lua"}  % (find-LATEX "dednat6load.lua")

\def\True {\textit{true}}
\def\False{\textit{false}}

% (find-belltpage (+ 14  70) "Logic operations, axioms and inference rules")
\def\L{\text{L}}

% (find-belltpage (+ 14  71) "basic axioms")
\def\Taut{\text{Taut}}
\def\Unit{\text{Unit}}
\def\Equa{\text{Equa}}
\def\Produ{\text{Produ}}
\def\Compr{\text{Compr}}
% (find-belltpage (+ 14  71) "rules of inference")
\def\Thin {\text{Thin}}
\def\Cut  {\text{Cut}}
\def\Subst{\text{Subst}}
\def\Ext  {\text{Ext}}
\def\Equiv{\text{Equiv}}

% (find-belltpage (+ 14 69) "(T6)")
% \setofsc is like \setofst but uses a colon instead of a "such that" bar
\def\setofc#1#2{\{\,#1\;:\;#2\,\}}
\def\setofc#1#2{\{\,#1\,:\,#2\,\}}
\def\setofc#1#2{\{\,#1  :  #2\,\}}



{\setlength{\parindent}{0em}
\footnotesize

Notes on Bell's ``Toposes and Local Set Theories'' (Oxford, 1988).

\ssk

These notes are at:

\url{http://angg.twu.net/LATEX/2020bell-lst.pdf}

\ssk

See:

\url{http://angg.twu.net/LATEX/2020favorite-conventions.pdf}

\url{http://angg.twu.net/math-b.html\#favorite-conventions}

I wrote these notes mostly to test if the conventions above
are good enough.

}



% «3._local_set_theory»  (to ".3._local_set_theory")

\section*{3. Local Set Theories}

(Page 70):

$$\begin{tabular}{llll}
  (L1) & $α⇔β$    & for & $α=β$ \\
  (L2) & $\True$  & for & $*=*$ \\
  (L3) & $α∧β$    & for & $〈α,β〉 = 〈\True,\True〉$ \\
  (L4) & $α⇒β$    & for & $(α∧β)⇔α$ \\
  (L5) & $∀xα$    & for & $\setofc{x}{α} = \setofc{x}{\True}$ \\
  (L6) & $\False$ & for & $∀ω.ω$ \\
  (L7) & $¬α$     & for & $α⇒\False$ \\
  (L8) & $α∨β$    & for & $∀ω[(α⇒ω∧β⇒ω)⇒ω]$ \\
  (L9) & $∃xα$    & for & $∀ω[∀x(α⇒ω)⇒ω]$ \\
  \end{tabular}
$$



(Page 71):

% (find-belltpage (+ 14  71) "basic axioms")
% (find-belltpage (+ 14  71) "rules of inference")

Basic axioms (left) and rules of inference (right):
%
%:
%:    ---\Taut
%:    α:α
%:
%:    ^Taut
%:
%:    ----\Unit
%:    :x_1=*
%:
%:    ^Unit
%:
%:    -----------------\Equa
%:    x=y,α(z/x):α(z/y)
%:
%:    ^Equa
%:
%:    -----------------\Produ
%:    :(〈x_1,\ldots,x_n〉)_i=x_i
%:
%:    ^Produ1
%:
%:    -----------------\Produ
%:    :x=〈(x)_1,\ldots,(x)_n)〉
%:
%:    ^Produ2
%:
%:    -----------------\Compr
%:    :x∈\setofc{x}{α}⇔α
%:
%:    ^Compr
%:
%:
%:     Γ:α
%:    -----\Thin
%:    β,Γ:α
%:
%:    ^Thin
%:
%:    Γ:α   α,Γ:β
%:    -----------\Cut
%:       Γ:β
%:
%:       ^Cut
%:
%:     Γ:α
%:    ------------\Subst
%:    Γ(x/τ):α(x/τ)
%:
%:    ^Subst
%:
%:    Γ:x∈σ⇔x∈τ
%:    ---------\Ext
%:      Γ:σ=τ
%:
%:      ^Ext
%:
%:    α,Γ:β  β,Γ:α
%:    ---------\Equiv
%:      Γ:α⇔β
%:
%:      ^Equiv
%:
$$\pu
  \begin{array}{c}
    \ded{Taut}   \\ \\
    \ded{Unit}   \\ \\
    \ded{Equa}   \\ \\
    \ded{Produ1} \\ \\
    \ded{Produ2} \\ \\
    \ded{Compr}  \\
  \end{array}
  \qquad
  \begin{array}{c}
    \ded{Thin}   \\ \\
    \ded{Cut}    \\ \\
    \ded{Subst}  \\ \\
    \ded{Ext}    \\ \\
    \ded{Equiv}  \\ \\
  \end{array}
$$


(Page 71):

(3.1.5) (i) and (ii):
%
%:
%:                                             ----\Unit   
%:                                             :*=*        
%:                                            ------(\L2)   
%:                                            :\True       
%:                              ---\Taut     -------\Thin  
%:                              α:α          α:\True       
%:                          ---------\Thin  ---------\Thin 
%:                          \True,α:α       α,α:\True      
%:              ---------   -------------------------\Equiv
%:  \True,α:α   α,α:\True        α:α⇔\True                 
%:  ---------------------        ---------(\L1)             
%:    α:α=\True                  α:α=\True                 
%:                                                         
%:    ^p73.1                     ^p73.1-my                 
%:
%:  
%:  
%:  
%:  
%:  
%:  
%:  
%:  
%:  
%:  
%:  
%:  
%:
%:  
%:
$$\pu
  \ded{p73.1}
  \quad \squigto \quad
  % \qquad
  \ded{p73.1-my}
$$
%:
%:
%:  ω=ω',ω':ω
%:  ---------------   ------
%:  α=\True,\True:α   :\True
%:  ------------------------
%:    α=\True:α
%:
%:    ^p73.2
%:
%:             ---------\Equa       
%:              ω=ω',ω':ω           
%:             ---------------\Subst
%:             α=\True,\True:α      
%:  ======     ---------------
%:  :\True     \True,α=\True:α
%:  --------------------------\Cut
%:    α=\True:α
%:
%:    ^p73.2-my
%:
%:
$$\pu
  \ded{p73.2}
  \quad \squigto \quad
  % \qquad
  \ded{p73.2-my}
$$


% (find-belltpage (+ 14  68) "3. Local Set Theories")
% (find-belltpage (+ 14  73)  "3.1 Conjunction")

\newpage

%  _____ _ _             _____      _ 
% | ____| (_)_ __ ___   | ____|_  _| |
% |  _| | | | '_ ` _ \  |  _| \ \/ / |
% | |___| | | | | | | | | |___ >  <|_|
% |_____|_|_|_| |_| |_| |_____/_/\_(_)
%                                     
% «3.8._elim-ex-unique»  (to ".3.8._elim-ex-unique")
% (lstp 3 "3.8._elim-ex-unique")
% (lst    "3.8._elim-ex-unique")

% (find-books "__cats/__cats.el" "bell-lst")
% (find-belltpage (+ 14 81) "Our final task in this section")
%
% (find-books "__cats/__cats.el" "taylor")
% (find-taylorpfmpage (+ 14  61)   "8. (...) proof-box rules for Ex!")
%
% (find-books "__logic/__logic.el" "mendelson")

\subsection*{3.8 Eliminability of descriptions}

(Page 81):

Our final task in this section is to show that local set theories
satisfy {\sl eliminability of descriptions for formulae} and {\sl for
  terms of power type}. To explain this, define the {\sl unique
  existential quantifier} $∃!$ by writing
%
$$∃!xα \quad \text{for} \quad ∃x(α∧∀y(α(x/y)⇒x=y)),$$
%
where $y$ is different from $x$ and not free in $α$. Then, if $α(x)$
is any formula and $x$ is any variable either of type $Ω$ or of power
type, we will exhibit a term $τ$ of the same type as $x$, for which we
have
%
$$∃!xα⊢α(x/τ)$$
%
$τ$ is thus an explicit term satisfying the description: `the unique
$x$ such that $α$'.

\msk

{\bf 3.8. Proposition} (Eliminability of descriptions for formulae)
%
$$∃!ωα ⊢ α(ω/α(ω/\True))$$




%  ____  _                               
% / ___|| |__   ___  __ ___   _____  ___ 
% \___ \| '_ \ / _ \/ _` \ \ / / _ \/ __|
%  ___) | | | |  __/ (_| |\ V /  __/\__ \
% |____/|_| |_|\___|\__,_| \_/ \___||___/
%                                        

\newpage

% «5._from_logic_to_sheaves»  (to ".5._from_logic_to_sheaves")
% (lstp 3 "5._from_logic_to_sheaves")
% (lst    "5._from_logic_to_sheaves")
% (find-books "__cats/__cats.el" "bell-lst")
% (find-belltpage (+ 14 162) "5. From Logic to Sheaves")
% (find-belltpage (+ 14 162)    "truth-set")
\section*{5. From Logic to Sheaves}

(Page 162):

{\bf Truth-sets, modalities, and universal closure operations}

(...)

More generally, an $S$-set $T$ such that $⊢T⊆Ω$ is called a {\sl
  truth-set} in $S$ if it satisfies the same conditions, viz.:

\msk

$\begin{array}{rl}
 (tr_0)  &  ⊢T⊆Ω      \\
 (tr_1)  &  ⊢\True∈T  \\
 (tr_2)  &  α⊢β \quad \text{implies} \quad α∈T⊢β∈T \\
 (tr_3)  &  (α∈T)∈T⊢α∈T  \\
 \end{array}
$

Let's write $α^*$ for $α∈T$. We can rewrite the above as:

$\begin{array}{rl}
 (tr_1)  &  ⊢\True^*  \\
 (tr_2)  &  α⊢β \quad \text{implies} \quad α^*⊢β^* \\
 (tr_3)  &  α^{**}⊢α^*  \\
 \end{array}
$


\msk

%  ____   _ 
% | ___| / |
% |___ \ | |
%  ___) || |
% |____(_)_|
%           
% «5.1.»  (to ".5.1.")
% (lstp 3 "5.1.")
% (lst    "5.1.")
% (find-belltpage (+ 14 162) "5.1. Proposition")

{\bf 5.1. Proposition.} Let $T$ be a truth-set in $S$. Then:

$\begin{array}{rl}
 (i)   & α∈T,β∈T ⊢ α∧β∈T,  \\
 (ii)  & α∈T, α⇒β∈T ⊢ β∈T, \\
 (iii) & α⇒β ⊢ α∈T⇒β∈T     \\
 \end{array}
$

i.e.,

$\begin{array}{rl}
 (i)   & α^*,β^*⊢(α∧β)^*      \\
 (ii)  & α^*, (α⇒β)^* ⊢ β^*   \\
 (iii) & α⇒β ⊢ α^*⇒β^*        \\
 \end{array}
$


\msk

Proof. (i) Let us write $α^*$ for $α∈T$. Then from $α⊢β=α∧β$ we deduce
$α⊢β^*=(α∧β)^*$, whence $α⊢β^*⇒(α∧β)^*$, so that
%
$$α,β^*⊢(α∧β)^*. \qquad (1)$$
%
Replacing $α$ by $α^*$ gives
%
$$α^*,β^*⊢(α^*∧β)^*, \qquad (2)$$
%
and interchanging $α$ and $β$ in (1) yields
%
$$α^*,β^*⊢(α^*∧β)^*, \qquad (3)$$
%

% (find-belltpage (+ 14 162) "5.1. Proposition")

(3) gives $...$, so by (tr2) $...$, whence $...$ by (tr3). This,
together with (2), gives $...$.

\newpage

%  ____   _      _____                    
% | ___| / |    / (_) \   _ __ ___  _   _ 
% |___ \ | |   | || || | | '_ ` _ \| | | |
%  ___) || |_  | || || | | | | | | | |_| |
% |____(_)_(_) | ||_|| | |_| |_| |_|\__, |
%               \_\ /_/             |___/ 
%
% «5.1.(1)_my_proof»  (to ".5.1.(1)_my_proof")
% (lstp 4 "5.1.(1)_my_proof")
% (lst    "5.1.(1)_my_proof")

{\bf My proof of 5.1.(1).}

%:
%:              -----                                          -----   
%:              α∧β⊢β                                          \a∧β⊢β   
%:   -------    ------                          -----------    --------  
%:   α∧β⊢α∧β    ⊢α∧β⇒β                          \a∧β⊢\a∧β      ⊢\a∧β⇒β  
%:   -------    -------                         -----------    -----------
%:   α⊢β⇒α∧β    α⊢α∧β⇒β                         \a⊢β⇒\a∧β      \a⊢\a∧β⇒β 
%:   ------------------                         -------------------------- 
%:      α⊢β=α∧β                                    \a⊢β=\a∧β         
%:      -------------                              ---------------
%:      α⊢β^*=(α∧β)^*                              \a⊢β^*=(\a∧β)^*   
%:      -------------      =================       ---------------
%:      α∧β^*⊢(α∧β)^*      α^*∧β^*⊢(α^*∧β)^*       \a∧β^*⊢(\a∧β)^*     
%:                                                                 
%:      ^5.1.(i)_a         ^5.1.(i)_b              5.1.(i)_awithdef            
%:
$$\pu
  \begin{array}{c}
  \ded{5.1.(i)_a} \qquad \ded{5.1.(i)_b} \\
  \end{array}
$$




{\bf Old stuff:}



%:
%:                         
%:   α⊢β=α{∧}β             α^*⊢β=α^*{∧}β             
%:   ---------------       ---------------       
%:   α⊢β^*=(α{∧}β)^*       α^*⊢β^*=(α^*{∧}β)^*       
%:   -----------------     -----------------     
%:   α⊢β^*{⇒}(α{∧}β)^*     α^*⊢β^*{⇒}(α^*{∧}β)^*      
%:   -----------------     -----------------     
%:   α,β^*⊢(α{∧}β)^*       α^*,β^*⊢(α^*{∧}β)^*       
%:   
%:   ^f1                   ^f2
%:
$$\pu
  \begin{array}{c}
  \ded{f1} \qquad \ded{f2} \\
  \end{array}
$$

%:
%:                             -----------                       -----------      
%:   α⊢β=α{∧}β                α^*⊢β=α^*{∧}β                      β⊢α=α{∧}β          
%:   ---------------          -----------------                 -----------------
%:   α⊢β^*=(α{∧}β)^*          α^*⊢β^*=(α^*{∧}β)^*                β⊢α^*=(α{∧}β)^*    
%:   -----------------       ---------------------                 -----------------
%:   α⊢β^*{⇒}(α{∧}β)^*       α^*⊢β^*{→}(α^*{∧}β)^*              β⊢α^*{→}(α{∧}β)^*     
%:   -----------------       ---------------------                 -----------------
%:   α,β^*⊢(α{∧}β)^*           α^*,β^*⊢(α^*{∧}β)^*               α^*,β⊢(α{∧}β)^*    
%:   -----------------         --------------------                 -----------------
%:   α{∧}β^*⊢(α{∧}β)^*         α^*{∧}β^*⊢(α^*{∧}β)^*            α^*{∧}β⊢(α{∧}β)^*    
%:   -----------------         ---------------------                 -----------------
%:   (α{∧}β^*)^*⊢(α{∧}β)^{**}   (α^*{∧}β^*)^*⊢(α^*{∧}β)^{**}    (α^*{∧}β)^*⊢(α{∧}β)^{**}    
%:   -----------------             -----------------                 -----------------
%:   (α{∧}β^*)^*⊢(α{∧}β)^*      (α^*{∧}β^*)^*⊢(α^*{∧}β)^*      (α^*{∧}β)^*⊢(α{∧}β)^*    
%:                                                                          
%:   ^foo1                              ^foo2                         ^foo3            
%:
$$\pu
  \begin{array}{c}
  \ded{foo1} \qquad \ded{foo2} \qquad \ded{foo3} \\
  \end{array}
$$




(What are these?)

$(tr'_1) \qquad ⊢⊤^*$

$(tr'_2) \qquad α⊢β \qquad α^*⊢β^*$

$(tr'_3) \qquad α^{**}⊢α^*$

$(tr'_4) \qquad α⊢α^*$

\msk

% (find-belltpage (+ 14 163)    "modality")
% (find-belltpage (+ 14 164)    "universal closure operation")



%:
%:                                                            ---------         ---------
%:                                                            α{∧}β⊢α         α{∧}β⊢β
%:   ========================    ========================     ---------------   ----------
%:   α^*{∧}β^*⊢(α^*{∧}β)^*    (α^*{∧}β)^*⊢(α{∧}β)^*          (α{∧}β)^*⊢α^*   (α{∧}β)^*⊢β^*
%:   ----------------------------------------------------       --------------------------------
%:   α^*{∧}β^*⊢(α{∧}β)^*                                         (α{∧}β)^*⊢α^*{∧}β^*
%:   ------------------------------------------------------------------------------------
%:                     ⊢α^*{∧}β^*=(α{∧}β)^*
%:
%:                      ^foo4  
%:   
%:                               =======================
%:                               ⊢α^*{∧}β^*=(α{∧}β)^*
%:                               -----------------------------
%:                               ⊢(α^*{∧}β^*)^*=(α{∧}β)^{**}
%:                               -----------------------------
%:                               ⊢(α^*{∧}β^*)^*=(α{∧}β)^*
%:   =======================     -----------------------------
%:   ⊢α^*{∧}β^*=(α{∧}β)^*        ⊢(α{∧}β)^*=(α^*{∧}β^*)^*
%:   -------------------------------------------------------
%:          ⊢α^*{∧}β^*=(α{∧}β)^*=(α^*{∧}β^*)^*
%:
%:            ^foo5
%:
$$\pu
  \begin{array}{c}
  \ded{foo4} \\ \\
  (i'): \quad \ded{foo5} \\
  \end{array}
$$
%:
%:                           ------------
%:                           α,α{→}β⊢β
%:                           ------------
%:                           α∧(α{→}β)⊢β
%:                           --------------------
%:                           (α∧(α{→}β))^*⊢β^*
%:                           --------------------
%:                           α^*∧(α{→}β)^*⊢β^*
%:                           --------------------
%:                           α^*,(α{→}β)^*⊢β^*
%:   ------------------      --------------------
%:   α{→}β⊢(α{→}β)^*         (α{→}β)^*⊢α^*{→}β^*
%:   ----------------------------------------------
%:       α{→}β⊢(α{→}β)^*⊢α^*{→}β^*
%:
%:         ^bar1
%:
%:
%:   -------------------   ----
%:   α{→}β⊢(α{→}β)=⊤       ⊤∈T
%:   --------------------------
%:      α{→}β⊢(α{→}β)∈T           α{→}β⊢(α{→}β)^*
%:
%:
%:   -------  ----
%:   α⊢α=⊤  ⊤∈T
%:   -------------
%:      α⊢α∈T
%:      -------
%:      α⊢α^*
%:
%:      ^tr4
%:
$$\pu
  \begin{array}{c}
  (0'): \quad \ded{tr4} \qquad
  (ii',iii'): \quad \ded{bar1} \\ \\
  \end{array}
$$



\newpage

Notes from 2017...

\msk

\def\dt#1#2{\sm{#1\\#2}}
\def\DT#1#2{\mat{#1\\↓\\#2}}
\def\PDT#1#2{\pmat{#1\\↓\\#2}}
\def\mt#1#2#3#4{\dt#1#2{↦}\dt#3#4}

$Ω=\PDT{\{\dt00,\dt01,\dt11\}}{\{\dt·0,\dt·1\}}$

$\{⊤\}=\PDT{\{\dt11\}}{\{\dt·1\}}$

\msk

$012$:
\quad
$μ=\PDT{\cmat{\mt0011,\, \mt0111,\, \mt1111}}{\cmat{\mt·0·1,\, \mt·1·1}}$
\quad
$T=Ω=\PDT{\{\dt00,\dt01,\dt11\}}{\{\dt·0,\dt·1\}}$

\msk

$0|12$:
\quad
$μ=\PDT{\cmat{\mt0000,\, \mt0111,\, \mt1111}}{\cmat{\mt·0·0,\, \mt·1·1}}$
\quad
$T=\PDT{\{\dt01,\dt11\}}{\{\dt·1\}}$

\msk

$01|2$:
\quad
$μ=\PDT{\cmat{\mt0001,\, \mt0101,\, \mt1111}}{\cmat{\mt·0·1,\, \mt·1·1}}$
\quad
$T=\PDT{\{\dt11\}}{\{\dt·0,\dt·1\}}$

\msk

$0|1|2$:
\quad
$μ=\PDT{\cmat{\mt0000,\, \mt0101,\, \mt1111}}{\cmat{\mt·0·0,\, \mt·1·1}}$
\quad
$T=\{⊤\}=\PDT{\{\dt11\}}{\{\dt·1\}}$




% (find-angg "LATEX/2017bell.tex")





% Gente, posso fazer uma pergunta sobre Local Set Theories? Se voces nao
% souberem eu pergunto no Zulip Chat, mas prefiro perguntar aqui
% primeiro...
% 
% Na pagina 71 o Bell define "sequents" e 5 regras de inferencia
% basicas, e a partir dai' ele mostra um monte de arvores de deducao
% nesse sistema dele, e vai definindo um monte de regras derivadas...
% 
% Em algum lugar bem mais adiante - num capitulo que eu entendo mal -
% ele define a Local Set Theory associada a um topos dado qualquer, e
% acho que so' a partir dai' esses sequentes vao passar a ter uma
% semantica clara.
% 
% Digamos que a gente esta' num topos E que a gente escolheu, e que a
% gente escolheu valores para P e Q - P e Q sao valores de verdade.
% 
% (Eu tenho tentado montar sempre exemplos concretos... por exemplo, na
% pagina 12 daqui - http://angg.twu.net/LATEX/2017planar-has-1.pdf - tem
% umas contas com desenhos em que eu fixo uma algebra de Heyting,
% escolho valores pra P e Q nessa HA - P := 10 e Q := 01 - e ai' calculo
% o valor de uma expressao grande envolvendo P e Q...)
% 
% Entao, digamos que a gente escolheu o topos E e valores de verdade P e
% Q.
% 
% A semantica para o sequente P:Q vai dizer que o "valor" de P:Q e' um
% valor de verdade "classico", i.e., ou "verdadeiro" ou "falso"? Ou vai
% dizer que o valor de P:Q vai ser um valor de verdade do topos, podendo
% ser algum valor intermediario entre "falso" e "verdadeiro"?
% 
% Obs: talvez eu devesse ter usado "|-_{S}" ao inves de ":" em alguns
% lugares...
% 
% Obs 2: o Bell prova um "soundness theorem" nas paginas 97 ate' 103,
% que nao sei se responde a minha pergunta - ainda nao entendi qual e' a
% semantica de cada sequente P:Q e de cada arvore de derivacao...
% 
% José Alvim
% puts, eu não sei não. Vou ter que pensar
% 
% Eduardo Ochs
% Tou achando que as duas semanticas funcionam, mas a em que o valor de
% verdade de cada sequente e' so' ou verdadeiro ou falso e' mais
% parecida com a que o Bell usa...


%\printbibliography

\end{document}

%  __  __       _        
% |  \/  | __ _| | _____ 
% | |\/| |/ _` | |/ / _ \
% | |  | | (_| |   <  __/
% |_|  |_|\__,_|_|\_\___|
%                        
% <make>

 (eepitch-shell)
 (eepitch-kill)
 (eepitch-shell)
# (find-LATEXfile "2019planar-has-1.mk")
make -f 2019.mk STEM=2020bell-lst veryclean
make -f 2019.mk STEM=2020bell-lst pdf

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