% Part: many-valued-logic
% Chapter: syntax-and-semantics
% Section: valuations-sat

\documentclass[../../../include/open-logic-section]{subfiles}

\begin{document}

\olfileid{mvl}{syn}{val}

\olsection{\usetoken{P}{valuation} and Satisfaction}

\begin{defn}[!!^{valuation}s] 
Let $V$ be a set of truth values. A \emph{!!{valuation}} for
$\Lang{L}$ into~$V$ is a
function~$\pAssign{v}$ assigning !!a{element} of~$V$ to the
!!{propositional variable}s of the language, i.e., $\pAssign{v} \colon
\PVar \to V$.
\end{defn}

\begin{defn}\ollabel{defn:pValue}
  Given !!a{valuation}~$\pAssign{v}$ into the set of truth values~$V$ of a
  many-valued logic~$\Log L$, define the evaluation function
  $\pValue{v} \colon \Frm[L] \to V$ inductively by:
  \begin{enumerate}
    \item $\pValue{v}(\Obj p_n) = \pAssign{v}(\Obj p_n)$; 
    \item If $\star$ is a $0$-place connective, then $\pValue{v}(\star)  = \tf{\star}[\Log L]$;
    \item If $\star$ is an $n$-place connective, then 
    \[
      \pValue{v}(\star(!A_1, \dots, !A_n)) = \tf{\star}[\Log L]
      (\pValue{v}(!A_1), \dots, \pValue{v}(!A_n)).
    \]
  \end{enumerate}
\end{defn}

\begin{defn}[Satisfaction]
\ollabel{defn:satisfaction} The !!{formula}~$!A$ is \emph{satisfied}
  by !!a{valuation}~$\pAssign{v}$, $\pSat{v}{!A}[\Log L]$, iff
  $\pValue{v}(!A)[\Log L] \in V^+$, where $V^+$ is the set of
  designated truth values of~$\Log L$. 
  
  We write $\pSat/{v}{!A}[\Log L]$ to mean ``not $\pSat{v}{!A}[\Log
  L]$.'' If $\Gamma$ is a set of !!{formula}s, $\pSat{v}{\Gamma}[\Log
  L]$ iff $\pSat{v}{!A}[\Log L]$ for every~$!A \in \Gamma$.
\end{defn}

\end{document}