\documentclass{llncs}

\usepackage[utf8]{inputenc}
\usepackage[english]{babel}
\usepackage{amssymb}
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{graphicx}
\usepackage{rotating}
\usepackage{multirow}
\usepackage{multicol}
\usepackage{hyperref}
\usepackage{subcaption}
\usepackage{qtree}\usepackage{newfloat}\DeclareFloatingEnvironment[fileext=lod]{diagram}
%
\newtheorem{mytheorem}{Proposition} 
%
\begin{document}
\title{Tableaux for Murphree's Numerical Term Logic}
\author{J.-Mart\'in Castro-Manzano}
\institute{Faculty of Philosophy, UPAEP University\\21 sur 1103, Puebla, Mexico\\
\email{josemartin.castro@upaep.mx}}

\maketitle

\begin{abstract}
Murphree’s Numerical Term Logic is a logic capable of representing and performing inference with numerical quantifiers by modifying Sommers Term Functor Logic: in this contribution we offer a tableaux method for it.
\end{abstract}
\keywords{Semantic trees, term logic, numerical term logic.}

\section{Introduction}
In other places we have developed tableaux for Sommers' Term Functor Logic \cite{sommers:1982,englebretsen:1996,sommers:2000}, Intermediate Term Functor Logic \textit{à la} Thompson~\cite{thompson:1982}, and Englebretsen's Modal Term Logic~\cite{englebretsen:1988}. In this contribution we continue our exploration into the realm of term logics and, by using Murphree's Numerical Term Logic~\cite{murphree:1998}, we present tableaux for a family of term logics comprising Term Functor Logic, Intermediate Term Functor Logic, and Numerical Term Logic. Hence, for a more detailed exposition of Term Functor Logic and its tableaux, we refer the reader to our previous work~\cite{castro:2018}. Meanwhile, in order to achieve our present goal, we first provide a summary of some preliminary concepts (syllogistic, term functor logic, and term functor logic tableaux), then we explain the basics of Murphree's logic (namely, its syntax and rules) and, finally, we develop tableaux for it (including some metalogical results).
 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Preliminaries}
\subsection{Syllogistic}
\emph{Syllogistic} is a term logic that has its origins in Aristotle's \emph{Prior Analytics}~\cite{aristotle:1989} and deals with inference between categorical propositions. A \emph{categorical proposition} is a proposition composed by two terms, a quantity, and a quality. The subject and the predicate of a proposition are called \emph{terms}: the term-schema $\mathsf{S}$ denotes the subject term of the proposition and the term-schema $\mathsf{P}$ denotes the predicate. The \emph{quantity} may be either universal (\emph{All}) or particular (\emph{Some}) and the \emph{quality} may be either affirmative (\emph{is}) or negative (\emph{is not}). These categorical propositions have a \emph{type} denoted by a label (either $\mathsf{a}$ (universal affirmative, $\mathsf{SaP}$), $\mathsf{e}$ (universal negative, $\mathsf{SeP}$), $\mathsf{i}$ (particular affirmative, $\mathsf{SiP}$), or $\mathsf{o}$ (particular negative, $\mathsf{SoP}$)) that allows us to  determine a \emph{mood}, that is, a sequence of three categorical propositions ordered in such a way that two propositions are premises and the last one is a conclusion. A \textit{categorical syllogism}, then, is a mood with three terms one of which appears in both premises but not in the conclusion. This particular term, usually denoted with the term-schema $\mathsf{M}$, works as a link between the remaining terms and is known as the middle term. According to the position of this middle term, four \emph{figures} can be set up in order to encode the valid syllogistic moods (Table~\ref{tab:a1}).\footnote{For sake of brevity, but without loss of generality, here we omit the syllogisms that require existential import.} 

\begin{table}[!htbp]\centering
	\begin{tabular}{cccc}
	\hline\noalign{\smallskip}
	First &  Second & Third  & Fourth \\
	figure & figure & figure & Figure\\
	\noalign{\smallskip}\hline\noalign{\smallskip}
	$\mathsf{aaa}$ & $\mathsf{eae}$ & $\mathsf{iai}$ & $\mathsf{aee}$\\
	$\mathsf{eae}$ & $\mathsf{aee}$ & $\mathsf{aii}$ & $\mathsf{iai}$\\
	$\mathsf{aii}$ & $\mathsf{eio}$ & $\mathsf{oao}$ & $\mathsf{eio}$\\ 
	$\mathsf{eio}$ & $\mathsf{aoo}$ & $\mathsf{eio}$ &    \\  
	\noalign{\smallskip}\hline
	\end{tabular} \caption{Valid syllogistic moods}\label{tab:a1}
\end{table}

\subsection{Term Functor Logic}
\textit{Term Functor Logic} (TFL)~\cite{sommers:1967,sommers:1982,sommers:2000,englebretsen:1987,englebretsen:1996,englebretsen:2011} is basically a plus-minus algebra that employs terms rather than first order language elements such as individual variables or quantifiers (cf.~\cite{quine:1971,noah:1980,kuhn:1983,sommers:1982,sommers:2005,moss:2015}). According to this algebra, the four categorical propositions can be represented by the following syntax~\cite{englebretsen:1996}:

\begin{itemize}
	\item[a.] $\mathsf{SaP := -S+P}$
	\item[b.] $\mathsf{SeP := -S-P}$
	\item[c.] $\mathsf{SiP := +S+P}$
	\item[d.] $\mathsf{SoP := +S-P}$
\end{itemize}

Given this representation, this plus-minus algebra provides a simple rule for syllogistic inference: a conclusion follows validly from a set of premises if and only if \emph{i)} the sum of the premises is algebraically equal to the conclusion and \emph{ii)} the number of conclusions with particular quantity (viz., zero or one) is the same as the number of premises with particular quantity~\cite[p.167]{englebretsen:1996}. Thus, for instance, if we consider a valid syllogism, say the mood $\mathsf{aaa}$ from the first figure (i.e. $\mathsf{aaa}$-1), we can see how the application of this method produces the right conclusion (Table~\ref{tab:2}). 

\begin{table}[!htbp]\centering
	\begin{tabular}{lll}
	\hline\noalign{\smallskip}
	 & Proposition & TFL \\
	\noalign{\smallskip}\hline\noalign{\smallskip}
	1. & All dogs are animals. & $\mathsf{-D+A}$\\
	2. & All German Shepherds are dogs. & $\mathsf{-G+D}$\\
	$\vdash$ & All German Shepherds are animals. & $\mathsf{-G+A}$\\ 
	\noalign{\smallskip}\hline
	\end{tabular} \caption{A valid syllogism: $\mathsf{aaa}$-1}\label{tab:2}
\end{table} 

\sloppy In the previous example we can clearly see how the method works: \emph{i)} if we add up the premises we obtain the algebraic expression $\mathsf{(­-D+A)+(-G+D)=-­D+A-G+D}$ $\mathsf{=-­G+A}$, so that the sum of the premises is algebraically equal to the conclusion and the conclusion is ­$\mathsf{-G+A}$, rather than $\mathsf{+A-­G}$, because \emph{ii)} the number of conclusions with particular quantity (zero in this case) is the same as the number of premises with particular quantity (zero in this case).

\subsection{TFL tableaux}
As in \cite{castro:2018}, we say a \emph{tableau} is an acyclic connected graph determined by nodes and vertices~\cite{handbook:1999,priest:2008}. The node at the top is called \emph{root}. The nodes at the bottom are called \emph{tips}. Any path from the root down a series of vertices is a \emph{branch}. To test an inference for validity we construct a tableau which begins with a single branch at whose nodes occur the premises and the rejection of the conclusion: this is the \emph{initial list}. We then apply the rules that allow us to extend the initial list (Diagram~\ref{diag:1}).

\begin{diagram}[!htbp]
\begin{multicols}{2}
\Tree [.$\mathsf{-A\pm B}$ [.$\mathsf{-A}^i$ ] $\mathsf{\pm B}^i$ ]

\Tree [.$\mathsf{+A\pm B}$ [.$\mathsf{+A}^i$ $\mathsf{\pm B}^i$ ]]
\end{multicols}
\caption{TFL tableaux rules}\label{diag:1}
\end{diagram}

In Diagram~\ref{diag:1}, from left to right, the first rule is the rule for $\mathsf{a}$ ($\mathsf{e}$)  propositions, and the second rule is the rule for $\mathsf{i}$ ($\mathsf{o}$) propositions. Notice that, after applying a rule, we introduce some index $i\in \lbrace 1, 2, 3, \ldots \rbrace$. For propositions $\mathsf{a}$ and $\mathsf{e}$, the index may be any number; for propositions $\mathsf{i}$ and $\mathsf{o}$, the index has to be a new number if they do not already have an index. Also, following TFL tenets, we assume the followings rules of rejection: $-(\pm\mathsf{A}) = \mp\mathsf{A}$, $-(\pm \mathsf{A}\pm \mathsf{B})=\mp \mathsf{A}\mp \mathsf{B}$, and $\mathsf{-(--A--A)=+(-A)+(-A)}$.

As usual, a tableau is \emph{complete} if and only if every rule that can be applied has been applied. A branch is \emph{closed} if and only if there are terms of the form $\pm \mathsf{A}^i$ and $\mp \mathsf{A}^i$ on two of its nodes; otherwise it is \emph{open}. A closed branch is indicated by writing a $\bot$ at the end of it; an open branch is indicated by writing $\infty$. A tableau is \emph{closed} if and only if every branch is closed; otherwise it is \emph{open}. So, again as usual, $\mathsf{A}$ is a logical consequence of the set of terms $\Gamma$ (i.e. $\Gamma\vdash\mathsf{A}$) if and only if there is a complete closed tableau whose initial list includes the terms of $\Gamma$ and the rejection of $\mathsf{A}$ (i.e. $\Gamma\cup\lbrace\mathsf{-A}\rbrace\vdash\bot$). Accordingly, up next we provide some examples for basic syllogistic (Diagram~\ref{diag:2}).

\begin{diagram}[!htbp]
\begin{multicols}{2}
\Tree[.{$\mathsf{-M+P}$\\$\mathsf{-S+M}$\\$\vdash\mathsf{-S+P}$\\$\mathsf{-(-S+P)}$\\$\mathsf{+S-P}$} [.{$\mathsf{+S}^1$} [.{$\mathsf{-P}^1$} {$\mathsf{-S}^1$\\$\bot$}  [.{$\mathsf{+M}^1$} {$\mathsf{-M}^1$\\$\bot$} {$\mathsf{+P}^1$\\$\bot$} !{\qbalance} ]
!\qsetw{3cm} ] ] ]

\Tree[.{$\mathsf{-M-P}$\\$\mathsf{-S+M}$\\$\vdash\mathsf{-S-P}$\\$\mathsf{-(-S-P)}$\\$\mathsf{+S+P}$} [.{$\mathsf{+S}^1$} [.{$\mathsf{+P}^1$} {$\mathsf{-S}^1$\\$\bot$}  [.{$\mathsf{+M}^1$} {$\mathsf{-M}^1$\\$\bot$} {$\mathsf{-P}^1$\\$\bot$} !{\qbalance} ]
!\qsetw{3cm} ] ] ]

\Tree[.{$\mathsf{-M+P}$\\$\mathsf{+S+M}$\\$\vdash\mathsf{+S+P}$\\$\mathsf{-(+S+P)}$\\$\mathsf{-S-P}$} [.{$\mathsf{+S}^1$} [.{$\mathsf{+M}^1$} {$\mathsf{-M}^1$\\$\bot$}  [.{$\mathsf{+P}^1$} {$\mathsf{-S}^1$\\$\bot$} {$\mathsf{-P}^1$\\$\bot$} !{\qbalance} ]
!\qsetw{3cm} ] ] ]

\Tree[.{$\mathsf{-M-P}$\\$\mathsf{+S+M}$\\$\vdash\mathsf{+S-P}$\\$\mathsf{-(+S-P)}$\\$\mathsf{-S+P}$} [.{$\mathsf{+S}^1$} [.{$\mathsf{+M}^1$} {$\mathsf{-M}^1$\\$\bot$}  [.{$\mathsf{-P}^1$} {$\mathsf{-S}^1$\\$\bot$} {$\mathsf{+P}^1$\\$\bot$} !{\qbalance} ]
!\qsetw{3cm} ] ] ]
\end{multicols}
\caption{Moods $\mathsf{aaa}$-1, $\mathsf{eae}$-1, $\mathsf{aii}$-1, and $\mathsf{eio}$-1}\label{diag:2}
\end{diagram}

\section{Murphree's Numerical Term Logic}\label{sec:2}
In Szabolcsi's view~\cite[p.3]{szabolcsi:2008}, quantification within first order logic systems is ``extremist'' in the sense that it is limited to represent two extremes: either everything or something.\footnote{This is not completely true because, for example, we have the proposals developed by~\cite{mostowski:1957,westerstahl:1989} (however, since these are not part of first order logic  \textit{prima facie} and they are developed by and for first order languages, we omit their treatment in this contribution) and, in all fairness, we can charge TFL with the same offense.} Indeed, it is usual to find logical treatments that assume that intermediate or subjective quantifiers~\cite[p.26ff]{szabolcsi:2008} such as ``many'', ``most'', or ``few'' (cf.~\cite{peterson:1979,thompson:1982}) have to be treated as simple cases of existential quantifiers, and numerical or objetive quantifiers usually suffer the same fate. However, such a treatment is far from being justified. There are several reasons to support this claim, but in the interest of time, consider that reasoning in natural language includes more quantifiers than the usual ``all'' or ``some''. For instance, regard that both ``most'' and ``some'' are particular (i.e. non-universal) quantifiers, but they do not express the same meaning: the former implies the latter, but the converse is false; and the same occurs when reasoning with numerical quantifiers. Given this situation, Murphree~\cite{murphree:1998}, and Szabolcsi~\cite{szabolcsi:2008} developed numerical extensions of Sommers' Term Functor Logic: in this work, however, we focus only on Murphree's~\cite{murphree:1998}.

Murphree's Numerical Term Logic (NTL) is a term logic capable of representing and performing inference with numerical quantifiers by modifying TFL's syntax and rule of inference. Thus, NTL offers the following syntax for numerically quantified propositions:

\begin{itemize}
	\item[e.] All but $n$ $\mathsf{S}$ are $\mathsf{P}$ $\mathsf{:= -_nS+P}$
	\item[f.] At most $n$ $\mathsf{S}$ are $\mathsf{P}$ $\mathsf{:= -_nS-P}$
	\item[g.] At least $n$ $\mathsf{S}$ are $\mathsf{P}$ $\mathsf{:= +_nS+P}$
	\item[h.] At least $n$ $\mathsf{S}$ are not $\mathsf{P}$ $\mathsf{:= +_nS-P}$
\end{itemize}

To better explain this representation, consider the next examples:

\begin{itemize}
	\item[1.] At least 15 Americans are republicans $\mathsf{:= +_{15}A+R}$
	\item[2.] All but 120 students understand logic $\mathsf{:= -_{120}S+U}$
	\item[3.] At most 150,000 Europeans are male $\mathsf{:= -_{150,000}E-A}$
	\item[4.] There are at least 33 mathematicians $\mathsf{:= +_{33}M+M}$
	\item[5.] At least 66 logicians are not democrats $\mathsf{:= +_{66}L-D}$
\end{itemize}

Now, at this point it is important to notice that when $n=0$ ($n=1$), the traditional universal (particular) categorical propositions are included within NTL:

\begin{itemize}
	\item[6.] All $\mathsf{S}$ is $\mathsf{P}$ = All but 0 $\mathsf{S}$ are $\mathsf{P}$ $\mathsf{:= -_0S+P}$
	\item[7.] No $\mathsf{S}$ is $\mathsf{P}$ = At most 0 $\mathsf{S}$ are $\mathsf{P}$ $\mathsf{:= -_0S-P}$
	\item[8.] Some $\mathsf{S}$ are $\mathsf{P}$ = At least 1 $\mathsf{S}$ is $\mathsf{P}$ $\mathsf{:= +_1S+P}$
	\item[9.] Some $\mathsf{S}$ are not $\mathsf{P}$ = At least 1 $\mathsf{S}$ is not $\mathsf{P}$ $\mathsf{:= +_1S-P}$
\end{itemize}

Also, by adapting some ideas by Szabolcsi, in NTL we can represent exact (10), fractionary (12), and subjective (13) quantifiers. This last example shows in what sense the intermediate propositions of Intermediate Term Functor Logic (TFL$^+$) are included within NTL:

\begin{itemize}
	\item[10.] Exactly $n$ $\mathsf{S}$ are $\mathsf{P}$ $\mathsf{:= +(+_{n-1}S+P)+(-_nS-P)}$
	\item[11.] At most $r/q$ of $\mathsf{S}$ are $\mathsf{P}$ $\mathsf{:= -_{r/q}S-P}$
	\item[12.] Many $\mathsf{S}$ are $\mathsf{P}$ $\mathsf{:= +_mS+P}$
\end{itemize}

Given these syntactical tweaks, NTL modifies TFL's rule of inference as follows: a conclusion follows validly from a set of premises if and only if $i)$ the sum of the premises is algebraically equal to the conclusion, $ii)$ the number of conclusions with particular quantity (viz., zero or one) is the same as the number of premises with particular quantity, and $iii)$ either $(a)$ the value of a universal conclusion is equal to the sum of the values of the universal premises, or $(b)$ the value of a particular conclusion is equal to the difference of the universal premise minus the particular.\footnote{This last condition is different from Szabolcsi's, who considers that the value of the premises need be equal or greater than the value of the conclusion (cf.~\cite[p.45]{szabolcsi:2008}.} Hence, TFL and TFL$^+$ are sublogics of NTL. To exemplify NTL, let us consider some valid inferences (Tables~\ref{tab:8}-\ref{tab:11}).

\begin{table}[!htbp]\centering
	\begin{tabular}{lll}
	\hline\noalign{\smallskip}
	 & Proposition & NTL \\
	\noalign{\smallskip}\hline\noalign{\smallskip}
	1. & All but 6 philosophers are logical. & $\mathsf{-_6P+L}$\\
	2. & All but 20 smart people are philosophers. & $\mathsf{-_{20}S+P}$\\
	$\vdash$ & All but 26 smart people are logical. & $\mathsf{-_{26}S+L}$\\ 
	\noalign{\smallskip}\hline
	\end{tabular} \caption{A valid numerical syllogism (adapted from~\cite{murphree:1998})}\label{tab:8}      
\end{table} 

Before we move on, and in order to reach our goal, we need to make a little syntax modification that will come in handy in due time: we add the predicate term of a proposition an arbitrary natural number $\mathsf{e}>n$ for any other natural $n$. This results in the following syntax for NTL:

\begin{itemize}
	\item[e'.] All but $n$ $\mathsf{S}$ are $\mathsf{P}$ $\mathsf{:= -_nS+_e P}$
	\item[f'.] At most $n$ $\mathsf{S}$ are $\mathsf{P}$ $\mathsf{:= -_nS-_e P}$
	\item[g'.] At least $n$ $\mathsf{S}$ are $\mathsf{P}$ $\mathsf{:= +_nS+_e P}$
	\item[h'.] At least $n$ $\mathsf{S}$ are not $\mathsf{P}$ $\mathsf{:= +_nS-_e P}$
\end{itemize}

\begin{table}[!htbp]\centering
	\begin{tabular}{lll}
	\hline\noalign{\smallskip}
	 & Proposition & NTL \\
	\noalign{\smallskip}\hline\noalign{\smallskip}
	1. & All but 11 anarchists are logicians. & $\mathsf{-_{11}A+_e L}$\\
	2. & At least 30 Mexicans are anarchists. & $\mathsf{+_{30}M+_e A}$\\
	$\vdash$ & At least 19 Mexicans are logicians. & $\mathsf{+_{19}M+_e L}$\\ 
	\noalign{\smallskip}\hline
	\end{tabular} \caption{A valid numerical syllogism (adapted from~\cite{murphree:1998})}\label{tab:9}      
\end{table}

\begin{table}[!htbp]\centering
	\begin{tabular}{lll}
	\hline\noalign{\smallskip}
	 & Proposition & NTL \\
	\noalign{\smallskip}\hline\noalign{\smallskip}
	1. & Most guys are friendly. & $\mathsf{-_mG+_e F}$\\
	2. & All those who are friendly are tolerant. & $\mathsf{-_0F+_e T}$\\
	$\vdash$ & Most guys are tolerant. & $\mathsf{-_mG+_e T}$\\ 
	\noalign{\smallskip}\hline
	\end{tabular} \caption{A valid numerical syllogism (adapted from ~\cite[p.53]{szabolcsi:2008})}\label{tab:10}      
\end{table}

\begin{table}[!htbp]\centering
	\begin{tabular}{lll}
	\hline\noalign{\smallskip}
	 & Proposition & NTL \\
	\noalign{\smallskip}\hline\noalign{\smallskip}
	1. & All but 3 teachers gave 4 books to all but 5 students. & $\mathsf{-_3T+(+(+_e G+_4B)-_5S)}$\\
	2. & All but 2 teachers are underpaid persons. & $\mathsf{-_2T+_e U}$\\
	3. & Every book is expensive & $\mathsf{-_0B+_e E}$\\
	4. & All but 7 students are ingrates. & $\mathsf{-_7S+_e I}$\\
	5. & There are at least 50 students. & $\mathsf{+_{50}S+_e S}$\\
	6. & There are at least 10 teachers. & $\mathsf{+_{10}T+_e T}$\\
	$\vdash$ & At least 5 underpaid persons gave 4 expensive & $\mathsf{+_5U+(+(+_e G+_4E)+_{38}I)}$\\ 
	   & things to 38 ingrates. & \\
	\noalign{\smallskip}\hline
	\end{tabular} \caption{A valid numerical syllogism (adapted from~\cite{murphree:1998})}\label{tab:11}      
\end{table}

\pagebreak

With these elements, we now introduce the tableaux rules for NTL in Diagram~\ref{diag:5}: from left to right, the first rule is for universal propositions, the second rule is for particular propositions. Notice that after applying a rule we introduce some index $i\in \lbrace 1, 2, 3, \ldots \rbrace$ just as in TFL tableaux; but also, notice that after applying a rule we create a vector $v$ by keeping track of the numerical value $\mathsf{n}$ of the proposition. The third diagram, on the other hand, is a rule for ordering atomic terms with a ``+'' attached. Now, given these rules, we say $\mathsf{A}$ is a logical consequence of the set of terms $\Gamma$ if and only if there is a complete closed tableau whose initial list includes the terms of $\Gamma$ and the rejection of $\mathsf{A}$, and $v=0$. Accordingly, up next we show some examples of valid inferences (Diagrams~\ref{diag:6} and~\ref{diag:7}) and then we argue that a valid inference in NTL produces a closed complete tree with $v=0$ and vice versa.

\begin{diagram}[h]
\begin{multicols}{3}
\Tree [.$\mathsf{-_nA\pm_e B}$ [.$\mathsf{-_nA}^i$ ] $\mathsf{\pm_e B}^i$ ]\\ \hspace*{1.5cm} $v=\mathsf{n}$

\Tree [.$\mathsf{+_nA\pm_e B}$ [.$\mathsf{+_nA}^i$ $\mathsf{\pm_e B}^i$ ]]\\ \hspace*{1.5cm} $v=\mathsf{n}$

\Tree [.$\mathsf{+_nA}$ [.$\mathsf{+_{k\leq n}A}$ ]]
\end{multicols}
\caption{NTL tableux rules}\label{diag:5}
\end{diagram}

\begin{diagram}[h!]
\begin{multicols}{3}
\Tree[.{$\mathsf{-_{6}C+_e L}$\\$\mathsf{-_{20}S+_e C}$\\$\vdash\mathsf{-_{26}S+_e L}$\\$\mathsf{-(-_{26}S+_e L)}$\\$\mathsf{+_{26}S-_e L}$} [.{$\mathsf{+_{26}S}^1$} [.{$\mathsf{-_e L}^1$} [.{$\mathsf{+_{20}S}^1$} {$\mathsf{-_{20}S}^1$\\$\bot$}  [.$\mathsf{+_e C}^1$ [.$\mathsf{+_6C}^1$ {$\mathsf{-_6C}^1$\\$\bot$} {$\mathsf{+_e L}_1$\\$\bot$} !{\qbalance} ]
!\qsetw{3cm} ] ] ] ] ] \\ $v=+26-20-6=0$ 
 
\Tree[.{$\mathsf{-_{11}A+_e L}$\\$\mathsf{+_{30}M+_e A}$\\$\vdash\mathsf{+_{19}M+_e L}$\\$\mathsf{-(+_{19}M+_e L)}$\\$\mathsf{-_{19}M-_e L}$} [.{$\mathsf{+_{30}M}^1$} [.{$\mathsf{+_e A}^1$} [.{$\mathsf{+_{19}M}^1$} {$\mathsf{-_{19}M}^1$\\$\bot$}  [.$\mathsf{-_e L}^1$ [.$\mathsf{+_{11}A}^1$ {$\mathsf{-_{11}A}^1$\\$\bot$} {$\mathsf{+_e L}_1$\\$\bot$} !{\qbalance} ]
!\qsetw{3cm} ] ] ] ] ] \\$v=+30-19-11=0$ 

\Tree[.{$\mathsf{-_{m}G+_e F}$\\$\mathsf{-_{0}F+_e T}$\\$\vdash\mathsf{-_{m}G+_e T}$\\$\mathsf{-(-_{m}G+_e T)}$\\$\mathsf{+_{m}G-_e T}$} [.{$\mathsf{+_{m}G}^1$} [.{$\mathsf{-_e T}^1$} {$\mathsf{-_{m}G}^1$\\$\bot$}  [.$\mathsf{+_e F}^1$ [.$\mathsf{+_0F}^1$ {$\mathsf{-_0F}^1$\\$\bot$} {$\mathsf{+_e T}_1$\\$\bot$} !{\qbalance} ]
!\qsetw{3cm} ] ] ] ] \\$v=+m-m-0=0$ 
\end{multicols}
\caption{From left to right, tableaux for Tables~\ref{tab:8},~\ref{tab:9}, and~\ref{tab:10}}\label{diag:6}
\end{diagram}

\begin{diagram}
\small
\Tree[.{$\mathsf{-_3T+(+(+_e G+_4B)-_5S)}$\\$\mathsf{-_2T+_e U}$\\$\mathsf{-_0 B+_e E}$\\$\mathsf{-_7S+_e I}$\\$\mathsf{+_{50}S+_e S}$\\$\mathsf{+_{10}T+_e T}$\\$\vdash\mathsf{+_5U+(+(+_e G+_4E)+_{38}I}$\\$\mathsf{-(+_5U+(+(+_e G+_4E)+_{38}I)}$\\$\mathsf{-_5U-(+(+_e G+_4E)+_{38}I}$} [.{$\mathsf{+_{50}S}^1$} [.{$\mathsf{+_e S}^1$} [.{$\mathsf{+_{10}T}^2$} [.{$\mathsf{+_e T}^2$} [.{$\mathsf{+_2T}^2$} $\mathsf{-_2T}^2$\\$\bot$ [.$\mathsf{+_e U}^2$ [.$\mathsf{+_7S}^1$ {$\mathsf{-_7S}^1$\\$\bot$}  [.{$\mathsf{+_e I}^1$} [.{$\mathsf{+_{38}I}^1$} [.$\mathsf{+_3T}^2$ {$\mathsf{-_3T}^2$\\$\bot$} [.$\mathsf{+(+_e G+_4B)-_5S}^2$ [.$\mathsf{+_e G}^2$ [.$\mathsf{+_4B}^2$ [.$\mathsf{-_5S}^2$ [.$\mathsf{+_0B}^2$ {$\mathsf{-_0B}^2$\\$\bot$} [.$\mathsf{+_e E}^2$ [.$\mathsf{+_4E}^2$ [.$\mathsf{+_5U}^2$ {$\mathsf{-_5U}^2$\\$\bot$} [.$\mathsf{-(+(+_e G+_4E)+_{38}I}^2$\\$\mathsf{-(+_e G+_4E)-_{38}I}^2$ {$\mathsf{-_{38}I}^1$\\$\bot$} [.$\mathsf{-(+_e G+_4E)}^1$\\$\mathsf{-_e G-_4E}^1$ {$\mathsf{-_e G}^2$\\$\bot$} {$\mathsf{-_4E}^2$\\$\bot$}  !{\qbalance} ]
!\qsetw{3cm}  ] ] ] ] ] ] ] ] ] ] ] ] ] ] ] ] ] ] ] ] \\ \hspace*{4cm}  $v=+50+10-2-7-3+4-5-0-5-38-4=0$
\caption{Tableau for Table~\ref{tab:11}}\label{diag:7}
\end{diagram}

\newpage

\begin{mytheorem}
A valid inference in NTL is a closed complete tree with $v=0$.
\end{mytheorem}

\begin{proof}
Consider that a valid inference in NTL may be of two basic general forms (Table~\ref{tab:12}).

\begin{table}[!htbp]\centering
	\begin{tabular}{lll}
	\hline\noalign{\smallskip}
	 & Form 1 & Form 2 \\
	\noalign{\smallskip}\hline\noalign{\smallskip}
	1. & $\mathsf{-_nX\pm_e Y}$ & $\mathsf{-_nX\pm_e Y}$\\
	2. & $\mathsf{-_mZ\pm_e X}$  & $\mathsf{+_{m+n}Z\pm_e X}$\\
	$\vdash$ & $\mathsf{-_{n+m}Z\pm_e Y}$  & $\mathsf{+_mZ\pm_e Y}$ \\ 
	\noalign{\smallskip}\hline
	\end{tabular} \caption{Basic general forms of a valid inference in NTL}\label{tab:12}      
\end{table}

Now, besides these two general forms, we must consider two cases. For the base case let us consider each basic form. For form 1, take $\mathsf{n}=\mathsf{m}=0$, and for form 2 take $\mathsf{n}=0$ and $\mathsf{m}=1$. Hence, NTL collapses with TFL, in which case we just obtain closed complete trees in TFL. For the inductive case, take $\mathsf{n=k}$ and $\mathsf{m=j}$. Such a replacement yields a valid inference in NTL, since all the conditions of a valid inference in NTL are preserved. Now, suppose that each form is also valid in NTL for $\mathsf{n=k+1}$ and $\mathsf{m=j+1}$ for $\mathsf{k},\mathsf{j}>0$, then the trees would look as follows:

\begin{diagram}[h]\scriptsize
\begin{multicols}{2}
\Tree[.{$\mathsf{-_{k+1}X\pm_e Y}$\\$\mathsf{-_{j+1}Z+_e X}$\\$\vdash\mathsf{-_{k+j+2}Z\pm_e Y}$\\$\mathsf{-(-_{k+j+2}Z\pm_e Y)}$\\$\mathsf{+_{k+j+2}Z\mp_e Y}$} [.{$\mathsf{+_{k+j+2}Z}^1$} [.{$\mathsf{\mp_e Y}^1$} [.{$\mathsf{+_{k+j+2>j+1,\forall k,j>0}Z}^1$} {$\mathsf{-_{j+1}Z}^1$\\$\bot$}  [.$\mathsf{+_e X}^1$ [.$\mathsf{+_{e>k+1,\forall k}X}^1$ {$\mathsf{-_{k+1}X}^1$\\$\bot$} {$\mathsf{\pm_e Y}_1$\\$\bot$} !{\qbalance} ]
!\qsetw{3cm} ] ] ] ] ]\\ \hspace*{.5cm} $v=\mathsf{+k+j+2-(j+1)-(k+1)}=0$

\Tree[.{$\mathsf{-_{k+1}X\pm_e Y}$\\$\mathsf{+_{k+j+2}Z+_e X}$\\$\vdash\mathsf{+_{j+1}Z\pm_e Y}$\\$\mathsf{-(+_{j+1}Z\pm_e Y)}$\\$\mathsf{-_{j+1}Z\mp_e Y}$} [.{$\mathsf{+_{k+j+2}Z}^1$} [.{$\mathsf{+_e X}^1$} [.{$\mathsf{+_{k+j+2>j+1,\forall k,j>0}Z}^1$} {$\mathsf{-_{j+1}Z}^1$\\$\bot$}  [.$\mathsf{\mp_e Y}^1$ [.$\mathsf{+_{e>k+1,\forall k}X}^1$ {$\mathsf{-_{k+1}X}^1$\\$\bot$} {$\mathsf{\pm_e Y}_1$\\$\bot$} !{\qbalance} ]
!\qsetw{3cm} ] ] ] ] ]\\ \hspace*{.5cm} $v=\mathsf{+k+j+2-(j+1)-(k+1)}=0$
\end{multicols}
\end{diagram}
\end{proof}

\newpage

\begin{mytheorem}
A closed complete tree with $v=0$ is a valid inference in NTL.
\end{mytheorem}

\begin{proof} 
Suppose there is a closed complete tree with $v=0$ that is not a valid inference in NTL. Then there is a closed complete tree whose initial list includes a set of terms $\Gamma$, the rejection of the conclusion and $v=0$, but from $\Gamma$ we cannot develop a proof of the conclusion by following the rules of NTL. Without loss of generality, consider the trees corresponding to the valid basic forms of Table~\ref{tab:12}. Then we have two alternatives whose conclusions are, respectively, $\mathsf{-_{n+m}X\pm_e Y}$, and $\mathsf{+_mX\pm_e Y}$. Now, since each tree is complete, the rules for generating the trees have been applied; and since each tree is closed, each tree has to have the following forms:

\begin{diagram}[h]\scriptsize
\begin{multicols}{2}
\Tree[.{$\Gamma$\\$\vdash\mathsf{-_{n+m}X\pm_e Y}$\\$\mathsf{-(-_{n+m}X\pm_e Y)}$\\$\mathsf{+_{n+m}X\mp_e Y}$} [.{$\mathsf{+_{n+m}X}^i$} [.{$\mathsf{\mp_e Y}^i$} [.$\vdots$ {$\mathsf{-_{n+m}X}^i\in\Gamma$\\$\bot$} {$\mathsf{\pm_e Y}^i\in\Gamma$\\$\bot$} !{\qbalance} ]
!\qsetw{3cm} ] ] ]  

\Tree[.{$\Gamma$\\$\vdash\mathsf{+_mX\pm_e Y}$\\$\mathsf{-(+_mX\pm_e Y)}$\\$\mathsf{-_mX\mp_e Y}$} [.{$\mathsf{+_{n+m}X}^i\in\Gamma$} [.{$\mathsf{\pm_e Y}^i\in\Gamma$} [.$\mathsf{+_mX}^i$ [.$\vdots$ {$\mathsf{-_mX}^i$\\$\bot$} {$\mathsf{\mp_e Y}^i$\\$\bot$} !{\qbalance} ]
!\qsetw{3cm} ] ] ] ]
\end{multicols}
\end{diagram}

\pagebreak

Suppose, then, that we have an instance of the first tree but that the resulting proof is not valid, that is to say, where $\Gamma^+=\Gamma\cup\lbrace \mathsf{+_{n+m}X\mp_e Y}\rbrace$, $\Gamma^+\vdash\bot$, but the application of the rule of inference to $\Gamma$ does not allow us to produce $\mathsf{-_{n+m}X\pm_e Y}$. Now, since the tree of the diagram is complete, all the tips are closed, hence the previous nodes have to include something of the form $\mathsf{-_{m+n}X\pm_e Y}$ or $\mathsf{-_mZ\pm_e Y}$ and $\mathsf{-_nX+_e Z}$, that is to say, $\Gamma=\lbrace \mathsf{-_{m+n}X\pm_e Y}\rbrace$ or $\Gamma=\lbrace \ldots, \mathsf{-_mZ\pm_e Y}, \mathsf{-_nX+_e Z}, \ldots\rbrace$. But then, in any case, if we apply condition $i)$ to $\Gamma$ we obtain something of the form $\mathsf{-X\pm_e Y}$, and not the other way around due to condition $ii)$; and last, by condition $iii) (a)$, the conclusion has to be of the form $\mathsf{-_{m+n}X\pm_e Y}$. But that contradicts the assumption that we cannot develop a proof of such conclusion by using the rule of NTL. The same occurs, \textit{mutatis mutandis}, for the second tree. Thus, $\Gamma=\lbrace \mathsf{+_mX\pm_e Y}\rbrace$ or $\Gamma=\lbrace \ldots, \mathsf{-_nZ\pm_e Y}, \mathsf{+_{m+n}X+_e Z}, \ldots\rbrace$. In any case, if we apply condition $i)$ to $\Gamma$ we obtain something of the form $\mathsf{+_mX\pm_e Y}$, and not the other way around due to condition $ii)$; and last, by the condition $iii) (b)$, the conclusion has to be something of the form $\mathsf{+_mX\pm_e Y}$. But that contradicts the assumption that we cannot develop a proof of such conclusion. 
\end{proof}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Conclusions}
In this contribution we have attempted to offer a tableaux method for a family of term logics comprising Term Functor Logic, Intermediate Term Functor Logic, and Numerical Term Logic by using and adapting Murphree's system. This is possible because TFL and TFL$^+$ are sublogics of NTL and so, in some sense, the method we have developed for NTL represents this family of Sommersian term logics. Now, we have to mention that for the purposes of this paper we have focused only on the terministic features of NTL, but further comparison is required with the algebraic proof systems introduced by \cite{carnielli:2001,1423156}; and alternative term logics like Szabolcsi's~\cite{szabolcsi:2008}, for they may have more or less the same motivation but not the same rules. 

\section*{Acknowledgments}
We would like to thank the anonymous reviewers for their precise corrections and useful comments. Financial support given by UPAEP Research Grant.

%%%%%%%%%%%% Bibliography %%%%%%%%%%%%

\bibliographystyle{plain}
\bibliography{ref} 

\end{document}
