Many-valued logics

Sequent Calculus

content/many-valued-logic/sequent-calculus/sequent-calculus.tex

% Part: many-valued-logic% Chapter: three-valued-logics\documentclass[../../../include/open-logic-chapter]{subfiles}\begin{document}\olchapter{mvl}{seq}{Sequent Calculus}\olimport{introduction}\olimport{rules-and-proofs}\olimport{structural-rules}\olimport{propositional-rules}\OLEndChapterHook\end{document}

content/many-valued-logic/sequent-calculus/introduction.tex

% Part: many-valued-logic% Chapter: sequent-calculus% Section: introduction\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{mvl}{seq}{int}\olsection{Introduction}The sequent calculus for classical logic is an efficient and simple!!{derivation} system. If a many-valued logic is defined by a matrix withfinitely many truth values, i.e., $V$ is finite, it is possible toprovide a sequent calculus for it.  The idea for how to do this comesfrom considering the meanings of sequents and the form of inferencerules in the classical case. Now recall that a sequent \begin{align*}    !A_1, \dots, !A_n & \Sequent !B_1, \dots, !B_n\intertext{can be interpreted as the !!{formula}}    (!A_1 \land \cdots \land !A_m) & \lif (!B_1 \lor \cdots \lor!B_n)\end{align*}In other words, !!^a{valuation}~$\pAssign{v}$ \emph{satisfies} asequent $\Gamma \Sequent \Delta$ iff either $\pValue{v}(!A) = \False$for some $!A \in \Gamma$ or $\pValue{v}(!A) = \True$ for some $!A \in\Delta$. On this interpretation, initial sequents $!A \Sequent !A$ arealways satisfied, because either $\pValue v(!A) = \True$ or $\pValue(!A) =\False$.Here are the inference rules for the conditional in~$\Log{LK}$, withside formulas $\Gamma$, $\Delta$ left out:\begin{defish}    \Axiom$ \fCenter !A$    \Axiom$ !B \fCenter $    \RightLabel{\LeftR{\lif}}    \BinaryInf$ !A \lif !B \fCenter $    \DisplayProof    \hfill    \Axiom$ !A \fCenter !B$    \RightLabel{\RightR{\lif}}    \UnaryInf$ \fCenter !A \lif !B $    \DisplayProof\end{defish}If we apply the above semantic interpretation of a sequent, we canread the $\LeftR{\lif}$ rule as saying that if $\pValue v(!A) = \True$and $\pValue v(!B) = \False$, then $\pValue v(!A \lif !B) = \False$.Similarly, the $\RightR{\lif}$ rule says that if either $\pValue v(!A)= \False$ or $\pValue v(!B) = \True$, then $\pValue v(!A \lif !B) =\True$. And in fact, these conditionals are actually biconditionals.In the case of the $\LeftR{\land}$ and $\RightR{\lor}$ rules in theirstandard formulation, the corresponding conditionals would not bebiconditionals. But there are alternative versions of these ruleswhere they are:\begin{defish}    \Axiom$!A, !B, \Gamma \fCenter \Delta$    \RightLabel{\LeftR{\land}}    \UnaryInf$!A \land !B, \Gamma \fCenter \Delta$    \DisplayProof    \hfill    \Axiom$ \Gamma \fCenter \Delta, !A, !B$    \RightLabel{\RightR{\lor}}    \UnaryInf$ \Gamma \fCenter \Delta, !A \lor !B$    \DisplayProof\end{defish}This basic idea, applied to an $n$-valued logic, then results in asequent calculus with $n$ instead of two places, one for each truthvalue. For a three-valued logic with $V = \{\False, \Undef, \True\}$,a sequent is an expression $\Gamma \mid \Pi \mid \Delta$. It issatisfied in !!a{valuation}~$\pAssign v$ iff either $\pValue{v}(!A) =\False$ for some $!A \in \Gamma$ or $\pValue{v}(!A) = \True$ for some$!A \in \Delta$ or $\pValue{v}(!A) = \Undef$ for some $!A \in \Pi$.Consequently, initial sequents $!A \mid !A \mid !A$ are alwayssatisfied.\end{document}

content/many-valued-logic/sequent-calculus/rules-and-proofs.tex

% Part: first-order-logic% Chapter: sequent-calculus% Section: rules-and-proofs\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{mvl}{seq}{rul}\olsection{Rules and \usetoken{P}{derivation}}For the following, let $\Gamma, \Delta, \Pi, \Lambda$ represent finitesequences of !!{sentence}s.\begin{defn}[Sequent]An \emph{$n$-sided sequent} is an expression of the form\[\Gamma_1 \nSequent \dots \nSequent \Gamma_n\]where each $\Gamma_1$ is a finite (possibly empty) sequences of!!{sentence}s of the language~$\Lang L$.\end{defn}\begin{defn}[Initial Sequent]An \emph{$n$-sided initial sequent} is an $n$-sided sequent of theform $!A \nSequent \dots \nSequent !A$ for any !!{sentence} $!A$ inthe language.If the language contains a $0$-place connective~$\star$, i.e., apropositional constant, then we also take the sequent $\dots \nSequent\star \nSequent \dots$ where $\star$ appears in the space for the truthvalue associated with~$\tf{\star} \in V$, and is empty otherwise. \end{defn}For each connective of an $n$-valued logic~$\Log{L}$, there is alogical rule for each truth value that this connective can takein~$\Log{L}$. !!^{derivation}s in an $n$-sided sequent calculusfor~$\Log{L}$ are trees of sequents, where the topmost sequents areinitial sequents, and if a sequent stands below one or more othersequents, it must follow correctly by a rule of inference for theconnectives of~$\Log{L}$.\begin{defn}[Theorems]!!^a{sentence}~$!A$ is a \emph{theorem} of an $n$-valuedlogic~$\Log{L}$ if there is !!a{derivation}of the $n$-sequent containing $!A$ in each position corresponding to adesignated truth value of~$\Log{L}$.  We write $\Proves[\Log{L}]!A$ if $!A$ is a theorem and $\Proves/[\Log{L}] !A$ if it is not.\end{defn}\begin{defn}[!!^{derivability}]!!^a{sentence}~$!A$ is \emph{!!{derivable} from} a set of!!{sentence}s~$\Gamma$ in an $n$-valued logic~$\Log{L}$, $\Gamma\Proves[\Log{L}] !A$, iff there is a finite subset~$\Gamma_0 \subseteq\Gamma$ and a sequence $\Gamma_0'$ of the !!{sentence}s in~$\Gamma_0$such that the following sequent has  !!a{derivation}:\[ \Lambda_1 \nSequent \dots \nSequent \Lambda_n \] where $\Lambda_i$is $!A$ if position $i$ corresponds to a designated truth value, and$\Gamma_0'$otherwise. If $!A$ is not !!{derivable} from $\Gamma$ wewrite $\Gamma \Proves/ !A$.\end{defn}For instance, $3$-valued \L ukasiewicz logic has a $3$-sided sequentcalculus. In a $3$-sided sequent $\Gamma \nSequent \Pi \nSequent\Delta$, $\Gamma$ corresponds to~$\False$, $\Delta$ to~$\True$, and$\Pi$ to~$\Undef$.  Axioms are $!A \nSequent !A \nSequent !A$. Sinceonly $\True$ is designated, $\Gamma \Proves[\LogLuk[3]] !A$ iff thesequent $\Gamma \nSequent \Gamma \nSequent !A$ has !!a{derivation}.(If $\Undef$ were also designated, we would need !!a{derivation} of$\Gamma \nSequent !A \nSequent !A$.)\end{document}

content/many-valued-logic/sequent-calculus/structural-rules.tex

% Part: many-valued-logics% Chapter: sequent-calculus% Section: structural-rules\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{mvl}{seq}{str}\olsection{Structural Rules}The structural rules for $n$-sided sequent calculus operate as in theclassical case, except for each position~$i$.\begin{defish}\begin{center}\AxiomC{$ \Gamma_1 \nSequent \dots \nSequent \phantom{!A,}\Gamma_i \nSequent \dots \nSequent \Gamma_n $}\RightLabel{$\iR{\Weakening}{i}$}\UnaryInfC{$\Gamma_1 \nSequent \dots \nSequent !A, \Gamma_i \nSequent \dots \nSequent \Gamma_n$}\DisplayProof\\[2ex]\AxiomC{$ \Gamma_1 \nSequent \dots \nSequent !A, !A, \Gamma_i \nSequent \dots \nSequent \Gamma_n $}\RightLabel{$\iR{\Contraction}{i}$}\UnaryInfC{$\Gamma_1 \nSequent \dots \nSequent \phantom{!A,}!A, \Gamma_i \nSequent\dots \nSequent \Gamma_n$}\DisplayProof\\[2ex]\AxiomC{$ \Gamma_1 \nSequent \dots \nSequent \Gamma_i, !A, !B, \Gamma_i' \nSequent \dots \nSequent \Gamma_n $}\RightLabel{$\iR{\Exchange}{i}$}\UnaryInfC{$\Gamma_1 \nSequent \dots \nSequent \Gamma_i, !B, !A, \Gamma_i' \nSequent \dots\nSequent \Gamma_n$}\DisplayProof\end{center}\end{defish}A series of weakening, contraction, and exchange inferences will oftenbe indicated by double inference lines.The \Cut{} rule comes in several forms, one for every combination ofdistinct positions in the sequent $i \neq j$:\begin{defish}\[\AxiomC{$ \Gamma_1 \nSequent \dots \nSequent !A, \Gamma_i \nSequent \dots \nSequent \Gamma_n $}\AxiomC{$ \Delta_1 \nSequent \dots \nSequent !A, \Delta_j \nSequent \dots \nSequent \Delta_n $}\RightLabel{$\iR{\Cut}{i,j}$}\BinaryInfC{$\Gamma_1,\Delta_1 \nSequent \dots \nSequent \Gamma_n, \Delta_n$}\DisplayProof\]\end{defish}\end{document}

content/many-valued-logic/sequent-calculus/propositional-rules.tex

% Part: first-order-logic% Chapter: sequent-calculus% Section: propositional-rules\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{mvl}{seq}{prl}\olsection{Propositional Rules for Selected Logics}The inference rules for a connective in an $n$-sided sequent calculusonly depend on the characteristic truth function for the connective.Thus, if some connective is defined by the same truth function indifferent logics, these $n$-sided sequent rules for the connective arethe same in those logics.\subsection{Rules for $\lnot$}The following rules for $\lnot$ apply to \L ukasiewicz and Kleenelogics, and their variants.\begin{defish}  \begin{center}\AxiomC{$ \Gamma \nSequent \Pi \nSequent \Delta, !A $}\RightLabel{\iR{\lnot}{\False}}\UnaryInfC{$ \lnot !A, \Gamma \nSequent \Pi \nSequent \Delta$}\DisplayProof\\[2ex]\AxiomC{$ \Gamma \nSequent !A, \Pi \nSequent \Delta $}\RightLabel{\iR{\lnot}{\Undef}}\UnaryInfC{$\Gamma \nSequent \lnot !A, \Pi \nSequent \Delta$}\DisplayProof\\[2ex]\AxiomC{$!A, \Gamma \nSequent \Pi \nSequent \Delta$}\RightLabel{\iR{\lnot}{\True}}\UnaryInfC{$\Gamma \nSequent \Pi \nSequent \Delta,  \lnot !A$}\DisplayProof  \end{center}\end{defish}The following rules for $\lnot$ apply to G\"odel logic.\begin{defish}\AxiomC{$ \Gamma \nSequent !A, \Pi \nSequent \Delta, !A $}\RightLabel{\iR{\lnot}{\False}[\LogGod]}\UnaryInfC{$ \lnot !A, \Gamma \nSequent \Pi \nSequent \Delta$}\DisplayProof\hfill\AxiomC{$!A, \Gamma \nSequent \Pi \nSequent \Delta$}\RightLabel{\iR{\lnot}{\True}[\LogGod]}\UnaryInfC{$\Gamma \nSequent \Pi \nSequent \Delta,  \lnot !A$}\DisplayProof\hfill\end{defish}(In G\"odel logic, $\lnot !A$ can never take the value~$\Undef$, sothere is no rule for the middle position.)\subsection{Rules for $\land$}These are the rules for $\land$ in \L ukasiewicz, strong Kleene, andG\"odel logic.\begin{defish}\begin{center}  \AxiomC{$!A, !B, \Gamma \nSequent \Pi \nSequent \Delta$}  \RightLabel{$\iR{\land}{\False}$}  \UnaryInfC{$!A \land !B, \Gamma \nSequent \Pi \nSequent \Delta$}  \DisplayProof\\[2ex]  \AxiomC{$\Gamma \nSequent !A, \Pi \nSequent !A, \Delta$}  \AxiomC{$\Gamma \nSequent !B, \Pi \nSequent !B, \Delta$}  \AxiomC{$\Gamma \nSequent !A, !B, \Pi \nSequent \Delta$}  \RightLabel{$\iR\land\Undef$}  \TrinaryInfC{$\Gamma \nSequent !A \land !B, \Pi \nSequent \Delta$}  \DisplayProof  \\[2ex]    \AxiomC{$\Gamma \nSequent \Pi \nSequent \Delta, !A$}  \AxiomC{$\Gamma \nSequent \Pi \nSequent \Delta, !B$}  \RightLabel{$\iR\land\True$}  \BinaryInfC{$\Gamma \nSequent \Pi \nSequent \Delta, !A \land !B$}  \DisplayProof\end{center}\end{defish}\subsection{Rules for $\lor$}These are the rules for $\lor$ in \L ukasiewicz, strong Kleene, andG\"odel logic.\begin{defish}\begin{center} \AxiomC{$!A, \Gamma \nSequent \Pi \nSequent \Delta$}  \AxiomC{$!B, \Gamma \nSequent \Pi \nSequent \Delta$}  \RightLabel{$\iR\lor\False$}  \BinaryInfC{$!A \lor !B, \Gamma \nSequent \Pi \nSequent \Delta$}  \DisplayProof\\[2ex]  \AxiomC{$!A, \Gamma \nSequent !A, \Pi \nSequent \Delta$}  \AxiomC{$!B, \Gamma \nSequent !B, \Pi \nSequent \Delta$}  \AxiomC{$\Gamma \nSequent !A, !B, \Pi \nSequent \Delta$}  \RightLabel{$\iR\lor\Undef$}  \TrinaryInfC{$\Gamma \nSequent !A \lor !B, \Pi \nSequent \Delta$}  \DisplayProof  \\[2ex]    \AxiomC{$\Gamma \nSequent \Pi \nSequent \Delta, !A, !B$}  \RightLabel{$\iR\lor\True$}  \UnaryInfC{$\Gamma \nSequent \Pi \nSequent \Delta, !A \lor !B$}  \DisplayProof\end{center}\end{defish}\subsection{Rules for $\lif$}These are the rules for $\lif$ in \L ukasiewicz logic.\begin{defish}\begin{center}  \AxiomC{$\Gamma \nSequent \Pi \nSequent \Delta, !A$}  \AxiomC{$!B, \Gamma \nSequent \Pi \nSequent \Delta$}  \RightLabel{$\iR\lif\False[\LogLuk[3]]$}  \BinaryInfC{$!A \lif !B, \Gamma \nSequent \Pi \nSequent \Delta$}  \DisplayProof  \\[2ex]  \AxiomC{$\Gamma \nSequent !A, !B, \Pi \nSequent \Delta$}  \AxiomC{$!B, \Gamma \nSequent \Pi \nSequent \Delta, !A$}  \RightLabel{$\iR\lif\Undef[\LogLuk[3]]$}  \BinaryInfC{$\Gamma \nSequent !A \lif !B, \Pi \nSequent \Delta$}  \DisplayProof\\[2ex]  \AxiomC{$!A, \Gamma \nSequent !B, \Pi \nSequent \Delta, !B$}  \AxiomC{$!A, \Gamma \nSequent !A, \Pi \nSequent \Delta, !B$}  \RightLabel{$\iR{\lif}{\True}[\LogLuk[3]]$}  \BinaryInfC{$\Gamma \nSequent \Pi \nSequent \Delta, !A \lif !B$}  \DisplayProof\end{center}\end{defish}These are the rules for $\lif$ in strong Kleene logic.\begin{defish}\begin{center}  \AxiomC{$\Gamma \nSequent \Pi \nSequent \Delta, !A$}  \AxiomC{$!B, \Gamma \nSequent \Pi \nSequent \Delta$}  \RightLabel{$\iR\lif\False[\LogKs]$}  \BinaryInfC{$!A \lif !B, \Gamma \nSequent \Pi \nSequent \Delta$}  \DisplayProof  \\[2ex]  \AxiomC{$!B, \Gamma \nSequent !B, \Pi \nSequent \Delta$}  \AxiomC{$\Gamma \nSequent !A, !B, \Pi \nSequent \Delta$}  \AxiomC{$\Gamma \nSequent !A, \Pi \nSequent \Delta, !A$}  \RightLabel{$\iR\lif\Undef[\LogKs]$}  \TrinaryInfC{$\Gamma \nSequent !A \lif !B, \Pi \nSequent \Delta$}  \DisplayProof\\[2ex]  \AxiomC{$!A, \Gamma \nSequent \Pi \nSequent \Delta, !B$}  \RightLabel{$\iR{\lif}{\True}[\LogKs]$}  \UnaryInfC{$\Gamma \nSequent \Pi \nSequent \Delta, !A \lif !B$}  \DisplayProof\end{center}\end{defish}These are the rules for $\lif$ in G\"odel logic.\begin{defish}\begin{center}  \AxiomC{$\Gamma \nSequent !A, \Pi \nSequent \Delta, !A$}  \AxiomC{$!B, \Gamma \nSequent \Pi \nSequent \Delta$}  \RightLabel{$\iR\lif\False[\LogGod[3]]$}  \BinaryInfC{$!A \lif !B, \Gamma \nSequent \Pi \nSequent \Delta$}  \DisplayProof  \\[2ex]  \AxiomC{$\Gamma \nSequent !B, \Pi \nSequent \Delta$}  \AxiomC{$\Gamma \nSequent \Pi \nSequent \Delta, !A$}  \RightLabel{$\iR\lif\Undef[\LogGod[3]]$}  \BinaryInfC{$\Gamma \nSequent !A \lif !B, \Pi \nSequent \Delta$}  \DisplayProof\\[2ex]  \AxiomC{$!A, \Gamma \nSequent !B, \Pi \nSequent \Delta, !B$}  \AxiomC{$!A, \Gamma \nSequent !A, \Pi \nSequent \Delta, !B$}  \RightLabel{$\iR{\lif}{\True}[\LogGod[3]]$}  \BinaryInfC{$\Gamma \nSequent \Pi \nSequent \Delta, !A \lif !B$}  \DisplayProof\end{center}\end{defish}\begin{sidewaysfigure}  \begin{center}    \AxiomC{$A \nSequent A \nSequent A$}  \RightLabel{\iR \Weakening \True}  \UnaryInfC{$A \nSequent A \nSequent B, A$}  \RightLabel{\iR \Weakening \Undef}  \UnaryInfC{$A \nSequent B, A \nSequent B, A$}  \RightLabel{\iR \Weakening \Undef}  \UnaryInfC{$A \nSequent A, B, A \nSequent B, A$}  \AxiomC{$A \nSequent A \nSequent A$}  \RightLabel{\iR \Weakening \True}  \UnaryInfC{$A \nSequent A \nSequent A, A$}  \RightLabel{\iR \Weakening \True}  \UnaryInfC{$A \nSequent A \nSequent B, A, A$}  \RightLabel{\iR \Weakening \False}  \UnaryInfC{$B, A \nSequent A \nSequent B, A, A$}  \RightLabel{$\iR\lif\Undef$}  \BinaryInfC{$A \nSequent A \lif B, A \nSequent B, A$}  \AxiomC{$B \nSequent B \nSequent B$}  \RightLabel{\iR \Weakening \Undef}  \UnaryInfC{$B \nSequent A, B \nSequent B$}  \RightLabel{\iR \Exchange \Undef}  \UnaryInfC{$B \nSequent B, A \nSequent B$}  \RightLabel{\iR \Weakening \Undef}  \UnaryInfC{$B \nSequent A, B, A \nSequent B$}  \RightLabel{\iR \Weakening \False}  \UnaryInfC{$A, B \nSequent A, B, A \nSequent B$}  \RightLabel{\iR \Exchange \False}  \UnaryInfC{$B, A \nSequent A, B, A \nSequent B$}  \AxiomC{$A \nSequent A \nSequent A$}  \RightLabel{\iR \Weakening \True}  \UnaryInfC{$A \nSequent A \nSequent B, A$}  \RightLabel{\iR \Weakening \False}  \UnaryInfC{$B, A \nSequent A \nSequent B, A$}  \RightLabel{\iR \Weakening \False}  \UnaryInfC{$B, B, A \nSequent A \nSequent B, A$}  \RightLabel{$\iR\lif\Undef$}  \BinaryInfC{$B, A \nSequent A \lif B, A \nSequent B$}  \RightLabel{$\iR\lif\False$}  \BinaryInfC{$A \lif B, A \nSequent A \lif B, A \nSequent B$}  \DisplayProof  \end{center}  \caption{Example !!{derivation} in~$\LogLuk[3]$}\end{sidewaysfigure}\end{document}