\section*{Introduction} \label{sec:introduction}

Logics of evidence and truth  (\textit{LET}s) are paradefinite (i.e.~paraconsistent and paracomplete)  logics that  extend  the logic of first-degree entailment (\ensuremath{FDE}), also known as Belnap-Dunn 4-valued logic, with a unary operator \ensuremath{{\circ}}\ that
recovers excluded middle and explosion
for sentences in its scope.   
    \textit{LET}s\  stemmed from the logics of formal inconsistency 
    (\textit{LFI}s, see e.g.~\cite{car.con.2016.book,car.con.mar.2007}), which, in turn, are a further development of the seminal work of da Costa  on paraconsistency (see e.g. \cite{costa1963,costa1974}).     In the latter, a sentence $\ensuremath{{\circ}} A$ means that $A$ is `well-behaved', and in \textit{LFI}s, that $A$ is `consistent'.\footnote{In da Costa's work, the notation is a bit different, it is written $A^\ensuremath{{\circ}}$     instead of $\ensuremath{{\circ}} A$. The notation $\ensuremath{{\circ}} A$ has been introduced  by Carnielli and Marcos  in \citep{car.mar.2002.tax}. } 
 \textit{LET}s, however,  have been conceived with a specific purpose, viz., to formalize the deductive behavior of positive and negative evidence, 
which   can be conclusive or non-conclusive (see e.g. \citep{qletf,letj,rod.ant.lu,letf}). 
    Thus, according to the intended intuitive interpretation,  a sentence  
$\ensuremath{{\circ}} A $ means that there is conclusive evidence for $A$, it is assumed that sentences for which the evidence 
available is considered conclusive behave classically, and \ensuremath{{\circ}}\ is called a classicality operator. 
 \textit{LET}s\  can    also be interpreted as   information-based logics, which are     
     logics suitable for processing
information in the sense of taking a database as a set of premises and drawing
conclusions from these premises in a sensible way. 
 In this case a
sentence $\ensuremath{{\circ}} A$  means that the information $A$, positive or negative,
is reliable. 

  

Sentential logics of evidence and truth studied so far comprise the logics  $LET_{F}$\ \citep{letf},  \ensuremath{LET_{K}}\ \cite{kolkata}, and \ensuremath{LET_{J}}\ \citep{letj}. 
\ensuremath{LET_{J}}\   and \ensuremath{LET_{K}}\ extend, respectively, Nelson's logic \textit{N4}\ and 
the logic \ensuremath{FDE^{\to}}\ with  
the following inferences: 
\begin{enumerate}
\item
$\ensuremath{{\circ}} A, A, \neg A \vdash B$,   \label{prop.exp.con}
\item
$\ensuremath{{\circ}} A \vdash   A \lor  \neg A $. \label{prop.pem.con}  
\end{enumerate} 
\noindent 
  \ensuremath{FDE^{\to}}\  is   \ensuremath{FDE}\ added with a classical implication, or equivalently obtained by adding  Peirce Law to \textit{N4}.    
$LET_{F}$\ \citep{letf} extends \ensuremath{FDE}\ with the inferences above and also a 
 non-classicality operator 
\ensuremath{{\bullet}},  dual to \ensuremath{{\circ}}, 
  the intuitive meaning of $\ensuremath{{\bullet}} A$ being  that there is no conclusive evidence available for $A$. 
The logic \ensuremath{LET_{F}^-}, which  is $LET_{F}$\ without the operator \ensuremath{{\bullet}},  is a  minimal logic of evidence and truth 
that extends \ensuremath{FDE}\ with only the inferences \ref{prop.exp.con} and  \ref{prop.pem.con} above. 
 Kripke models for a  first-order version of \ensuremath{LET_{F}^-}\ 
have been investigated in \citep{rod.ant.lu}.   Sound and complete non-deterministic  valuation semantics for sentential \textit{LET}s\ 
 can be found in \citep{kolkata, letj, letf} and Kripke-style   semantics in \citep{axioms, handbook.2022}. 
 None of these logics have been provided with deterministic finite-valued semantics, and we conjecture that they are indeed not (deterministically) finitely-valued. 
  Our main aim here is to obtain a finite-valued non-deterministic semantics for \ensuremath{LET_{K}}, as well as to introduce the sentential logics \ensuremath{LET_{K}^+}\ and \ensuremath{LET_{F}^+}\ together with sound, complete, and decidable  
6-valued semantics for them. 
These logics extend, respectively, \ensuremath{LET_{K}}\ and \ensuremath{LET_{F}^-}\ with  rules 
 of propagation of clasicality, which are  inference rules 
that express how the 
operator \ensuremath{{\circ}}\ is transmitted from less complex to more complex sentences, and vice-versa. 

\vspace{2mm}

The remaining of this paper is structured as follows. 
In Section~\ref{sec.lets.fde} we review the motivations and the conceptual aspects of \textit{LET}s, in particular how \textit{LET}s\ 
extend the four scenarios of \ensuremath{FDE}\ with two more scenarios of positive and negative reliable information.\footnote{Parts of Section 
\ref{sec.lets.fde} have already appeared in \citep{rod.ant.lu}. }   
In Section~\ref{sec.letk}, a natural deduction  system for \ensuremath{LET_{K}}\ is presented, together 
with a sound, complete, and decidable  6-valued semantics based on Nmatrices. 
This semantics is  non-deterministic, which means that the semantic values of complex formulas 
are not always functionally determined by the semantic values of their parts.   
Section~\ref{sec.letkp} introduces the  logic \ensuremath{LET_{K}^+}\  together 
with a sound, complete, and decidable \textit{deterministic} 6-valued semantics.
The latter is obtained by means of restrictions imposed to the non-deterministic 6-valued 
semantics for \ensuremath{LET_{K}}, and such restrictions correspond exactly to the rules of 
propagation of classicality added to \ensuremath{LET_{K}}. In this section we also show 
 that \ensuremath{LET_{K}^+}\ is algebraizable in the   sense of  
 Blok and  Pigozzi  \cite{blok:pig:89}. 
  In Section~\ref{sect-lattice}  
 we will show  how 
 the underlying algebra of the  logical matrices of \ensuremath{LET_{K}^+},   presented as a three-dimensional twist-structure,  
can be  generalized to twist-algebras based on arbitrary Boolean algebras.  
This yields a class of sound and complete twist-models for \ensuremath{LET_{K}^+}.  
It is also   proved that these models are, indeed, bounded lattices with 
    top and bottom elements   given by the semantic values $T$ and $F$, which correspond, respectively, to 
   the two scenarios of positive and negative 
   reliable     information added to the four scenarios of  \ensuremath{FDE}.  
 In this section we also discuss the lattice  \textbf{L6} and the semi-lattice \textbf{A6} as expansions of the 
well-known  lattices \textbf{L4} and \textbf{A4}, defined by the the four values of \ensuremath{FDE}\ in Belnap \cite{belnap.1977.how}. 
 In Section~\ref{sec.letfp}  we turn to the logic  \ensuremath{LET_{F}^+}, and show how the results obtained so far can be extended to \ensuremath{LET_{F}^+}. This analysis will raise an interesting relation between \ensuremath{LET_{F}^+}\  and the degree-preserving logic associated to a variety of algebras known as involutive Stone algebras.







\section{Logics of evidence and truth as extensions of \ensuremath{FDE}} \label{sec.lets.fde}



Belnap in  \citep{belnap.1977.how} introduced a 4-valued semantics for \ensuremath{FDE}\ designed to 
 represent the information stored in a possibly inconsistent and incomplete database.  The 
 motivation was to apply \ensuremath{FDE}\ as the underlying logic of   
 a  question-answering computer capable of dealing with incomplete and inconsistent information.  
Let positive information $A$ be the information conveyed by a sentence  $A$, while negative information $A$ is 
conveyed by $\neg A$. 
 The semantic values \textit{T}, \textit{F}, \textit{B} and \textit{N} 
   allow the following four scenarios to be expressed with respect to a given sentence $A$: 

\begin{enumerate}[resume]
 \item[i.] $v(A) = T$: $A$ holds and $\neg A$ does not hold (only positive information $A$); 
 \item[ii.]  $v(A) = F$: $\neg A$ holds and $A$ does not hold (only negative information $A$); 
  \item[iii.]  $v(A) = B$: both $A$ and $\neg A$ hold (contradictory information about $A$);  
  \item[iv.]  $v(A) = N$: neither $A$ nor $\neg A$ holds (no information about $A$).\footnote{Note that the 
  relational semantics introduced by 
Dunn \citep{dunn76} is essentially the same idea. Although the interpretation in terms of information was spelled out by 
Belnap in \citep{belnap.1977.how}, the corresponding conceptual and technical ideas were worked out by Dunn as well.  
For the historical background of \ensuremath{FDE}\ and its interpretation in terms of information, see Dunn \citep{dunn2019}.} 
\end{enumerate}

\noindent 
The semantic values \textit{T} and \textit{F} are not to be understood in the strong sense of 
the standard truth-values of classical
logic.  
Assigned to a sentence $A$, \textit{T}  is a `told true' sign, in the sense that the computer  `has been told' (only) that $A$ is true, 
while \textit{F}  is a `told false' sign, in the sense that the computer  `has been told' (only) that $A$ is false.  
It may be that the computer `has been told' both that $A$ is true and false, and in this case the value \textit{B} is assigned 
to $A$, and if the computer has no information about $A$, the value \textit{N} is assigned to $A$. 



Now, we turn to \textit{LET}s. As argued in  \cite[Sect.~2.3]{rod.car.llp}, 
the notion of evidence underlying \textit{LET}s\  
can be explained as the notion of information as \textit{meaningful data} (see e.g.~\cite{fetzer2004a}) \label{mean.data} 
to which a 
possibly non-factive justification has been added.   
Evidence, thus, is close to the notion of information underlying the interpretation of
\ensuremath{FDE}\  proposed by Belnap  and Dunn  (see e.g.  \citep{belnap.1977.how,dunn76,dunn2019}).   
\textit{LET}s,  indeed,  admit an interpretation in terms of positive and negative information, and in this case a
sentence $\ensuremath{{\circ}} A$ is intended to mean that the information $A$, positive or negative,
is reliable, 
 and when $\ensuremath{{\circ}} A$ does not hold, it means 
 that there is no reliable information about $A$. Note that $\ensuremath{{\circ}} A$, in fact, act as an additional information about some information: 
 it conveys the information that either the positive information $A$ or the negative information $A$ (i.e. $\neg A$) is considered 
 reliable.\footnote{For a more detailed discussion of the notion of evidence, see \citep{rod.car.llp}. Concerning the intuitive interpretation of \textit{LET}s\ in terms of information, see 
\citep{rod.ant.lu}.}  
 Thus, with the help of the classicality operator \ensuremath{{\circ}}, in addition to the four scenarios of \ensuremath{FDE}, two  more scenarios  can be expressed: 
 
\begin{enumerate}[resume]
 \item[v.] $\ensuremath{{\circ}} A$ and $A$ hold: reliable information that $A$ is true;  
 \item[vi.]  $\ensuremath{{\circ}} A$ and $\neg A$ hold: reliable information that $A$ is false.
 \end{enumerate}


\noindent 
\textit{LET}s\  establish a distinction that cannot be established within \ensuremath{FDE}, 
 for when the values \textit{T} or \textit{F} are assigned to $A$  in \ensuremath{FDE}\ this does not specify  
 whether such information is or is not reliable, which is precisely the
difference between scenarios (i) and (v), and (ii) and (vi) above. \textit{LET}s, thus,  are able to express the following 
six scenarios with respect to a sentence $A$: 


\begin{itemize}
\setlength\itemsep{-0.2em} \label{6-scenarios}
	\item[] {When} $ \ensuremath{{\circ}} A$ does not hold:
 \begin{itemize} 
	\item[i.] $ A$ holds, $ \neg A$ does not hold:   only positive information  $A$;
	\item[ii.] $ A$ does not hold, $ \neg A$ holds:  only negative information $A$;
	\item[iii.] Both $ A$ and $ \neg A$ hold: contradictory information about $A$;
	\item[iv.] Neither $ A$ nor $ \neg A$ hold: no information at all about $A$.
\end{itemize} 

 \vspace{1mm}

	\item[] {When} $ \ensuremath{{\circ}} A$ holds:

\begin{itemize}
	\item[v.]$ A$ holds: reliable positive information   $A$;
	\item[vi.]$ \neg A$ holds:  reliable negative information   $A$.
	\end{itemize}
\end{itemize}

\noindent\textit{LET}s, therefore,  combine  
Belnap and Dunn's proposal of a logic designed to be the underlying logic of
inconsistent and incomplete information bases with  the idea of a unary connective \ensuremath{{\circ}}\ added to a 
sub-classical logic  that  recovers classical logic for sentences in its scope.  
In the case of \textit{LET}s,
such sub-classical logic is \ensuremath{FDE}\ or an extension of \ensuremath{FDE}. 

 

\section{The logic \ensuremath{LET_{K}}}    \label{sec.letk}

We start by the logic \ensuremath{LET_{K}}, which extends the logic \ensuremath{FDE^{\to}}, which in turn is \ensuremath{FDE}\ extended with classical implication. 
 \ensuremath{FDE^{\to}}\ can also be defined just by adding $A\lor (A\to B)$ to Nelson's logic \textit{N4}. 
 From the semantical point of view, \ensuremath{FDE^{\to}}\ admits a 4-valued semantics 
that extends in a natural way the semantics of \ensuremath{FDE}\ (see \cite[p.~1036]{omo.wan.2017}). 
{As far as we know, the logic \ensuremath{FDE^{\to}}\ 
appeared for the first time in Pynko \cite[p.~70]{pynko.1999}, under the name $\mathcal{IDM}4$. It 
 appears in  Hazen et al. \cite[p.~165]{hazen} under the name \ensuremath{FDE^{\to}}, that we adopt here. }  
 
The sentential logic \ensuremath{LET_{K}}\ is \ensuremath{FDE^{\to}}\ extended with  the operator \ensuremath{{\circ}}\ and  rules that recover explosion and excluded middle, the inferences~\ref{prop.exp.con} and~\ref{prop.pem.con} above.   As already mentioned, to the best of our knowledge, \ensuremath{LET_{K}}\ is not (deterministically) finitely-valued.  It admits a Kripke-style semantics \cite{handbook.2022} and a valuation semantics  \citep{kolkata}.  
 The latter is a bivalued non-deterministic semantics, an approach introduced and investigated in the 1970s onwards by da Costa and  Loparic, among others (see e.g. \cite{costa1974,loparic.1986,loparic.alves,loparic.costa.1984}).     
The underlying idea of valuation semantics is to `mirror' the axioms and rules in terms of the semantic values 1 and 0. 
Since \ensuremath{LET_{K}}\ is paradefinite, the semantic values of literals $p$ and $\neg p$ are totally independent of each other, 
which is precisely the point of the four scenarios of \ensuremath{FDE}.  

 In what follows we will see a natural deduction system for \ensuremath{LET_{K}}, 
 together with an adequate valuation semantics.  
 Then, we will propose a 6-valued semantics for \ensuremath{LET_{K}}, based on Nmatrices,  
 with the semantic values $T, T_0, \textsf{b}, \textsf{n}, F_0, \mbox{ and } F$. 
 These values correspond to the six scenarios expressed by \textit{LET}s\ we just seen above: 
 $T$ and  $F$ mean, respectively,  
 positive and negative reliable information, $T_0$ and  $F_0$ mean, respectively,   
 positive and negative information 
 not marked as reliable, $\textsf{b}$ and $\textsf{n}$ mean, respectively, conflicting and absence of information.  
 We will see that the 6-valued semantics combine these six scenarios 
in a sensible way but,  as expected, it  is non-deterministic.  



 \begin{definition} \label{def.ND.letk} \ 

\vspace{1mm} \noindent
Consider the propositional signature  $\Sigma=\{\land,\lor,\to,\neg,\ensuremath{{\circ}}\}$.
A natural deduction system
over $\Sigma$ for the logic \ensuremath{LET_{K}}\ is given by the following inference rules: 

\vspace{2mm}

\begin{center}
 $\infer [{\land I}] {A \land B} {A & B}$ \hspace{1.6cm}
$\infer [{\land E}]  {A} {A \land B}  \hspace{2 mm} \infer []  {B} {A \land B}  $ \hspace{6mm}

\

$\infer [{\lor I}] {A \lor B} {A} \hspace{2 mm} \infer [] {A \lor B} {B}$ \hspace{1cm}
$\infer [{\lor E}] {C} {A \lor B & \infer*{C} {[A]} & \infer*{C} {[B]}}$\hspace{6mm}

\
 

$\infer [{\neg {\land} I}] {\neg(A \land B)} {\neg A } \hspace{2 mm} \infer [] {\neg(A \land B)} {\neg B}$\hspace{1cm}
$\infer [{\neg {\land} E}] {C} {\neg(A \land B) & \infer*{C} {[\neg A]} & \infer*{C} {[\neg B]}}$\hspace{6mm}

\

$\infer [{\neg {\lor} I}] {\neg(A \lor B)} {\neg A & \neg B}$ \hspace{1.2cm}
$\infer [{\neg {\lor} E}]  {\neg A} {\neg (A \lor B)}  \hspace{2 mm} \infer []  {\neg B} {\neg (A \lor B)}  $ \hspace{1mm}

\ 

$\infer [{DN}] {\neg \neg A} {A}  \hspace{2 mm} \infer [] {A} {\neg \neg A} $

\



 


		$\infer [{{\rightarrow} I}] {A \rightarrow B} {\infer*{B} {[A]}}$ \hspace{1cm}
		$\infer [\rightarrow E] {B} {A \rightarrow B & A}$ \hspace{7mm}
		$\infer [{\to_{CL}}] {A \lor (A \to B)} {} $


		\

		\vspace{1mm}

		$\infer [{\neg {\rightarrow} I}] {\neg(A \rightarrow B)} {A & \neg B}$\hspace{1.5cm}
		$\infer [{\neg {\rightarrow E}}] {A} {\neg (A \rightarrow B)} \hspace{2 mm} \infer [] {\neg B} {\neg (A \rightarrow B)}$

\

$\infer [{EXP^{\circ}}] {B} {\circ A & A & \neg A }$ \hspace{10 mm} 
 $\infer [{PEM^\ensuremath{{\circ}}}] {A \vee \neg A} {\ensuremath{{\circ}} A}$\hspace{6mm}

\end{center}

\vspace{1mm}\noindent A deduction of  $A$ from a set of premises $\Gamma$, $\Gamma\vdash_{\ensuremath{LET_{K}}} A$, 
is defined as usual  for natural deduction systems. 


\vspace{1mm} \noindent
The rules $\lor E$, $\neg {\land} E$ and ${\rightarrow} I$ are called {\em improper}, while the others are {\em proper}.  The axiom $\to_{CL}$ is neither a proper nor an improper inference rule. 
 

\end{definition}




\subsection{Valuation semantics for \ensuremath{LET_{K}}} \label{sec.bivalued.letk}

A sound and complete bivalued non-deterministic  semantics (a valuation semantics) for \ensuremath{LET_{K}}\ is given below (cf. \cite[Sects.~3.3.1-2]{kolkata}): 



\begin{definition}  \label{def-val-LETK} \

\vspace{1mm}
\noindent 
A  {\em bivaluation} for \ensuremath{LET_{K}}\ is a function $\rho:For(\Sigma) \to \{0,1\}$ satisfying the following properties:\\[1mm]
$\begin{array}{ll}
\mbox{(v1)} & \mbox{$\rho(A \land B)=1$ iff $\rho(A)=1$ and $\rho(B)=1$};\\[1mm]
\mbox{(v2)} & \mbox{$\rho(A \lor B)=1$ iff $\rho(A)=1$ or $\rho(B)=1$};\\[1mm]
\mbox{(v3)} &  \mbox{$\rho(A \to B)=1$ iff $\rho(A)=0$ or $\rho(B)=1$};\\[1mm]
\mbox{(v4)} & \mbox{$\rho(\neg\neg A) = 1$ iff $\rho(A) = 1$};\\[1mm]
\mbox{(v5)} & \mbox{$\rho(\neg (A \land B)) = 1$ iff $\rho(\neg A) = 1$ or  $\rho(\neg B) = 1$};\\[1mm]
\mbox{(v6)} & \mbox{$\rho(\neg (A \lor B)) = 1$ iff $\rho(\neg A) = 1$ and  $\rho(\neg B) = 1$};\\[1mm]
\mbox{(v7)} & \mbox{$\rho(\neg (A \to B)) = 1$ iff $\rho(A) = 1$ and  $\rho(\neg B) = 1$};\\[1mm]
\mbox{(v8)} & \mbox{if $\rho(\ensuremath{{\circ}} A)=1$, then: $\rho(\neg A)=1$ iff $\rho(A)=0$}.
\end{array}$\\[1mm]

\vspace{1mm} 

\noindent The semantical consequence relation $\models_{\ensuremath{LET_{K}}}^2$ of \ensuremath{LET_{K}}\ with respect to  bivaluations is defined as follows:  $\Gamma\models_{\ensuremath{LET_{K}}}^2 A$ \ if and only if, for every bivaluation $\rho$ for \ensuremath{LET_{K}}, if $\rho(B)=1$ for every $B \in \Gamma$ then $\rho(A)=1$.
\end{definition}



\begin{remark} \label{val-Boole}
The set ${\bf 2}=\{0,1\}$ can be equipped with a structure of Boolean algebra, where the operations are given as follows (with the natural order $0 \leq 1$): 
\begin{enumerate}
\item[i.] $\ensuremath{{\sim}} 0=1$ \ and \ $\ensuremath{{\sim}} 1=0$ (Boolean complement);
\item[ii.] $a \sqcap b = min\{a,b\}$ (infimum);
\item[iii.] $a \sqcup b = max\{a,b\}$ (supremum);
\item[iv.]  $a \Rightarrow b = max\{\ensuremath{{\sim}} a,b\}= \ensuremath{{\sim}} a \sqcup b$ (implication).
\end{enumerate}
The 2-element Boolean algebra with domain  {\bf2} will be denoted by  $\mathcal{B}_2$. It is well-known that $\mathcal{B}_2$ is the {\em generator} of the variety of Boolean algebras, which implies that a given equation in the signature of Boolean algebras holds in $\mathcal{B}_2$ iff it holds in {\em every} Boolean algebra (this fact will be used later in the proof of Theorem~\ref{sound-compLETKPswap}). 
\end{remark}

 
 
\begin{proposition} \ 

\vspace{1mm} 
\noindent A function $\rho:For(\Sigma) \to {\bf 2}$ is a bivaluation for \ensuremath{LET_{K}}\ if and only if it satisfies the following properties, expressed in the language of Boolean algebras:\\[1mm]


$\begin{array}{ll}
\mbox{(v1)}' & \rho(A \land B)= \rho(A) \sqcap \rho(B);\\[1mm]
\mbox{(v2)}' &  \rho(A \lor B)= \rho(A) \sqcup \rho(B);\\[1mm]
\mbox{(v3)}' &   \rho(A \to B)= \rho(A) \Rightarrow \rho(B)=\ensuremath{{\sim}} \rho(A) \sqcup \rho(B);\\[1mm]
\mbox{(v4)}' & \rho(\neg\neg A) = \rho(A);\\[1mm]
\mbox{(v5)}' & \rho(\neg (A \land B)) = \rho(\neg A) \sqcup \rho(\neg B);\\[1mm]
\mbox{(v6)}' & \rho(\neg (A \lor B)) = \rho(\neg A) \sqcap \rho(\neg B);\\[1mm]
\mbox{(v7)}' & \rho(\neg (A \to B)) = \rho(A) \sqcap \rho(\neg B);\\[1mm]
\mbox{(v8)}' & \rho(\ensuremath{{\circ}} A) \leq \rho(A) \sqcup \rho(\neg A) \ \mbox{ and } \ \rho(A) \sqcap \rho(\neg A) \sqcap \rho(\ensuremath{{\circ}} A)=0.
\end{array}$
\end{proposition} 

\noindent It is straightforward to  see that clauses (v1)$'-$(v7)$'$ correspond to clauses (v1)-(v7) of Definition~\ref{def-val-LETK}. 
Concerning the clause (v8)$'$, note that it corresponds  to the rules $PEM^\ensuremath{{\circ}}$ and $EXP^\ensuremath{{\circ}}$. 

\subsubsection{Soundness and completeness}

The proofs of soundness and completeness of \ensuremath{LET_{K}}\ with respect to the semantics above can be found in 
 \citep{kolkata}. However, in order to keep this paper as self-contained as possible, we will provide the main ideas behind these proofs, which will be adapted and extended to the system \ensuremath{LET_{K}^+}\ to be studied in the next sections.


\begin{definition} \label{def-F-sat-LETK}
Let $\Delta$ be a set of formulas over $\Sigma$, and let $F$ be a formula over $\Sigma$. The set $\Delta$ is said to be {\em $F$-saturated in \ensuremath{LET_{K}}} if: (1) $\Delta \nvdash_{\ensuremath{LET_{K}}} F$; and (2) if $A \notin \Delta$ then $\Delta,A \vdash_{\ensuremath{LET_{K}}} F$. 
\end{definition}


\begin{remark} \label{Lindenbaum-Los}
From a very general result for logic systems due to Lindenbaum and \L o\'s (see, for example, \cite[Theorem 22.2]{woj:84} or~\cite[Theorem~2.2.6]{car.con.2016.book}), 
the following property holds in \ensuremath{LET_{K}}\ (and, in fact, in any Tarskian and finitary logic): 

\begin{itemize}
\item[] If $\Gamma \nvdash_{\ensuremath{LET_{K}}} A$, then there exists a set $\Delta$ such that $\Gamma \subseteq \Delta$ and $\Delta$ is $A$-saturated in \ensuremath{LET_{K}}.
\end{itemize}
\end{remark}



\begin{proposition}\label{F-sat-LETK} \

\vspace{1mm}\noindent
Let $\Delta$ be an $F$-saturated set in \ensuremath{LET_{K}}. Then:\\[1mm]
(1) $A \in \Delta$ iff $\Delta \vdash_{\ensuremath{LET_{K}}} A$; \\[1mm]
(2) $A \land B \in \Delta$ iff $A \in \Delta$ and $B \in \Delta$; \\[1mm]
(3) $A \lor B \in \Delta$ iff $A \in \Delta$ or $B \in \Delta$;\\[1mm]
(4) $A \to B \in \Delta$ iff $A \notin \Delta$ or $B \in \Delta$;\\[1mm]
(5) $\neg(A \land B) \in \Delta$ iff $\neg A \in \Delta$ or $\neg B \in \Delta$;\\[1mm]
(6) $\neg(A \lor B) \in \Delta$ iff $\neg A \in \Delta$ and $\neg B \in \Delta$;\\[1mm]
(7) $\neg(A \to B) \in \Delta$ iff $A \in \Delta$ and $\neg B \in \Delta$;\\[1mm]
(8) $\neg\neg A \in \Delta$  iff $A \in \Delta$;\\[1mm]
(9) If $\ensuremath{{\circ}} A \in \Delta$  then: either $A \in \Delta$ or $\neg A \in \Delta$, but not both.
\begin{proof} Left to the reader (see  \citep{kolkata}). 
\end{proof}\end{proposition}



\begin{corollary} \label{val-F-sat-LETK}
Let $\Delta$ be a set of formulas which is  $F$-saturated in \ensuremath{LET_{K}}. Let $\rho_\Delta:For(\Sigma) \to {\bf 2}$ be the characteristic function of $\Delta$, that is: for every formula $A$, $\rho_\Delta(A)=1$ iff $A \in \Delta$ (iff $\Delta \vdash_{\ensuremath{LET_{K}}} A$, by Proposition~\ref{F-sat-LETK}(1)). Then, $\rho_\Delta$ is a bivaluation for \ensuremath{LET_{K}}.
\begin{proof}
It is an immediate consequence of Proposition~\ref{F-sat-LETK}(2)-(9).
\end{proof}
\end{corollary}




\begin{theorem}  [Soundness and completeness of \ensuremath{LET_{K}}\ w.r.t. bivaluation semantics] \label{adeq-LETK-bival}  \ 

\vspace{1mm}\noindent
For every set of formulas $\Gamma \cup \{A\} \subseteq For(\Sigma)$: 
$\Gamma \vdash_{\ensuremath{LET_{K}}} A$ \ iff \  $\Gamma\models_{\ensuremath{LET_{K}}}^2 A$.
\begin{proof} We will present only an sketch of the prof (see   details in  \citep{kolkata}). \ \\[1mm]
{\em `Only if' part (soundness)}: Let $\rho$ be a bivaluation for \ensuremath{LET_{K}}. It is immediate to see that, for every instance $A$ of an axiom of \ensuremath{LET_{K}}, $\rho(A)=1$. On the other hand, for every proper rule of \ensuremath{LET_{K}}\ (ie, for every rule which does not discharge hypothesis), if $\rho(A)=1$ for every premise of the rule then $\rho(B)=1$ for the consequence of the rule. Finally, if $B$ is the consequence of an improper rule (that is, a rule which depends on previous derivations in which some  hypothesis are discharged), it is also immediate to see, by induction hypothesis and by definition of $\rho$, that $\rho(B)=1$ provided that $\rho$ satisfies all the assumptions of the rule.\\[1mm]
{\em `If' part (completeness)}: Suppose that $\Gamma \nvdash_{\ensuremath{LET_{K}}} A$.  By Remark~\ref{Lindenbaum-Los}, there exists a set $\Delta$ such that $\Gamma \subseteq \Delta$ and $\Delta$ is $A$-saturated in \ensuremath{LET_{K}}. By Corollary~\ref{val-F-sat-LETK}, the characteristic function $\rho_\Delta$ of  $\Delta$ is a bivaluation for \ensuremath{LET_{K}}\ such that $\rho_\Delta(B)=1$ for every $B \in \Gamma$, but $\rho_\Delta(A)=0$. This shows that $\Gamma \not\models_{\ensuremath{LET_{K}}}^2 A$.
\end{proof}\end{theorem}



\subsection{A 6-valued (non-deterministic) semantics for \ensuremath{LET_{K}}} \label{sec.six.valued.semantics.LETK.decid}


  In this section we will present a 6-valued non-deterministic semantics for \ensuremath{LET_{K}}\  based on \textit{Nmatrices}. 
 The latter  are defined  from the bivalued semantics for \ensuremath{LET_{K}}\ we have just seen (Definition \ref{def-val-LETK}) 
 by means of {\em swap structures}, as will be  described below.


  
 An Nmatrix is a non-deterministic matrix yielded by a \textit{multialgebra}, which is  
  an algebraic structure  equipped with at least one \textit{multioperation}. The latter is  
  an operation that returns, to each input, a non-empty set of values instead of a single value.   
 Nmatrices are a generalization of logical matrices in which each entry of the matrices interpreting the connectives can produce a non-empty set of possible semantic values. 
 The valuations defined by means of Nmatrices choose an arbitrary value on such sets, returning thus a single semantic value for each formula. Nmatrices were formally introduced by Avron and Lev  \cite{avr:lev:01,avr:lev:05}, but there are several earlier antecedents in the literature of the use of non-deterministic matrices 
    (see e.g.~\cite{ivl:73,ivl:88,kear:81,res:62}). 
   
 

 A swap structure  for \ensuremath{LET_{K}}\ 
 is a multialgebra  whose domain is formed by triples $(z_1,z_2,z_3)$, called {\em snapshots}, over a
  Boolean algebra. 
 Each snapshot 
 represents a three-dimensional  semantic value in which the first coordinate $z_1$ represents the 
 (one-dimensional) semantic value of a formula $A$ in a given bivaluation $\rho$, while the other coordinates $z_2$ and $z_3$ represent  the  semantic values of $\neg A$ and $\circ A$, respectively, in this same bivaluation $\rho$.  
 A swap structure for a given logic {\bf L} yields a 
  non-de\-ter\-min\-is\-tic matrix in which the set of designated values is formed 
 by the snapshots $z$ such that $z_1=1$, which means that the formula in the position $z_1$ holds, or `is true'. 
 Nmatrices, from the technical point of view,  are multialgebras   
  together with a non-empty subset of its domain, which is the set  of {\em designated} values. Let us recall the formal notion of Nmatrices, as introduced in Avron \cite{avr:lev:01,avr:lev:05}:
  
 


\begin{definition}
Let $\Theta$ be a propositional signature. A non-deterministic matrix (Nmatrix, in short) is a structure $\mathcal{M}= \langle M, \textrm{D}, \mathcal{O}\rangle$ such that $M$ and \textrm{D} are non-empty sets (of truth-values and designated truth-values, respectively) such that $\textrm{D} \subseteq M$.  $\mathcal{O}$ is a map which assigns, to each $n$-ary connective $\#$ of $\Theta$, a function $\mathcal{O}(\#):M^n \to \wp(M)\setminus\{\emptyset\}$. A (legal) valuation over $\mathcal{M}$ is a function $v:For(\Theta) \to M$ such that $v(\#(A_1,\ldots,A_n)) \in  \mathcal{O}(\#)(v(A_1),\ldots,v(A_n))$ for every formula $\#(A_1,\ldots,A_n)$ over $\Theta$, where $\#$ is a $n$-ary connective. The consequence relation $\models_\mathcal{M}$ induced by $\mathcal{M}$ is defined as follows: given a set of formulas $\Gamma \cup \{A\}$,  $\Gamma \models_\mathcal{M} A$ if and only, for any valuation $v$  over $\mathcal{M}$,  $v(A) \in \textrm{D}$ provided that $v(B) \in \textrm{D}$ for every $B \in \Gamma$.
\end{definition}

\begin{remark} \label{val-matr}
It is worth noting that an ordinary logical matrix $\mathcal{M}$ is a particular case of Nmatrix in which each entry of each operator $\mathcal{O}(\#)$ returns a singleton set. Moreover, any valuation over a logical matrix $\mathcal{M}$, that is, any  function $v:For(\Theta) \to M$ such that $v(\#(A_1,\ldots,A_n)) = \mathcal{O}(\#)(v(A_1),\ldots,v(A_n))$ is a valuation over   $\mathcal{M}$ (seen as an Nmatrix).
\end{remark}

Now, from the bivalued semantics of \ensuremath{LET_{K}}\ (Definition \ref{def-val-LETK}),  
a 6-valued swap structure can be defined in a  natural way, yielding  a 6-valued Nmatrix for \ensuremath{LET_{K}}.
 Recall from Remark~\ref{val-Boole} the 
 two element Boolean algebra  $\mathcal{B}_2= \langle {\bf 2}, \sqcap,\sqcup,\Rightarrow,\ensuremath{{\sim}},0,1 \rangle$. We denote by ${\bf 2}^3$ the set of triples $z=(z_1,z_2,z_3)$ over ${\bf 2}$.

\begin{definition} \label{defNmatLETK}
The Nmatrix  $\mathcal{M}_{\ensuremath{LET_{K}}}= \langle \textsc{B}_{\ensuremath{LET_{K}}}, \textrm{D}, \mathcal{O}\rangle$  for \ensuremath{LET_{K}}\ over the Boolean algebra $\mathcal{B}_2$ is defined as follows: its domain is the set 
$$\textsc{B}_{\ensuremath{LET_{K}}}=\{z \in {\bf 2}^3 \ : \ z_3 \leq z_1 \sqcup z_2 \ \mbox{ and } \ z_1 \sqcap z_2 \sqcap z_3=0  \}.$$ 
That is, $\textsc{B}_{\ensuremath{LET_{K}}} = \big\{T, \, T_0, \, \textsf{b}, \, \textsf{n}, \, F_0, \, F\big\}$, where
$$\begin{array}{cc}
T=(1,0,1) & \textsf{n}=(0,0,0)\\
T_{0}=(1,0,0) & F_{0}=(0,1,0)\\
\textsf{b}=(1,1,0) &  F=(0,1,1)
\end{array}$$
The set of designated elements of $\mathcal{M}_{\ensuremath{LET_{K}}}$ is $\textrm{D}=\big\{z \in \textsc{B}_{\ensuremath{LET_{K}}} \ : \ z_1=1\big\} = \big\{T, \, T_0, \, \textsf{b}\big\}$, while $\textrm{ND}=\big\{z \in \textsc{B}_{\ensuremath{LET_{K}}} \ : \ z_1\neq 1\big\} = \big\{F, \, F_0, \, \textsf{n}\big\}$ is the set of non-designated truth-values. For  $\# \in \{\land, \lor, \to, \neg, \circ\}$
the multioperations $\mathcal{O}(\#)=\tilde{\#}$  are defined as follows, for every $z$ and $w$ in $\textsc{B}_{\ensuremath{LET_{K}}}$:\footnote{Note that $\textsc{B}_{\ensuremath{LET_{K}}}$, as well as its multioperations, can be defined over an arbitrary Boolean algebra besides $\mathcal{B}_2$. This will be done in Section~\ref{sect-lattice}.}

\begin{itemize} 
	\item[(i)] $z\,\tilde{\land}\,w = \{u\in \textsc{B}_{\ensuremath{LET_{K}}} \ : \ u_1=z_1\sqcap w_1 \ \mbox{ and } u_2=z_2\sqcup w_2\}$;
	\item[(ii)] $z\,\tilde{\lor}\,w = \{u\in \textsc{B}_{\ensuremath{LET_{K}}} \ : \ u_1=z_1\sqcup w_1 \ \mbox{ and } u_2=z_2\sqcap w_2\}$;
		\item[(iii)] $z\,\tilde{\to}\,w = \{u\in \textsc{B}_{\ensuremath{LET_{K}}} \ : \ u_1=z_1\Rightarrow w_1 \ \mbox{ and } u_2=z_1\sqcap w_2\}$;
\item[(iv)] $\tilde{\neg}\,z = \{u\in \textsc{B}_{\ensuremath{LET_{K}}} \ : \ u_1=z_2 \ \mbox{ and } u_2=z_1\}$;
	\item[(v)] $\tilde{\circ}\,z = \{u\in \textsc{B}_{\ensuremath{LET_{K}}} \ : \ u_1=z_3\}$.
\end{itemize}
\end{definition}

 


\begin{remark} \label{rem.swap-LETK} \ 
 
 \vspace{1mm}\noindent (i) The domain $\textsc{B}_{\ensuremath{LET_{K}}}$ above does not contain the triples $(0,0,1)$ and $(1,1,1)$.  
This  is justified as follows.   
A snapshot $z$ in $\textsc{B}_{\ensuremath{LET_{K}}}$ represents a triple   $(\rho(A),\rho(\neg A),\rho(\circ A))$ for some formula $A$ 
and bivaluation $\rho$ for \ensuremath{LET_{K}}. 
The restrictions  $z_3 \leq z_1 \sqcup z_2$ and $z_1 \sqcap z_2 \sqcap z_3=0$ comply with the  rules 
$PEM^\ensuremath{{\circ}}$ and $EXP^\ensuremath{{\circ}}$ and the clause (v8) of Definition~\ref{def-val-LETK}, which 
do not allow bivaluations $\rho$ such that $\rho(A) = \rho(\neg A)=0, \rho(\circ A) =1$, 
 nor $\rho(A) = \rho(\neg A)=\rho(\circ A) =   1$. 
 
  
\vspace{1mm}\noindent (ii) The bivalued semantics for \ensuremath{LET_{K}}\ makes it clear that   
the semantic values of $\neg A$ and $\ensuremath{{\circ}} A$ are not  functionally determined by the value of $A$. 
This is in line with the idea of  the six scenarios expressed by \textit{LET}s\ 
presented at page \pageref{6-scenarios} above. 
 The snapshots, in turn,  are able to express simultaneously the value of $A$, $\neg A$, and $\ensuremath{{\circ}} A$ in a given bivaluation, 
and so they are able to express (and to combine, as we will see in the item (iii) below) these six scenarios by means of the six semantic values:     
$T$ and $F$ represent, respectively, reliable information $A$ and $\neg A$;  
$T_0$ and $F_0$ represent     information $A$ and $\neg A$ not marked as reliable;  
and  $B$ and $N$ represent the scenarios with contradictory information and no information at all about $A$ (note that the values  $T$ and $F$ of \ensuremath{FDE}\ have became here $T_0$ and $F_0$). 


\vspace{1mm}\noindent (iii) The multioperations of Definition \ref{defNmatLETK} can also be presented
as follows:
\begin{itemize} 
	\item[(1)] $(z_1,z_2,z_3)\,\tilde{\land}\,(w_1,w_2,w_3) = (z_1\sqcap w_1,z_2\sqcup w_2,\_ )$;
	\item[(2)] $(z_1,z_2,z_3)\,\tilde{\lor}\,(w_1,w_2,w_3) = (z_1\sqcup w_1,z_2\sqcap w_2,\_ )$;
	\item[(3)] $(z_1,z_2,z_3)\,\tilde{\to}\,(w_1,w_2,w_3) = (z_1\Rightarrow w_1,z_1\sqcap w_2,\_ )$;
	\item[(4)] $\tilde{\neg}\,(z_1,z_2,z_3) = (z_2,z_1,\_ )$;
	\item[(5)] $\tilde{\circ}\,(z_1,z_2,z_3) = (z_3,\_ ,\_ )$.
\end{itemize}

\noindent Here, `$\_$' means that the respective coordinate can be filled arbitrarily with 0 or 1,
provided that the resulting triple belongs to $\textsc{B}_{\ensuremath{LET_{K}}}$,   i.e., the triple  is a snapshot for \ensuremath{LET_{K}}. 
 To illustrate  how these multioperations combine the six scenarios  expressed by  \textit{LET}s, consider a sentence $A \land B$ in a scenario 
such that there is   positive information  $A$ marked as reliable and negative information $B$ not marked as 
reliable.  
This would be expressed by a bivaluation $\rho$ such that:  
\begin{itemize}
\item[] $\rho(A)= 1, \rho(\neg A)= 0$, $\rho(\ensuremath{{\circ}} A)=1 \mbox{ and }   \rho(B)=0$, $\rho(\neg B)=1, \rho(\ensuremath{{\circ}} B)= 0,  $
\end{itemize}
\noindent and the corresponding snapshots 
\begin{itemize}
\item[] $ ( 1,  0 ,  1) = T \mbox{ and }   (0,1,0) = F_0.$
\end{itemize}
\noindent From Definition~\ref{def-val-LETK} (bivaluations),  we have that 
\begin{itemize}
\item[] $ \rho(A \land B) = 0$,  $\rho(\neg(A \land B)) = 1$,  and  $ \rho(\ensuremath{{\circ}} (A \land B))$ is undetermined, 
\end{itemize}
\noindent 
which is expressed by the triple $(0,1,\_)$, and the latter 
 is exactly what is given by the operation 
 $\tilde{\land}$ applied to the triples $(1,0,1)$ and  $(0,1,0)$. 
 In terms of the six semantic values, we have that when $v(A)= T$ and $v(B) = F_0$, $v(A\land B)$ is either $F$ 
 or $F_0$. 
\end{remark}

 
\subsubsection{Non-deterministic tables for \ensuremath{LET_{K}}}  \label{tablesLETKP}

The multioperations (1)-(5) above    can also be  described by means of the following non-deterministic
tables:

\

{\tiny \begin{center}
\noindent
\begin{tabular}{|c|c|c|c|c|c|c|} 
\hline
 $\tilde{\wedge}$ & $T$  & $T_0$   & $\textsf{b}$ & $\textsf{n}$ & $F_0$  & $F$\\[1mm]
 \hline \hline
    $T$    & $T, T_0$  & $T, T_0$ & $\textsf{b}$ & $\textsf{n}$ & $F, F_0$ & $F, F_0$   \\[1mm] \hline
     $T_0$    & $T, T_0$  & $T, T_0$ & $\textsf{b}$ & $\textsf{n}$ & $F, F_0$ & $F, F_0$  \\[1mm] \hline
     $\textsf{b}$    & $\textsf{b}$  & $\textsf{b}$ & $\textsf{b}$ & $F, F_0$ & $F, F_0$ & $F, F_0$  \\[1mm] \hline
     $\textsf{n}$    & $\textsf{n}$  & $\textsf{n}$ & $F, F_0$ & $\textsf{n}$ & $F, F_0$ & $F, F_0$  \\[1mm] \hline
     $F_0$    & $F, F_0$  & $F, F_0$ & $F, F_0$ & $F, F_0$ & $F, F_0$ & $F, F_0$  \\[1mm] \hline
     $F$    & $F, F_0$  & $F, F_0$ & $F, F_0$ & $F, F_0$ & $F, F_0$ & $F, F_0$  \\[1mm] \hline
\end{tabular}
\hspace{1mm}
\begin{tabular}{|c|c|c|c|c|c|c|}
\hline
 $\tilde{\vee}$ & $T$  & $T_0$  & $\textsf{b}$ & $\textsf{n}$ & $F_0$  & $F$ \\[1mm]
 \hline \hline
    $T$    & $T, T_0$  & $T, T_0$ & $T, T_0$ & $T, T_0$ & $T, T_0$ & $T, T_0$   \\[1mm] \hline
     $T_0$    & $T, T_0$  & $T, T_0$ & $T, T_0$ & $T, T_0$ & $T, T_0$ & $T, T_0$   \\[1mm] \hline
     $\textsf{b}$    & $T, T_0$  & $T, T_0$ & $\textsf{b}$ & $T, T_0$ & $\textsf{b}$ & $\textsf{b}$   \\[1mm] \hline
     $\textsf{n}$    & $T, T_0$  & $T, T_0$ & $T, T_0$ & $\textsf{n}$ & $\textsf{n}$ & $\textsf{n}$   \\[1mm] \hline
     $F_0$    & $T, T_0$  & $T, T_0$ & $\textsf{b}$ & $\textsf{n}$ & $F, F_0$ & $F, F_0$   \\[1mm] \hline
     $F$    & $T, T_0$  & $T, T_0$ & $\textsf{b}$ & $\textsf{n}$ & $F, F_0$ & $F, F_0$  \\[1mm] \hline
\end{tabular}
\end{center}
 }

\

{\tiny
\begin{center} \label{tables.letk}
\begin{tabular}{|c|c|c|c|c|c|c|}
\hline
 $\tilde{\to}$ & $T$  & $T_0$  & $\textsf{b}$ & $\textsf{n}$ & $F_0$  & $F$ \\[1mm]
 \hline \hline
    $T$    & $T, T_0$  & $T, T_0$ & $\textsf{b}$ & $\textsf{n}$ & $F, F_0$ & $F, F_0$   \\[1mm] \hline
     $T_0$    & $T, T_0$  & $T, T_0$ & $\textsf{b}$ & $\textsf{n}$ & $F, F_0$ & $F, F_0$  \\[1mm] \hline
     $\textsf{b}$    & $T, T_0$  & $T, T_0$ & $\textsf{b}$ & $\textsf{n}$ & $F, F_0$ & $F, F_0$  \\[1mm] \hline
     $\textsf{n}$    & $T, T_0$  & $T, T_0$ & $T, T_0$ & $T, T_0$ & $T, T_0$ & $T, T_0$  \\[1mm] \hline
     $F_0$    & $T, T_0$  & $T, T_0$ & $T, T_0$ & $T, T_0$ & $T, T_0$ & $T, T_0$  \\[1mm] \hline
     $F$    & $T, T_0$  & $T, T_0$ & $T, T_0$ & $T, T_0$ & $T, T_0$ & $T, T_0$  \\[1mm] \hline
\end{tabular}
\hspace{0.3cm}
\begin{tabular}{|c||c|} \hline
$\quad$ & $\tilde{\neg}$ \\[1mm]
 \hline \hline
    $T$   & $F, F_0$    \\[1mm] \hline
     $T_0$   & $F, F_0$    \\[1mm] \hline
     $\textsf{b}$   &$\textsf{b}$    \\[1mm] \hline
     $\textsf{n}$   & $\textsf{n}$    \\[1mm] \hline
     $F_0$   & $T, T_0$    \\[1mm] \hline
     $F$   & $T, T_0$    \\[1mm] \hline
\end{tabular}
\hspace{0.3cm}
\begin{tabular}{|c||c|}
\hline
 $\quad$ & $\tilde{\circ}$ \\[1mm]
 \hline \hline
    $T$   & \textrm{D}    \\[1mm] \hline
     $T_0$   & \textrm{ND}    \\[1mm] \hline
     $\textsf{b}$   & \textrm{ND}    \\[1mm] \hline
     $\textsf{n}$   & \textrm{ND}    \\[1mm] \hline
     $F_0$   & \textrm{ND}    \\[1mm] \hline
     $F$   & \textrm{D}    \\[1mm] \hline
\end{tabular}
\end{center}
}

\  


\noindent By simplicity, we write $X$ and $X,Y$ instead of $\{X\}$ and $\{X,Y\}$. 
Recall that $D$ and $ND$ denote, respectively, the set of  
designated and  non-designated values. 

 


\subsubsection{Soundness and completeness of the 6-valued semantics}


The 6-valued  semantics above,  as expected, is equivalent to the bivalued semantics 
of Definition   \ref{def-val-LETK}. 
Recall that, if $z \in \textsc{B}_{\ensuremath{LET_{K}}}$ then $z_i$ denotes the $ith$-coordinate of the triple $z$. Then: 

 
\begin{proposition} \label{lemma-sound-LETK}
For every valuation $v$  over the Nmatrix $\mathcal{M}_{\ensuremath{LET_{K}}}$  the mapping $\rho_v:For(\Sigma) \to {\bf2}$ given by $\rho_v(A)=v(A)_1$ is a bivaluation for \ensuremath{LET_{K}}\ such that: $\rho_v(A)=1$ \ iff \ $v(A) \in \textrm{D}$, for every formula $A$.
\begin{proof} Let $A,B \in For(\Sigma)$. Since $v$ is a valuation over $\mathcal{M}_{\ensuremath{LET_{K}}}$ it satisfies the following:
$$\begin{array}{ll}
	v(\#\,A) \in  \tilde{\#}\,v(A) & \mbox{ for $\# \in \{\neg,\ensuremath{{\circ}}\}$}\\
	v(A \,\#\, B) \in v(A) \,\tilde{\#}\, v(B) & \mbox{ for $\# \in \{\land,\lor,\to\}$}\\
	\end{array}$$
Thus, by definition of $\rho_v$, by Definition~\ref{defNmatLETK} and by the fact that $v$ is a valuation over  $\mathcal{M}_{\ensuremath{LET_{K}}}$, $\rho_v(\neg A)=v(\neg A)_1=v(A)_2$ and $\rho_v(\ensuremath{{\circ}} A)=v(\ensuremath{{\circ}} A)_1=v(A)_3$. Moreover: 
	$$\begin{array}{lll}
	\rho_v(A \land B) &=&  v(A\land B)_1=v(A)_1 \sqcap v(B)_1=\rho_v(A) \sqcap \rho_v(B)\\
	\rho_v(A \lor B) &=&  v(A\lor B)_1=v(A)_1 \sqcup v(B)_1=\rho_v(A) \sqcup \rho_v(B)\\
	\rho_v(A \to B) &=&  v(A\to B)_1=v(A)_1 \Rightarrow v(B)_1=\rho_v(A) \Rightarrow \rho_v(B).
	\end{array}$$
Hence, by Remark~\ref{val-Boole}, $\rho_v$ satisfies clauses (v1)-(v3). On the other hand, $\rho_v(\neg\neg A)=v(\neg A)_2=v(A)_1=\rho_v(A)$ and so $\rho_v$ satisfies (v4). In addition, 
$$\rho_v(\neg(A \land B))=v(\neg(A \land B))_1=v(A \land B)_2=v(A)_2 \sqcup v(B)_2=\rho_v(\neg A) \sqcup \rho_v(\neg B)$$
and so $\rho_v$ satisfies clause (v5), by Remark~\ref{val-Boole}. Analogously, it is proven that $\rho_v$ satisfies clauses (v6) and (v7). Finally, since $v(A) \in \textsc{B}_{\ensuremath{LET_{K}}}$ then $v(A)_3 \leq v(A)_1 \sqcup v(A)_2$ and $v(A)_1 \sqcap v(A)_2 \sqcap v(A)_3=0$. That is, $\rho_v(\ensuremath{{\circ}} A) \leq \rho_v(A) \sqcup \rho_v(\neg A)$ and $\rho_v(A) \sqcap \rho_v(\neg A) \sqcap \rho_v(\ensuremath{{\circ}} A)=0$. By Remark~\ref{val-Boole}, this means that $\rho_v$ satisfies (v8). This shows that $\rho_v$ is a bivaluation for \ensuremath{LET_{K}}\ such that, by definition,  $\rho_v(A)=1$ \ iff \ $v(A) \in \textrm{D}$, for every formula $A$.
\end{proof}
\end{proposition}



\begin{theorem} [Soundness of \ensuremath{LET_{K}}\ w.r.t. the Nmatrix $\mathcal{M}_{\ensuremath{LET_{K}}}$] \label{sound-Nmat-LETK} \ \\
	For every set of formulas $\Gamma \cup \{A\} \subseteq For(\Sigma)$: 
	$\Gamma \vdash_{\ensuremath{LET_{K}}} A$ \ implies that \  $\Gamma\models_{\mathcal{M}_{\ensuremath{LET_{K}}}} A$.
\begin{proof} 
Suppose that $\Gamma \vdash_{\ensuremath{LET_{K}}} A$. By Theorem~\ref{adeq-LETK-bival},  $\Gamma\models_{\ensuremath{LET_{K}}}^2 A$. Let $v$ be a valuation  over the Nmatrix $\mathcal{M}_{\ensuremath{LET_{K}}}$ such that $v(B)  \in \textrm{D}$ for every $B \in \Gamma$, and let $\rho_v$ be the bivaluation for \ensuremath{LET_{K}}\ defined from $v$ as in Proposition~\ref{lemma-sound-LETK}. Since $\rho_v(B)=1$ for every $B \in \Gamma$ then $\rho_v(A) =1$, given that $\Gamma\models_{\ensuremath{LET_{K}}}^2 A$. From this $v(A)\in D$, showing that $\Gamma\models_{\mathcal{M}_{\ensuremath{LET_{K}}}} A$.
\end{proof}\end{theorem}


\vspace{1mm}

The completeness of \ensuremath{LET_{K}}\ w.r.t.~the 6-valued Nmatrix semantics will be proved in a similar way, based once again on Theorem~\ref{adeq-LETK-bival}.

\begin{proposition} \label{lemma-comple-LETK}
For every bivaluation $\rho$ for \ensuremath{LET_{K}}\  the mapping $v_{\rho}:For(\Sigma) \to \textsc{B}_{\ensuremath{LET_{K}}}$ given by $v_{\rho}(A)=(\rho(A),\rho(\neg A),\rho(\circ A))$ is a valuation over the Nmatrix $\mathcal{M}_{\ensuremath{LET_{K}}}$ such that: $v_{\rho}(A) \in \textrm{D}$ \ iff \ $\rho(A)=1$, for every formula $A$.
\begin{proof} Clearly $v_{\rho}(A) \in \textsc{B}_{\ensuremath{LET_{K}}}$, hence the function is well-defined. Let $A,B \in For(\Sigma)$. Then, if $a=\rho(\circ (A \land B))$ we have: 
	$$\begin{array}{lll}
	v_{\rho}(A \land B) &=&  (\rho(A\land B),\rho(\neg(A\land B)),a)\\
	&=& (\rho(A)\sqcap \rho(B),\rho(\neg A)\sqcup \rho(\neg B),a) \in v_{\rho}(A)\,\tilde{\land}\, v_{\rho}(B).
	\end{array}$$
The cases of $\lor$ and $\to$ are proved analogously. Concerning negation, let $b=\rho(\circ \neg A)$. Then:
	$$\begin{array}{lll}
	v_{\rho}(\neg A) &=&  (\rho(\neg A),\rho(\neg\neg A),b)\\
	&=& (\rho(\neg A),\rho(A),b) \in \tilde{\neg}\, v_{\rho}(A).
	\end{array}$$
Finally, if $a=\rho(\neg\ensuremath{{\circ}} A)$ and $b=\rho(\ensuremath{{\circ}}\cons A)$ then
	$$\begin{array}{lll}
	v_{\rho}(\ensuremath{{\circ}} A) &=&  (\rho(\ensuremath{{\circ}} A),a,b)  \in \tilde{\ensuremath{{\circ}}}\, v_{\rho}(A).
	\end{array}$$
		This shows that $v_\rho$ is a bivaluation for \ensuremath{LET_{K}}\ such that, by definition,   $v_\rho(A) \in \textrm{D}$ \ iff \ $\rho(A)=1$, for every formula $A$.       
\end{proof}\end{proposition}



\begin{theorem} [Completeness of \ensuremath{LET_{K}}\ w.r.t. the Nmatrix $\mathcal{M}_{\ensuremath{LET_{K}}}$] \label{comp-Nmat-LETK} \ \\
	For every set of formulas $\Gamma \cup \{A\} \subseteq For(\Sigma)$: 
	$\Gamma \models_{\mathcal{M}_{\ensuremath{LET_{K}}}} A$ \ iff \  $\Gamma \vdash_{\ensuremath{LET_{K}}} A$.
\begin{proof} Assume that $\Gamma\models_{\mathcal{M}_{\ensuremath{LET_{K}}}} A$, and let $\rho$ be a bivaluation for \ensuremath{LET_{K}}\ such that $\rho(B)=1$ for every $B \in \Gamma$. Let $v_{\rho}$ be defined from $\rho$ as in Proposition~\ref{lemma-comple-LETK}. Then, $v_{\rho}$ is a valuation over $\mathcal{M}_{\ensuremath{LET_{K}}}$ such that $v_{\rho}(B) \in \textrm{D}$, for every $B \in \Gamma$. By hypothesis, $v_{\rho}(A) \in \textrm{D}$, whence $\rho(A)=1$. This shows that  $\Gamma\models_{\ensuremath{LET_{K}}}^2 A$. By completeness of \ensuremath{LET_{K}}\ w.r.t. bivaluations, $\Gamma \vdash_{\ensuremath{LET_{K}}} A$.
\end{proof}\end{theorem}



\begin{corollary} \ 

\vspace{2mm}\noindent 
The 6-valued  Nmatrix $\mathcal{M}_{\ensuremath{LET_{K}}}$ provides a decision procedure for \ensuremath{LET_{K}}. 
\begin{proof}
It is well-known that finite Nmatrices, like the one above, provide  
 decision procedures. This is because  the number of sentential variables is finite, 
 the number of bifurcated lines  is always finite, and clearly there is no loop in the procedure. 
\end{proof}
\end{corollary}


 

\section{Adding propagation rules to \ensuremath{LET_{K}}: the logic \ensuremath{LET_{K}^+}} \label{sec.letkp}



 
 
 
In a wide sense, propagation of  classicality is how classical   behavior propagates from less complex to more complex sentences, 
and vice-versa. The   \textit{LET}s\ investigated so far (\ensuremath{LET_{J}}, $LET_{F}$, \ensuremath{LET_{K}}, \ensuremath{LET_{F}^-}) enjoy the following property: 


\begin{proposition}\label{propag.cla} \

\vspace{1mm}
\noindent Let $\textbf{L} \in \{ \mbox{\ensuremath{LET_{F}^-}, \ensuremath{LET_{J}}, \ensuremath{LET_{K}}, $LET_{F}$} \}$.  
Let $\Gamma = \{\circ \neg^{n_1}A_1, \dots, \circ \neg^{n_m}A_m \}$, for $n_i \geq 0$ (where $ \neg^{n_i} $,  
		$ n_i \geq 0 $, represents $ n_i $ occurrences  of negations before the formula $ A_i $). Then, for any formula $B$ formed with $A_1, \dots, A_m $ over the  signature $\{ \neg, \land, \lor, \to\}$ (and $\{ \neg, \land, \lor  \}$ in the case of $LET_{F}$\ and \ensuremath{LET_{F}^-}), 
$\Gamma\vdash_{\textbf{L}} B \lor \neg B $, and $\Gamma, B , \neg B \vdash_{\textbf{L}} C$, 
that is, $B$ behaves classically in this context. 

	\begin{proof} This result is proved for $LET_{F}$\ in   \cite[Fact~31]{letf}, and for \ensuremath{LET_{J}}\ in \cite[Proposition~7]{axioms}. 
	Proofs for \ensuremath{LET_{F}^-}\ and \ensuremath{LET_{K}}\ can be obtained similarly. 
	\end{proof} \end{proposition}

\noindent However, although in the \textit{LET}s\ studied so far the classical behavior is transmitted 
from less complex to more complex formulas, 
the classicality operator \ensuremath{{\circ}}\ is not, 
that is, the  inferences 
$\ensuremath{{\circ}} p \vdash \ensuremath{{\circ}}\neg p$ and $\ensuremath{{\circ}} p,\ensuremath{{\circ}} q \vdash \ensuremath{{\circ}}(p \ast q)$ ($\ast \in \{\lor, \land \}$), 
for example,  do not hold.  
 This should be clear in \ensuremath{LET_{K}}, for example,  from the fact that there is no introduction rule for \ensuremath{{\circ}}, 
 but    the reader can also check that from the 6-valued matrices presented in 
 Section~\ref{sec.six.valued.semantics.LETK.decid}, 
 which explicitly display 
the non-deterministic behavior of \ensuremath{{\circ}}. 
 But to express rigorously  the idea of dividing the sentences of the language into two groups, 
which is an essential 
point of \textit{LET}s\  (and \textit{LFI}s\ and  da Costa's $Cn$ hierarchy)  
it would be desirable for the classicality operator \ensuremath{{\circ}}\  to be transmitted as well.



   
We find in the literature two ways of establishing the propagation of \ensuremath{{\circ}}, 
but neither fits  
 the intended interpretation  of \textit{LET}s.  
 In da Costa's $Cn$ hierarchy, the well-behavior of $A$ (originally represented by $A^\ensuremath{{\circ}}$) 
propagates as follows:  

\begin{enumerate}[resume]
\item  $\ensuremath{{\circ}} A \land \ensuremath{{\circ}} B \vdash \ensuremath{{\circ}}(A \ast B), \ast  \in \{ \land, \lor, \to \}. $ \label{prop.newton}
\end{enumerate}

\noindent Although   \ref{prop.newton} fits  with   Proposition \ref{propag.cla} above, it puts a too strong condition 
for propagation of classicality.  
Indeed, we will see that it is not always necessary that both $\ensuremath{{\circ}} A$ and $\ensuremath{{\circ}} B$ hold for concluding $\ensuremath{{\circ}} (A \ast B)$. 
On the other hand,  in the logic  \textit{Cilo}, an \textit{LFI}\ investigated in  \cite[pp.~116ff.]{car.con.2016.book}, consistency propagates as follows:    
\begin{enumerate}[resume]
\item  $\ensuremath{{\circ}} A \lor \ensuremath{{\circ}} B \vdash \ensuremath{{\circ}}(A \ast B), \ast  \in \{ \land, \lor, \to \}. $ \label{prop.bez}
\end{enumerate}
\noindent The condition for propagation in \ref{prop.bez}, however, is too weak in the sense that 
it allows to conclude $\ensuremath{{\circ}} (A \ast B)$ in circumstances where it should not be concluded. 
Let us illustrate this by taking a look at how \ensuremath{{\circ}}\ should be transmitted over $\lor $. 

 
Recall that  $\ensuremath{{\circ}} A \land A$  and   $\ensuremath{{\circ}} A \land \neg A$  
are intended to mean  that the  information conveyed, respectively,  by $A$ 
 and by $\neg A$, is considered reliable. 
  Besides, 
  positive and negative reliable  information behaves like truth and falsity in classical logic.  
 As a consequence, from  $\ensuremath{{\circ}} A \land A$ one should be able to infer  that $A \lor B$ is also 
reliable, for any $B$, no matter whether $\ensuremath{{\circ}} B$ 
holds or not, and so $\ensuremath{{\circ}}(A \lor B) \land (A \lor B)$ 
holds. 
For if this were not the case, that is, if both $(A \lor B)$ and $\neg(A \lor B)$ held, 
$\ensuremath{{\circ}} A$ could not hold, 
since $\neg (A \lor B)$ implies $\neg A$. 
On the other hand, from  $\ensuremath{{\circ}} A \land \neg A$, it cannot be inferred that $\neg(A \lor B)$ is 
reliable, because 
  to conclude $\neg(A \lor B)$ both $\neg A$ and $\neg B$ are required. Hence, from $\ensuremath{{\circ}} A \land \neg A$, 
  $\ensuremath{{\circ}}(A \lor B)$ cannot be inferred. 
This    suggests the validity of the following inferences:   
\begin{enumerate}[resume]
\item $\ensuremath{{\circ}} A, A \vdash \ensuremath{{\circ}} (A \lor B) \land (A \lor B)$,  \label{inf.1}
\item $\ensuremath{{\circ}} B, B \vdash \ensuremath{{\circ}} (A \lor B) \land (A \lor B)$, 
\item $\ensuremath{{\circ}} A, \neg A, \ensuremath{{\circ}}  B, \neg B \vdash \ensuremath{{\circ}} (A \lor B) \land \neg(A \lor B)$. \label{inf.last}  
\end{enumerate}

\noindent and so on.   The point of these inferences is that  
positive (resp. negative) 
reliable information behaves like truth  (resp. falsity) 
in  classical logic: in order to have a $A \lor B$ false,  we need both $A$ and $B$ false, 
but $A$ true is enough to conclude 
$A\lor B$ true.\footnote{It is to be noted  that the fact that reliable information is subjected to classical logic,  
 and so  to the rules of preservation of truth,  
 does not mean, of course, that reliable information is  being \textit{identified}   with truth,  
 in the realist sense of the notion of truth that underlies the standard  interpretation 
 of classical logic. 
We are, rather, making the weaker claim that people reason with reliable information as if it were 
true, and so classical logic is appropriate to express the deductive behavior of reliable information.}  
  In the following, in order to   define the system \ensuremath{LET_{K}^+}, 
 we will extend this line of reasoning to  the connectives $\ensuremath{\lnot}$, 
  $\land$,  and $\to$. 


\begin{definition}    \label{propag-rules}  \ 

\vspace{1mm}\noindent Notational Definitions: for any formula $A$, let  $A^T \ensuremath{~\stackrel{\text{{\tiny def }}}{=}~} \ensuremath{{\circ}} A \land A$ and $A^F \ensuremath{~\stackrel{\text{{\tiny def }}}{=}~} \ensuremath{{\circ}} A \land \neg A$.  

\vspace{1mm}\noindent A natural deduction system for \ensuremath{LET_{K}^+}\ is obtained by adding the following axiom and rules to the  system 
of \ensuremath{LET_{K}}\ (Definition~\ref{def.ND.letk}): 


\begin{center}

\vspace{4mm}

$\infer [_{[I \ensuremath{{\circ}}]}] {\ensuremath{{\circ}}\cons A}{}$ \hspace{12mm} $\infer[_{[I \neg\ensuremath{{\circ}}]}] {\ensuremath{{\circ}} \neg A}{\ensuremath{{\circ}} A}$  \hspace{12mm} $\infer [_{[E \neg\ensuremath{{\circ}}]}] {\ensuremath{{\circ}} A} {\ensuremath{{\circ}} \neg A}$


\vspace{4mm}

$\infer [_{[I\land T]}] {(A \land B)^T} {A^T & B^T}$ \hspace{12mm}
$\infer [_{[I\land F]}] {(A \land B)^F} {A^F} \hspace{2 mm} \infer [] {(A \land B)^F} {B^F}$ \hspace{10mm}


\vspace{4mm}

$\infer [_{[I\lor T]}] {(A \lor B)^T} {A^T} \hspace{2 mm} \infer [] {(A \lor B)^T} {B^T}$ \hspace{10mm}
$\infer [_{[I\lor F]}] {(A \lor B)^F} {A^F & B^F}$ \hspace{10mm}


\vspace{4mm}

$  \infer  [_{[I\to T]}] {(A \to B)^T} {A^F} \hspace{2mm}  \infer [] {(A \to B)^T}  {B^T} $ \hspace{10mm}
$ \infer [_{[I\to F]}]  {(A \to B)^F} {A  & B^F }$

\vspace{4mm}

 $\infer [_{[E\land T]}]  {A^T} {(A \land B)^T}  \hspace{2 mm} \infer []  {B^T} {(A \land B)^T}  $ \hspace{10mm}
$\infer [_{[E\land F]}] {C} {(A \land B)^F & \infer*{C} {[A^F]} & \infer*{C} {[B^F]}}$\hspace{6mm}


\vspace{4mm}


 $\infer [_{[E\lor T]}] {C} {(A \lor B)^T & \infer*{C} {[A^T]} & \infer*{C} {[B^T]}}$\hspace{10mm}
$\infer [_{[E\lor F]}]  {A^F} {(A \lor B)^F}  \hspace{2 mm} \infer []  {B^F} {(A \lor B)^F}  $ \hspace{8mm}

\vspace{4mm} 


$\infer [_{[E\to T]}] {C} {(A \to B)^T & \infer*{C} {[A^F]} & \infer*{C} {[B^T]}}$
\hspace{10mm}
$\infer [_{[E\to F]}]  {A} {(A \to B)^F}  \hspace{2 mm} \infer []  {B^F} {(A \to B)^F}  $ \hspace{8mm}
\end{center}


\vspace{2mm}

\noindent A deduction of  $A$ from a set of premises $\Gamma$, $\Gamma\vdash_{\ensuremath{LET_{K}^+}} A$, 
is defined as usual  for natural deduction systems. 

\end{definition}


\begin{proposition} \label{der-rules} \ 

\vspace{1mm}\noindent 
The following  rules are derived in  \ensuremath{LET_{K}^+}:  

\begin{center}
$\infer [_{[Cons]}]  {B} {\ensuremath{{\circ}} A & \neg\ensuremath{{\circ}} A}$  \hspace{10mm} 
$\infer [_{[Comp]}] {B} {\infer*{B} {[\ensuremath{{\circ}} A]} & \infer*{B} {[\neg\ensuremath{{\circ}} A]}} $
\end{center}
\begin{proof}
The rules above are obtained in a few steps  from $EXP^\ensuremath{{\circ}}$, $PEM^\ensuremath{{\circ}}$,  
and $I\ensuremath{{\circ}}$. 
\end{proof}
\end{proposition}


\noindent The axiom $I \ensuremath{{\circ}}$ establishes  that   classicality    behaves classically. 
Indeed, from the perspective of the intuitive interpretation it is not only plausible
 but also desirable 
that either there is or there is not the information that   $A$ ($\neg A$) is reliable, which means that 
sentences $\ensuremath{{\circ}} A$ and $\neg\ensuremath{{\circ}} A$ should behave classically. 
 This is precisely the point of the rules $Cons$ and $Comp$ of 
 Proposition~\ref{der-rules} above, 
 which can be derived from $I \ensuremath{{\circ}}$ together with $PEM^\ensuremath{{\circ}}$   and $EXP^\ensuremath{{\circ}}$. 
The rules $I \neg \ensuremath{{\circ}}$ and  $E \neg \ensuremath{{\circ}}$ express 
 the idea that reliable information about $A$ 
  also contains reliable information about $\neg A$, and vice-versa.  
Regarding the remaining rules, the introduction rules express the  underlying idea 
of the inferences 
\ref{inf.1} to \ref{inf.last}, and the elimination rules are obtained from the introduction rules applying 
the well-known  inversion principle proposed Gentzen \citep{gentzen1935} and made precise by Prawitz 
 \cite[p.~33]{prawitz1965}, according to which the elimination rules can be `extracted' from the introduction rules.  
   It is easy to see, indeed, how the elimination rules for $\land$ and $\lor$ are obtained 
from the respective introduction rules. 
Let us take a more detailed look 
at the rules for $\to$.  
The introduction rules for $(A\to B)^T$  correspond to the classical material conditional: either the 
falsity of $A$ or the truth of $B$ are enough to conclude the truth of $A\to B$. The corresponding elimination rule is then 
obtained analogously to the elimination rule of $\lor$. 
The introduction rule for $(A\to B)^F$ is similar to the introduction rule for $\neg(A\to B)$ of \ensuremath{LET_{K}}, but with a difference: 
 $A^T$ is not required,  that is, only $A$ must hold -- it does not matter whether $\ensuremath{{\circ}} A$ holds or not. 
 This is because even if $\neg A$ also holds, this is not sufficient 
 for concluding $\neg(A\to B)$. The corresponding elimination rule is now straightforward obtained with the help of the 
 inversion principle. 

 




 
 
       
 
\subsection{Valuation semantics for \ensuremath{LET_{K}^+}}
The   rules and the axiom of \ensuremath{LET_{K}^+}\ added to \ensuremath{LET_{K}}\ induce, in a very natural way, the following   bivalued 
semantics:

\begin{definition} [Valuation semantics for \ensuremath{LET_{K}^+}] \label{val-sem-propag} \ 

\vspace{1mm}\noindent A bivaluation for \ensuremath{LET_{K}^+}\ is a bivaluation $\rho:For(\Sigma) \to {\bf2}$ for \ensuremath{LET_{K}}\ (Definition~\ref{def-val-LETK}) satisfying, in addition, the following clauses: 

\begin{itemize}  
\item[] (vp1) $\rho(\ensuremath{{\circ}} \ensuremath{{\circ}} A)=1$,
\item[]  \mbox{(vp2)} $ \rho(\ensuremath{{\circ}} \neg A)=\rho(\ensuremath{{\circ}} A)$,
\item[] \mbox{(vp3)}  \mbox{If $\rho(\ensuremath{{\circ}} A)=\rho(A)=1$ and $\rho(\ensuremath{{\circ}} B)=\rho(B)=1$  then $\rho(\ensuremath{{\circ}}(A \land B))=1$};
\item[] \mbox{(vp4)}  \mbox{If $\rho(\ensuremath{{\circ}} A)=\rho(\neg A)=1$  then $\rho(\ensuremath{{\circ}}(A \land B))=1$};
\item[] \mbox{(vp5)}  \mbox{If $\rho(\ensuremath{{\circ}} B)=\rho(\neg B)=1$  then $\rho(\ensuremath{{\circ}}(A \land B))=1$};
\item[] \mbox{(vp6)}  \mbox{If $\rho(\ensuremath{{\circ}}(A \land B))=\rho(A)=\rho(B)=1$  then $\rho(\ensuremath{{\circ}} A) = \rho(\ensuremath{{\circ}} B)=1$};
\item[] \mbox{(vp7)}   \mbox{If $\rho(\ensuremath{{\circ}}(A \land B))=1$, and either $\rho(\neg A)=1$ or $\rho(\neg B)=1$,  then:} \\
  \mbox{\quad \quad \quad  \quad    either $\rho(\ensuremath{{\circ}} A) = \rho(\neg A)=1$ or  $\rho(\ensuremath{{\circ}} B)=\rho(\neg B)=1$};
\item[] \mbox{(vp8)}   \mbox{If $\rho(\ensuremath{{\circ}} A)=\rho(A)=1$  then $\rho(\ensuremath{{\circ}}(A \lor B))=1$};
\item[] \mbox{(vp9)}   \mbox{If $\rho(\ensuremath{{\circ}} B)=\rho(B)=1$  then $\rho(\ensuremath{{\circ}}(A \lor B))=1$};
\item[] \mbox{(vp10)}  \mbox{If $\rho(\ensuremath{{\circ}} A)=\rho(\neg A)=1$ and $\rho(\ensuremath{{\circ}} B)=\rho(\neg B)=1$   then $\rho(\ensuremath{{\circ}}(A \lor B))=1$};
 \item[] \mbox{(vp11)}  \mbox{If $\rho(\ensuremath{{\circ}}(A \lor B))=1$, and either $\rho(A)=1$ or $\rho(B)=1$,  then:} \\ 
 \mbox{\quad \quad \quad  \quad   either $\rho(\ensuremath{{\circ}} A) = \rho(A)=1$ or  $\rho(\ensuremath{{\circ}} B)=\rho(B)=1$};
\item[] \mbox{(vp12)}  \mbox{If $\rho(\ensuremath{{\circ}}(A \lor B))=1$ and $\rho(A)=\rho(B)=0$  then $\rho(\ensuremath{{\circ}} A) = \rho(\ensuremath{{\circ}} B)=1$};
\item[] \mbox{(vp13)}   \mbox{If $\rho(\ensuremath{{\circ}} A)=\rho(\neg A)=1$  then $\rho(\ensuremath{{\circ}}(A \to B))=1$};
\item[] \mbox{(vp14)}   \mbox{If $\rho(\ensuremath{{\circ}} B)=\rho(B)=1$  then $\rho(\ensuremath{{\circ}}(A \to B))=1$};
\item[] \mbox{(vp15)}   \mbox{If $\rho(A)=1$ and $\rho(\ensuremath{{\circ}} B)=\rho(\neg B)=1$   then $\rho(\ensuremath{{\circ}}(A \to B))=1$};
\item[] \mbox{(vp16)}   \mbox{If $\rho(\ensuremath{{\circ}}(A \to B))=1$, and either $\rho(A)=0$ or $\rho(B)=1$,  then:} \\ 
 \mbox{\quad\quad\quad\quad  either $\rho(\ensuremath{{\circ}} A) =\rho(\neg A)=1$ or  $\rho(\ensuremath{{\circ}} B)=\rho(B)=1$};
\item[] \mbox{(vp17)}  \mbox{If $\rho(\ensuremath{{\circ}}(A \to B))=1$ and $\rho(A)=\rho(\neg B)=1$  then $\rho(\ensuremath{{\circ}} B)=1$}.
\end{itemize}

\end{definition}


Now, we prove soundness and completeness of \ensuremath{LET_{K}^+}\ w.r.t.~the bivalued semantics above. 
The definition of $F$-saturated sets in \ensuremath{LET_{K}^+}\ is analogous to the one for \ensuremath{LET_{K}}\ (Definition~\ref{def-F-sat-LETK}). 




\begin{proposition}\label{F-sat-LETKP} \ 

\vspace{1mm}\noindent 
Let $\Delta$ be an $F$-saturated set in \ensuremath{LET_{K}^+}. Then, it is a closed theory (that is, $A \in \Delta$ iff $\Delta \vdash_{\ensuremath{LET_{K}^+}} A$) and it satisfies properties (2)-(9) of Proposition~\ref{F-sat-LETK} plus the following:  



\begin{itemize}  
\item[] (vp1$'$) $\ensuremath{{\circ}}\cons A \in \Delta$;
\item[] (vp2$'$) $\ensuremath{{\circ}} A \in \Delta$  iff $\ensuremath{{\circ}}\neg A \in \Delta$;
\item[] (vp3$'$)  If $\ensuremath{{\circ}} A \in \Delta$, $A \in \Delta$, $\ensuremath{{\circ}} B \in \Delta$ and $B\in \Delta$ then $\ensuremath{{\circ}}(A \land B)\in \Delta$;
\item[] (vp4$'$) If $\ensuremath{{\circ}} A\in \Delta$ and $\neg A\in \Delta$  then $\ensuremath{{\circ}}(A \land B)\in \Delta$;
\item[] (vp5$'$) If $\ensuremath{{\circ}} B\in \Delta$ and $\neg B\in \Delta$  then $\ensuremath{{\circ}}(A \land B)\in \Delta$;
\item[] (vp6$'$) If $\ensuremath{{\circ}}(A \land B)\in \Delta$, $A\in \Delta$ and $B\in \Delta$  then $\ensuremath{{\circ}} A\in \Delta$ and $\ensuremath{{\circ}} B\in \Delta$;
\item[] (vp7$'$) If $\ensuremath{{\circ}}(A \land B)\in \Delta$, and either $\neg A\in \Delta$ or $\neg B\in \Delta$,  then: \\
\mbox{\quad\quad\quad\quad} either $\ensuremath{{\circ}} A\in \Delta$ and  $\neg A\in \Delta$ or  $\ensuremath{{\circ}} B\in \Delta$ and $\neg B\in \Delta$;
\item[] (vp8$'$) If $\ensuremath{{\circ}} A\in \Delta$ and $A\in \Delta$  then $\ensuremath{{\circ}}(A \lor B)\in \Delta$;
\item[] (vp9$'$) If $\ensuremath{{\circ}} B\in \Delta$ and $B\in \Delta$  then $\ensuremath{{\circ}}(A \lor B)\in \Delta$;
\item[] (vp10$'$) If $\ensuremath{{\circ}} A\in \Delta$, $\neg A\in \Delta$, $\ensuremath{{\circ}} B \in \Delta$ and $\neg B \in \Delta$   then $\ensuremath{{\circ}}(A \lor B)\in \Delta$;
\item[] (vp11$'$) If $\ensuremath{{\circ}}(A \lor B)\in \Delta$, and either $A\in \Delta$ or $B\in \Delta$,  then: \\
\mbox{\quad\quad\quad\quad} either $\ensuremath{{\circ}} A\in \Delta$ and $A\in \Delta$ or  $\ensuremath{{\circ}} B\in \Delta$ and $B\in \Delta$;
\item[] (vp12$'$) If $\ensuremath{{\circ}}(A \lor B)\in \Delta$, $A\notin \Delta$ and $B \notin  \Delta$  then $\ensuremath{{\circ}} A\in \Delta$ and $\ensuremath{{\circ}} B\in \Delta$;
\item[] (vp13$'$) If $\ensuremath{{\circ}} A\in \Delta$ and $\neg A\in \Delta$  then $\ensuremath{{\circ}}(A \to B)\in \Delta$;
\item[] (vp14$'$) If $\ensuremath{{\circ}} B\in \Delta$ and $B\in \Delta$  then $\ensuremath{{\circ}}(A \to B)\in \Delta$;
\item[] (vp15$'$) If $A\in \Delta$, $\ensuremath{{\circ}} B \in \Delta$ and $\neg B\in \Delta$   then $\ensuremath{{\circ}}(A \to B)\in \Delta$;
\item[] (vp16$'$) If $\ensuremath{{\circ}}(A \to B) \in \Delta$, and either $A \notin \Delta$ or $B \in \Delta$,  then: \\
\mbox{\quad\quad\quad\quad} either $\ensuremath{{\circ}} A \in \Delta$ and  $\neg A \in \Delta$ or  $\ensuremath{{\circ}} B \in \Delta$ and $B \in \Delta$;
\item[] (vp17$'$) If $\ensuremath{{\circ}}(A \to B) \in \Delta$, $A \in \Delta$ and $\neg B \in \Delta$  then $\ensuremath{{\circ}} B \in \Delta$.

\end{itemize}


\end{proposition}
\begin{proof}
It is immediate to see that an $F$-saturated set is a closed theory in any Tarskian logic.
The proof of items (2)-(9) follows from \ensuremath{LET_{K}}.  
The  proofs of items vp$1'$ to vp$17'$ follow easily from the axiom and rules added to \ensuremath{LET_{K}}\ in Definition~\ref{propag-rules}. Details are left to the reader.
\end{proof}


\begin{corollary} \label{val-F-sat}
Let $\Delta$ be a set of formulas which is  $F$-saturated in \ensuremath{LET_{K}^+}. Let $\rho_\Delta:For(\Sigma) \to {\bf 2}$ be the characteristic function of $\Delta$, that is: for every formula $A$, $\rho_\Delta(A)=1$ iff $A \in \Delta$ (iff $\Delta \vdash_{\ensuremath{LET_{K}^+}} A$, by Proposition~\ref{F-sat-LETKP}(1)). Then, $\rho_\Delta$ is a bivaluation for \ensuremath{LET_{K}^+}.
\begin{proof}
It is an immediate consequence of Proposition~\ref{F-sat-LETKP}. 
\end{proof}\end{corollary}



\begin{theorem}  [Soundness and completeness of \ensuremath{LET_{K}^+}\ w.r.t. bivaluation semantics] \label{adeq-LETKP-bival}  \ 

\vspace{2mm}\noindent 
For every set of formulas $\Gamma \cup \{A\} \subseteq For(\Sigma)$: 
$\Gamma \vdash_{\ensuremath{LET_{K}^+}} A$ \ iff \  $\Gamma\models_{\ensuremath{LET_{K}^+}}^2 A$.
\begin{proof} \ \\
{\em `Only if' part (soundness)}: By Theorem~\ref{adeq-LETK-bival}, it suffices proving that any bivaluation for \ensuremath{LET_{K}^+}\ satisfies the axiom and rules of Definition~\ref{propag-rules}. But it is immediate, taking into account the other properties inherited from bivaluations for \ensuremath{LET_{K}}. The details are left to the reader.\\[1mm]
{\em `If' part (completeness)}: It is also an extension of the proof of completeness of \ensuremath{LET_{K}}\ w.r.t. bivaluations. Thus, suppose that $\Gamma \nvdash_{\ensuremath{LET_{K}^+}} A$.  As observed in Remark~\ref{Lindenbaum-Los}, being \ensuremath{LET_{K}^+}\ a Tarskian and finitary logic, there exists a set $\Delta$ such that $\Gamma \subseteq \Delta$ and $\Delta$ is $A$-saturated in \ensuremath{LET_{K}^+}. By Corollary~\ref{val-F-sat}, the characteristic function $\rho_\Delta$ of  $\Delta$ is a bivaluation for \ensuremath{LET_{K}^+}\ such that $\rho_\Delta(B)=1$ for every $B \in \Gamma$, but $\rho_\Delta(A)=0$. This shows that $\Gamma \not\models_{\ensuremath{LET_{K}^+}}^2 A$.
\end{proof}\end{theorem}


\subsection{A 6-valued semantics for \ensuremath{LET_{K}^+}}  \label{sec.six.valued.letkp}



 Let us recall the Nmatrix for \ensuremath{LET_{K}}\ introduced in Section~\ref{sec.six.valued.semantics.LETK.decid}. 
 The snapshots $z=(z_1,z_2,z_3)$ represent triples of the form
 $(\rho(A), \rho(\neg A),\rho(\ensuremath{{\circ}} A))$, for a bivaluation $\rho$ for \ensuremath{LET_{K}}\ and a formula $A$. 
 With this  in mind, and taking into account the definition of the six snapshots of $\textsc{B}_{\ensuremath{LET_{K}}}$, 
 in what follows we will see how the clauses of Definition~\ref{val-sem-propag} 
 impose  restrictions to the multioperators  of \ensuremath{LET_{K}}, 
 which turn out to be deterministic in \ensuremath{LET_{K}^+}.  

\begin{proposition} \label{prop.reasoning.6.val}
\item 
 Clauses (vp3)-(vp7) of Definition~\ref{val-sem-propag} 
 impose the following restrictions  to the multioperator $\tilde{\land}$ of the Nmatrix of \ensuremath{LET_{K}}: 
\begin{itemize} \setlength\itemsep{-0.2em} 
\item[] (vp3): $T \,\tilde{\land}\, T=T$; 
\item[] (vp4)-(vp5): $F \,\tilde{\land}\, \_=\_ \,\tilde{\land}\, F=F$; 
\item[] (vp6):  $z \,\tilde{\land}\, w=T$ implies  that $z=w=T$. 
Hence,  $T \,\tilde{\land}\, T_0=T_0 \,\tilde{\land}\, T=T_0 \,\tilde{\land}\, T_0=T_0$; 
\item[] (vp7):  $z \,\tilde{\land}\, w=F$ implies  that $z=F$ or $w=F$. 
Hence,  $\textsf{b} \,\tilde{\land}\, \textsf{n}=\textsf{n} \,\tilde{\land}\, \textsf{b}=F_0 \,\tilde{\land}\, z=z \,\tilde{\land}\, F_0=F_0$, for $z \neq F$.
\end{itemize}
\noindent This shows that  $\tilde{\land}$ is deterministic in  \ensuremath{LET_{K}^+}\ 
and can be defined as 
\begin{itemize}
\item[(i)] $(z_1,z_2,z_3)\,\tilde{\land}\,(w_1,w_2,w_3) =  (z_1\sqcap w_1,z_2\sqcup w_2,(z_1 \sqcap z_3 \sqcap w_1 \sqcap w_3) \sqcup (z_2 \sqcap z_3) \sqcup (w_2 \sqcap w_3))$. 
\end{itemize} 
   Concerning  $\tilde{\lor}$, clauses (vp8)-(v12) impose   the following restrictions: 
\begin{itemize} \setlength\itemsep{-0.2em}  
\item[] (vp8)-(vp9): $T \,\tilde{\lor}\, \_=\_ \,\tilde{\lor}\, T=T$; 
\item[]  (vp10): $F \,\tilde{\lor}\, F=F$; 
\item[]  (vp11):  $z \,\tilde{\lor}\, w=T$ implies  that $z=T$ or $w=T$. Hence,  $\textsf{b} \,\tilde{\lor}\, \textsf{n}=\textsf{n} \,\tilde{\lor}\, \textsf{b}=T_0 \,\tilde{\lor}\, z=z \,\tilde{\lor}\, T_0=T_0$, for $z \neq T$; 
\item[]  (vp12):  $z \,\tilde{\lor}\, w=F$ implies  that $z=w=F$. Hence,  $F_0 \,\tilde{\lor}\, F_0=F_0 \,\tilde{\lor}\, F=F \,\tilde{\lor}\, F_0=F_0$.
\end{itemize}
\noindent Thus, $\tilde{\lor}$ turns out to be deterministic in  \ensuremath{LET_{K}^+}\   
 and can be defined as 
\begin{itemize}
\item[(ii)] $(z_1,z_2,z_3)\,\tilde{\lor}\,(w_1,w_2,w_3)  =  (z_1\sqcup w_1,z_2\sqcap w_2, (z_2 \sqcap z_3 \sqcap w_2 \sqcap w_3) \sqcup (z_1 \sqcap z_3) \sqcup (w_1 \sqcap w_3))$. 
\end{itemize}
   With respect to  $\tilde{\to}$, clauses (vp13)-(v17) impose  the following restrictions:
\begin{itemize} \setlength\itemsep{-0.2em}  
\item[]   (vp13): $F \,\tilde{\to}\, \_=T$;
\item[] (vp14): $\_ \,\tilde{\to}\, T=T$;
\item[] (vp15): $z \,\tilde{\to}\, F=F$, for $z \in \textrm{D}$. Hence,  $T \,\tilde{\to}\, F=T_0 \,\tilde{\to}\, F=\textsf{b} \,\tilde{\to}\, F=F$;
\item[] (vp16): $z \,\tilde{\to}\, w=T$ implies that $z=F$ or $w=T$.  Hence, $\textsf{n} \,\tilde{\to}\, w=F_0 \,\tilde{\to}\, w=T_0$, for $w \neq T$; and  $z\,\tilde{\to}\, T_0=T_0$, for $z \in \textrm{D}$; 
\item[] (vp17):  $z \,\tilde{\to}\, w=F$ implies  that $w=F$. Hence, $z \,\tilde{\to}\, F_0=F_0$, for $z \in \textrm{D}$.
\end{itemize}
 \noindent Thus, $\tilde{\to}$ also turns out to be deterministic, defined as 
\begin{itemize}
\item[(iii)]  $(z_1,z_2,z_3)\,\tilde{\to}\,(w_1,w_2,w_3)  =  (z_1\Rightarrow w_1,z_1\sqcap w_2, (z_1 \sqcap w_2 \sqcap w_3) \sqcup (z_2 \sqcap z_3) \sqcup (w_1 \sqcap w_3))$. 
\end{itemize}
   Given the clause (vp2), 
the third coordinate of the snapshot will not 
 be changed by the operation $\tilde{\neg}$. 
 For this reason,   
 the negation $\tilde{\neg}$ in \ensuremath{LET_{K}^+}\  also turns out to be deterministic: 
 $\tilde{\neg} T = F$, $\tilde{\neg} F = T$, $\tilde{\neg} T_0 = F_0$, and $\tilde{\neg} F_0 = T_0$.   
 It will be defined as  
 \begin{itemize}
\item[(iv)]   $\tilde{\neg}\,(z_1,z_2,z_3) = (z_2,z_1,z_3)$.
\end{itemize} 
   Finally, the classicality operator $\tilde{\circ}$ of \ensuremath{LET_{K}^+}, by virtue of (vp1), which fixes the value of the third coordinate, 
 also becomes deterministic: for $z = T$ or $z=F$, $\tilde{\ensuremath{{\circ}}} z = F$;        
 otherwise $\tilde{\ensuremath{{\circ}}} z = F$.  
 It  will be defined as:  
 \begin{itemize}
 \item[(v)] $\tilde{\circ}\,(z_1,z_2,z_3) = (z_3,\ensuremath{{\sim}} z_3,1)$
 \end{itemize}
  \end{proposition}



\vspace{3mm}

The reasoning above yields the following deterministic  6-valued matrix for \ensuremath{LET_{K}^+}, obtained 
by applying the corresponding restrictions to  the 6-valued Nmatrix for \ensuremath{LET_{K}}:

\begin{definition} \ \label{def.six.val.LETKP}

\vspace{1mm}\noindent Let  $\mathcal{M}_6$ be the 6-valued logical matrix with domain $\textsc{B}_{\ensuremath{LET_{K}}}$, set of designated values $\textrm{D}=\{T,T_0,\textsf{b}\}$ and operations given by the tables below.


\vspace{2mm}


\begin{center}
\begin{tabular}{|c|c|c|c|c|c|c|}
\hline
 $\tilde{\wedge}$ & $T$  & $T_0$   & $\textsf{b}$ & $\textsf{n}$ & $F_0$  & $F$\\[1mm]
 \hline \hline
    $T$    & $T$  & $T_0$ & $\textsf{b}$ & $\textsf{n}$ & $F_0$ & $F$   \\[1mm] \hline
     $T_0$    & $T_0$  & $T_0$ & $\textsf{b}$ & $\textsf{n}$ & $F_0$ & $F$  \\[1mm] \hline
     $\textsf{b}$    & $\textsf{b}$  & $\textsf{b}$ & $\textsf{b}$ & $F_0$ & $F_0$ & $F$  \\[1mm] \hline
     $\textsf{n}$    & $\textsf{n}$  & $\textsf{n}$ & $F_0$ & $\textsf{n}$ & $F_0$ & $F$  \\[1mm] \hline
     $F_0$    & $F_0$  & $F_0$ & $F_0$ & $F_0$ & $F_0$ & $F$  \\[1mm] \hline
     $F$    & $F$  & $F$ & $F$ & $F$ & $F$ & $F$  \\[1mm] \hline
\end{tabular}
\hspace{1cm}
\begin{tabular}{|c|c|c|c|c|c|c|}
\hline
 $\tilde{\vee}$ & $T$  & $T_0$  & $\textsf{b}$ & $\textsf{n}$ & $F_0$  & $F$ \\[1mm]
 \hline \hline
    $T$    & $T$  & $T$ & $T$ & $T$ & $T$ & $T$   \\[1mm] \hline
     $T_0$    & $T$  & $T_0$ & $T_0$ & $T_0$ & $T_0$ & $T_0$   \\[1mm] \hline
     $\textsf{b}$    & $T$  & $T_0$ & $\textsf{b}$ & $T_0$ & $\textsf{b}$ & $\textsf{b}$   \\[1mm] \hline
     $\textsf{n}$    & $T$  & $T_0$ & $T_0$ & $\textsf{n}$ & $\textsf{n}$ & $\textsf{n}$   \\[1mm] \hline
     $F_0$    & $T$  & $T_0$ & $\textsf{b}$ & $\textsf{n}$ & $F_0$ & $F_0$   \\[1mm] \hline
     $F$    & $T$  & $T_0$ & $\textsf{b}$ & $\textsf{n}$ & $F_0$ & $F$  \\[1mm] \hline
\end{tabular}


\

\


\begin{tabular}{|c|c|c|c|c|c|c|}
\hline
 $\tilde{\to}$ & $T$  & $T_0$  & $\textsf{b}$ & $\textsf{n}$ & $F_0$  & $F$ \\[1mm]
 \hline \hline
    $T$    & $T$  & $T_0$ & $\textsf{b}$ & $\textsf{n}$ & $F_0$ & $F$   \\[1mm] \hline
     $T_0$    & $T$  & $T_0$ & $\textsf{b}$ & $\textsf{n}$ & $F_0$ & $F$  \\[1mm] \hline
     $\textsf{b}$    & $T$  & $T_0$ & $\textsf{b}$ & $\textsf{n}$ & $F_0$ & $F$  \\[1mm] \hline
     $\textsf{n}$    & $T$  & $T_0$ & $T_0$ & $T_0$ & $T_0$ & $T_0$  \\[1mm] \hline
     $F_0$    & $T$  & $T_0$ & $T_0$ & $T_0$ & $T_0$ & $T_0$  \\[1mm] \hline
     $F$    & $T$  & $T$ & $T$ & $T$ & $T$ & $T$  \\[1mm] \hline
\end{tabular}
\hspace{1.5cm}
\begin{tabular}{|c||c|} \hline
$\quad$ & $\tilde{\neg}$ \\[1mm]
 \hline \hline
    $T$   & $F$    \\[1mm] \hline
     $T_0$   & $F_0$    \\[1mm] \hline
     $\textsf{b}$   &$\textsf{b}$    \\[1mm] \hline
     $\textsf{n}$   & $\textsf{n}$    \\[1mm] \hline
     $F_0$   & $T_0$    \\[1mm] \hline
     $F$   & $T$    \\[1mm] \hline
\end{tabular}
\hspace{1.5cm}
\begin{tabular}{|c||c|}
\hline
 $\quad$ & $\tilde{\circ}$ \\[1mm]
 \hline \hline
    $T$   & $T$    \\[1mm] \hline
     $T_0$   & $F$     \\[1mm] \hline
     $\textsf{b}$   & $F$     \\[1mm] \hline
     $\textsf{n}$   & $F$     \\[1mm] \hline
     $F_0$   & $F$     \\[1mm] \hline
     $F$   & $T$    \\[1mm] \hline
\end{tabular}
\end{center}
\end{definition}

\vspace{2mm}

\begin{remark} \label{twist-LETKP} \  \\[1mm]
(i) Let $\mathcal{A}_{\ensuremath{LET_{K}}}$ be the 6-valued multialgebra underlying the Nmatrix  $\mathcal{M}_{\ensuremath{LET_{K}}}$ for \ensuremath{LET_{K}}\ 
and $\mathcal{A}_6$  the 6-valued algebra  underlying the matrix 
$\mathcal{M}_6$. 
Since every algebra is  a multialgebra in which 
each entry of each multioperator returns a singleton set, it is immediate
to see that  $\mathcal{A}_6$ is a submultialgebra of $\mathcal{A}_{\ensuremath{LET_{K}}}$. 
Consider now that $\tilde{\#}_6$ and $\tilde{\#}_{\ensuremath{LET_{K}}}$ denote, respectively, the interpretation of the connective $\#$
 in the multialgebras $\mathcal{A}_6$ and $\mathcal{A}_{\ensuremath{LET_{K}}}$. 
Thus,    $\tilde{\#}_6 \, z \subseteq \tilde{\#}_{\ensuremath{LET_{K}}}\,z$ and $z\,\tilde{\#'}_6\,w \subseteq z\,\tilde{\#'}_{\ensuremath{LET_{K}}}\,w$ 
for every $z,w \in \textsc{B}_{\ensuremath{LET_{K}}}$, $\# \in \{\neg,\ensuremath{{\circ}}\}$ and $\#' \in \{\land,\lor,\to\}$. 
Therefore, 
any valuation over the matrix $\mathcal{M}_6$ is a valuation over the Nmatrix $\mathcal{M}_{\ensuremath{LET_{K}}}$.  
 
 
\vspace{1mm}\noindent (ii)  Recall from Definition~\ref{propag-rules} that   $A^T \ensuremath{~\stackrel{\text{{\tiny def }}}{=}~} \ensuremath{{\circ}} A \land A$ and $A^F \ensuremath{~\stackrel{\text{{\tiny def }}}{=}~} \ensuremath{{\circ}} A \land \neg A$, for every formula $A$. 
Accordingly, let   $z^T \ensuremath{~\stackrel{\text{{\tiny def }}}{=}~} \tilde{\ensuremath{{\circ}}} z \ \tilde{\land} \ z$ and  $z^F \ensuremath{~\stackrel{\text{{\tiny def }}}{=}~} \tilde{\ensuremath{{\circ}}} z \ \tilde{\land} \ \tilde{\neg} z$, 
for every $z \in B_{\ensuremath{LET_{K}}}$, where the operations correspond to  $\mathcal{M}_6$. 
 It is easy to see that, for every  $z \in B_{\ensuremath{LET_{K}}}$: $z^T = T$ if $z=T$, and $z^T=F$ otherwise; 
 and  $z^F = T$ if $z=F$, and $z^F=F$ otherwise.  
Clearly, for every valuation $v$  over the logical matrix  $\mathcal{M}_6$ (recall Remark~\ref{val-matr}), $v(A^T) = v(A)^T$ and $v(A^F) = v(A)^F$.  
\end{remark}


 
 


 

\subsection{Soundness and completeness of the 6-valued semantics of \ensuremath{LET_{K}^+}}
The next task is to prove  soundness and completeness   of \ensuremath{LET_{K}^+}\ w.r.t. the semantics given by $\mathcal{M}_6$. 
The proof is obtained by adapting  to \ensuremath{LET_{K}^+}\ the proof of Theorems~\ref{sound-Nmat-LETK} and~\ref{comp-Nmat-LETK}. 
The definition of $F$-saturated sets in \ensuremath{LET_{K}^+}\ is analogous to the one for \ensuremath{LET_{K}}\ (recall Definition~\ref{def-F-sat-LETK}). 
 



\begin{proposition} \label{lemma-sound-LETKP}
For every valuation $v$  over the matrix $\mathcal{M}_{6}$  the mapping $\rho_v:For(\Sigma) \to {\bf2}$ given by $\rho_v(A)=v(A)_1$ is a bivaluation for \ensuremath{LET_{K}^+}\ such that: $\rho_v(A)=1$ \ iff \ $v(A) \in \textrm{D}$, for every formula $A$.
\end{proposition}
\begin{proof}  As noted in Remark~\ref{twist-LETKP}, any valuation over the matrix $\mathcal{M}_{6}$ is a valuation over the Nmatrix $\mathcal{M}_{\ensuremath{LET_{K}}}$. Thus, given a valuation $v$  over $\mathcal{M}_{6}$, the function $\rho_v$ defined as above is a bivaluation for \ensuremath{LET_{K}}, by Proposition~\ref{lemma-sound-LETK}. It remains to prove that $\rho_v$ satisfies clauses (vp1)-(vp17) from Definition~\ref{val-sem-propag}. Thus, let $A,B \in For(\Sigma)$. Then $\rho_v(\ensuremath{{\circ}}\cons A)=v(\ensuremath{{\circ}} A)_3=(\tilde{\ensuremath{{\circ}}}\,v(A))_3=1$, by definition of $\mathcal{M}_{6}$. This shows that $\rho_v$ satisfies (vp1). Using again the definition of $\mathcal{M}_{6}$, $\rho_v(\ensuremath{{\circ}}\neg A)=v(\neg A)_3=(\tilde{\neg}\,v(A))_3=v(A)_3=\rho_v(\ensuremath{{\circ}} A)$. 
In order to prove that $\rho_v$ satisfies (vp3), suppose that $\rho_v(\ensuremath{{\circ}} A)=\rho_v(A)=1$ and  $\rho_v(\ensuremath{{\circ}} B)=\rho_v(B)=1$. Then $v(A)_3=v(A)_1=1$ and  $v(B)_3=v(B)_1=1$, that is, $v(A)=v(B)=T$. Hence, $v(A \land B)=v(A)\,\tilde{\land}\,v(B)=T\,\tilde{\land}\,T=T$. From this, $\rho_v(\ensuremath{{\circ}}(A \land B))=v(A \land B)_3=1$. For (vp4), suppose that $\rho_v(\ensuremath{{\circ}} A)=\rho_v(\neg A)=1$. Then $v(A)_3=v(A)_2=1$, that is, $v(A)=F$. Hence, $v(A \land B)=v(A)\,\tilde{\land}\,v(B)=F\,\tilde{\land}\,v(B)=F$, for every $B$. From this, $\rho_v(\ensuremath{{\circ}}(A \land B))=v(A \land B)_3=1$. Analogously it is proved that $\rho_v$ satisfies (vp5). For (vp7), suppose that $\rho_v(\ensuremath{{\circ}}(A \land B))=1$, and either $\rho_v(\neg A)=1$ or $\rho_v(\neg B)=1$. Then, $v(A \land B)_3=1$ and $v(A)_2=1$ or $v(B)_2=1$, hence $v(A \land B)_2=1$. Then, $v(A \land B)=F$ and so either $v(A)=F$ or $v(B)=F$. That is, either $v(A)_3=v(A)_2=1$ or $v(B)_3=v(B)_2=1$. Hence,  $\rho_v(\ensuremath{{\circ}} A) = \rho_v(\neg A)=1$ or  $\rho_v(\ensuremath{{\circ}} B)=\rho_v(\neg B)=1$ and so $\rho_v$ satisfies (vp7).  For (vp8), suppose that $\rho_v(\ensuremath{{\circ}} A)=\rho_v(A)=1$. Then, $v(A)_3=v(A)_1=1$, that is, $v(A)=T$. Then, $v(A \vee B)=T$ and so $v(A \lor B)_3=1$, for any $B$. That is,  $\rho_v(\ensuremath{{\circ}}(A \lor B))=1$, for any $B$, and so $\rho_v$ satisfies (vp8). Clause (vp9) is proved analogously. For (vp16), assume that $\rho_v(\ensuremath{{\circ}}(A \to B))=1$, and either $\rho_v(A)=0$ or $\rho_v(B)=1$. Then, $v(A \to B)_3=1$, and either $v(A)_1=0$ or $v(B)_1=1$, that is, $v(A \to B)_1=1$. This means that $v(A \to B)=T$, and so either $v(A)=F$ or $v(B)=T$. That is, either $v(A)_3 =v(A)_2=1$ or  $v(B)_3=v(B)_1=1$. This means that either $\rho_v(\ensuremath{{\circ}} A) =\rho_v(\neg A)=1$ or  $\rho_v(\ensuremath{{\circ}} B)=\rho_v(B)=1$. Hence, $\rho_v$ satisfies clause (vp16). 
The rest of the clauses are proved by similar arguments. 
This shows that $\rho_v$ is a bivaluation for \ensuremath{LET_{K}^+}\ such that, by definition,  $\rho_v(A)=1$ \ iff \ $v(A) \in \textrm{D}$, for every formula $A$.
\end{proof}

 
\begin{theorem}  [Soundness of \ensuremath{LET_{K}^+}\ w.r.t. the 6-valued logical matrix $\mathcal{M}_6$] \label{sound-LETKP-matrix}  \ 

\vspace{1mm}\noindent 
For every set of formulas $\Gamma \cup \{A\} \subseteq For(\Sigma)$: 
$\Gamma \vdash_{\ensuremath{LET_{K}^+}} A$ \ implies that \  $\Gamma\models_{\mathcal{M}_6} A$.
\end{theorem}
\begin{proof} 
Assume that $\Gamma \vdash_{\ensuremath{LET_{K}^+}} A$. By Theorem~\ref{adeq-LETKP-bival},  $\Gamma\models_{\ensuremath{LET_{K}^+}}^2 A$. Now, let $v$ be a valuation  over the matrix $\mathcal{M}_{6}$ such that $v(B)  \in \textrm{D}$ for every $B \in \Gamma$, and let $\rho_v$ be the bivaluation for \ensuremath{LET_{K}^+}\ defined from $v$ as in Proposition~\ref{lemma-sound-LETKP}. Hence $\rho_v(B)=1$ for every $B \in \Gamma$ and so $\rho_v(A)=1$, since $\Gamma\models_{\ensuremath{LET_{K}^+}}^2 A$. From this it follows that $v(A) \in \textrm{D}$. Therefore, $\Gamma\models_{\mathcal{M}_{6}} A$.
\end{proof}

 

\begin{remark} \label{clause-refor}
It is worth noting that clauses (vp6), (vp7), (vp11), (vp12), (vp16) and (vp17) are equivalent, by contraposition, to the following ones:\\[1mm]
$\begin{array}{ll}
\mbox{(vp6)'} & \mbox{If $\rho(A)=\rho(B)=1$ and  either $\rho(\ensuremath{{\circ}} A) = 0$ or  $\rho(\ensuremath{{\circ}} B)=0$, then  $\rho(\ensuremath{{\circ}}(A \land B))=0$};\\[1mm]
\mbox{(vp7)'} & \mbox{If either $\rho(\neg A)=1$ or $\rho(\neg B)=1$; either $\rho(\ensuremath{{\circ}} A) = 0$ or $\rho(\neg A)=0$;}\\[1mm]
& \mbox{and either  $\rho(\ensuremath{{\circ}} B) = 0$ or $\rho(\neg B)=0$, then $\rho(\ensuremath{{\circ}}(A \land B))=0$};\\[1mm]
\mbox{(vp11)'} & \mbox{If either $\rho(A)=1$ or $\rho(B)=1$; either $\rho(\ensuremath{{\circ}} A) = 0$ or $\rho(A)=0$;}\\[1mm]
& \mbox{and either  $\rho(\ensuremath{{\circ}} B) = 0$ or $\rho(B)=0$, then $\rho(\ensuremath{{\circ}}(A \lor B))=0$};\\[1mm]
\mbox{(vp12)'} & \mbox{If $\rho(A)=\rho(B)=0$ and  either $\rho(\ensuremath{{\circ}} A) = 0$ or  $\rho(\ensuremath{{\circ}} B)=0$, then  $\rho(\ensuremath{{\circ}}(A \lor B))=0$};\\[1mm]
\mbox{(vp16)'} & \mbox{If either $\rho(A)=0$ or $\rho(B)=1$; either $\rho(\ensuremath{{\circ}} A) = 0$ or $\rho(\neg A)=0$;}\\[1mm]
& \mbox{and either  $\rho(\ensuremath{{\circ}} B) = 0$ or $\rho(B)=0$, then $\rho(\ensuremath{{\circ}}(A \to B))=0$};\\[1mm]
\mbox{(vp17)'} & \mbox{If $\rho(A)=\rho(\neg B)=1$ and $\rho(\ensuremath{{\circ}} B)=0$, then  $\rho(\ensuremath{{\circ}}(A \to B))=0$}.
\end{array}$\\[1mm]
This reformulation of that clauses will be useful for the  proof of completeness of \ensuremath{LET_{K}^+}\ w.r.t. $\mathcal{M}_6$. Moreover, in Proposition~\ref{charact-bival-LETKP} a more compact characterization of bivaluations for \ensuremath{LET_{K}^+}\ will be given.
\end{remark}

 

\begin{proposition} \label{lemma-comple-LETKP}
For every bivaluation $\rho$ for \ensuremath{LET_{K}^+}\  the mapping $v_{\rho}:For(\Sigma) \to \textsc{B}_{\ensuremath{LET_{K}}}$ given by $v_\rho(A)=(\rho(A),\rho(\neg A),\rho(\circ A))$ is a valuation over the matrix $\mathcal{M}_6$ such that: $v_\rho(A) \in \textrm{D}$ \ iff \ $\rho(A)=1$, for every formula $A$.
\end{proposition}
\begin{proof} It is clear that $v_\rho(A) \in \textsc{B}_{\ensuremath{LET_{K}}}$, hence the function is well-defined. Let us prove now that $v_\rho$ is a valuation over $\mathcal{M}_6$. Thus, let $A,B \in For(\Sigma)$ (in the sequel, recall clauses (v1)-(v8) and (vp1)-(vp17) from Definitions~\ref{def-val-LETK} and~\ref{val-sem-propag}), as well as clauses (vp6)', (vp7)', (vp11)', (vp12)', (vp16)' and (vp17)' from Remark~\ref{clause-refor}).

\vspace{1mm}\noindent {\em Conjunction:} Suppose that $v_\rho(A)=v_\rho(B)=T$. Then, $\rho(\ensuremath{{\circ}} A)=\rho(A)=1$ and $\rho(\ensuremath{{\circ}} B)=\rho(B)=1$ and so, by (vp3) and (v1), $\rho(\ensuremath{{\circ}}(A \land B))=\rho(A \land B)=1$. Hence, $v_\rho(A\land B)=T=v_\rho(A) \,\tilde{\land}\, v_\rho(B)$. Now, suppose that $v_\rho(A)=T_0$ and $v_\rho(B) \in \{T,T_0\}$. Then, $\rho(A)=1$, $\rho(\neg A)=\rho(\ensuremath{{\circ}} A)=0$, $\rho(B)=1$ and $\rho(\neg B)=0$. By (v1), (v5) and (vp6)', $\rho(A \land B)=1$, $\rho(\neg(A \land B))=0$ and $\rho(\ensuremath{{\circ}}(A \land B))=0$. That is, $v_\rho(A\land B)=T_0=v_\rho(A) \,\tilde{\land}\, v_\rho(B)$. Analogously we prove that, if $v_\rho(B)=T_0$ and $v_\rho(A) \in \{T,T_0\}$ then $v_\rho(A\land B)=T_0=v_\rho(A) \,\tilde{\land}\, v_\rho(B)$. 
Assume now that $v_\rho(A)=\textsf{b}$ and $v_\rho(B) \in \textrm{D}$. Then, $\rho(A)=\rho(\neg A)=1$, $\rho(\ensuremath{{\circ}} A)=0$ and $\rho(B)=1$. By (v1), (v5) and (v8), $\rho(A \land B)=\rho(\neg(A \land B))=1$ and $\rho(\ensuremath{{\circ}}(A \land B))=0$. That is, $v_\rho(A\land B)=\textsf{b}=v_\rho(A) \,\tilde{\land}\, v_\rho(B)$. Analogously we prove that, if $v_\rho(B)=\textsf{b}$ and $v_\rho(A) \in \textrm{D}$ then $v_\rho(A\land B)=\textsf{b}=v_\rho(A) \,\tilde{\land}\, v_\rho(B)$. 
Now, assume that $v_\rho(A)=\textsf{n}$ and $v_\rho(B) \in \{T,T_0,\textsf{n}\}$. Then, $\rho(A)=\rho(\neg A)=\rho(\ensuremath{{\circ}} A)=0$ and $\rho(\neg B)=0$. Hence, by (v1) and (v5) and (v8), $\rho(A \land B)=\rho(\neg(A \land B))=\rho(\ensuremath{{\circ}}(A \land B))=0$. That is, $v_\rho(A\land B)=\textsf{n}=v_\rho(A) \,\tilde{\land}\, v_\rho(B)$. Analogously we prove that, if $v_\rho(B)=\textsf{n}$ and $v_\rho(A) \in \{T,T_0\}$ then $v_\rho(A\land B)=\textsf{n}=v_\rho(A) \,\tilde{\land}\, v_\rho(B)$. Suppose now that $v_\rho(A)=F_0$ and $v_\rho(B)  \neq F$. Then $\rho(A)=0$, $\rho(\neg A)=1$, $\rho(\ensuremath{{\circ}} A)=0$ and: either $\rho(\neg B)=0$ or $\rho(\ensuremath{{\circ}} B)=0$. Hence, by (v1), (v5) and (vp7)', $\rho(A \land B)=0$, $\rho(\neg(A \land B))=1$  and $\rho(\ensuremath{{\circ}}(A \land B))=0$. That is,  $v_\rho(A\land B)=F_0=v_\rho(A) \,\tilde{\land}\, v_\rho(B)$. Analogously we prove that, if $v_\rho(B)=F_0$ and $v_\rho(A) \neq F$ then $v_\rho(A\land B)=F_0=v_\rho(A) \,\tilde{\land}\, v_\rho(B)$.  Assume now that $v_\rho(A)=\textsf{b}$ and $v_\rho(B)=\textsf{n}$. Then $\rho(A)=\rho(\neg A)=1$, $\rho(\ensuremath{{\circ}} A)=0$ and $\rho(B)=\rho(\neg B)=\rho(\ensuremath{{\circ}} B)=0$. Thus, by (v1), (v5) and (vp7)', $\rho(A \land B)=0$, $\rho(\neg(A \land B))=1$  and $\rho(\ensuremath{{\circ}}(A \land B))=0$. That is,  $v_\rho(A\land B)=F_0=v_\rho(A) \,\tilde{\land}\, v_\rho(B)$. Analogously we prove that, if $v_\rho(B)=\textsf{n}$ and $v_\rho(A)=\textsf{b}$ then $v_\rho(A\land B)=F_0=v_\rho(A) \,\tilde{\land}\, v_\rho(B)$. Finally, suppose that either $v_\rho(A)=F$ or $v_\rho(B)=F$. Then, either  $\rho(\ensuremath{{\circ}} A)=\rho(\neg A)=1$ or $\rho(\ensuremath{{\circ}} B)=\rho(\neg B)=1$ and so, by (vp4), (vp5) and (v5), $\rho(\ensuremath{{\circ}}(A \land B))=\rho(\neg(A \land B))=1$. Therefore $v_\rho(A\land B)=F=v_\rho(A) \,\tilde{\land}\, v_\rho(B)$.  

\vspace{1mm}\noindent{\em Disjunction:} Suppose that  either $v_\rho(A)=T$ or $v_\rho(B)=T$. Then, either  $\rho(\ensuremath{{\circ}} A)=\rho(A)=1$ or $\rho(\ensuremath{{\circ}} B)=\rho(B)=1$ and so, by (vp8), (vp9) and (v2), $\rho(\ensuremath{{\circ}}(A \lor B))=\rho(A \lor B)=1$. Therefore $v_\rho(A\lor B)=T=v_\rho(A) \,\tilde{\lor}\, v_\rho(B)$. Suppose now that $v_\rho(A)=T_0$ and $v_\rho(B)  \neq T$. Then $\rho(A)=1$, $\rho(\neg A)=0$, $\rho(\ensuremath{{\circ}} A)=0$ and: either $\rho(B)=0$ or  $\rho(\ensuremath{{\circ}} B)=0$. By (v2),(v6) and  (vp11)' it follows that  $\rho(A \lor B)=1$, $\rho(\neg(A \lor B))=0$ and $\rho(\ensuremath{{\circ}}(A \lor B))=0$. That is,  $v_\rho(A\lor B)=T_0=v_\rho(A) \,\tilde{\lor}\, v_\rho(B)$. Analogously we prove that, if $v_\rho(B)=T_0$ and $v_\rho(A) \neq T$ then $v_\rho(A\lor B)=T_0=v_\rho(A) \,\tilde{\lor}\, v_\rho(B)$. Now, assume that $v_\rho(A)=\textsf{b}$ and $v_\rho(B) \in \{\textsf{b},F_0,F\}$. Then, $\rho(A)=\rho(\neg A)=1$, $\rho(\ensuremath{{\circ}} A)=0$ and $\rho(\neg B)=1$. Hence, by (v2), (v6) and (v8), $\rho(A \lor B)=\rho(\neg(A \lor B))=1$ and $\rho(\ensuremath{{\circ}}(A \lor B))=0$. That is, $v_\rho(A\lor B)=\textsf{b}=v_\rho(A) \,\tilde{\lor}\, v_\rho(B)$. Analogously we prove that, if $v_\rho(B)=\textsf{b}$ and $v_\rho(A) \in \{F,F_0\}$ then $v_\rho(A\lor B)=\textsf{b}=v_\rho(A) \,\tilde{\lor}\, v_\rho(B)$. Suppose now that $v_\rho(A)=\textsf{b}$ and $v_\rho(B)=\textsf{n}$. Then $\rho(A)=\rho(\neg A)=1$, $\rho(\ensuremath{{\circ}} A)=0$ and $\rho(B)=\rho(\neg B)=\rho(\ensuremath{{\circ}} B)=0$. Then, by (v2), (v6) and (vp11)', $\rho(A \lor B)=1$, $\rho(\neg(A \lor B))=0$  and $\rho(\ensuremath{{\circ}}(A \lor B))=0$. That is,  $v_\rho(A\lor B)=T_0=v_\rho(A) \,\tilde{\lor}\, v_\rho(B)$. Analogously we prove that, if $v_\rho(B)=\textsf{n}$ and $v_\rho(A)=\textsf{b}$ then $v_\rho(A\lor B)=T_0=v_\rho(A) \,\tilde{\lor}\, v_\rho(B)$. 
Assume now that $v_\rho(A)=\textsf{n}$ and $v_\rho(B) \in \textrm{ND}$. Then, $\rho(A)=\rho(\neg A)=\rho(\ensuremath{{\circ}} A)=0$ and $\rho(B)=0$. By (v2), (v6) and (v8), $\rho(A \lor B)=\rho(\neg(A \lor B))=\rho(\ensuremath{{\circ}}(A \lor B))=0$. That is, $v_\rho(A\lor B)=\textsf{n}=v_\rho(A) \,\tilde{\lor}\, v_\rho(B)$. Analogously we prove that, if $v_\rho(B)=\textsf{n}$ and $v_\rho(A) \in \textrm{ND}$ then $v_\rho(A\lor B)=\textsf{n}=v_\rho(A) \,\tilde{\lor}\, v_\rho(B)$. Now, suppose that  $v_\rho(A)=F_0$ and $v_\rho(B) \in \{F,F_0\}$. Then, $\rho(A)=0$, $\rho(\neg A)=1$, $\rho(\ensuremath{{\circ}} A)=0$, $\rho(B)=0$ and $\rho(\neg B)=1$. By (v2), (v6) and (vp12)', $\rho(A \lor B)=1$, $\rho(\neg(A \lor B))=0$ and $\rho(\ensuremath{{\circ}}(A \lor B))=0$. That is, $v_\rho(A\lor B)=F_0=v_\rho(A) \,\tilde{\lor}\, v_\rho(B)$. Analogously we prove that, if $v_\rho(B)=F_0$ and $v_\rho(A) \in \{F,F_0\}$ then $v_\rho(A\lor B)=F_0=v_\rho(A) \,\tilde{\lor}\, v_\rho(B)$. Finally, suppose that $v_\rho(A)=v_\rho(B)=F$. Then, $\rho(A)=0$, $\rho(\ensuremath{{\circ}} A)=\rho(\neg A)=1$, $\rho(B)=0$ and $\rho(\ensuremath{{\circ}} B)=\rho(\neg B)=1$ and so, by (vp10) and (v2), $\rho(\ensuremath{{\circ}}(A \lor B))=1$ and $\rho(A \lor B)=1$. Hence, $v_\rho(A\lor B)=F=v_\rho(A) \,\tilde{\lor}\, v_\rho(B)$. 

\vspace{1mm}\noindent{\em Implication:} Suppose that $v_\rho(A)=F$. Then, $\rho(A)=0$, $\rho(\neg A)=1$ and $\rho(\ensuremath{{\circ}} A)=1$. Using (v3), (v7) and (vp13) it follows that, for any $B$, $\rho(A \to B)=1$, $\rho(\neg(A \to B))=0$ and $\rho(\ensuremath{{\circ}}(A \to B))=1$. That is, $v_\rho(A \to B)=T=v_\rho(A) \,\tilde{\to}\, v_\rho(B)$. Analogously (but now by using (vp14)) it is proven that, if  $v_\rho(B)=T$, $v_\rho(A \to B)=T=v_\rho(A) \,\tilde{\to}\, v_\rho(B)$ for any $A$.  Suppose now that $v_\rho(A)=F_0$ and $v_\rho(B)  \neq T$. Then $\rho(A)=0$, $\rho(\neg A)=1$, $\rho(\ensuremath{{\circ}} A)=0$ and: either $\rho(B)=0$ or  $\rho(\ensuremath{{\circ}} B)=0$. By (v3),(v7) and  (vp16)' it follows that  $\rho(A \to B)=1$, $\rho(\neg(A \to B))=0$ and $\rho(\ensuremath{{\circ}}(A \to B))=0$. That is,  $v_\rho(A\to B)=T_0=v_\rho(A) \,\tilde{\to}\, v_\rho(B)$. Analogously we prove that, if $v_\rho(B)=T_0$ and $v_\rho(A) \neq F$ then $v_\rho(A\to B)=T_0=v_\rho(A) \,\tilde{\to}\, v_\rho(B)$.
Assume now that $v_\rho(B)=\textsf{b}$ and $v_\rho(A) \in \textrm{D}$. Then, $\rho(B)=\rho(\neg B)=1$, $\rho(\ensuremath{{\circ}} B)=0$ and $\rho(A)=1$. By (v3), (v7) and (v8), $\rho(A \to B)=\rho(\neg(A \to B))=1$ and $\rho(\ensuremath{{\circ}}(A \to B))=0$. That is, $v_\rho(A\to B)=\textsf{b}=v_\rho(A) \,\tilde{\to}\, v_\rho(B)$. Analogously we prove that, if $v_\rho(B)=\textsf{n}$ and $v_\rho(A) \in \textrm{D}$ then $v_\rho(A\to B)=\textsf{n}=v_\rho(A) \,\tilde{\to}\, v_\rho(B)$. 
Now, assume that $v_\rho(B)=F_0$ and $v_\rho(A) \in \textrm{D}$. Then, $\rho(B)=0$, $\rho(\neg B)=1$, $\rho(\ensuremath{{\circ}} B)=0$ and $\rho(A)=1$. By (v3), (v7) and (vp17)', $\rho(A \to B)=0$, $\rho(\neg(A \to B))=1$ and $\rho(\ensuremath{{\circ}}(A \to B))=0$. That is, $v_\rho(A\to B)=F_0=v_\rho(A) \,\tilde{\to}\, v_\rho(B)$. Suppose now that $v_\rho(B)=F$ and $v_\rho(A) \in \textrm{D}$.  Then, $\rho(B)=0$, $\rho(\neg B)=1$, $\rho(\ensuremath{{\circ}} B)=1$ and $\rho(A)=1$. By (v3), (v7) and (vp15), $\rho(A \to B)=0$, $\rho(\neg(A \to B))=1$ and $\rho(\ensuremath{{\circ}}(A \to B))=1$. That is, $v_\rho(A\to B)=F=v_\rho(A) \,\tilde{\to}\, v_\rho(B)$.
Finally, suppose that $v_\rho(A)=\textsf{n}$ and $v_\rho(B) \in \{\textsf{b},\textsf{n},F_0,F\}$. Then, $\rho(A)=\rho(\neg A)=\rho(\ensuremath{{\circ}} A)=0$ and: either $\rho(\ensuremath{{\circ}} B)=0$ or $\rho(B)=0$. By (v3), (v7) and (vp16)', $\rho(A \to B)=0$, $\rho(\neg(A \to B))=1$ and $\rho(\ensuremath{{\circ}}(A \to B))=0$. That is, $v_\rho(A\to B)=T_0=v_\rho(A) \,\tilde{\to}\, v_\rho(B)$.


\vspace{1mm}\noindent{\em Negation:}
Let $v_\rho(A)=(\rho(A),\rho(\neg A),\rho(\ensuremath{{\circ}} A))$. Then, 
by (v4) and (vp2): 
	$$\begin{array}{lll}
	v_\rho(\neg A) &=&  (\rho(\neg A),\rho(\neg\neg A),\rho(\ensuremath{{\circ}}\neg A))\\
	&=& (\rho(\neg A),\rho(A),\rho(\ensuremath{{\circ}} A))= \tilde{\neg}\, v_\rho(A).
	\end{array}$$

\vspace{1mm}\noindent{\em Classicality:}
Let $v_\rho(A)=(\rho(A),\rho(\neg A),\rho(\ensuremath{{\circ}} A))$. 
Then, by (vp1):
	$$\begin{array}{lll}
	v_\rho(\ensuremath{{\circ}} A) &=&  (\rho(\ensuremath{{\circ}} A),\rho(\neg \ensuremath{{\circ}} A),\rho(\ensuremath{{\circ}}\cons A))\\
	&=& (\rho(\ensuremath{{\circ}} A),\ensuremath{{\sim}} \rho(\ensuremath{{\circ}} A),1)= \tilde{\ensuremath{{\circ}}}\, v_\rho(A).
	\end{array}$$ \
	
\vspace{1mm} \noindent This shows that $v_{\rho}$ is a valuation over the matrix $\mathcal{M}_{6}$ such that, 
for every formula $A$, $v_\rho(A) \in \textrm{D}$ \ iff \ $\rho(A)=1$.
\end{proof}

\vspace{2mm}

\begin{theorem}  [Completeness of \ensuremath{LET_{K}^+}\ w.r.t. the 6-valued logical matrix $\mathcal{M}_6$] \label{comple-LETKP-matrix}  \ \\
For every set of formulas $\Gamma \cup \{A\} \subseteq For(\Sigma)$: 
$\Gamma\models_{\mathcal{M}_6} A$ \ implies that \ $\Gamma \vdash_{\ensuremath{LET_{K}^+}} A$.
\begin{proof} 
Assume that $\Gamma\models_{\mathcal{M}_{6}} A$, and let $\rho$ be a bivaluation for \ensuremath{LET_{K}^+}\ such that $\rho(B)=1$ for every $B \in \Gamma$. Let $v_{\rho}$ be defined as in Proposition~\ref{lemma-comple-LETKP}. Then, $v_{\rho}$ is a valuation over $\mathcal{M}_{6}$ such that $v_{\rho}(B) \in \textrm{D}$, for every $B \in \Gamma$. By hypothesis, $v_{\rho}(A) \in \textrm{D}$, whence $\rho(A)=1$. This shows that  $\Gamma\models_{\ensuremath{LET_{K}^+}}^2 A$. By Theorem~\ref{adeq-LETKP-bival}, $\Gamma \vdash_{\ensuremath{LET_{K}^+}} A$.
\end{proof}\end{theorem}



\begin{proposition} \label{charact-bival-LETKP} Let $\rho$ be a bivaluation for \ensuremath{LET_{K}}. Then, $\rho$ is a bivaluation for \ensuremath{LET_{K}^+}\ iff it satisfies, in addition,  (vp1) and (vp2) (from Definition~\ref{val-sem-propag}) plus the following properties:\\[1mm]
\hspace*{-2mm}$\begin{array}{ll}
\mbox{(v9)} &\hspace*{-2mm} \rho(\ensuremath{{\circ}}(A \land B))=(\rho(A) \sqcap \rho(\ensuremath{{\circ}} A) \sqcap \rho(B) \sqcap \rho(\ensuremath{{\circ}} B)) \sqcup (\rho(\neg A) \sqcap \rho(\ensuremath{{\circ}} A))\sqcup(\rho(\neg B) \sqcap \rho(\ensuremath{{\circ}} B));\\[1mm]
\mbox{(v10)} &\hspace*{-2mm}  \rho(\ensuremath{{\circ}}(A \lor B))=(\rho(\neg A) \sqcap \rho(\ensuremath{{\circ}} A) \sqcap \rho(\neg B) \sqcap \rho(\ensuremath{{\circ}} B)) \sqcup (\rho(A) \sqcap \rho(\ensuremath{{\circ}} A))\sqcup(\rho(B) \sqcap \rho(\ensuremath{{\circ}} B));\\[1mm]
\mbox{(v11)} &\hspace*{-2mm}  \rho(\ensuremath{{\circ}}(A \to B))= (\rho(A) \sqcap \rho(\neg B) \sqcap \rho(\ensuremath{{\circ}} B)) \sqcup (\rho(\neg A) \sqcap \rho(\ensuremath{{\circ}} A)) \sqcup (\rho(B) \sqcap \rho(\ensuremath{{\circ}} B)).
\end{array}$
\begin{proof} It follows by a tedious but straightforward verification.
\end{proof}\end{proposition}


\subsection{\ensuremath{LET_{K}^+}\ is Blok-Pigozzi algebraizable} \label{sect-BPalg}

In this section we show that \ensuremath{LET_{K}^+}\ has enough expressive power  to be algebraizable in the general sense proposed by 
 Blok and  Pigozzi in \cite{blok:pig:89} (see also  \cite{Font:book}).

First, note that  in \ensuremath{LET_{K}^+}\  a bi-implication $A \leftrightarrow B $ defined as $ (A \to B) \land (B \to A)$ does not preserve logical equivalence through the connectives: for instance, $T_0 \leftrightarrow \textsf{b}$ gets the designated value $\textsf{b}$, but $\neg T_0 \leftrightarrow \neg \textsf{b}= F_0 \leftrightarrow \textsf{b}=F_0$, which is non-designated. In \textit{N4}\ and $\textit{N4}^\bot$ an `equivalence' operator which preserves logical  equivalence through the connectives (that is, defines a logical congruence) is defined as follows: $A \Leftrightarrow B \ensuremath{~\stackrel{\text{{\tiny def }}}{=}~} (A \leftrightarrow B) \land (\neg A \leftrightarrow \neg B)$. In terms of its (two-dimensional) twist structures, this means that two pairs are equal when the respective coordinates coincide. But in \ensuremath{LET_{K}^+}\ we are dealing with three-dimensional twist structures, that is, the snapshots are triples instead of pairs. Since we have twist operators to `read' each coordinate of the snapshots ($\tilde{\neg}$ `reads' the second coordinate, while $\tilde{\ensuremath{{\circ}}}$ `reads' the third one) an appropriate  notion of  `equivalence' (representing identity between triples) in \ensuremath{LET_{K}^+}\ should be the following:
$$A \equiv B \ensuremath{~\stackrel{\text{{\tiny def }}}{=}~} (A \leftrightarrow B) \land (\neg A \leftrightarrow \neg B) \land (\ensuremath{{\circ}} A \leftrightarrow \ensuremath{{\circ}} B).$$
The  table of the interpretation $\tilde{\equiv}$ of this  connective in $\mathcal{M}_6$ is as follows: 

\begin{center}
\begin{tabular}{|c|c|c|c|c|c|c|}
\hline
 $\tilde{\equiv}$ & $T$  & $T_0$  & $\textsf{b}$ & $\textsf{n}$ & $F_0$  & $F$ \\[1mm]
 \hline \hline
    $T$    & $T$  & $F$ & $F$ & $F$ & $F$ & $F$   \\[1mm] \hline
     $T_0$    & $F$  & $T_0$ & $F_0$ & $\textsf{n}$ & $F_0$ & $F$  \\[1mm] \hline
     $\textsf{b}$    & $F$  & $F_0$ & $\textsf{b}$ & $\textsf{n}$ & $F_0$ & $F$  \\[1mm] \hline
     $\textsf{n}$    & $F$  & $\textsf{n}$ & $\textsf{n}$ & $T_0$ & $\textsf{n}$ & $F$  \\[1mm] \hline
     $F_0$    & $F$  & $F_0$ & $F_0$ & $\textsf{n}$ & $T_0$ & $F$  \\[1mm] \hline
     $F$    & $F$  & $F$ & $F$ & $F$ & $F$ & $T$  \\[1mm] \hline
\end{tabular}
\end{center}

\

\noindent
From the  table above, it is immediate to prove the following relevant properties of $\equiv$:

\begin{proposition} \label{prop-equivBP}
The following properties hold in  $\mathcal{M}_6$:\\[1mm]
(1) \ For every $z,w \in \textsc{B}_{\ensuremath{LET_{K}}}$, $(z \,\tilde{\equiv}\, w) \in \textrm{D}$ \ iff \ $z=w$.\\[1mm]
(2) \ For every formulas $A$ and $B$, and for every valuation $v$ over $\mathcal{M}_6$: 
$v(A \equiv B)  \in \textrm{D} \ \mbox{ iff } \ v(A)=v(B).$ \\[1mm] 
(3) \ $\models_{\mathcal{M}_6} (A \equiv A)$ \ for every formula $A$.\\[1mm]
(4) \ $(A \equiv B) \models_{\mathcal{M}_6} (B \equiv A)$ for every formulas $A$ and $B$. \\[1mm]
(5) \ $(A \equiv B), (B \equiv C) \models_{\mathcal{M}_6} (A \equiv C)$ for every formulas $A$, $B$ and $C$.\\[1mm]
(6) \ $(A \equiv B) \models_{\mathcal{M}_6} (\#\, A \equiv \#\, B)$ for every formulas $A$ and $B$ and $\# \in \{\neg,\ensuremath{{\circ}}\}$. \\[1mm]
(7) \ $(A \equiv B), (C \equiv D) \models_{\mathcal{M}_6} (A\,\#\,C \equiv B\,\#\,D)$ for every formulas $A$, $B$, $C$ and $D$ and $\# \in \{\land,\lor,\to\}$.\\[1mm]
(8) \ $(A \equiv (A \to A))  \models_{\mathcal{M}_6} A$, and $A  \models_{\mathcal{M}_6} (A \equiv (A \to A))$  \ for every formula $A$.
\begin{proof}
Item (1) is immediate from the truth-table for $\tilde{\equiv}$ displayed above. An analytical proof can be done as follows: For every $z,w \in \textsc{B}_{\ensuremath{LET_{K}}}$ let  $z \,\tilde{\leftrightarrow}\, w \ensuremath{~\stackrel{\text{{\tiny def }}}{=}~} (z \,\tilde{\to}\, w) \,\tilde{\land}\, (w \,\tilde{\to}\, z)$. Then, $(z \,\tilde{\leftrightarrow}\, w)_1=(z_1 \Rightarrow w_1) \sqcap (w_1 \Rightarrow z_1)$ and so $z \,\tilde{\leftrightarrow}\, w \in \textrm{D}$ iff $z_1=w_1$.  From this, 
$\tilde{\neg}\,z \,\tilde{\leftrightarrow}\, \tilde{\neg}\,w \in \textrm{D}$ iff $z_2=w_2$, and $\tilde{\ensuremath{{\circ}}}\,z \,\tilde{\leftrightarrow}\, \tilde{\ensuremath{{\circ}}}\,w \in \textrm{D}$ iff $z_3=w_3$. This means that $(z \,\tilde{\equiv}\, w) \in \textrm{D}$ \ iff $z_i=w_i$ for $i=1,2,3$, iff $z=w$. Item~(2) follows from~(1) and from the fact that $v(A \equiv B)= (v(A) \,\tilde{\equiv}\, v(B))$ for every formulas $A$ and $B$, and every valuation $v$  over $\mathcal{M}_6$. Items (3)-(7) are immediate from~(2), taking into account (for items~(6) and~(7)) that the operations in $\mathcal{M}_6$ are functional, that is, deterministic. For (8), let $v$ be a valuation over  $\mathcal{M}_6$ such that $v(A \equiv (A \to A)) \in \textrm{D}$. By~(2), $v(A)=v(A \to A)=v(A) \,\tilde{\to}\, v(A)$. But $z \,\tilde{\to}\, z\in \textrm{D}$ for every $z \in \textsc{B}_{\ensuremath{LET_{K}}}$. Hence, $v(A) \in \textrm{D}$, showing that $(A \equiv (A \to A))  \models_{\mathcal{M}_6} A$. Conversely, let $v$  be a valuation over  $\mathcal{M}_6$ such that $v(A) \in \textrm{D}$. Hence, $v(A \to A)=v(A) \,\tilde{\to}\, v(A)=v(A)$, by definition of $\tilde{\to}$ (since  $z \,\tilde{\to}\, z=z$ for every $z\in \textrm{D}$). By~(2), $v(A \equiv (A \to A)) \in \textrm{D}$. This shows that $A  \models_{\mathcal{M}_6} (A \equiv (A \to A))$.
\end{proof}\end{proposition}




\begin{theorem} \ 

\vspace{1mm}\noindent
The logic \ensuremath{LET_{K}^+}\ is algebraizable in the sense of Blok-Pigozzi.
\begin{proof}
Let $p_1$ and $p_2$ be two different propositional variables, and consider the sets 
$$\Delta(p_1,p_2)=\{(p_1 \equiv p_2)\} \ \mbox{  and } \ E(p_1)=\{\langle p_1, (p_1 \to p_1)\rangle\}.$$
By items~(3)-(8) of Proposition~\ref{prop-equivBP}, the sets $\Delta(p_1,p_2)$ and $E(p_1)$ show that the logic \ensuremath{LET_{K}^+}, presented by means of $\mathcal{M}_6$, is algebraizable in the sense of Blok-Pigozzi. Indeed, conditions (3)-(8) of Proposition~\ref{prop-equivBP} are exactly the requirements for $\Delta(p_1,p_2)$ and $E(p_1)$ stated in Theorem~4.7 of~\cite{blok:pig:89} for a given logic being algebraizable.\footnote{Observe that conditions~(6) and~(7) of Proposition~\ref{prop-equivBP} depend on the signature of the given logic. In the terminology of~\cite{blok:pig:89}, it can be said that $\Delta(p_1,p_2)$ is a system of equivalence formulas, while $E(p_1)$ (written as $p_1 \approx (p_1 \to p_1)$) is a system of defining equations for the deductive system generated by $\mathcal{M}_6$, that is, \ensuremath{LET_{K}^+}.}
\end{proof}\end{theorem}
 

   
\noindent This result, combined with the family of twist models for \ensuremath{LET_{K}^+}\ as well as the relationship of \ensuremath{LET_{K}^+}\ with involutive Stone algebras, to be studied in the following two sections, open interesting possibilities for future research of \ensuremath{LET_{K}^+}\ from the perspective of abstract algebraic logic.



\section{Twist models for \ensuremath{LET_{K}^+}\ } \label{sect-lattice}


In Section~\ref{sec.six.valued.letkp} we have seen how the restrictions imposed on the Nmatrix of \ensuremath{LET_{K}}\ by the rules of propagation 
of classicality  yield  a (deterministic) 6-valued semantics for \ensuremath{LET_{K}^+}, the matrix $\mathcal{M}_6$. 


  $\mathcal{A}_{\ensuremath{LET_{K}}}$ is  the 6-valued multialgebra underlying the Nmatrix  $\mathcal{M}_{\ensuremath{LET_{K}}}$,  
which was presented as a  swap structure in Definition~\ref{defNmatLETK}.   
 In order to comply with the  axiom and rules of propagation of classicality of  \ensuremath{LET_{K}^+}, 
$\mathcal{A}_{\ensuremath{LET_{K}}}$,
becomes the algebra $\mathcal{A}_6$ for \ensuremath{LET_{K}^+}. The latter  is the underlying algebra of the  logical matrix $\mathcal{M}_6$.   


Twist structures  are special cases of swap structures: while the latter can be multialgebras, 
the former are algebras,  based on 
operations instead of multioperations, and so the respective semantics are deterministic.\footnote{For a more detailed discussion 
of swap and twist structures, see Coniglio et al. \cite{con.fig.gol.2018},  in particular sections 9.3 and 9.4.} 
In what follows, the algebra $\mathcal{A}_6$ will be presented  as a 
\textit{three-dimensional twist structure}. 
We will show  how  $\mathcal{A}_6$
can be  generalized to twist algebras generated by arbitrary Boolean algebras. 
This will produce a class of twist-valued models for \ensuremath{LET_{K}^+}, one for each Boolean algebra, 
which characterizes \ensuremath{LET_{K}^+}. 
Moreover, it will be proved that these models are, indeed, bounded lattices in which 
 suprema and infima are respectively given by the operators $\tilde{\land}$ and $\tilde{\lor}$ and 
  the top and bottom elements are given by $T$ and $F$. 












\begin{definition} [Twist structures for \ensuremath{LET_{K}^+}]  \label{twist-BA} \ 

\vspace{1mm}\noindent 
Let $\mathcal{B}= \langle {\bf B}, \sqcap,\sqcup,\Rightarrow,\ensuremath{{\sim}},0,1 \rangle$ be a Boolean algebra. The {\em twist structure for \ensuremath{LET_{K}^+}\ induced by $\mathcal{B}$} is the algebra $\mathcal{T}_{\mathcal{B}}=\langle \textsc{B}_{\ensuremath{LET_{K}}}^{\mathcal{B}}, \tilde{\land},\tilde{\lor},\tilde{\to},\tilde{\neg},\tilde{\ensuremath{{\circ}}}\rangle$ over $\Sigma$ such that
$$\textsc{B}_{\ensuremath{LET_{K}}}^{\mathcal{B}}=\{z \in {\bf B}^3 \ : \ z_3 \leq z_1 \sqcup z_2 \ \mbox{ and } \ z_1 \sqcap z_2 \sqcap z_3=0  \}$$
and the operations are defined as follows:  
\begin{itemize}\setlength\itemsep{-0.2em} 
\item[(i)] $(z_1,z_2,z_3)\,\tilde{\land}\,(w_1,w_2,w_3) =  (z_1\sqcap w_1,z_2\sqcup w_2,(z_1 \sqcap z_3 \sqcap w_1 \sqcap w_3) \sqcup (z_2 \sqcap z_3) \sqcup (w_2 \sqcap w_3))$,
\item[(ii)] $(z_1,z_2,z_3)\,\tilde{\lor}\,(w_1,w_2,w_3)  =  (z_1\sqcup w_1,z_2\sqcap w_2, (z_2 \sqcap z_3 \sqcap w_2 \sqcap w_3) \sqcup (z_1 \sqcap z_3) \sqcup (w_1 \sqcap w_3))$,
\item[(iii)] $(z_1,z_2,z_3)\,\tilde{\to}\,(w_1,w_2,w_3)  =  (z_1\Rightarrow w_1,z_1\sqcap w_2, (z_1 \sqcap w_2 \sqcap w_3) \sqcup (z_2 \sqcap z_3) \sqcup (w_1 \sqcap w_3))$,
\item[(iv)] $\tilde{\neg}\,(z_1,z_2,z_3)  =  (z_2,z_1,z_3)$, 
\item[(v)] $\tilde{\circ}\,(z_1,z_2,z_3)  =  (z_3,\ensuremath{{\sim}} z_3,1)$.


\end{itemize}
\end{definition}

\vspace{1mm}\noindent Note  that  $\mathcal{T}_{\mathcal{B}_2}$ is exactly $\mathcal{A}_6$. Each twist structure $\mathcal{T}_{\mathcal{B}}$ for \ensuremath{LET_{K}^+}\ naturally induces a logical matrix $\mathcal{M}(\mathcal{B}) = \langle \mathcal{T}_{\mathcal{B}}, \textrm{D}_{\mathcal{B}}\rangle$ where $\textrm{D}_{\mathcal{B}}=\{z \in \textsc{B}_{\ensuremath{LET_{K}}}^{\mathcal{B}} \ : \ z_1 =1 \}$. Let $Mat(\ensuremath{LET_{K}^+})$ be the class of logical matrices of the form $\mathcal{M}(\mathcal{B})$, and let $\models_{Mat(\ensuremath{LET_{K}^+})}$ be the associated consequence relation. Notice that $\mathcal{M}(\mathcal{B}_2)=\mathcal{M}_6$.


 
In Definition~\ref{defNmatLETK} the multioperations of the multialgebra $\mathcal{A}_{\ensuremath{LET_{K}}}$ were presented
 in the framework of a  non-deterministic swap structure in which the third coordinate of each snapshot of \ensuremath{LET_{K}}\ 
 \textit{is not} functionally 
 determined from the input(s). 
 On the other hand,  the tables of \ensuremath{LET_{K}^+}, presented in Definition~\ref{def.six.val.LETKP}, 
 make it clear that in  
 $\mathcal{A}_6$, the third coordinate of snapshots, obtained by applying the respective operation, is functionally determined  
 from the input(s). Note, in addition, that a snapshot is `classical' -- that is, it belongs to $\{T,F\}$ --  
 exactly when the third coordinate is 1. 
 Thus, in the case of $\tilde{\land}$, the output $z \,\tilde{\land}\, w$ is `classical' exactly when: (i)  $z=w=T$, or (ii) $z=F$, or $w=F$. This yields  the item (i) above. 
  
 By   analogous reasoning for  $\tilde{\lor}$ and $\tilde{\to}$, we obtain  items (ii) and (iii) 
above.  
Given the equivalence between $\ensuremath{{\circ}} A$ and  $\ensuremath{{\circ}} \neg A$
the negation $\tilde{\neg}$ in \ensuremath{LET_{K}^+}\  is deterministic, and defined by item (iv). 
Finally, the classicality operator $\tilde{\circ}$ of \ensuremath{LET_{K}^+},  given clause (vp1)
of Definition~\ref{val-sem-propag},  
also becomes  deterministic, and so defined by item (v).   
Indeed, by (vp1), $\rho(\ensuremath{{\circ}}\cons A)=1$. This, together with Proposition~\ref{der-rules},  
 implies that $\rho(\neg \ensuremath{{\circ}} A)=\ensuremath{{\sim}} \rho(\ensuremath{{\circ}} A)$. Hence, by (vp1), $\rho(\neg A)=\ensuremath{{\sim}} \rho(A)$ and $\rho(\ensuremath{{\circ}}\cons A)=1$. 



\begin{remark} \label{formulas-terms}
Let  $A(p_1,\ldots,p_k)$ be a formula over the signature of \ensuremath{LET_{K}^+}\ depending at most on the propositional variables $p_1,\ldots,p_k$, and let $v$ be a valuation over a matrix $\mathcal{M}(\mathcal{B})$ for \ensuremath{LET_{K}^+}. Since $v(p_i)$ is an arbitrary snapshot, its value can be represented by 3 new propositional variables $p_i^j$, each one representing $v(p_i)_j$, the $jth$-projection of $v(p_i)$ for $j=1,2,3$. Let $\mathcal{V}_3=\{p_i^j \ : \ 1 \leq i \leq n$ and $1 \leq j \leq 3\}$ be the set of such new propositional variables. Hence, the formal expression for $v(A)_1$ (that is, the first coordinate of $v(A)$) can be represented by a term $\tau_A$ in the signature $\Sigma_{BA}=\{\sqcap,\sqcup,\Rightarrow, \ensuremath{{\sim}},\bot,\top\}$ of Boolean algebras over the variables $\mathcal{V}_3$.  For instance, given $A=(p_1 \land \neg p_2) \vee \ensuremath{{\circ}} p_1$ and $B=\neg ((p_1 \land \neg p_2) \vee \ensuremath{{\circ}} p_1)$ then $v(A)_1$ and $v(B)_1$ are represented, respectively, by the terms $\tau_A=(v(p_1)_1 \sqcap v(\neg p_2)_1) \sqcup v(\ensuremath{{\circ}} p_1)_1 = (v(p_1)_1 \sqcap v(p_2)_2) \sqcup v(p_1)_3 = (p_1^1 \sqcap p_2^2) \sqcup p_1^3$ and $\tau_B=v(\neg ((p_1 \land \neg p_2) \vee \ensuremath{{\circ}} p_1))_1=v((p_1 \land \neg p_2) \vee \ensuremath{{\circ}} p_1)_2 = (v(p_1)_2 \sqcup v(\neg p_2)_2) \sqcap v(\ensuremath{{\circ}} p_1)_2 = (v(p_1)_2 \sqcup v(p_2)_1) \sqcap \ensuremath{{\sim}} v(p_1)_3 = (p_1^2 \sqcup p_2^1) \sqcap \ensuremath{{\sim}} p_1^3$ over the signature of Boolean algebras over the variables $\mathcal{V}_3$.
The fact that $v(p_i)$ is an snapshot instead of an arbitrary  triple in ${\bf B}^3$ is represented by the term $\tau=\tau_1 \sqcap \ldots \sqcap \tau_k$ such that $\tau_i=(p_i^3 \Rightarrow (p_i^1 \sqcup p_i^2)) \sqcap \ensuremath{{\sim}}(p_i^1 \sqcap p_i^2 \sqcap p_i^3)$.

Now,  suppose that $\Gamma \models_{\mathcal{M}_6} A$ such that $\Gamma = \{A_1, \ldots A_n\}$ is non-empty and all these formulas depend on $p_1,\ldots, p_k$. Let $B=A_1 \land \ldots \land A_n$, and let $v$ be a valuation over $\mathcal{M}_6$. Then, $v(B)_1=1$ implies that $v(A)_1=1$, which is equivalent to say that $v(B)_1 \Rightarrow v(A)_1=1$ or, equivalently, that the equation $(\tau_B \Rightarrow \tau_A) \approx \top$ holds in $\mathcal{B}_2$, provided that the variables $p_i^j$ satisfy the restriction represented by the term $\tau$ (i.e., provided that the equation $\tau \approx \top$ holds in $\mathcal{B}_2$). In other words, $\Gamma \models_{\mathcal{M}_6} A$ implies that $\mathcal{B}_2$ satisfies the equation $(\tau \Rightarrow (\tau_B \Rightarrow \tau_A))\approx \top$ in the language of Boolean algebras.  
\end{remark}

\begin{theorem} [Soundness and completeness of \ensuremath{LET_{K}^+}\ w.r.t. $Mat(\ensuremath{LET_{K}^+})$] \label{sound-compLETKPswap} For every set of formulas $\Gamma \cup \{A\}$ over $\Sigma$: $\Gamma \vdash_{\ensuremath{LET_{K}^+}} A$ \ iff \  $\Gamma \models_{Mat(\ensuremath{LET_{K}^+})} A$.
\begin{proof} 
(Left to right - Soundness): Suppose that $\Gamma \vdash_{\ensuremath{LET_{K}^+}} A$, and assume that $\Gamma = \{A_1, \ldots A_n\}$ is non-empty (the proof for the case $\Gamma=\emptyset$ is analogous but easier). By Theorem~\ref{sound-LETKP-matrix},   $\Gamma\models_{\mathcal{M}_6} A$. By Remark~\ref{formulas-terms} (and using the notation established therein) if follows that $\mathcal{B}_2$ satisfies the equation $(\tau \Rightarrow (\tau_B \Rightarrow \tau_A))\approx \top$ in the language of Boolean algebras. By Remark~\ref{val-Boole}, any Boolean algebra $\mathcal{B}$ satisfies the equation $(\tau \Rightarrow (\tau_B \Rightarrow \tau_A))\approx \top$. Now, let  $\mathcal{B}$ be a Boolean algebra and let $v$ be a valuation over the matrix $\mathcal{M}(\mathcal{B})$ such that $v(B) \in \textrm{D}_{\mathcal{B}}$, where $B=A_1 \land \ldots \land A_n$. By instantiating in  such equation each variable $p_i^j$ with the value $v(p_i)_j$ we get that  the equation $\tau \approx \top$ holds in $\mathcal{B}$ with valuation $v$, since $v(p_i) \in \textsc{B}_{\ensuremath{LET_{K}}}^{\mathcal{B}}$ for $1 \leq i \leq k$. From this, the equation  $(\tau_B \Rightarrow \tau_A)\approx \top$  holds in $\mathcal{B}$ with valuation $v$. But  the equation $\tau_B \approx \top$ holds in $\mathcal{B}$ with valuation $v$, given that  $v(B) \in \textrm{D}_{\mathcal{B}}$ (which means that $v(B)_1=1$). From this we conclude that  the equation $\tau_A \approx \top$ holds in $\mathcal{B}$ with valuation $v$. This means that $v(A)_1=1$, i.e., $v(A) \in \textrm{D}_{\mathcal{B}}$. This shows that $\Gamma \models_{\mathcal{M}(\mathcal{B})} A$ for every $\mathcal{B}$, hence  $\Gamma \models_{Mat(\ensuremath{LET_{K}^+})} A$.\\[1mm]
(Right to left - Completeness): Suppose that $\Gamma  \models_{Mat(\ensuremath{LET_{K}^+})} A$. Then, in particular,  $\Gamma \models_{\mathcal{M}(\mathcal{B}_2)} A$. But $\mathcal{M}(\mathcal{B}_2)$ is $\mathcal{M}_6$, hence $\Gamma \models_{\mathcal{M}_6} A$. By Theorem~ \ref{comple-LETKP-matrix}, $\Gamma \vdash_{\ensuremath{LET_{K}^+}} A$.
\end{proof}\end{theorem}


\begin{remark} \label{lattice}
Recall that, besides the usual order-theoretic definition,   a  {\em lattice} can be defined as an algebra $\langle L, \sqcap,\sqcup\rangle$ such that: 
\begin{itemize} 
\item[] (1)~$a \sqcap a= a = a \sqcup a$; 
\item[] (2)~$a \sqcap b=b \sqcap a$ and $a \sqcup b=b \sqcup a$; 
\item[] (3)~$a \sqcap(b \sqcap c)=(a \sqcap b) \sqcap c$ and $a \sqcup(b \sqcup c)=(a \sqcup b) \sqcup c$; and
\item[] (4) $a \sqcap(a \sqcup b)=a= a \sqcup(a \sqcap b)$, for every $a,b,c \in L$.
\end{itemize}
\noindent 
It follows that, in any  algebra as above, $a=a \sqcap b$ iff $b= a \sqcup b$, for every $a,b \in L$. Then, the relation $a \leq b$ iff  $a=a \sqcap b$ (iff $b= a \sqcup b$) is a partial order over $L$ such that $a \sqcap b$ and $a \sqcup b$ are the infimum and supremum, respectively, of the set $\{a,b\}$ w.r.t. the partial order $\leq$. This means that $\langle L,\leq\rangle$ is a lattice in the order-theoretic sense. 
\end{remark}


\begin{theorem}  \label{twist-lattice}
For every Boolean algebra $\mathcal{B}$ the twist structure $\mathcal{T}_{\mathcal{B}}$ is a bounded lattice in which the infimum and supremum are given by $\tilde{\land}$ and $\tilde{\lor}$, respectively, and  $T=(1,0,1)$ and $F=(0,1,1)$ are the top and bottom elements (where $1$ and $0$ are the top and bottom elements of $\mathcal{B}$).
\begin{proof} It will be shown that, for every Boolean algebra $\mathcal{B}$, the algebra $\mathcal{T}_{\mathcal{B}}$ is such that $\tilde{\land}$ and $\tilde{\lor}$ satisfy conditions (1)-(4) of Remark~\ref{lattice}.

\vspace{1mm}\noindent  
(1) Let $\#\in \{\land,\lor\}$. Given that $\mathcal{B}$ satisfies condition~(1), it is clear that $(z \,\tilde{\#}\, z)_i=z_i$ for $i=1,2$. On the other hand,  $(z \,\tilde{\#}\, z)_3=(z_1 \sqcap z_3) \sqcup (z_2 \sqcap z_3)= z_3 \sqcap (z_1 \sqcup z_2)=z_3$. Hence, $z \,\tilde{\#}\, z=z$ for every $z$ and $\#\in \{\land,\lor\}$.

\vspace{1mm}\noindent 
(2) Clearly $z \,\tilde{\#}\, w=w\,\tilde{\#}\, z$ for every $z,w$ and  $\#\in \{\land,\lor\}$, by the very definitions and by the that $\mathcal{B}$ satisfies condition~(2). 

\vspace{1mm}\noindent 
(3) Let us first prove that $z \,\tilde{\land}\,(w \,\tilde{\land}\, u)=(z \,\tilde{\land}\, w) \,\tilde{\land}\, u$. Observe that $(z \,\tilde{\land}\,(w \,\tilde{\land}\, u))_i=((z \,\tilde{\land}\, w) \,\tilde{\land}\, u)_i$ for $i=1,2$, by definition of $\tilde{\land}$ and the fact that $\mathcal{B}$ satisfies condition~(3). Now,  let $a \ensuremath{~\stackrel{\text{{\tiny def }}}{=}~} (w \,\tilde{\land}\, u)_3=(w_1 \sqcap w_3 \sqcap u_1 \sqcap u_3) \sqcup (w_2 \sqcap w_3) \sqcup (u_2 \sqcap u_3)$ and $b\ensuremath{~\stackrel{\text{{\tiny def }}}{=}~} (z \,\tilde{\land}\, w)_3= (z_1 \sqcap z_3 \sqcap w_1 \sqcap w_3) \sqcup (z_2 \sqcap z_3) \sqcup (w_2 \sqcap w_3)$. Hence,

\begin{itemize}\setlength\itemsep{-0.2em} 
\item[] $c\ensuremath{~\stackrel{\text{{\tiny def }}}{=}~} (z \,\tilde{\land}\,(w \,\tilde{\land}\, u))_3=(z_1 \sqcap z_3 \sqcap (w_1 \sqcap u_1) \sqcap a) \sqcup (z_2 \sqcap z_3) \sqcup ((w_2 \sqcup u_2) \sqcap a)$, and
\item[] $d\ensuremath{~\stackrel{\text{{\tiny def }}}{=}~} ((z \,\tilde{\land}\, w) \,\tilde{\land}\, u)_3=((z_1 \sqcap w_1) \sqcap b \sqcap u_1 \sqcap u_3) \sqcup ((z_2 \sqcup w_2) \sqcap b) \sqcup (u_2 \sqcap u_3)$.
\end{itemize}

\noindent By using an automatic prover for  tautologies in \text{\it CPL}\ it is immediate to check that the formula $A_c \leftrightarrow A_d$ is a tautology, where $A_c$ and $A_d$ are the propositional formulas respectively obtained from the terms $c$ and $d$ by replacing $z_i, w_i,u_i$ by different propositional variables $p_i,q_i,r_i$ (for $i=1,2,3$), and where $\sqcap$ and $\sqcup$ are replaced by conjunction $\land$ and disjunction $\lor$. This means that the equation $c=d$ holds in $\mathcal{B}_2$ and so it holds in every Boolean algebra $\mathcal{B}$, as observed in Remark~\ref{val-Boole}. That is, $(z \,\tilde{\land}\,(w \,\tilde{\land}\, u))_3=((z \,\tilde{\land}\, w) \,\tilde{\land}\, u)_3$ for every $\mathcal{B}$ and every $z,w,u$ in $\textsc{B}_{\ensuremath{LET_{K}}}^{\mathcal{B}}$. Therefore, $z \,\tilde{\land}\,(w \,\tilde{\land}\, u)=(z \,\tilde{\land}\, w) \,\tilde{\land}\, u$  for every $\mathcal{B}$ and every $z,w,u \in \textsc{B}_{\ensuremath{LET_{K}}}^{\mathcal{B}}$. The proof of associativity of $\tilde{\lor}$ is obtained by similar arguments.

\vspace{1mm}\noindent
(4) Observe that, by definition of $\tilde{\land}$ and $\tilde{\lor}$, $z_i=(z \,\tilde{\lor}\,(z \,\tilde{\land}\, w))_i$ for every $z,w$ and $i=1,2$, given that $\mathcal{B}$ has property~(4). Now, let  $a\ensuremath{~\stackrel{\text{{\tiny def }}}{=}~} (z \,\tilde{\land}\, w)_3= (z_1 \sqcap z_3 \sqcap w_1 \sqcap w_3) \sqcup (z_2 \sqcap z_3) \sqcup (w_2 \sqcap w_3)$ and $b \ensuremath{~\stackrel{\text{{\tiny def }}}{=}~} (z \,\tilde{\lor}\,(z \,\tilde{\land}\, w))_3=(z_2 \sqcap z_3 \sqcap(z_2 \sqcup w_2) \sqcap a) \sqcup (z_1 \sqcap z_3) \sqcup(z_1 \sqcap w_1 \sqcap a)$. Let $A_b$ be the propositional formula obtained by replacing $z_i$ and $w_i$ in the term $b$ by different propositional variables $p_i$ and $q_i$ (for $i=1,2,3$) and where $\sqcap$ and $\sqcup$ are replaced by conjunction $\land$ and disjunction $\lor$. By using an automatic prover for  tautologies in \text{\it CPL}\ it can be checked that the formula $A \ensuremath{~\stackrel{\text{{\tiny def }}}{=}~} p_3 \leftrightarrow A_b$ {\em is not} a tautology. However, the  only rows in which $A$ gets the value $0$ is when the triple $p=(p_1,p_2,p_3)$ gets the value $(0,0,1)$ or when the triple $q=(q_1,q_2,q_3)$ gets the value $(1,1,1)$, and these triples do not correspond to snapshots in $\textsc{B}_{\ensuremath{LET_{K}}}$. Consider then the formula 

\begin{itemize}
\item[] $B\ensuremath{~\stackrel{\text{{\tiny def }}}{=}~}((p_3 \to (p_1 \vee p_2)) \land (q_3 \to (q_1 \vee q_2)) \land \ensuremath{{\sim}}(p_1 \land p_2 \land p_3) \land \ensuremath{{\sim}}(q_1 \land q_2 \land q_3)) \to A.$ 
\end{itemize}
\noindent By the previous considerations, it follows that $B$ is a tautology. Thus, if 
\begin{itemize}
\item[] $c=(z_3 \Rightarrow (z_1 \sqcup z_2)) \sqcap (w_3 \Rightarrow (w_1 \sqcup w_2)) \sqcap \ensuremath{{\sim}}(z_1 \sqcap z_2 \sqcap z_3) \sqcap \ensuremath{{\sim}}(w_1 \sqcap w_2 \sqcap w_3)$,
\end{itemize}
\noindent then  the equation 
\begin{itemize}
\item[] $(c \Rightarrow ((z_3 \Rightarrow b) \sqcap (b \Rightarrow z_3)))=1$
\end{itemize}
\noindent  
holds  in $\mathcal{B}_2$ and so it holds in every Boolean algebra $\mathcal{B}$, for every $z=(z_1,z_2,z_3)$ and $w=(w_1,w_2,w_3)$ in  $\mathcal{B}^3$. Now, let $z=(z_1,z_2,z_3)$ and $w=(w_1,w_2,w_3)$ in $\textsc{B}_{\ensuremath{LET_{K}}}^{\mathcal{B}}$. Then, $c=1$ for such $z$ and $w$ and so $((z_3 \Rightarrow b) \sqcap (b \Rightarrow z_3))=1$. This means that $z_3=b=(z \,\tilde{\lor}\,(z \,\tilde{\land}\, w))_3$, hence $z=z \,\tilde{\lor}\,(z \,\tilde{\land}\, w)$ for every $z,w$  in $\textsc{B}_{\ensuremath{LET_{K}}}^{\mathcal{B}}$. In a similar way it can be proved that $z=z \,\tilde{\land}\,(z \,\tilde{\lor}\, w)$ for every $z,w$  in $\textsc{B}_{\ensuremath{LET_{K}}}^{\mathcal{B}}$. 

\vspace{1mm}\noindent This shows that the twist structure $\mathcal{T}_{\mathcal{B}}$ is a lattice, for every Boolean algebra $\mathcal{B}$. Clearly, $z \,\tilde{\land}\, T= z = z \,\tilde{\lor}\, F$, for every $z \in \textsc{B}_{\ensuremath{LET_{K}}}^{\mathcal{B}}$. Therefore  $\mathcal{T}_{\mathcal{B}}$ is a bounded lattice with top and bottom elements given by $T$ and $F$, respectively.
\end{proof}\end{theorem}

 



\begin{proposition} \label{def-order-twist}
The order  in the lattice $\mathcal{T}_{\mathcal{B}}$ is given as follows:
\begin{itemize}
\item[] $(z_1,z_2,z_3) \leq (w_1,w_2,w_3)  $  if and only if:   

\ \quad \quad \quad  $ z_1 \leq w_1, \ z_2 \geq w_2, \ z_2 \sqcap z_3 \geq w_2 \sqcap w_3,   
\mbox{ and } z_3 \leq (z_1 \sqcap w_3) \sqcup z_2$.
\end{itemize}
\begin{proof}
By definition of the order $\leq$ in $\textsc{B}_{\ensuremath{LET_{K}}}^{\mathcal{B}}$ induced by the algebraic lattice structure of $\mathcal{T}_{\mathcal{B}}$,  and  according to Theorem~\ref{twist-lattice}, it follows that 
$(z_1,z_2,z_3) \leq (w_1,w_2,w_3)$ \ iff  \ $z_1 \leq w_1$, $z_2 \geq w_2$,  \  and \\[1mm]
\indent $(\ast) \ \ \ z_3=(z_1 \sqcap z_3 \sqcap w_3) \sqcup (z_2 \sqcap z_3) \sqcup (w_2 \sqcap w_3)$.\\[1mm] 
By taking infimum w.r.t. $z_2$ in both sides of $(\ast)$ we get that $z_2 \sqcap z_3 = (z_2 \sqcap z_1 \sqcap z_3 \sqcap w_3) \sqcup (z_2 \sqcap z_3) \sqcup (z_2 \sqcap w_2 \sqcap w_3)$. Given that $z_2 \sqcap z_1 \sqcap z_3=0$ and $z_2 \sqcap w_2=w_2$ (since $z_2 \geq w_2$), this implies that $z_2 \sqcap z_3 = (z_2 \sqcap z_3) \sqcup (w_2 \sqcap w_3)$. That is,  $z_2 \sqcap z_3 \geq w_2 \sqcap w_3$. Moreover, by consider the latter relation in equation $(\ast)$ we get that $z_3 = (z_1 \sqcap z_3 \sqcap w_3) \sqcup (z_2 \sqcap z_3) = z_3 \sqcap ((z_1 \sqcap w_3) \sqcup z_2)$.  This means that $ z_3 \leq (z_1 \sqcap w_3) \sqcup z_2$. The proof of the converse is analogous (but a little easier).
\end{proof}\end{proposition}


  
\subsection{On the lattice structure of \ensuremath{LET_{K}^+}} \label{SectSix}


In Belnap  \citep{belnap.1977.how} we find two lattice-orderings defined by the four semantic values of \ensuremath{FDE}\ (and 
 by the four values of \ensuremath{FDE^{\to}}\ as well), called 
\textbf{A4} and \textbf{L4}. 
 The lattice \textbf{A4} has   \textit{N} at the bottom and \textit{B} at the top: 

$$\xymatrix{
&{B} \ar@{-}[dl]\ar@{-}[dr] &&\\
T \ar@{-}[dr]   & & F \ar@{-}[dl]  \\
& N &
}$$ 
 
 \vspace{1mm}\noindent
The partial order  $a \leq b$ is read `$a$ approximates the information in $b$'.   
 The underlying idea is that 
 the amount of information     grows from  bottom to top, 
 in the sense that \textit{T} and \textit{F} convey  more information that \textit{N}, 
 and \textit{B} conveys more information than both  \textit{T} and \textit{F} -- in Belnap's words,   


\begin{quote}
None is at the bottom because it gives no information at all; and Both is at the top because it gives too much (inconsistent) information 
\cite[p.~39]{belnap.1977.how}.  
\end{quote}

\noindent  This order  is  clear if we think of the values \textit{N}, \textit{F}, \textit{T}, and 
 \textit{B}  as subsets of $\{ 0,1\}$,   respectively, $\emptyset$, $\{ 0\}$, $\{1 \}$, and $\{0,1 \}$, 
 and $\leq$ as the relation of inclusion $\subseteq$.  
Note that (i) positive and negative information, represented by the values \textit{T} and \textit{F} assigned to a sentence $A$, 
are on a par in this order, and (ii)  it is    assumed that a contradiction   
 $A\land\neg A$ not only does contain information but also contains the highest amount of information on $A$. 
 This is in line with 
  the already mentioned notion  of information as meaningful data, which considers false information as information (see, e.g., 
    \cite{dunn2008,fetzer2004a}), and is the notion of information that underlies the  
 interpretation of \ensuremath{FDE}\ worked out by Belnap and Dunn, as well as  the intended interpretation of \textit{LET}s\ in terms of information.   
 
The \textit{logical lattice} \textbf{L4}, on the other hand,    
 has   \textit{F} at the bottom and \textit{T} at the top. 
 The join operation is given by $\tilde{\lor}$ and the meet by $\tilde{\land}$. 
 It is represented by the following diagram: 

$$\xymatrix{
&{T} \ar@{-}[dl]\ar@{-}[dr] &&\\
N \ar@{-}[dr]   & & B \ar@{-}[dl]  \\
& F &
}$$


\noindent The partial order of \textbf{L4} can be defined as follows. Think  of the values $T, F, B,$ and $N$ as pairs $(a_1,a_2)$, 
where $a_1$ and $a_2$ represent, respectively, the values of  formulas $A$ and $\neg A$ in a given bivaluation. 
Thus, $T, F, B,$ and $N$ are represented, respectively, by the pairs $(1,0), (0,1), (1,1),$ and $(0,0)$. 
Now, the order is given as follows: $(a_1,a_2) \leq ( b_1,b_2)$ if and only if $a_1 \leq b_1 $ and $ a_2 \geq b_2$. 
This order 
is informally explained by Belnap as follows: 
\begin{quote}
[T]he worst thing is to be told something
is false, simpliciter. You are better off (it is one of our hopes) in either being told nothing
about it, or in being told both that it is true and also that it is false; while of course best
of all is to be told it is true
\cite[p.~42]{belnap.1977.how}.
\end{quote}
 
Now, let us call \textbf{L6} the lattice obtained by extending 
 \textbf{L4}  to six values. 
The values \textit{T} and \textit{F} of \ensuremath{FDE}\ became $T_0$  and $F_0$, and we add the values \textit{T} and \textit{F} of \ensuremath{LET_{K}^+}\ 
as, respectively,  a new top  and a new bottom. 
The order of \textbf{L6} has been given in Proposition~\ref {def-order-twist}. This lattice structure can be displayed  as follows:

 $$\xymatrix{
&T\ar@{-}[d]&\\
& T_0\ar@{-}[dl]\ar@{-}[dr] &\\
\textsf{n} \ar@{-}[dr] & & \textsf{b}\ar@{-}[dl]\\
& F_0\ar@{-}[d]\\
&F&
}$$

It should be observed that the 6-valued lattice above is exactly the lattice $\mathcal{T}_{\mathcal{B}_2}$
with the order defined as in Proposition~\ref{def-order-twist}.

In the diagram above,  \textbf{L4} corresponds to  the inner diamond.
The order of \textbf{L6} can be explained by modifying  the quotation above from Belnap:   
the worst thing is to be told something
has been \textit{conclusively} established as false, which is the value \textit{F},   
not too bad is to be false but not conclusively false, the value $F_0$. 
To be told something is true, although not conclusively, the value $T_0$,  
is better, but the best of all is to be told it is conclusively true, which is the value \textit{T}.





Finally, it is worth mentioning that  if we lay on its side the \textbf{L6} lattice, with \textit{N} at the bottom,   
we obtain a  meet-semilattice, call it \textbf{A6},  that fits the idea of the approximation lattice \textbf{A4}: 
  the amount of information     grows from  bottom to top, but 
  from the nodes $T_0$ and  $F_0$, the new information can be that the information already available is reliable, and in this case
  we get the values $T$ and $F$ respectively, or that conflicting information is obtained, and in this case $T_0$ and  $F_0$ 
   collapse    in the value $B$. 
  
  The order of \textbf{A6} can be represented by the relation of inclusion $\subseteq$. Consider the set $\{ 0, 1, \mathsf{c} \}$, 
  where 0 and 1 mean, respectively, negative and positive information, and $\mathsf{c} $, together with 0 or 1, means that the 
  respective information is reliable. The six values \textit{N}, $T_0$, $F_0$, \textit{T}, \textit{F}, \textit{B}  correspond, 
  respectively, to the following sets:  $\emptyset$, $\{ 1\}$, $\{ 0 \}$, $\{ 1, \mathsf{c} \}$, $\{ 0, \mathsf{c} \}$, 
   $\{ 1,0 \}$. Note that the sets $\{ 0,1,\mathsf{c} \}$ and $\{ \mathsf{c} \}$ have been dropped from the powerset of 
   $\{ 0, 1, \mathsf{c} \}$: the former because it cannot be that positive and negative information together are reliable, 
   and the latter because $\mathsf{c}$ only makes sense together with either positive or negative information. 
The meets are  given by $\cap$  and the (existing) joins by $\cup$, both operations      
   restricted to the given domain of six subsets of $\{0,1,\mathsf{c}\}$. 
   Taking this into account, $\{ 0, \mathsf{c} \} \cap  \{ 1,\mathsf{c} \} $   is the empty set, rather than $\{ \mathsf{c} \}$, 
   since the latter  does not belong to the domain of the meet-semilattice.
  Analogously, note  that the join of  \textit{T} and \textit{F}, as well as the joins of   \textit{T} and \textit{B}, and 
  also \textit{B} and  
  \textit{F},  do  not exist in the meet-semilattice.   
   Then, the least element is  \textit{N}, but there is no greatest element. 
   
    


$$\xymatrix{
T \ar@{-}[dr]   &{}&{B} \ar@{-}[dl]\ar@{-}[dr] & & F\ar@{-}[dl]&\\
&T_0 \ar@{-}[dr]   & & F_0 \ar@{-}[dl]  \\
&& N   &
}$$

\vspace{1mm}\noindent Note that the diagram above can  be interpreted bottom-up as stages of a database with respect  to a sentence $A$. 
In the bottom there is no information about $A$, neither positive nor negative, which corresponds to the semantic value 
\textit{N} assigned to $A$.  
From this stage, there are two alternatives: either positive information $A$ or negative information $A$ (i.e. $\neg A$) 
is obtained, that is, $A$ is assigned, respectively, $T_0$ and $F_0$. Now, in each case, two alternatives are possible: 
either the information that  $A$ ($\neg A$) is reliable is obtained, yielding the value $T$ ($F$), or contradictory 
information is obtained, and so $B$ is assigned to $A$ (and to $\neg A$ as well).   
 


 
\section{Extending a minimal $LET$: the logic \ensuremath{LET_{F}^+}}   \label{sec.letfp}

We have  already mentioned the logic  \ensuremath{LET_{F}^-}, a  minimal logic of evidence and truth that extends \ensuremath{FDE}\ with the classicality operator  
\ensuremath{{\circ}}\  and the  rules $EXP^{\circ}$  and $PEM^{\circ}$.  
The logic  \ensuremath{LET_{F}^+}\  is  the extension of \ensuremath{LET_{F}^-}\  with the axiom $\ensuremath{{\circ}}\con A$ and the rules of propagation of 
classicality for $\lor$, $\land$, and \ensuremath{\lnot}\ taken from Definition~\ref{propag-rules}.  
 It can also be  defined as the $\rightarrow$-free fragment of \ensuremath{LET_{K}^+}. 

  
In this brief section we start by \ensuremath{LET_{F}^-}, which admits a valuation semantics and  a (non-deterministic) sound and complete 
6-valued semantics based on swap-structures.  We then move to \ensuremath{LET_{F}^+}\ which, like \ensuremath{LET_{K}^+}, is semantically characterized by a 6-valued logical matrix, as well as by a class of logical matrices based on twist structures. 



Thus, consider the propositional signature  $\Sigma_1=\{\land,\lor, \neg,\ensuremath{{\circ}}\}$.
A natural deduction system for  \ensuremath{LET_{F}^-}\   
is obtained    by dropping  rules ${\to} I$, ${\to} E$, $\to_{CL}$, $\neg{\to} I$, and $\neg{\to} E$ 
from Definition~\ref{def.ND.letk}. 
A  bivalued semantics  for \ensuremath{LET_{F}^-}\ is obtained by dropping clauses (v3) and (v7) from Definition~\ref{def-val-LETK}.   
 An Nmatrix  ${\mathcal{M}_{\ensuremath{LET_{F}^-}}}$ for \ensuremath{LET_{F}^-}\ is obtained 
 by dropping clause (iii) of Definition~\ref{defNmatLETK}, which produces the 6-valued (non-deterministic)  truth-tables obtained just by dropping  the table for implication of \ensuremath{LET_{K}}\ displayed in Subsection~\ref{tablesLETKP}.
 As expected,  the syntactic consequence ($ \vdash_{\ensuremath{LET_{F}^-}}  $) and the semantic consequence, defined by 
either the bivalued semantics   ($\models_{\ensuremath{LET_{F}^-}}^2$) or by the 6-valued semantics ($ \models_{\mathcal{M}_{\ensuremath{LET_{F}^-}}}  $),  
are equivalent:  
\begin{enumerate}[resume]
\item $\Gamma\vdash_{\ensuremath{LET_{F}^-}} A$ \ if and only if \ $\Gamma\models_{\ensuremath{LET_{F}^-}}^2 A$ \ if and only if \ $\Gamma\models_{\mathcal{M}_{\ensuremath{LET_{F}^-}}} A$. \label{prop.sound.comp.letfm
\end{enumerate} 
\noindent The  proof of  \ref{prop.sound.comp.letfm}  can be easily adapted 
from the proofs  of Theorems \ref{adeq-LETK-bival}, \ref{sound-Nmat-LETK}, and \ref{comp-Nmat-LETK}.   
    The Nmatrix $\mathcal{M}_{\ensuremath{LET_{F}^-}}$, of course, provides a decision procedure for \ensuremath{LET_{F}^-}. 

  \vspace{1mm} 
  
We now turn to the logic \ensuremath{LET_{F}^+}. Recall from Remark~\ref{twist-LETKP}  that  $\mathcal{A}_6$ denotes the 6-valued algebra  underlying the matrix $\mathcal{M}_6$ of \ensuremath{LET_{K}^+}. Let $\mathcal{A}_6^1$ be the 6-valued algebra  underlying the matrix $\mathcal{M}_6^1$ obtained from $\mathcal{M}_6$ by removing the implication operator $\to$. Consider the valuation semantics for \ensuremath{LET_{F}^+}\ obtained from the one for \ensuremath{LET_{K}^+}\ by removing the clauses for implication $\to$. It is easy to see, by adapting the corresponding proofs for \ensuremath{LET_{K}^+}, that
\begin{enumerate}[resume]  
\item $\Gamma\vdash_{\ensuremath{LET_{F}^+}} A$ \ if and only if \ $\Gamma\models_{\ensuremath{LET_{F}^+}}^2 A$ \ if and only if \ $\Gamma\models_{\mathcal{M}_6^1} A$. \label{prop.sound.comp.letfp
\end{enumerate} 
\noindent Generalizing: given a twist structure $\mathcal{T}_{\mathcal{B}}$ for \ensuremath{LET_{K}^+}\ induced by a Boolean algebra  $\mathcal{B}$ (recall Definition~\ref{twist-BA}) let $\mathcal{T}_{\mathcal{B}}^1$ be its implication-less reduct to $\Sigma_1$. Let $\mathcal{M}^1(\mathcal{B})$ be the induced Nmatrix as in the case of \ensuremath{LET_{K}^+}. Clearly,  $\mathcal{T}_{\mathcal{B}_2}^1$ is exactly $\mathcal{A}_6^1$, while $\mathcal{M}^1(\mathcal{B}_2)=\mathcal{M}_6^1$.  Let $Mat(\ensuremath{LET_{F}^+})$ be the class of logical matrices of the form $\mathcal{M}^1(\mathcal{B})$, and let $\models_{Mat(\ensuremath{LET_{F}^+})}$ be the associated consequence relation. Then, 
\begin{enumerate}[resume] 
\item $\Gamma\vdash_{\ensuremath{LET_{F}^+}} A$ \ if and only if \ $\Gamma\models_{Mat(\ensuremath{LET_{F}^+})} A$. \label{prop.sound.comp.swap.letfp
\end{enumerate} 
\noindent 



\subsection{\ensuremath{LET_{F}^+}\ and involutive Stone Algebras} \label{sectISAs}

By convenience, in this subsection we will consider that \ensuremath{LET_{K}^+}\ and \ensuremath{LET_{F}^+}\ are defined over a signature containing the constants $\top$ and $\bot$.
A curious and unexpected relationship between \ensuremath{LET_{F}^+}\ and a variety of algebras known as {\em Involutive Stone Algebras}  (ISAs, for short) can now be established. Involutive Stone algebras are De Morgan algebras with an additional unary operator $\nabla$ satisfying some specific equations. That is, ISAs are algebras defined over the signature $\{\land,\lor,\neg,\nabla, \bot,\top\}$. The variety of ISAs was introduced by R. Cignoli and M. de Galego in~\cite{cig:gal:81} in the context of \L ukasiewicz-Moisil algebras.  In~\cite{cig:gal:83} they prove that the variety of ISAs is generated by $\mathbb{S}_6$, a 6-element ISA  whose $\{\land,\lor,\neg\}$-reduct coincides with the corresponding reduct {\bf L6} of $\mathcal{A}_6$ displayed in Subsection~\ref{SectSix}. In  $\mathbb{S}_6$ the $\nabla$ operator is given by $\nabla(a)=T$ if $a \neq F$, and $\nabla(F)=F$. Observe that, in $\mathcal{A}_6^1$, $\nabla$ can be defined by means of the formula $\nabla A \ensuremath{~\stackrel{\text{{\tiny def }}}{=}~} A \vee  \neg \ensuremath{{\circ}} A$. On the other hand, it is clear that the formula $\ensuremath{{\circ}} A \ensuremath{~\stackrel{\text{{\tiny def }}}{=}~} \neg \nabla A \vee \neg \nabla \neg A$ defines in $\mathbb{S}_6$ the operator $\tilde{\ensuremath{{\circ}}}$. This shows that the 6-valued algebra $\mathbb{S}_6$ is  equivalent in expressive power to the algebra $\mathcal{A}_6^1$ for \ensuremath{LET_{F}^+}.

L. Cant\'u and M. Figallo studied in~\cite{cant:fig:18} the logic preserving degrees of truth of the variety of ISAs, which is defined as follows (taking into account that $\mathbb{S}_6$ generates the variety): $\Gamma \models_{\mathbb{S}_6}^\leq A$ iff either $v(A)=1$, for every valuation $v$ over $\mathbb{S}_6$, or there exist $A_1,\ldots,A_n \in \Gamma$ such that $v(A_1) \sqcap \ldots \sqcap v(A_n) \leq v(A)$, for every valuation $v$ over $\mathbb{S}_6$.   
They  prove in their Theorem~5.5 that the logic {\bf Six}  generated by the 4 matrices over $\mathbb{S}_6$ with set of designated  values $\{\textsf{n},T_0,T\}$,  $\{F_0,\textsf{n},T_0,T\}$, $\{T_0,T\}$ and $\{T\}$ coincides with the logic preserving degrees of truth of the variety of ISAs. On the other hand,  in~\cite{marc:riv:22}, Proposition~4.1, it was shown that  {\bf Six} can be characterized by the logical matrix over $\mathbb{S}_6$ with set of designated  values $\{\textsf{b},T_0,T\}$. As a consequence of these results, we obtain the following:

\begin{proposition} \label{logi-ISA}
Let $\mathbb{I}\mathbb{S}\mathbb{A}$ be the variety of involutive Stone algebras presented in the signature $\{\land,\lor,\neg,\ensuremath{{\circ}}, \bot,\top\}$. Then, \ensuremath{LET_{F}^+}\ coincides with the logic preserving degrees of truth of $\mathbb{I}\mathbb{S}\mathbb{A}$.\footnote{As observed above, \ensuremath{LET_{F}^+}\ was expanded with the  definable constants $\bot$ and $\top$.}
\end{proposition}


\begin{remarks} \label{Six}  \ \\ 
(1) It is worth noting that \ensuremath{LET_{K}^+}\ {\em is not} the expansion of the logic {\bf Six} by adding an implication. Indeed, the logic of \ensuremath{LET_{K}^+}\ is not the logic preserving degrees of truth of  $\mathcal{A}_6$ (the expansion of $\mathbb{S}_6$ with the implication $\tilde{\to}$) given that, for instance, $\neg(A \to B) \vdash_{\ensuremath{LET_{K}^+}} A$, but    $\neg(A \to B) \not\models_{\mathcal{A}_6}^\leq A$, where $\Gamma \models_{\mathcal{A}_6}^\leq A$ iff, either $v(A)=1$, for every valuation $v$ over $\mathcal{A}_6$, or there exist $A_1,\ldots,A_n \in \Gamma$ such that $v(A_1) \sqcap \ldots \sqcap v(A_n) \leq v(A)$, for every valuation $v$ over $\mathcal{A}_6$. In fact, it is enough considering a valuation $v$ such that $v(A)=\textsf{b}$ and $v(B)=\textsf{n}$ (which is perfectly possible when $A$ and $B$ are two propositional variables). In this case, $v(\neg(A \to B))=v(A \to B)=\textsf{b} \,\tilde{\to}\, \textsf{n}=\textsf{n} \not\leq \textsf{b}= v(A)$, hence   $\neg(A \to B) \not\models_{\mathcal{A}_6}^\leq A$.\\[1mm]
(2) The algebrization of \ensuremath{LET_{K}^+}\ obtained  in Section~\ref{sect-BPalg} shows that there is an additional difference with its implication-free fragment \ensuremath{LET_{F}^+}. Indeed, as shown in~\cite[Proposition~4.2]{marc:riv:22},  the logic  {\bf Six} it is not algebraizable, although it is selfextensional. By Proposition~\ref{logi-ISA}, the same holds for \ensuremath{LET_{F}^+}.
Despite these differences, it would be interesting to analyze \ensuremath{LET_{K}^+}\ and \ensuremath{LET_{F}^+}\ with relation to  involutive Stone algebras.
\end{remarks}

 
\input{sn-sample-bib}

\end{document}
 

