In
- Avellone, A and Ferrari, M Almost duplication-free tableau calculi for propositional Lax logics (1996): pages 6-7
seemingly ambiguous tableaux rules are formulated. The authors employ a proof system based $\textit{signed formulas}$ (utilised in Melyvn Fitting's "Intuitionistic Logic, Model Theory and Forcing" (1969), Chapter 2, pg. 28), where a signed formula is of the form $\textbf{T}X, \textbf{F}X, \textbf{F$_c$}X$, where $\textbf{T}$ denotes truth, $\textbf{F}$ denotes falsity and $\textbf{F$_c$}$ denotes certain falsity.
To give an indication of how such tableaux rules work with signed formulas, consider a 'branching' tableaux rule, such as $\lor$-rule for classical propositional tableaux, which is formulated thus by Fitting:
$$\frac{S, \textbf{T}(X \lor Y) } {S, \hspace{0.2cm} \textbf{T}X \thinspace| \thinspace S, \hspace{0.2cm} \textbf{T}Y } \hspace{0.4cm}\textbf{T$\lor$} $$
We can visualise the application of $\textbf{T}\lor$ by imagining two branches, one on which we have $S, \textbf{T}X$, the other on which we have $S, \textbf{T}Y$. Thus, the notation '$|S$' seems to indicate that the branch operation may be applied in accordance with $\textbf{T}\lor$. However, imagine we have a rule such as the one Avellone and Ferrari propose:
$$\frac{S, \textbf{T}(\bigcirc A \rightarrow B) } {S, \hspace{0.2cm} \textbf{F}\bigcirc A, \hspace{0.2cm} \textbf{T}(\bigcirc A \rightarrow B)|S, \hspace{0.2cm} \textbf{T}B } \hspace{0.4cm}\textbf{T}_{\rightarrow\bigcirc} $$
Visualising the application of this rule $\textbf{T}_{\rightarrow\bigcirc}$, the rule seems to be ambiguous between three ways we could imagine extending branches. I want to know which one is correct (unfortunately their paper does not seem to answer my question).
On the first option we extend three branches: on the first branch we have $S, \textbf{F}\bigcirc A$, on the second we have $S, \textbf{T}(\bigcirc A \rightarrow B)$ and on the third we have $S, \textbf{T}B$. Perhaps this option is incorrect, since it seems to be infinitely looping (we can apply the rule again to the second branch $\textbf{T}(\bigcirc A \rightarrow B)$ $\textit{ad infinitum}$.)
On the second option we extend two branches: on the first branch we have $S, \textbf{F}\bigcirc A, \textbf{T}(\bigcirc A \rightarrow B)$, and on the second branch we have $S, \textbf{T}B$, all by itself.
On the third option we have two branches: on the first branch we have $S, \textbf{F}\bigcirc A, \textbf{T}(\bigcirc A \rightarrow B)$ Take the rule $\textbf{T}_{\rightarrow\bigcirc}$ and on the second branch we have $S, \textbf{F}\bigcirc A, \textbf{T}B$.
There are other ways I could imagine extending the branches. However I would like to know which one they intend. If we have $S, A|B, C$ are we to extend three branches, or just two?
We also have the rules $$\frac{S, \textbf{T}((A \rightarrow B) \rightarrow C) } {S, \hspace{0.2cm} \textbf{F}(A \rightarrow B),\hspace{0.2cm} \textbf{T}(B \rightarrow C) \thinspace |S, \textbf{T}C } \hspace{0.4cm}\textbf{T$\twoheadrightarrow$} $$
and
$$\frac{S, \thinspace \textbf{F$_c$}\bigcirc A} {S, \hspace{0.2cm} \textbf{F}A,\hspace{0.2cm} \textbf{F$_c$}A \hspace{0.2cm} |\thinspace S, \textbf{T}\bot } \hspace{0.4cm}\textbf{F$_c$ $\bigcirc$} $$
On the suggestion of Mees de Vries these would both be binary branching: $\textbf{T$\twoheadrightarrow$}$ would have as its first branch $S, \textbf{F}(A \rightarrow B),\hspace{0.2cm} \textbf{T}(B \rightarrow C)$ and $\textbf{T}C$ as its second branch; whereas $\textbf{F$_c$ $\bigcirc$}$ would have as its first branch $\textbf{F}A,\hspace{0.2cm} \textbf{F$_c$}A$ and $\textbf{T}\bot$ as its second branch.
Is this suggestion correct?