# Measuring Conversational Productivity in Child Forensic Interviews

###### Abstract

Child Forensic Interviewing (FI) presents a challenge for effective
information retrieval and decision making. The high stakes associated with the
process demand that expert legal interviewers are able to effectively
establish a channel of communication and elicit substantive knowledge from the
child-client while minimizing potential for experiencing trauma. As a first
step toward computationally modeling and producing quality spoken interviewing
strategies and a generalized understanding of interview dynamics, we propose a
novel methodology to computationally model effectiveness criteria, by applying
summarization and topic modeling techniques to objectively measure and rank
the responsiveness and conversational productivity of a child during FI. We
score information retrieval by constructing an agenda to represent general
topics of interest and measuring alignment with a given response and
leveraging lexical entrainment for responsiveness. For comparison, we present
our methods along with traditional metrics of evaluation and discuss the use
of prior information for generating situational awareness.

Index Terms: Forensic interviews, Verbal productivity

##  1 Introduction

A Forensic Interview (FI) with a child involves a legal expert navigating a
semi-structured interaction with an objective to elicit substantive and
detailed information regarding abuse or neglect that the child might have
witnessed or been a victim of. Given the potential criminal underpinning,
risks, and consequences associated with these spoken interviews, it is
critical they are conducted to evoke genuine information from a possible
sufferer. We explore the role of speech and language processing to provide
supporting analytical tools in this domain.

Since FI is conducted with a potential victim of criminal maltreatment, it
runs the risk of emotionally impacting the child (e.g. potentially having a
victim re-experience trauma). Establishing a sense of trust and comfort with
the children strongly impacts the outcome of the interviews [1, 2]. FI with
children is further challenged as the child’s age and cognitive development
and state may impact their ability to provide a complete and accurate
response. For instance, [3] demonstrated that sexually-abused children were
more likely to deny the abuse during their first line of questioning. This
imposes a tremendous importance on developing strategies for rapport building
with the child which can adequately capture the multi-faceted complexity of
the objective and constraints.

In order to effectively research and develop best practices for FI, we find it
necessary to have an objective method to assess quality of interactions. A
number of contemporary studies [4, 5, 6] have evaluated interaction using a
measure of “productivity” scoring of child responses. The dominant metrics
used are utterance word count along with a variety of human-coded measures
such as “richness” [7] indicating the number of informative details provided
[8]. In this paper, we address the limitations of these methods and present a
novel approach to identify momentary instances of verbal productivity and
evaluate for each utterance.

This work both builds upon existing NLP methods and presents new metrics to
computationally model topics presented in goal-oriented dialogue, which extend
to a mathematical formulation and framework for extracting the conversational
“agenda” to represent information that the interviewer wishes to address. We
present a number of scoring methods which leverage both a child’s
responsiveness to an immediate prompt as well as the alignment of utterances
with the agenda. To the best of our knowledge, this is the first approach to
scoring verbal recall productivity using computational metrics, and believe
that it has the potential to strongly impact the field of FI, giving
researchers an objective measure which they can optimize, score, and inform
their decision making.

##  2 Background

FI of children is an important and active area of research in psychology and
law. The situational context is high stakes as children are frequently the
victims of crimes perpetrated by their caretakers or legal guardians [9],
creating a conflict for both interviewers and the child. Furthermore, children
are often the only witnesses to the abuse of others [10] making their recall
and accounts provided during interviews crucial to the legal process. Speech
and language analysis performed in [8] and [11] provides details on the
effectiveness across linguistic features for questions and show that
contemporary interviewing research is conducted using word count and human
coding of new relevant information .

Word count is generally recorded as a metric of responsiveness during rapport
building. Aside from establishing a comfortable setting, rapport building
phases are important to practicing narrative techniques in children [12].
However, Figure 1 shows that the expressiveness in terms of per-turn average
word count and its variability per group grows with a steady relation to their
age. Generally though, we see that most children will have relatively low
variance in the number of words they express during a session. Thus, word
count is more likely to be reflective of an individual’s language usage and
ability, rather than a indicator of expressiveness or narrative structuring.
By introducing a computational metric to capture responsiveness as a measure
of topic expression we hope to facilitate the evaluation with higher fidelity.
Furthermore, the ability to automate the interview evaluation alleviates some
of the need for human involvement in data creation and labeling, making the
process more scalable, faster, and less subjective.

Figure 1: Expressiveness (in terms of average turn-level word count) of
children across age groups collected over 527 Forensic Interview Transcripts

The importance of social cues and rapport during an interview make it similar
in nature to psychotherapeutic (PT) dialogues such as motivational
interviewing, where the interviewer (counselor) is guiding the subject
(client) towards a goal through appropriate dialogue actions[13]. Both FI and
PT require a foundation of trust, which is built over the interactions and do
not always align with the direct objectives of the dialogue. In psychotherapy
trust is used to promote behavioral change in the client, typically over a
series of sessions over a long period of time. However, the legal setting
surrounding FI limits engagement opportunities that interviewers have, and is
more focused in maximizing information elicitation from the subject without
coercion.

Previous work on dialogue-summarization shows success in tracking and modeling
topics discussed in dyadic conversations. One source of inspiration for our
work is the topic modeling performed in DiaSumm [14], which uses tf-idf and
TextTiling [15] to find topics and their boundaries in the CALLHOME dataset.
However, since we tasked with scoring the relevance of a response, our
approach only uses the interviewers side of the dialogue to extract the
topics.

The work presented in [16] takes advantage of knowledge-graphs (e.g.
Wikipedia) to improve dialogue summary and topic identification robustness.
However within the specific application of Child FI, the vocabulary used by
the client will be strongly influenced by the child’s language development. As
a result, semantic representations from these large knowledge-graphs do not
necessarily contain information that can improve the topic-modeling of the
dialogues.

Finally, both Question-Answering Systems (QASs) and Machine Dialogue Systems
(MDSs) provide frameworks for evaluating machine-generated responses. Many
different flavors exist for QASs, both Natural-Language-Understanding based
and structured-query, but both are assessed in whether or not the response was
correct in reference to a ground truth [17]. MDSs are generally evaluated for
“human-like” linguistic features using word-perplexity as a first pass, and
then relying on human analysis of the generated response [18, 19]. When
evaluating goal-oriented dialogue systems such as [20], the response is scored
by the final objective measure of the system’s ability to outperform a human
in a negotiation. Ultimately, both of these domains present relevant
methodologies towards how a dialogue may be scored, but neither present a
specific criteria that may be applied to the context of Child FI.

In juxtaposition, this paper presents a scoring metric which evaluates
dialogue interactions without a known ground truth which we hope to elicit,
nor a known objective metric that is being maximized through the interaction.
The methodologies presented in Sections 3.1 and 3.2 address the limitations of
human-coding scalability and word count applicability. Our results demonstrate
that despite these challenges a computationally motivated metric generates
robust and informative values indicative of interview effectiveness.

##  3 Methodology

Let us introduce some notation to begin. An interview
$\Psi=\\{(q_{0},r_{0}),\ldots,(q_{m},r_{m})\\}$ is denoted as a sequence of
questions ($q_{t}$) and response phrases ($r_{t}$). An interviewer has a
vocabulary $\mathcal{V}_{\Psi}$ which is a collection of unique n-grams for an
interviewer in $\Psi$. We chose arbitrary n = 3 and exclude stop words as they
by definition do not carry meaning.

###  3.1 Agenda

We define an agenda, for an interview session $\Psi$ in the following way

$\mathcal{A}_{\Psi}=\phi(\mathcal{V}_{\Psi},Q_{\Psi})=\langle
tf(v_{j},Q_{\Psi})\rangle_{\forall v_{j}\in\mathcal{V}_{\Psi}}$

Where $\phi$ is a function to construct a vector of term-frequency,
$tf(v,Q_{\Psi})$, of word $v$ in $Q_{\Psi}=\bigcup_{\forall t}q_{t}$.

We construct a vector to represent a response phrase $r_{t}$ within the
interviewers vocabulary $\mathcal{V}_{\Psi}$:

$\bm{{\textbf{r}}}_{t}=\phi(\mathcal{V}_{\Psi},r_{)}$

From this we present our first productivity score ($g$) of a given response
as:

$g(r_{t})=\textbf{r}_{t}\cdot\mathcal{A}_{\Psi}$

We will refer to this as the Agenda productivity, and justify that
$\mathcal{A}_{\Psi}$ is a representation of the topics, that are most relevant
to the dialogue. By taking the dot product we compare how much of the agenda
is expressed in the response as time $r_{t}$. This does not discredit the word
count, however we apply less weight to utterances that are not relevant to the
topics we believe require information.

###  3.2 Responsiveness

Observe that the agenda is constructed over the entire session. However,
during a dialogue the agenda becomes revealed over time, implying that early
interactions may be given low scores inherently because not enough of the
agenda has been revealed to the subject in order for them to respond
meaningfully. Simultaneously, there is a desire to assign productivity to the
response elicited if the child responded directly to a prompt from the
interviewer. We will use this as inspiration to construct a term that will
give benefit to responsiveness (immediate address of prompted agenda topic).
Let us then construct $a_{t}$ which is the rolling agenda, a measure of the
agenda that has been revealed:

$a_{t}=\phi(\mathcal{V}_{\Psi},q_{t})+\gamma
a_{t-1}=\sum_{i=0}^{t}\gamma^{i}\phi(\mathcal{V}_{\Psi},q_{t-i})$

This allows us to treat $a_{t}$ as a representation of recently evoked words
using $\gamma\in[0,1]$ to represent a discount on words or topics that are
brought up in the past. Alignment or use of these words can be observed as a
lexical entrainment or responsiveness to the question, which are indicators of
trust between the interviewer and the client. Entrainment refers to instances
when conversational partners begin to use the same vocabulary and match each
other’s speaking patterns [21]. We define an instance of entrainment or
responsiveness as the reuse of vocabulary from a previous point in time as:

$\rho(r_{t})=\textbf{r}_{t}\cdot a_{t}$

Then to capture both of the desired scores we construct the following
productivity measure:

$\pi^{*}(r_{t})=\beta\frac{\rho(r_{t})}{||a_{t}||}+(1-\beta)\frac{g(r_{t})}{||\mathcal{A}||}$

where $\beta\in[0,1]$ allows us to flexibly leverage the complementary
importance of the skills being captured by each sub-metric.

Figure 2: Age distribution across 527 sessions

##  4 Results and Discussion

Below, we apply the considered productivity scoring functions across a set of
527 child forensic interviews. Each data-point represents a single interview
between an expert-legal interviewer and a unique child (i.e. each interview is
with a different child). The children interviewed are aged between 2 and 17
years old with the exact distribution shown in Figure 2. The data are
collected as part of a study for the development of interviewing practices and
contain examples of various interviewing strategies. To validate our methods
we present samples randomly selected from the dataset, highlighting ability of
our method to extract important concepts and the differences observed across
the use of 4 different scoring metrics: word count, agenda ($g$) scoring,
responsiveness ($\rho$) scoring, and a combined responsiveness/agenda
($\pi^{*}$) scoring.

###  4.1 Agenda and Responsiveness

Table 1: Top 10 weighted words from 5 agendas $\Psi_{1}$ | $\Psi_{2}$ | $\Psi_{3}$ | $\Psi_{4}$ | $\Psi_{5}$
---|---|---|---|---
bathroom | mister | cousin | gonna | really
gonna | pinched | al | mommy | understand
outside | kids | cousin al | aunt | gonna
touched | thank | touched | touched | sometimes
garage | gonna | private | touching | times
uncle | mom | talking | michael | important
sitting | wrong | doors | clothes | clothes
clothes | kid | outside | peepee | kids
fix | id | gonna | pants | mom
mom | really | legs | grandma | touched

Table 1 shows examples of agendas that have been constructed using our methods
with simple stop-word filtering. The extraction clearly identifies important
concepts that are relevant to potential episodes of abuse that the subject
experiences or witnesses. Particularly we take note that these words were
extracted purely from the lexicon of the interviewer, and are not directly
modeling the response of the child. This is justified by the assumption that
in an interview setting, a concept that is repeated frequently in the
questions is indicative of a broader interest in that topic.

Table 2: Comparison of productivity produced by different methods and their relative rank (1 being highest rated rank). Demonstrates the ability to score substantive information from utterances. For Responsiveness+Agenda hyper-parameters $\gamma$ and $\beta$ are chosen to be 0.5 | Word Count | Agenda | Responsive | Responsiveness/Agenda
---|---|---|---|---
Utterance Excerpt |  |  ($g$) |  ($\rho$) |  ($\pi^{*}$)
I like to play with my friends. |  |  |  |
I have a new student … | 35 (1) | 0.00 (128) | 0.00 (129) | 0.00 (128)
Outside in the bathroom… |  |  |  |
(child reveals details) | 9 (26) | 27.00 (1) | 0.16 (3) | 0.23 (2)
Over my skirt clothes, |  |  |  |
but outside he got me under my clothes. | 12 (17) | 12.00 (3) | 0.37 (1) | 0.40 (1)

A closer exploration of utterance level interactions and their scoring can be
found in Table 2, which exhibits the differences and similarities between
scoring metrics. Comparing the rating of each method against the others’ top-
rated utterances informs us as to what features each criterion is sensitive
to.

When using the word count, a response to the interviewer asking the child to
talk about their experience in school is rated highly, despite not being
substantive to overall interview. While the response does generally contain a
lot of words (and thus information) and can be seen as an demonstration of
trust, it does not directly indicate any clues relevant to the suspected abuse
the child might have experienced. In contrast with word count, our scoring
metrics assign higher score to utterances that contain information relevant to
more targeted questions.

This is not to say that asking about the child’s schooling is unproductive to
the interview. Rather, the information explored in that specific utterance is
not indicative of the overall interview session’s effectiveness. The use of
the agenda allows us to assign higher productivity to utterances in which the
child reveals a strong cooperation with the goals of the interviewer. When
taken in conjunction with the possibility of value-iteration methods, we allow
for a decision theoretic model to assign value to rapport building dialogue
actions which will optimize for the desired objective of building responsive
communication and eliciting information.

###  4.2 Signal Sparsity

Figure 3: Various proposed productivity scores over the course of a single
session, agenda(top, left), responsiveness (top, right), combined (bottom,
left) and word count (bottom, right). Each score is normalized with respect to
its maximum.

By comparing the differences in signal sparsity shown in Figure 3, it can be
seen that the word count metric, while being highly abundant, also
demonstrates a highly volatile nature suggesting many hidden underlying
influences. The signal produced by the productivity metric, while sparser, can
be interpreted as a information-relevance filter convolved against the lexical
information provided by the child. This implies that sparsity will not hinder
the study of productivity, instead allows us to isolate the effects of
differing strategies specifically to the information retrieval criteria.

Table 3: Pearson correlation (r) indicating strength of relationship between different productivity metrics and the age of the child. All scores were significant at $p<0.001$. Metric | r
---|---
Word Count | 0.46
Agenda $g$ | 0.26
Responsive $\rho$ | 0.24
Responsive/Agenda $\pi^{*}$ | 0.25

###  4.3 Age-Related Analysis

For comparison with Figure 1, Figures 4 and 5 show us the resulting dependency
between productivity scores and child age. Moreover, Table 3 reveals the
difference in Pearson scores to be statistically significant, implying a
weaker correlation between age and productivity, further suggesting that the
metrics are also more robust to a specific child’s language ability and
development. From this we can extrapolate that these metrics can be used to
evaluate the productivity adaptively to each individual and capture a more
general set of interaction characteristics.

Figure 4: Distribution of scores and variances by age using only the Agenda
criterion Figure 5: Distribution of scores and variances by age using
Responsiveness scoring methods.

##  5 Conclusions

Our experiments and evaluations demonstrate the usefulness of using topic
modeling for productivity assessment. We further suggest the value captured by
measuring responsiveness is equivalent to a time-dilated matching of
vocabulary usage corresponding to lexical entrainment of local interactions, a
known indicator of trust in a dyadic interaction [22]. A number of promising
examples for these methods have been shown to significantly improve
productivity measurements of Child FI while also automating the process.
Furthermore, the results demonstrate that this can be achieved using a rather
simple trigram model.

By introducing hyper-parameters $\beta$ and $\gamma$ to the proposed
productivity measure we allow the system to maintain flexibility for different
criteria, without sacrificing consistency of scoring across specific examples.
For the first time, FI researchers will be able to rigorously assign a value
to a response within the context of a conversation. Aside from simply
reevaluating prior work, these techniques allow for interviewers to construct
“gold standard” agendas prior to the interview. Using these prepared agendas
will allow interviewers to use situational hypotheses and prior knowledge to
improve and inform the specific policy or strategy they employ.

More broadly, these techniques can be used to model similar goal-oriented
dialogues such as negotiation and question answering in an effort to make
information discovery a larger part of the dialogue process.

In conclusion, our results suggest that the computational models of these
interviews are better informed by the proposed measure of productivity. This
creates a clear criterion that can be evaluated and optimized, providing real-
time updates and adaptive scoring metrics.

##  6 Acknowledgements

We would like to thank our collaborators at the Child Interviewing Lab at the
Gould School of Law for their collection and sharing of the data presented in
this paper.

## References

  * [1] K. J. Sternberg, M. E. Lamb, I. Hershkowitz, L. Yudilevitch, Y. Orbach, P. W. Esplin, and M. Hovav, “Effects of introductory style on children’s abilities to describe experiences of sexual abuse,” _Child Abuse & Neglect_, vol. 21, no. 11, pp. 1133–1146, 1997.
  * [2] M. E. Lamb, Y. Orbach, K. J. Sternberg, J. Aldridge, S. Pearson, H. L. Stewart, P. W. Esplin, and L. Bowler, “Use of a structured investigative protocol enhances the quality of investigative interviews with alleged victims of child sexual abuse in britain,” _Applied cognitive psychology_ , vol. 23, no. 4, pp. 449–467, 2009.
  * [3] T. D. Lyon, “False denials: Overcoming methodological biases in abuse disclosure research,” _Child sexual abuse: Disclosure, delay and denial_ , pp. 41–62, 2007.
  * [4] E. C. Ahern, S. N. Stolzenberg, and T. D. Lyon, “Do prosecutors use interview instructions or build rapport with child witnesses?” _Behavioral sciences & the law_, vol. 33, no. 4, pp. 476–492, 2015.
  * [5] E. A. Price, E. C. Ahern, and M. E. Lamb, “Rapport-building in investigative interviews of alleged child sexual abuse victims,” _Applied Cognitive Psychology_ , vol. 30, no. 5, pp. 743–749, 2016.
  * [6] V. Talwar, K. Hubbard, C. Saykaly, K. Lee, R. Lindsay, and N. Bala, “Does parental coaching affect children’s false reports? comparing verbal markers of deception,” _Behavioral sciences & the law_, vol. 36, no. 1, pp. 84–97, 2018.
  * [7] M. E. Lamb, “Effects of investigative utterance types on israeli children’s responses,” _International Journal of Behavioral Development_ , vol. 19, no. 3, pp. 627–638, 1996. [Online]. Available: https://www.tandfonline.com/doi/abs/10.1080/016502596385721
  * [8] E. C. Ahern, S. J. Andrews, S. N. Stolzenberg, and T. D. Lyon, “The Productivity of Wh- Prompts in Child Forensic Interviews,” _Journal of Interpersonal Violence_ , p. 088626051562108, 2015. [Online]. Available: http://journals.sagepub.com/doi/10.1177/0886260515621084
  * [9] L. Radford, S. Corral, C. Bradley, H. Fisher, C. Bassett, N. Howat, and S. Collishaw, “Child abuse and neglect in the uk today,” 2011.
  * [10] M. E. Lamb, K. J. Sternberg, Y. Orbach, I. Hershkowitz, and D. Horowitz, “Differences between accounts provided by witnesses and alleged victims of child sexual abuse,” _Child Abuse and Neglect_ , vol. 27, no. 9, pp. 1019–1031, 2003.
  * [11] J. Z. Klemfuss, J. A. Quas, and T. D. Lyon, “Attorneys’ Questions and Children’s Productivity in Child Sexual Abuse Criminal Trials,” _HHS Public Access_ , vol. 51, no. 1, pp. 87–100, 2015.
  * [12] G. D. Anderson, J. N. Anderson, and J. F. Gilgun, “The influence of narrative practice techniques on child behaviors in forensic interviews,” _Journal of Child Sexual Abuse_ , vol. 23, no. 6, pp. 615–634, 2014. [Online]. Available: http://dx.doi.org/10.1080/10538712.2014.932878 https://doi.org/10.1080/10538712.2014.932878
  * [13] S. P. Lord, D. Can, M. Yi, R. Marin, C. W. Dunn, Z. E. Imel, P. Georgiou, S. Narayanan, M. Steyvers, and D. C. Atkins, “Advancing methods for reliably assessing motivational interviewing fidelity using the motivational interviewing skills code,” _Journal of Substance Abuse Treatment_ , vol. 49, pp. 50–57, 2015.
  * [14] K. Zechner and A. Waibel, “Flexible Summarization of Spontaneous Dialogues in Unrestricted Domains DiaSumm : 2 Issues and Approaches : Overview,” _Proceedings of the 18th Conference on Computational Linguistics_ , vol. 2, pp. 968–974, 2000.
  * [15] M. a. Hearst, “TextTiling: Segmenting text into multi-paragraph subtopic passages,” _Computational Linguistics_ , vol. 23, no. 1, pp. 33–64, 1997\.
  * [16] Y. Noh, J. W. Son, and S. B. Park, “Keyword extraction from dialogue sentences using semantic and topical relatedness,” _Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)_ , vol. 8226 LNCS, no. PART 1, pp. 129–136, 2013.
  * [17] A. Bouziane, D. Bouchiha, N. Doumi, and M. Malki, “Question Answering Systems: Survey and Trends,” _Procedia Computer Science_ , vol. 73, no. Awict, pp. 366–375, 2015. [Online]. Available: http://dx.doi.org/10.1016/j.procs.2015.12.005
  * [18] I. V. Serban, A. Sordoni, Y. Bengio, A. C. Courville, and J. Pineau, “Building End-To-End Dialogue Systems Using Generative Hierarchical Neural Network Models,” _Proceedings of the Thirtieth{AAAI} Conference on Artificial Intelligence_, pp. 3776–3784, 2016.
  * [19] X. Li, Y.-N. Chen, L. Li, J. Gao, and A. Celikyilmaz, “End-to-End Task-Completion Neural Dialogue Systems,” 2017. [Online]. Available: http://arxiv.org/abs/1703.01008
  * [20] M. Lewis, D. Yarats, Y. N. Dauphin, D. Parikh, and D. Batra, “Deal or No Deal? End-to-End Learning for Negotiation Dialogues,” 2017. [Online]. Available: http://arxiv.org/abs/1706.05125
  * [21] S. E. Brennan, “Lexical Entrainment in Spontaneous Dialog,” _Proceedings, 1996 International Symposium on Spoken Dialogue, ISSD-96_ , pp. 41–44, 1996.
  * [22] L. E. Scissors, A. J. Gill, K. Geraghty, and D. Gergle, “In CMC we trust: the role of similarity,” _27th international conference on Human factors in computing systems - CHI 09_ , pp. 527–536, 2009. [Online]. Available: http://dl.acm.org/citation.cfm?id=1518701.1518783


Non-standard modalities
in paraconsistent Gödel logicThe research of Marta Bílková was supported by the grant 22-01137S of the Czech Science Foundation. The research of Sabine Frittella and Daniil Kozhemiachenko was funded by the grant ANR JCJC 2019, project PRELAP (ANR-19-CE48-0006). This research is part of the MOSAIC project financed by the European Union's Marie Skłodowska-Curie grant No. 101007627.
Paraconsistent non-standard modalities

Marta Bílková10000-0002-3490-2083 Sabine Frittella20000-0003-4736-8614Daniil Kozhemiachenko20000-0002-1533-8034
Bílková et al.

The Czech Academy of Sciences, Institute of Computer Science, Prague

INSA Centre Val de Loire, Univ. Orléans, LIFO EA 4022, France

<EMAIL_ADDRESS><EMAIL_ADDRESS>
We introduce a paraconsistent expansion of the Gödel logic with a De Morgan negation $\neg$ and modalities $\blacksquare$ and $\blacklozenge$. We dub the logic $\infoGsquare$ and equip it with Kripke semantics on frames with two (possibly fuzzy) relations: $R^+$ and $R^-$ (interpreted as the degree of trust in affirmations and denials by a given source) and valuations $v_1$ and $v_2$ (positive and negative support) ranging over $[0,1]$ and connected via $\neg$.

We motivate the semantics of $\blacksquare\phi$ (resp., $\blacklozenge\phi$) as infima (suprema) of both positive and negative supports of $\phi$ in $R^+$- and $R^-$-accessible states, respectively. We then prove several instructive semantical properties of $\infoGsquare$. Finally, we devise a tableaux system for $\infoGsquare$ over finitely branching frames and establish the complexity of satisfiability and validity.

§ INTRODUCTION

When aggregating information from different sources, two of the simplest strategies are as follows: either one is sceptical and cautious regarding the information they provide thus requiring that they agree, or one is credulous and trusts their sources. In the classical setting, these two strategies can be modelled with $\Box$ and $\lozenge$ modalities defined on Kripke frames where states are sources, the accessibility relation represents references between them, and $w\vDash\phi$ is construed as ‘$w$ says that $\phi$ is true’. However, the sources can contradict themselves or be silent regarding a given question (as opposed to providing a clear denial). Furthermore, a source can provide a degree to their confirmation or denial. In all of these cases, classical logic struggles to formalise reasoning with such information.

Paraconsistent reasoning about imperfect data
In the situation described above, one can use the following setting. A source $w$ gives a statement $\phi$ two valuations over $[0,1]$: $v_1$ standing for the degree with which $w$ asserts $\phi$ (positive support or support of truth) and $v_2$ for the degree of denial (negative support or support of falsity). Classically, $v_1(\phi,w)+v_2(\phi,w)=1$; if a source provides contradictory information, then $v_1(\phi,w)+v_2(\phi,w)>1$; if the source provides insufficient information, then $v_1(\phi,w)+v_2(\phi,w)<1$.

Now, if we account for the nonclassical information provided by the sources, the two aggregations described above can be formalised as follows. For the sceptical case, the agent considers infima of positive and negative supports. For the credulous aggregation, one takes suprema of positive and negative supports.

These two aggregation strategies were initially proposed and analysed in [8]. There, however, they were described in a two-layered framework[We refer our readers to [3] and [7] for an exposition of two-layered modal logics.] which prohibits the nesting of modalities. Furthermore, the Belnap–Dunn logic [4] ($\BD$) that lacks implication was chosen as the propositional fragment. In this paper, we extend that approach to the Kripke semantics to incorporate possible references between the sources and the sources' ability to give modalised statements. Furthermore, we use a paraconsistent expansion $\Gsquare$ from [5] of Gödel logic $\mathsf{G}$ as the propositional fragment.

Formalising beliefs in modal expansions of $\mathsf{G}$
When information is aggregated, the agent can further reason with it. For example, if one knows the degrees of certainty of two given statements, one can add them up, subtract them from one another, or compare them. In many contexts, however, an ordinary person does not represent their certainty in a given statement numerically and thus cannot conduct arithmetical operations with them. What they can do instead, is to compare their certainty in one statement vs the other.

Thus, since Gödel logic expresses order and comparisons but not arithmetic operations, it can be used as a propositional fragment of a modal logic formalising beliefs. For example, $\mathbf{K45}$ and $\mathbf{KD45}$ Gödel logics can be used to formalise possibilistic reasoning since they are complete w.r.t. normalised and, respectively, non-normalised possibilistic frames [35].

Furthermore, adding coimplication $\coimplies$ or, equivalently, Baaz' Delta operator $\triangle$ (cf. [2] for details), results in bi-Gödel (‘symmetric Gödel’ in the terminology of [20]) logic that can additionally express strict order.

Modal expansions of $\mathsf{G}$ are well-studied. In particular, the Hilbert [15] and Gentzen [27, 28] formalisations of both $\Box$ and $\lozenge$ fragments of the modal logic $\KG$ [$\Box$ and $\lozenge$ are not interdefinable in $\KG$.] are known. There are also complete axiomatisations for both fuzzy [16] and crisp [36] bi-modal Gödel logics. It is known that they and some of their extensions are both decidable and $\pspace$ complete [13, 14, 17] even though they lack finite model property.

Furthermore, it is known that the addition of $\coimplies$ or $\triangle$ as well as of a paraconsistent negation $\neg$ that swaps the supports of truth and falsity does not increase the complexity. Namely, satisfiability of $\KbiG$ and $\mathsf{GTL}$ (modal and temporal bi-Gödel logics, respectively) (cf. [9, 6] for the former and [1] for the latter) as well as that of $\KGsquare$ (expansion of crisp $\KG$ with $\neg$[Note that in the presence of $\neg$, $\phi\coimplies\phi'$ is definable as $\neg(\neg\phi'\rightarrow\neg\phi)$.]) are in $\pspace$.

This paper
In this paper, we consider an expansion of $\Gsquare$ with modalities $\blacksquare$ and $\blacklozenge$ that stand for the cautious and credulous aggregation strategies. We equip them with Kripke semantics, construct a sound and complete tableaux calculus, and explore their semantical and computational properties. Our inspiration comes from two sources: modal expansions of Gödel logics that we discussed above and modal expansions of Belnap–Dunn logic with Kripke semantics on bi-valued frames as studied by Priest [33, 34], Odintsov and Wansing [31, 32], and others (cf. [18] and references therein to related work in the field). In a sense, $\infoGsquare$ can be thought of as a hybrid between modal logics over $\BD$

The remaining text is organised as follows. In Section <ref>, we define the language and semantics of $\infoGsquare$. Then, in Section <ref> we show how to define several important frame classes, in particular, finitely branching frames. We also argue for the use of $\fbinfoGsquare$ ($\infoGsquare$ over finitely branching frames) for the representation of agents' beliefs. In Section <ref> we present a sound and complete tableaux calculus for $\fbinfoGsquare$ and in Section <ref>, we use it to show that $\fbinfoGsquare$ validity and satisfiability are $\pspace$ complete. Finally, in Section <ref>, we wrap up the paper and provide a roadmap to future work.

§ LOGICAL PRELIMINARIES

In this section, we provide semantics of $\infoGsquare$ over both fuzzy and crisp frames. To make the presentation more approachable, we begin with bi-Gödel algebras.

The bi-Gödel algebra $[0,1]_{\mathsf{G}}=\langle[0,1],0,1,\wedge_\mathsf{G},\vee_\mathsf{G},\rightarrow_{\mathsf{G}},\coimplies\rangle$ is defined as follows: for all $a,b\in[0,1]$, we have $a\wedge_\mathsf{G}b=\min(a,b)$, $a\vee_\mathsf{G}b=\max(a,b)$. The remaining operations are defined below:

\begin{align*}
\begin{cases}
1,\text{ if }a\leq b\\
b\text{ else}
\end{cases}
\begin{cases}
0,\text{ if }a\leq b\\
a\text{ else}
\end{cases}
% \\
% {\sim_\mathsf{G}}a&=
% \begin{cases}
% 0,\text{ if }a>0\\
% 1\text{ else}
% \end{cases}
% &
% \triangle_\mathsf{G}a&=
% \begin{cases}
% 0,\text{ if }a<1\\
% 1\text{ else}
% \end{cases}
\end{align*}

We are now ready to define the language and semantics of $\infoGsquare$.

We fix a countable set of propositional variables $\Prop$ and define the language via the following grammar.

\[\infobimodalLsquare\ni\phi\coloneqq p\in\Prop\mid\neg\phi\mid(\phi\!\wedge\!\phi)\mid(\phi\!\rightarrow\!\phi)\mid\blacksquare\phi\mid\blacklozenge\phi\]

Constants $\mathbf{0}$ and $\mathbf{1}$, disjunction $\vee$, and coimplication $\coimplies$ as well as Gödel negation ${\sim}$ can be defined as expected:

\begin{align*}
\mathbf{1}&\coloneqq p\!\rightarrow\!p&\mathbf{0}&\coloneqq\neg\mathbf{1}&{\sim}\phi&\coloneqq\phi\!\rightarrow\!\mathbf{0}&\phi\!\vee\!\phi'&\coloneqq\neg(\neg\phi\!\wedge\!\neg\phi')&\phi\!\coimplies\!\phi'&\coloneqq\neg(\neg\phi'\!\!\rightarrow\!\!\neg\phi)
\end{align*}

A fuzzy bi-relational frame is a tuple $\mathfrak{F}=\langle W,R^+,R^-\rangle$ with $W\neq\varnothing$ and $R^+,R^-:W\times W\rightarrow[0,1]$. In a crisp frame, $R^+,R^-:W\times W\rightarrow\{0,1\}$. A model is a tuple $\mathfrak{M}=\langle W,R^+,R^-,v_1,v_2\rangle$ with $\langle W,R^+,R^-\rangle$ being a frame and $v_1,v_2:\Prop\rightarrow[0,1]$ that are extended to the complex formulas as follows.

$v_1(\neg\phi,w)$   $=$   $v_2(\phi,w)$   $v_2(\neg\phi,w)$   $=$   $v_1(\phi,w)$

$v_1(\phi\wedge\phi',w)$   $=$   $v_1(\phi,w)\wedge_\mathsf{G}v_1(\phi',w)$   $v_2(\phi\wedge\phi',w)$   $=$   $v_2(\phi,w)\vee_\mathsf{G}v_2(\phi',w)$

$v_1(\phi\rightarrow\phi',w)$   $=$   $v_1(\phi,w)\!\rightarrow_\mathsf{G}\!v_1(\phi',w)$   $v_2(\phi\rightarrow\phi',w)$   $=$   $v_2(\phi',w)\coimplies_\mathsf{G}v_2(\phi,w)$

$v_1(\blacksquare\phi,w)$   $=$   $\inf\limits_{w'\!\in\!W}\!\{wR^+w'\!\!\rightarrow_\mathsf{G}\!\!v_1(\phi,w')\}$

$v_2(\blacksquare\phi,w)$   $=$   $\inf\limits_{w'\!\in\!W}\!\{wR^-w'\!\!\rightarrow_\mathsf{G}\!\!v_2(\phi,w')\}$

$v_1(\blacklozenge\phi,w)$   $=$   $\sup\limits_{w'\!\in\!W}\!\{wR^+w'\!\wedge_\mathsf{G}\!v_1(\phi,w')\}$

$v_2(\blacklozenge\phi,w)$   $=$   $\sup\limits_{w'\!\in\!W}\!\{wR^-w'\!\wedge_\mathsf{G}\!v_2(\phi,w')\}$

We will further write $v(\phi,w)=(x,y)$ to designate that $v_1(\phi,w)=x$ and $v_2(\phi,w)=y$. Moreover, we set $S(w)=\{w':wSw'>0\}$.

We say that $\phi$ is $v_1$-valid on $\mathfrak{F}$ ($\mathfrak{F}\models^+\phi$) iff for every model $\mathfrak{M}$ on $\mathfrak{F}$ and every $w\in\mathfrak{M}$, it holds that $v_1(\phi,w)=1$. $\phi$ is $v_2$-valid on $\mathfrak{F}$ ($\mathfrak{F}\models^-\phi$) iff for every model $\mathfrak{M}$ on $\mathfrak{F}$ and every $w\in\mathfrak{M}$, it holds that $v_2(\phi,w)=0$. $\phi$ is strongly valid on $\mathfrak{F}$ ($\mathfrak{F}\models\phi$) iff it is $v_1$ and $v_2$-valid.

$\phi$ is $v_1$ (resp., $v_2$, strongly) $\infoGsquare$ valid iff it is $v_1$ (resp., $v_2$, strongly) valid on every frame. We will further use $\infoGsquare$ to designate the set of all $\infobimodalLsquare$ formulas strongly valid on every frame.

Observe in the definition above that the semantical conditions governing the support of truth of $\infoGsquare$ connectives (except for $\neg$) coincide with the semantics of $\KbiG$ (cf. [9] for the detailed semantics of the latter).

A tourist ($t$) wants to go to a restaurant and asks their two friends ($f_1$ and $f_2$) to describe their impressions regarding the politeness of the staff ($s$) and the quality of the desserts ($d$). Of course, the friends' opinions are not always internally consistent, nor is it always the case that one or the other even noticed whether the staff was polite or was eating desserts. Furthermore, $t$ trusts their friends to different degrees when it comes to their positive and negative opinions. The situation is depicted in Fig. <ref>.

The first friend says that half of the staff was really nice but the other half is unwelcoming and rude and that the desserts (except for the tiramisu and soufflé) are tasty. The second friend, unfortunately, did not have the desserts at all. Furthermore, even though, they praised the staff, they also said that the manager was quite obnoxious.

The tourist now makes up their mind. If they are sceptical w.r.t. $s$ and $d$, they look for trusted rejections[We differentiate between a rejection which we treat as lack of support and a denial, disproof, refutation, counterexample, etc. which we interpret as the negative support.] of both positive and negative supports of $s$ and $d$. Thus $t$ uses the values of $R^+$ and $R^-$ as thresholds above which the information provided by the source does not count as a trusted enough rejection. In our case, we have $v(\blacksquare s,t)=(0.5,0.5)$ and $v(\blacksquare d,t)=(0,0)$. On the other hand, if $t$ is credulous, they look for trusted confirmations of both positive and negative supports and use $R^+$ and $R^-$ as thresholds up to which they accept the information provided by the source. Thus, we have $v(\blacklozenge s,t)=(0.7,0.4)$ and $v(\blacklozenge d,t)=(0.7,0.3)$.

\[\xymatrix{f_1:\txt{$s=(0.5,0.5)$\\$d=(0.7,0.3)$}~&&~t~\ar[rr]^(.3){(0.7,0.2)}\ar[ll]_(.3){(0.8,0.9)}&&~f_2:\txt{$s=(1,0.4)$\\$d=(0,0)$}}\]

$(x,y)$ stands for $wR^+w'=x,wR^-w'=y$. $R^+$ (resp., $R^-$) is interpreted as the tourist's threshold of trust in positive (negative) statements by the friends.

More formally, note that we can combine $v_1$ and $v_2$ into a single valuation (denoted with $\bullet$) on the following bi-lattice on the right. Now, if we let $\sqcap$ and $\sqcup$ be the meet and join w.r.t. the rightward order, it is clear that $\blacksquare$ can be interpreted as an infinitary $\sqcap$ and $\blacklozenge$ as an infinitary $\sqcup$ across the accessible states, respectively.

(U1) at (0,-2) $(0,1)$;
(U2) at (-2,0) $(0,0)$;
(U3) at (2,0) $(1,1)$;
(U4) at (0,2) $(1,0) $;
(U5) at (0.2,0.6) $\bullet$;
(U6) at (0.2,0.4) $(x,y)$;
[-,draw] (U1) to (U2);
[-,draw] (U1) to (U3);
[-,draw] (U2) to (U4);
[-,draw] (U3) to (U4);

From here, it is expected that $\blacksquare$ and $\blacklozenge$ are not normal in the following sense: $\blacksquare(p\wedge q)\leftrightarrow(\blacksquare p\wedge\blacksquare q)$, $\blacksquare\mathbf{1}$, $\blacklozenge(p\vee q)\leftrightarrow(\blacklozenge p\vee\blacklozenge q)$, and $\blacklozenge\mathbf{0}\leftrightarrow\mathbf{0}$ are not valid.

Finally, we have called $\infoGsquare$ ‘paraconsistent’. In this paper, we consider the logic to be a set of valid formulas. It is clear that the explosion principle for $\rightarrow$ — $(p\wedge\neg p)\rightarrow q$ — is not valid. Furthermore, in contrast to $\mathbf{K}$, it is possible to believe in a contradiction without believing in every statement: $\blacklozenge(p\wedge\neg p)\rightarrow\blacklozenge q$ and $\blacksquare(p\wedge\neg p)\rightarrow\blacksquare q$ are not valid.

We end the section by proving that $\blacklozenge$ and $\blacksquare$ are not interdefinable.

$\blacksquare$ and $\blacklozenge$ are not interdefinable.

Denote with $\mathcal{L}_\blacksquare$ and $\mathcal{L}_\blacklozenge$ the $\blacklozenge$- and $\blacksquare$-free fragments of $\infobimodalLsquare$. We build a pointed model $\langle\mathfrak{M},w\rangle$ s.t. there is no $\blacklozenge$-free formula that has the same value at $w$ as $\blacksquare p$ (and vice versa). Consider Fig. <ref>.

\[\xymatrix{w_1:p=\left(\frac{2}{3},\!\frac{1}{2}\right)&\ar[l]\ar[r]w_0:p=(1,\!0)&w_2:p=\left(\frac{1}{3},\!\frac{1}{4}\right)}\]

All variables have the same values in all states exemplified by $p$. $R^+=R^-$, $v(\blacksquare p,w_0)=\left(\frac{1}{3},\frac{1}{4}\right)$, $v(\blacklozenge p,w_0)=\left(\frac{2}{3},\frac{1}{2}\right)$.

One can check by induction that if $\phi\in\infobimodalLsquare$, then

\begin{align*}
\end{align*}

\begin{align*}
\end{align*}

Moreover, on the single-point irreflexive frame whose only state is $u$, it holds for every $\phi(p)\in\infobimodalLsquare$, $v(\phi,u)\in\{v(p,u),v(\neg p,u),(1,0),(1,1),(0,0),(0,1)\}$.

Thus, for every $\blacklozenge$-free $\chi$ and every $\blacksquare$-free $\psi$ it holds that

\begin{align*}
\end{align*}

\begin{align*}
\end{align*}

Since $X$ and $Y$ are closed w.r.t. propositional operations, it is now easy to check by induction that for every $\chi'\in\mathcal{L}_\blacksquare$ and $\psi'\in\mathcal{L}_\blacklozenge$, $v(\chi',w_0)\in X$ and $v(\psi',w_0)\in Y$.

§ FRAME DEFINABILITY

In this section, we explore some classes of frames that can be defined in $\infobimodalLsquare$. However, since $\blacksquare$ and $\blacklozenge$ are non-normal and since we have two independent relations on frames, we expand the traditional notion of modal definability.

* $\phi$ positively defines a class of frames $\mathbb{F}$ iff for every $\mathfrak{F}$, it holds that $\mathfrak{F}\models^+\phi$ iff $\mathfrak{F}\in\mathbb{F}$.

* $\phi$ negatively defines a class of frames $\mathbb{F}$ iff for every $\mathfrak{F}$, every $w\in\mathfrak{F}$, it holds that $\mathfrak{F}\models^-\phi$ iff $\mathfrak{F}\in\mathbb{F}$.

* $\phi$ (strongly) defines a class of frames $\mathbb{F}$ iff for every $\mathfrak{F}$, it holds that $\mathfrak{F}\in\mathbb{F}$ iff $\mathfrak{F}\models\phi$.

With the help of the above definition, we can show that every class of frames definable in $\KbiG$ is positively definable in $\infoGsquare$.

Let $\mathfrak{F}=\langle W,S\rangle$ be a (fuzzy or crisp) frame.

* An $R^+$-counterpart of $\mathfrak{F}$ is any bi-relational frame $\mathfrak{F}^+=\langle W,S,R^-\rangle$.

* An $R^-$-counterpart of $\mathfrak{F}$ is any bi-relational frame $\mathfrak{F}^+=\langle W,R^+,S\rangle$.

Let $\phi$ be over $\{\wedge,\vee,\rightarrow,\coimplies,\Box,\lozenge\}$.

* We denote with $\phi^{+\bullet}$ the formula obtained from $\phi$ by replacing all $\Box$'s and $\lozenge$'s with $\blacksquare$'s and $\blacklozenge$'s.

* We denote with $\phi^{-\bullet}$ the formula obtained from $\phi$ by replacing all $\Box$'s and $\lozenge$'s with $\neg\blacksquare\neg$'s and $\neg\blacklozenge\neg$'s.

Let $\mathfrak{F}=\langle W,S\rangle$ and let $\mathfrak{F}^+$ and $\mathfrak{F}^-$ be its $R^+$ and $R^-$ counterparts. Then, for any $\phi$ be over $\{\wedge,\vee,\rightarrow,\coimplies,\Box,\lozenge\}$, it holds that

\[\mathfrak{F}\models_{\KbiG}\phi\quad\text{iff}\quad\mathfrak{F}^+\models^+\phi^{+\bullet}\quad\text{iff}\quad\mathfrak{F}^-\models^+\phi^{-\bullet}\]

Since the semantics of $\KbiG$ connectives is identical to $v_1$ conditions of Definition <ref>, we only prove that $\mathfrak{F}\models\phi$ iff $\mathfrak{F}^-\models^+\phi^{-\bullet}$. It suffices to prove by induction the following statement.

Let $\mathbf{v}$ be a $\KbiG$ valuation on $\mathfrak{F}$, $\mathbf{v}(p,w)=v_1(p,w)$ for every $w\in\mathfrak{F}$, and $v_2$ be arbitrary. Then $\mathbf{v}(\phi,w)=v_1(\phi^{-\bullet},w)$ for every $\phi$.

The case of $\phi=p$ holds by Convention <ref>, the cases of propositional connectives are straightforward. Consider $\phi=\Box\chi$. We have that $\phi^{-\bullet}=\neg\blacksquare\neg(\chi^{-\bullet})$ and thus

\begin{align*}
&=\inf\limits_{w'\in W}\{wSw'\rightarrow_\mathsf{G}v_2(\neg(\chi^{-\bullet}))\}\\
&=\inf\limits_{w'\in W}\{wSw'\rightarrow_\mathsf{G}v_1(\chi^{-\bullet})\}\\
&=\inf\limits_{w'\in W}\{wSw'\rightarrow_\mathsf{G}\mathbf{v}(\chi)\}\tag{by IH}\\
\end{align*}

The above theorem allows us to positively define in $\infoGsquare$ all classes of frames that are definable in $\KbiG$. In particular, all $\mathbf{K}$-definable frames are positively definable. Moreover, it follows that $\infoGsquare$ (as $\KG$ and $\KbiG$) lacks the finite model property: ${\sim}\Box(p\vee{\sim}p)$ is false on every finite frame, and thus, ${\sim}\blacksquare(p\vee{\sim}p)$ is too. On the other hand, there are infinite models satisfying this formula as shown below ($R^+$ and $R^-$ are crisp).

\[\xymatrix{w_1:p=\left(\frac{1}{2},0\right)&\ldots&w_n:p=\left(\frac{1}{n+1},0\right)&\ldots\\&w_0:p=(0,0)\ar[ul]|{+}\ar[ur]|{+}\ar[urr]|{+}\ar@(d,l)|{-}&&}\]

Furthermore, Theorem <ref> gives us a degree of flexibility. For example, one can check that $\neg\blacksquare\neg(p\vee q)\rightarrow(\neg\blacksquare\neg p\vee\neg\blacklozenge\neg q)$ positively defines frames with crisp $R^-$ but not necessarily crisp $R^+$. This models a situation when an agent completely (dis)believes in denials given by their sources while may have some degree of trust between $0$ and $1$ when the sources assert something. Let us return to Example <ref>.

Assume that the tourist completely trusts the negative (but not positive) opinions of their friends. Thus, instead of Fig. <ref>, we have the following model.

\[\xymatrix{f_1:\txt{$s=(0.5,0.5)$\\$d=(0.7,0.3)$}~&&~t~\ar[rr]^(.3){(0.7,1)}\ar[ll]_(.3){(0.8,1)}&&~f_2:\txt{$s=(1,0.4)$\\$d=(0,0)$}}\]

The new values for the cautious and credulous aggregation are as follows: $v(\blacksquare s,t)=(0.5,0.4)$, $v(\blacksquare d,t)=(0,0)$, $v(\blacklozenge s,t)=(0.7,0.5)$, and $v(\blacklozenge d,t)=(0.7,0.3)$.

Furthermore, the agent can trust the sources to the same degree no matter whether they confirm or deny statements. This can be modelled with mono-relational frames where $R^+\!=\!R^-$. We show that they are strongly definable.

$\mathfrak{F}$ is mono-relational iff $\mathfrak{F}\models\blacksquare\neg p\leftrightarrow\neg\blacksquare p$ and $\mathfrak{F}\models\blacklozenge\neg p\leftrightarrow\neg\blacklozenge p$.

Let $\mathfrak{F}$ be mono-relational and $R^+=R^-=R$. Now observe that

\begin{align*}
v_i(\blacksquare\neg p,w)&=\inf\limits_{w'\in W}\{wRw'\rightarrow_\mathsf{G}v_i(\neg p,w')\}\tag{$i\in\{1,2\}$}\\
&=\inf\limits_{w'\in W}\{wRw'\rightarrow_\mathsf{G}v_j(p,w')\}\tag{$i\neq j$}\\
&=v_j(\blacksquare p,w)\\
&=v_i(\neg\blacksquare p,w)
\end{align*}

For the converse, let $R^+\!\neq\!R^-$ and, in particular, $wR^+w'\!=\!x$ and $wR^-w'\!=\!y$. Assume w.l.o.g. that $x>y$. We set the valuation of $p$: $v(p,w')=(x,y)$ and for every $w''\neq w'$, we have $v(p,w'')=(1,1)$. It is clear that $v(\neg\blacksquare p,w)=(1,1)$. On the other hand, $v(\neg p,w')=(y,x)$, whence $v_1(\blacksquare\neg p)\neq1$.

The case of $\blacklozenge$ can be tackled in a dual manner.

In the remainder of the paper, we will be concerned with $\fbinfoGsquare$ — $\infoGsquare$ over finitely branching (both fuzzy and crisp) frames. This is for several reasons. First, in the context of formalising beliefs and reasoning with data acquired from sources, it is reasonable to assume that every source refers to only a finite number of other sources and that agents have access to a finite number of sources as well. This assumption is implicit in many classical epistemic and doxastic logics since they are often complete w.r.t. finitely branching models [19], although cannot define them. Second, in the finitely branching models, the values of modal formulas are witnessed: if $v_i(\blacksquare\phi,w)=x<1$, then, $v_i(\phi,w')=x$ for some $w'$, and if $v_i(\blacklozenge\phi,w)=x$, then $wRw'=x$ or $v_i(\phi,w')=x$ for some $w'$. Intuitively, this means that the degree of $w$'s certainty in $\phi$ is purely based on the information acquired from sources and from its degree of trust in those. Finally, the restriction to finitely branching frames allows for the construction of a simple constraint tableaux calculus that can be used in establishing the complexity valuation.

§ TABLEAUX CALCULUS

In this section, we construct a sound and complete constraint tableaux system $\mathcal{T}\left(\fbinfoGsquare\right)$ for $\fbinfoGsquare$. The first constraint tableaux were proposed in [21, 22, 23] as a decision procedure for the Łukasiewicz logic $\Luk$. A similar approach for the Rational Pawełka logic was proposed in [24]. In [5], we constructed constraint tableaux for $\Luk^2$ and $\Gsquare$ — the paraconsistent expansions of $\Luk$ and $\mathsf{G}$, and in [9] for modal expansions of the bi-Gödel logic and $\Gsquare$.

Constraint tableaux are analytic in the sense that their rules have subformula property. Moreover, they provide an easy way of the countermodel extraction from complete open branches. Furthermore, while the propositional connectives of $\Gsquare$ allow for the construction of an analytic proof system, e.g., a display calculus extending that of $\mathsf{I}_4\mathsf{C}_4$[This logic was introduced several times: in [38], then in [25], and further studied in [30]. It is, in fact, the propositional fragment of Moisil's modal logic [29]. We are grateful to Heinrich Wansing who pointed this out to us.] [38], the modal ones are not dual to one another w.r.t. $\neg$ nor the Gödel negation ${\sim}$. Thus, it is unlikely that an elegant (hyper-)sequent or display calculus for $\infoGsquare$ or $\fbinfoGsquare$ can be constructed.

The next definitions are adapted from [9].

We fix a set of state-labels $\mathsf{W}$ and let $\lesssim\in\!\{<,\leqslant\}$ and $\gtrsim\in\!\{>,\geqslant\}$. Let further $w\!\in\!\mathsf{W}$, $\mathbf{x}\!\in\!\{1,2\}$, $\phi\!\in\!\infobimodalLsquare$, and $c\!\in\!\{0,1\}$. A structure is either $w\!:\!\mathbf{x}\!:\!\phi$, $c$, $w\mathsf{R}^+w'$, or $w\mathsf{R}^+w'$. We denote the set of structures with $\Str$. Structures of the form $w\!:\!\mathbf{x}\!:\!p$, $w\mathsf{R}^+w'$, and $w\mathsf{R}^-w'$ are called atomic (denoted $\AStr$).

We define a constraint tableau as a downward branching tree whose branches are sets containing constraints $\mathfrak{X}\lesssim\mathfrak{X'}$ ($\mathfrak{X},\mathfrak{X'}\in\Str$). Each branch can be extended by an application of a rule[If $\mathfrak{X}\!<\!1,\mathfrak{X}\!<\!\mathfrak{X}'\!\in\!\mathcal{B}$ or $0\!<\!\mathfrak{X}',\mathfrak{X}\!<\!\mathfrak{X}'\!\in\!\mathcal{B}$, the rules are applied only to $\mathfrak{X}\!<\!\mathfrak{X}'$.] below (bars denote branching, $i,j\in\{1,2\}$, $i\neq j$).

\[\scriptsize{\begin{array}{cccc}
\neg_i\!\lesssim\!\dfrac{w\!:\!i\!:\!\neg\phi\!\lesssim\!\mathfrak{X}}{w\!:\!j\!:\!\phi\!\lesssim\!\mathfrak{X}}
\neg_i\!\gtrsim\!\dfrac{w\!:\!i\!:\!\neg\phi\!\gtrsim\!\mathfrak{X}}{w\!:\!j\!:\!\phi\!\gtrsim\!\mathfrak{X}}
\rightarrow_1\!\leqslant\!\dfrac{w\!:\!1\!:\!\phi\!\rightarrow\!\phi'\!\leqslant\!\mathfrak{X}}{\mathfrak{X}\!\geqslant\!{1}\left|\begin{matrix}\mathfrak{X}\!<\!{1}\\w\!:\!1\!:\!\phi'\!\leqslant\!\mathfrak{X}\\w\!:\!1\!:\!\phi\!>\!w\!:\!1\!:\!\phi'\end{matrix}\right.}
\rightarrow_2\!\geqslant\!\dfrac{w\!:\!2\!:\!\phi\rightarrow\phi'\!\geqslant\!\mathfrak{X}}{\mathfrak{X}\!\leqslant\!{0}\left|\begin{matrix}\mathfrak{X}\!>\!{0}\\w\!:\!2\!:\!\phi'\!\geqslant\!\mathfrak{X}\\w\!:\!2\!:\!\phi'\!>\!w\!:\!2\!:\!\phi\end{matrix}\right.}
\end{array}}\]

\[\scriptsize{\begin{array}{cccc}
\wedge_1\!\gtrsim\!\dfrac{w\!:\!1\!:\!\phi\!\wedge\!\phi'\!\gtrsim\!\mathfrak{X}}{\begin{matrix}w\!:\!1\!:\!\phi\!\gtrsim\!\mathfrak{X}\\w\!:\!1\!:\!\phi'\!\gtrsim\!\mathfrak{X}\end{matrix}}
\wedge_2\!\lesssim\!\dfrac{w\!:\!2\!:\!\phi\!\wedge\!\phi'\!\lesssim\!\mathfrak{X}}{\begin{matrix}w\!:\!2\!:\!\phi\!\lesssim\!\mathfrak{X}\\w\!:\!2\!:\!\phi'\!\lesssim\!\mathfrak{X}\end{matrix}}
\rightarrow_1\!<\!\dfrac{w\!:\!1\!:\!\phi\rightarrow\phi'\!<\!\mathfrak{X}}{\begin{matrix}w\!:\!1\!:\!\phi'\!<\!\mathfrak{X}\\w\!:\!1\!:\!\phi\!>\!w\!:\!1\!:\!\phi'\end{matrix}}
\rightarrow_2\!>\!\dfrac{w\!:\!2\!:\!\phi\rightarrow\phi'\!>\!\mathfrak{X}}{\begin{matrix}w\!:\!2\!:\!\phi'\!>\!\mathfrak{X}\\w\!:\!2\!:\!\phi'\!>\!w\!:\!2\!:\!\phi\end{matrix}}
\end{array}}\]

\[\scriptsize{\begin{array}{cc}
\wedge_1\!\lesssim\!\dfrac{w\!:\!1\!:\!\phi\wedge\phi'\!\lesssim\!\mathfrak{X}}{w\!:\!1\!:\!\phi\!\lesssim\!\mathfrak{X}\mid w\!:\!1\!:\!\phi'\!\lesssim\!\mathfrak{X}}
\wedge_2\!\gtrsim\!\dfrac{w\!:\!2\!:\!\phi\wedge\phi'\!\gtrsim\!\mathfrak{X}}{w\!:\!2\!:\!\phi\!\gtrsim\!\mathfrak{X}\mid w\!:\!2\!:\!\phi'\!\gtrsim\!\mathfrak{X}}
\end{array}}\]

\[\scriptsize{\begin{array}{cc}
\rightarrow_1\!\gtrsim\!\dfrac{w\!:\!1\!:\!\phi\!\rightarrow\!\phi'\!\gtrsim\!\mathfrak{X}}{w\!:\!1\!:\!\phi\!\leqslant\!w\!:\!1\!:\!\phi'\mid w\!:\!1\!:\!\phi'\!\gtrsim\!\mathfrak{X}}&\rightarrow_2\!\lesssim\!\dfrac{w\!:\!2\!:\!\phi\rightarrow\phi'\!\lesssim\!\mathfrak{X}}{w\!:\!2\!:\!\phi'\!\leqslant\!w\!:\!2\!:\!\phi\mid w\!:\!2\!:\!\phi'\!\lesssim\!\mathfrak{X}}
\end{array}}\]

\[\scriptsize{\begin{array}{ccc}
\blacksquare_i\!\!\gtrsim\!\dfrac{w\!:\!i\!:\!\blacksquare\phi\!\gtrsim\!\mathfrak{X}}{w'\!:\!i\!:\!\phi\gtrsim\mathfrak{X}\mid w\mathsf{S}w'\!\leqslant\!w'\!:\!i\!:\!\phi}
\blacksquare_i\!\!\leqslant\!\dfrac{w\!:\!i\!:\!\blacksquare\phi\!\leqslant\!\mathfrak{X}}{\mathfrak{X}\geqslant1\left|\begin{matrix}\mathfrak{X}\!<\!1\\w\mathsf{S}w''\!>\!w''\!:\!i\!:\!\phi\\w''\!:\!:\!i\!:\!\phi\leqslant\mathfrak{X}\end{matrix}\right.}
\blacksquare_i\!\!<\!\dfrac{w\!:\!i\!:\!\blacksquare\phi\!<\!\mathfrak{X}}{\begin{matrix}w\mathsf{S}w''\!>\!w''\!:\!i\!:\!\phi\\w''\!:\!:\!i\!:\!\phi\!<\!\mathfrak{X}\end{matrix}}
\end{array}}\]

\[\scriptsize{\begin{array}{ccc}
\blacklozenge_i\!\!\gtrsim\!\dfrac{w\!:\!i\!:\!\blacklozenge\phi\!\gtrsim\!\mathfrak{X}}{\begin{matrix}w\mathsf{S}w''\!\gtrsim\!\mathfrak{X}\\w''\!:\!i\!:\!\phi\!\gtrsim\!\mathfrak{X}\end{matrix}}
\blacklozenge_i\!\!\lesssim\!\dfrac{w\!:\!i\!:\!\blacklozenge\phi\!\lesssim\!\mathfrak{X}}{w'\!:\!i\!:\!\phi\lesssim\mathfrak{X}\mid w\mathsf{S}w'\!\lesssim\!\mathfrak{X}}&\quad
\left[\begin{matrix}
w''\text{ is fresh on the branch}\\
\text{if }i\!=\!1,\text{ then }\mathsf{S}\!=\!\mathsf{R}^+\\\text{if }i\!=\!2,\text{ then }\mathsf{S}\!=\!\mathsf{R}^-\\\text{in }\blacksquare_i\!\gtrsim,\blacklozenge_i\!\lesssim~w\mathsf{S}w'\text{ occurs on the branch}
\end{matrix}\right]
\end{array}}\]

A tableau's branch $\mathcal{B}$ is closed iff one of the following conditions applies:

* the transitive closure of $\mathcal{B}$ under $\lesssim$ contains $\mathfrak{X}<\mathfrak{X}$;

* ${0}\geqslant{1}\in\mathcal{B}$, or $\mathfrak{X}>{1}\in\mathcal{B}$, or $\mathfrak{X}<{0}\in\mathcal{B}$.

A tableau is closed iff all its branches are closed. We say that there is a tableau proof of $\phi$ iff there are closed tableaux starting from $w\!:\!1\!:\!\phi<1$ and $w\!:\!2\!:\!\phi>0$.

An open branch $\mathcal{B}$ is complete iff the following condition is met.

$*$If all premises of a rule occur on $\mathcal{B}$, then its one conclusion[Note that branching rules have two conclusions.] occurs on $\mathcal{B}$.

The table below summarises the interpretations of entries.

entry   interpretation
$w\!:1\!:\!\phi\leqslant w'\!:2\!:\!\phi'$   $v_1(\phi,w)\leq v_2(\phi',w')$

$w\!:\!2\!:\!\phi\leqslant c$   $v_2(\phi,w)\leq c$ with $c\in\{0,1\}$

$w\mathsf{R}^-w'\leqslant w'\!:2\!:\!\phi$   $wR^-w'\leq v_2(\phi,w')$

A model $\mathfrak{M}=\langle W,R^+,R^-,v_1,v_2\rangle$ with $W=\{w:w\text{ occurs on }\mathcal{B}\}$ realises a branch $\mathcal{B}$ of a tableau iff

there is a function $\real:\Str\rightarrow[0,1]$ s.t. for every $\mathfrak{X},\mathfrak{Y},\mathfrak{Y}',\mathfrak{Z},\mathfrak{Z}'\in\Str$ with $\mathfrak{X}=w:\mathbf{x}:\phi$, $\mathfrak{Y}=w_i\mathsf{R}^+w_j$, and $\mathfrak{Y}'=w'_i\mathsf{R}^-w'_j$ the following holds ($\mathbf{x}\in\{1,2\}$, ${c}\in\{0,1\}$).

* If $\mathfrak{Z}\lesssim\mathfrak{Z}'\in\mathcal{B}$, then $\real(\mathfrak{Z})\lesssim\real(\mathfrak{Z}')$.

* $\real(\mathfrak{X})=v_\mathbf{x}(\phi,w)$, $\real(c)=c$, $\real(\mathfrak{Y})=w_iR^+w_j$, $\real(\mathfrak{Y}')=w'_iR^-w'_j$

To facilitate the understanding of the rules, we give an example of a failed tableau proof and extract a counter-model. The proof goes as follows: first, we apply all the possible propositional rules, then the modal rules that introduce new states, and then those that use the states already on the branch. We repeat the process until all structures are decomposed into atomic ones.

smullyan tableaux

\[\xymatrix{w_0\ar@/^1pc/[rr]|{R^+=1}\ar@/_1pc/[rr]|{R^-=\frac{1}{2}}&&w_1:p=\left(\frac{1}{2},0\right)}\]

We can now extract a model from the complete open branch marked with $\frownie$ s.t. $v_2(\neg\blacksquare p\!\rightarrow\!\blacksquare\neg p,w_0)>0$. We use $w$'s that occur thereon as the carrier and assign the values of variables and relations so that they correspond to $\lesssim$.

$\phi$ is strongly valid in $\infoGsquare$ iff there is a tableau proof of $\phi$.

The proof is an easy adaptation of <cit.>, whence we provide only a sketch thereof. The skipped steps can be seen in Section <ref>.

To prove soundness, we need to show that if the premise of the rule is realised, then so is at least one of its conclusions. This can be done by a routine check of the rules. Note that since we work with finitely branching frames, infima and suprema from Definition <ref> become maxima and minima. Since closed branches are not realisable, the result follows.

To prove completeness, we show that every complete open branch $\mathcal{B}$ is realisable. We show how to construct a realising model from the branch. First, we set $W=\{w:w\text{ occurs in }\mathcal{B}\}$. Denote the set of atomic structures appearing on $\mathcal{B}$ with $\AStr(\mathcal{B})$ and let $\mathcal{B}^+$ be the transitive closure of $\mathcal{B}$ under $\lesssim$. Now, we assign values to them. For $i\in\{1,2\}$, if $w\!:\!i\!:\!p\geqslant1\in\mathcal{B}$, we set $v_i(p,w)=1$. If $w\!:\!i\!:\!p\leqslant0\in\mathcal{B}$, we set $v_i(p,w)=0$. If $w\mathsf{S}w'<\mathfrak{X}\notin\mathcal{B}^+$, we set $w\mathsf{S}w'=1$. If $w\!:\!i\!:\!p$ or $w\mathsf{S}w'$ does not occur on $\mathcal{B}$, we set $v_i(p,w)=0$ and $w\mathsf{S}w'=0$.

For each $\str\in\AStr$, we now set

\[[\str]\!=\!\left\{\str'\left| \; \begin{matrix}\str\leqslant\str'\in\mathcal{B}^+\text{ and }\str<\str
\notin\mathcal{B}^+\\
\text{or}\\
\str\geqslant\str'\in\mathcal{B}^+\text{ and }\str>\str'\notin\mathcal{B}^+
\end{matrix}\right.\right\}\]

Denote the number of $[\str]$'s with $\#^\mathsf{str}$. Since the only possible loop in $\mathcal{B}^+$ is $\str\leqslant\str'\leqslant\ldots\leqslant\str$ where all elements belong to $[\str]$, it is clear that $\#^\mathsf{str}\leq2\cdot|\AStr(\mathcal{B})|\cdot|W|$. Put $[\str]\prec[\str']$ iff there are $\str_i\in[\str]$ and $\str_j\in[\str']$ s.t. $\str_i<\str_j\in\mathcal{B}^+$. We now set the valuation of these structures as follows:

\begin{align*}
\str=\dfrac{|\{[\str']\mid[\str']\prec[\str]\}|}{\#^\mathsf{str}}%\tag{$*$}\label{valuationchain}
\end{align*}

It is clear that constraints containing only atomic structures and constants are now satisfied. To show that all other constraints are satisfied, we prove that if at least one conclusion of the rule is satisfied, then so is the premise. Again, the proof is a slight modification of <cit.> and can be done by considering the cases of rules (the details are in Section <ref>).

§ COMPLEXITY

In this section, we use the tableaux to provide the upper bound on the size of falsifying (satisfying) models and prove that satisfiability and validity[Satisfiability and falsifiability (non-validity) are reducible to each other: $\phi$ is satisfiable iff ${\sim\sim}(\phi\coimplies\mathbf{0})$ is falsifiable; $\phi$ is falsifiable iff ${\sim\sim}(\mathbf{1}\coimplies\phi)$ is satisfiable.] of $\fbinfoGsquare$ are $\pspace$ complete.

The following statement follows immediately from Theorem <ref>.

Let $\phi\in\infobimodalLsquare$ be not $\fbinfoGsquare$ valid, and let $k$ be the number of modalities in it. Then there is a model $\mathfrak{M}$ of the size $\leq k^{k+1}$ and depth $\leq k$ and $w\in\mathfrak{M}$ s.t. $v_1(\phi,w)\neq1$ or $v_2(\phi,w)\neq0$.

In Section <ref>.

We can now prove the $\pspace$ completeness result. The proof of $\pspace$ membership adapts the method from [9] and is inspired by the proof of the $\pspace$ membership of $\mathbf{K}$ from [10]. For the hardness part, we reduce the validity in $\mathbf{K}$ to $v_1$ and $v_2$ validities. We provide a sketch of the proof (the skipped steps are given in Section <ref>).

$\fbinfoGsquare$ validity and satisfiability are $\pspace$ complete.

For the membership, observe from the proof of Theorem <ref> that $\phi$ is satisfiable (falsifiable) on $\mathfrak{M}=\langle W,R^+,R^-,v_1,v_2\rangle$ iff all variables, $w\mathsf{R}^+w'$'s, and $w\mathsf{R}^-w'$'s have values from $\mathsf{V}=\left\{0,\frac{1}{\#^\str},\ldots,\frac{\#^\str-1}{\#^\str},1\right\}$ under which $\phi$ is satisfied (falsified).

Since $\#^\str$ is bounded from above, we can now replace constraints with labelled formulas and relational structures of the form $w\!:\!i\!:\!\phi\!=\!\mathsf{v}$ or $w\mathsf{S}w'\!=\!\mathsf{v}$ ($\mathsf{v}\in\mathsf{V}$) avoiding comparisons of values of formulas in different states. We close the branch if it contains $w\!:\!i\!:\!\psi\!=\!\mathsf{v}$ and $w\!:\!i\!:\!\psi\!=\!\mathsf{v}'$ for $\mathsf{v}\!\neq\!\mathsf{v}'$.

Now we replace the rules from Definition <ref> with new ones that work with labelled structures. Below, we give as an example the rules[For a value $\mathsf{v}>0$ of $\blacklozenge\phi$ at $w$, we add a new state that witnesses $\mathsf{v}$, and for a state on the branch, we guess a value smaller than $\mathsf{v}$. Other modal rules can be rewritten similarly.] that replace $\blacklozenge_i\!\!\lesssim$.

\begin{align*}
\dfrac{w\!:\!i\!:\!\blacklozenge\phi\!=\!\frac{r}{\#^\str}}{\left.\begin{matrix}w\mathsf{S}w'\!=\!1\\w\!:\!i\!:\!\phi\!=\!\frac{r}{\#^\str}\end{matrix}\right|\left.\begin{matrix}w\mathsf{S}w'\!=\!\frac{r}{\#^\str}\\w\!:\!i\!:\!\phi\!=\!1\end{matrix}\right|\ldots\left|\begin{matrix}w\mathsf{S}w'\!=\!\frac{r}{\#^\str}\\w\!:\!i\!:\!\phi\!=\!\frac{r}{\#^\str}\end{matrix}\right.}
\dfrac{w\!:\!i\!:\!\blacklozenge\phi\!=\!\frac{r}{\#^\str};(w\mathsf{S}w'\text{ occurs on the branch})}{w'\!:\!i\!:\!\phi\!=\!\frac{r-1}{\#^\str}\mid w\mathsf{S}w'\!=\!\frac{r-1}{\#^\str}\mid\ldots\mid w'\!:\!i\!:\!\phi\!=\!0}\end{align*}

Observe that once all rules are rewritten in this manner, we will not need to compare values of formulas in different states.

We then proceed as follows: first, we apply the propositional rules, then one modal rule requiring a new state (e.g., $w_0\!:\!i\!:\!\blacklozenge\phi\!=\!\frac{r}{\#^\str}$), then the rules that use that state guessing the tableau branch when needed. By repeating this process, we are building the model branch by branch. The model has the depth bounded by the length of $\phi$ and we work with modal formulas one by one, whence we need to store subformulas of $\phi$ and $w\mathsf{S}w'$'s with their values $O(|\phi|)$ times, so, we need only $O(|\phi|^2)$ space. Once the branch is constructed, we can delete the entries of the tableau and repeat the process with the next formula at $w_0$ that would introduce a new state.

For hardness, we reduce the $\mathbf{K}$ validity of $\{\mathbf{0},\wedge,\vee,\rightarrow,\Box,\lozenge\}$ formulas to $v_1$-validity and $v_2$-validity in $\fbinfoGsquare$. For the reduction to $v_1$-validity, we use the idea from <cit.>. Namely, given $\phi$, we denote with $\phi^\triangledown$ the formula whose every subformula is prenexed with ${\sim\sim}$ and where $\Box$ and $\lozenge$ are replaced with $\blacksquare$ and $\blacklozenge$. Since semantics for the Gödel modal logic and for the positive support ($v_1$ valuations, Definition <ref>) coincide, the result follows.

For the reduction to $v_2$-validity, we take $\phi$ and inductively define $\phi^\partial$:

\begin{align*}
p^\partial&=\mathbf{1}\coimplies(\mathbf{1}\coimplies p)\\
(\chi\circ\psi)^\partial&=\chi^\partial\bullet\psi^\partial\tag{$\circ,\bullet\in\{\wedge,\vee\}$, $\circ\neq\bullet$}\\
\end{align*}

One can check by induction that for every crisp finitely branching $\mathfrak{F}$ and every classical valuation $\mathbf{v}$ thereon, it holds that $\mathfrak{F},\mathbf{v},w\vDash\phi$ iff $v_2(\mathbf{1}\coimplies\phi^\partial,w)=0$ and $\mathfrak{F},\mathbf{v},w\nvDash\phi$ iff $v_2(\mathbf{1}\coimplies\phi^\partial,w)=1$ provided that $v_2=\mathbf{v}$.

For the converse, let $\mathfrak{M}=\langle W,R^+,R^-,v_1,v_2\rangle$ be a $\fbinfoGsquare$ model. Let $\mathfrak{M}^!=\langle W,R^!,v^!\rangle$ be s.t. $wR^!w'$ iff $wR^-w'=1$ and $w\in v^!(p)$ iff $v_2(p,w)=1$. Again, it is easy to verify that for every $\mathfrak{M}$, $v_2(\phi^\partial,w)=1$ iff $\mathfrak{M}^!,w\vDash\phi$.

It follows that $\phi$ is $\mathbf{K}$-valid iff $\mathbf{1}\coimplies\phi^\partial$ is $v_2$-valid.

§ CONCLUSIONS AND FUTURE WORK

We presented a modal expansion $\infoGsquare$ of $\Gsquare$ with non-normal modalities and provided it with Kripke semantics on bi-relational frames with two valuations. We established its connection with the bi-Gödel modal logic $\KbiG$ presented in [9, 6] and obtained decidability and complexity results considering $\infoGsquare$ over finitely branching frames.

The next steps are as follows. First of all, we plan to explore the decidability of the full $\infoGsquare$ logic. We conjecture that it is also $\pspace$ complete. However, the standard way of proving $\pspace$ completeness of Gödel modal logics described in [13, 14] and used in [6] to establish $\pspace$ completeness of $\KbiG$ may not be straightforwardly applicable here as the reduction from $\infoGsquare$ validity to $\KbiG$ validity can be hard to obtain for it follows immediately from Theorem <ref> that $\infoGsquare$ lacks negation normal forms.

Second, it is interesting to design a complete Hilbert-style axiomatisation of $\infoGsquare$ and study its correspondence theory w.r.t. strong validity. This can be non-trivial since $\blacksquare(p\rightarrow q)\rightarrow(\blacksquare p\rightarrow\blacksquare q)$ and $\blacklozenge(p\vee q)\rightarrow\blacklozenge p\vee\blacklozenge q$ are not $\infoGsquare$ valid, even though, it is easy to check that the following rules are sound.

\begin{align*}
\dfrac{\phi\rightarrow\chi}{\blacksquare\phi\rightarrow\blacksquare\chi}&&\dfrac{\phi\rightarrow\chi}{\blacklozenge\phi\rightarrow\blacklozenge\chi}
\end{align*}

The other direction of future research is to study global versions of $\blacksquare$ and $\blacklozenge$ as well as description logics based on them. Description Gödel logics are well-known and studied [11, 12] and allow for the representation of uncertain data that cannot be represented in the classical ontologies. Furthermore, they are the only decidable family of fuzzy description logics which contrasts them to e.g., Łukasiewicz description (and global) logics which are not even axiomatisable [37]. On the other hand, there are known description logics over $\BD$ (cf., e.g. [26]), and thus it makes sense to combine the two approaches.

[1]
Aguilera, J., Diéguez, M., Fernández-Duque, D., McLean, B.: Time and
Gödel: Fuzzy Temporal Reasoning in PSPACE. In: Logic, Language,
Information, and Computation, Lecture notes in computer science, vol. 13368,
pp. 18–35. Springer International Publishing, Cham (2022)

[2]
Baaz, M.: Infinite-valued Gödel logics with $0 $-$1 $-projections and
relativizations. In: Gödel'96: Logical foundations of mathematics,
computer science and physics—Kurt Gödel's legacy, Brno, Czech Republic,
August 1996, proceedings, pp. 23–33. Association for Symbolic Logic (1996)

[3]
Baldi, P., Cintula, P., Noguera, C.: Classical and Fuzzy Two-Layered Modal
Logics for Uncertainty: Translations and Proof-Theory. International Journal
of Computational Intelligence Systems  13,  988–1001 (2020).

[4]
Belnap, N.: How a computer should think. In: Omori, H., Wansing, H. (eds.) New
Essays on Belnap-Dunn Logic, Synthese Library (Studies in Epistemology,
Logic, Methodology, and Philosophy of Science), vol. 418. Springer, Cham

[5]
Bílková, M., Frittella, S., Kozhemiachenko, D.: Constraint tableaux for
two-dimensional fuzzy logics. In: Das, A., Negri, S. (eds.) Automated
Reasoning with Analytic Tableaux and Related Methods. Lecture Notes in
Computer Science, vol. 12842, pp. 20–37. Springer International Publishing

[6]
Bílková, M., Frittella, S., Kozhemiachenko, D.: Crisp bi-Gödel modal
logic and its paraconsistent expansion.
<https://arxiv.org/abs/2203.01060> (2022)

[7]
Bílková, M., Frittella, S., Kozhemiachenko, D., Majer, O.: Qualitative
reasoning in a two-layered framework. International Journal Approximate
Reasoning  154,  84–108 (2023)

[8]
Bílková, M., Frittella, S., Majer, O., Nazari, S.: Belief based on
inconsistent information. In: Martins, M.A., Sedlár, I. (eds.) Dynamic
Logic. New Trends and Applications. pp. 68–86. Springer International
Publishing, Cham (2020)

[9]
Bílková, M., Frittella, S., Kozhemiachenko, D.: Paraconsistent
Gödel Modal Logic. In: Automated Reasoning, Lecture notes in computer
science, vol. 13385, pp. 429–448. Springer International Publishing, Cham

[10]
Blackburn, P., Rijke, M.d., Venema, Y.: Modal logic. Cambridge tracts in
theoretical computer science 53, Cambridge University Press, 4. print. with
corr. edn. (2010)

[11]
Bobillo, F., Delgado, M., Gómez-Romero, J., Straccia, U.: Fuzzy
description logics under Gödel semantics. International Journal of
Approximate Reasoning  50(3),  494–514 (Mar 2009)

[12]
Bobillo, F., Delgado, M., Gómez-Romero, J., Straccia, U.: Joining
Gödel and Zadeh fuzzy logics in fuzzy description logics. International
Journal of Uncertainty Fuzziness and Knowledge-Based Systems
20(04),  475–508 (Aug 2012)

[13]
Caicedo, X., Metcalfe, G., Rodríguez, R., Rogger, J.: A finite model
property for Gödel modal logics. In: International Workshop on Logic,
Language, Information, and Computation. pp. 226–237. Springer (2013)

[14]
Caicedo, X., Metcalfe, G., Rodríguez, R., Rogger, J.: Decidability of
order-based modal logics. Journal of Computer and System Sciences
88,  53–74 (Sep 2017)

[15]
Caicedo, X., Rodriguez, R.: Standard Gödel modal logics. Studia Logica
94(2),  189–214 (2010)

[16]
Caicedo, X., Rodríguez, R.: Bi-modal Gödel logic over [0,1]-valued
Kripke frames. Journal of Logic and Computation  25(1),  37–55

[17]
Diéguez, M., Fernández-Duque, D.: Decidability for $\mathbf{S4}$
Gödel Modal Logics. In: Computational Intelligence and Mathematics for
Tackling Complex Problems, Studies in computational intelligence, vol. 4,
pp. 1–7. Springer International Publishing, Cham (2023)

[18]
Drobyshevich, S.: A general framework for $\mathsf{FDE}$-based modal logics.
Studia Logica  108(6),  1281–1306 (Dec 2020)

[19]
Fagin, R., Halpern, J., Moses, Y., Vardi, M.: Reasoning About Knowledge. MIT
Press, Cambridge, MA, USA (2003)

[20]
Grigolia, R., Kiseliova, T., Odisharia, V.: Free and projective bimodal
symmetric gödel algebras. Studia Logica  104(1),  115–143

[21]
Hähnle, R.: A new translation from deduction into integer programming. In:
International Conference on Artificial Intelligence and Symbolic Mathematical
Computing. pp. 262–275. Springer (1992)

[22]
Hähnle, R.: Many-valued logic and mixed integer programming. Annals of
mathematics and Artificial Intelligence  12(3-4),  231–263 (1994)

[23]
Hähnle, R.: Tableaux for many-valued logics. In: D’Agostino, M., Gabbay,
D., Hähnle, R., Posegga, J. (eds.) Handbook of Tableaux Methods. pp.
529–580. Springer-Science+Business Media, B.V. (1999)

[24]
Lascio, L.d., Gisolfi, A.: Graded tableaux for rational Pavelka logic.
International journal of intelligent systems  20(12),  1273–1285

[25]
Leitgeb, H.: Hype: A system of hyperintensional logic (with an application to
semantic paradoxes). Journal of Philosophical Logic  48(2),
305–405 (2019)

[26]
Ma, Y., Hitzler, P., Lin, Z.: Algorithms for paraconsistent reasoning with
OWL. In: The Semantic Web: Research and Applications. ESWC 2007, Lecture
notes in computer science, vol. 4519, pp. 399–413. Springer Berlin
Heidelberg, Berlin, Heidelberg (2007). 10.1007/978-3-540-72667-8_29

[27]
Metcalfe, G., Olivetti, N.: Proof systems for a Gödel modal logic. In:
Giese, M., Waaler, A. (eds.) International Conference on Automated Reasoning
with Analytic Tableaux and Related Methods, TABLEAUX-2009. Lecture Notes in
Artificial Intelligence, vol. 5607, pp. 265–279. Springer (2009)

[28]
Metcalfe, G., Olivetti, N.: Towards a Proof Theory of Gödel Modal Logics.
Logical Methods in Computer Science  7 (2011)

[29]
Moisil, G.: Logique modale. Disquisitiones mathematicae et physicae
2,  3–98 (1942)

[30]
Odintsov, S., Wansing, H.: Routley star and hyperintensionality. Journal of
Philosophical Logic  50,  33–56 (2021)

[31]
Odintsov, S., Wansing, H.: Modal logics with Belnapian truth values. Journal
of Applied Non-Classical Logics  20(3),  279–301 (2010).

[32]
Odintsov, S., Wansing, H.: Disentangling FDE-Based Paraconsistent Modal
Logics. Studia Logica  105(6),  1221–1254 (2017).

[33]
Priest, G.: An Introduction to Non-Classical Logic. From If to Is. Cambridge
University Press, 2nd edn. (2008)

[34]
Priest, G.: Many-valued modal logics: a simple approach. The Review of Symbolic
Logic  1(2),  190–203 (2008)

[35]
Rodriguez, R., Tuyt, O., Esteva, F., Godo, L.: Simplified Kripke semantics for
K45-like Gödel modal logics and its axiomatic extensions. Studia Logica
110(4),  1081–1114 (Aug 2022)

[36]
Rodriguez, R., Vidal, A.: Axiomatization of Crisp Gödel Modal Logic.
Studia Logica  109,  367–395 (2021)

[37]
Vidal, A.: On transitive modal many-valued logics. Fuzzy Sets and Systems
407,  97–114 (Mar 2021)

[38]
Wansing, H.: Constructive negation, implication, and co-implication. Journal of
Applied Non-Classical Logics  18(2–3),  341–364 (2008).

§ PROOFS

§.§ Proof of Theorem <ref>

We fill in the gaps in the sketch. First, we prove the soundness result. Since propositional rules are exactly the same as in $\mathcal{T}\left(\fbKGsquare\right)$ [9], we consider only the most interesting cases of modal rules. We tackle $\blacksquare_1\!\!\gtrsim$ and $\blacklozenge_2\!\!\gtrsim$ (cf. Definition <ref>) and show that in each case, if $\mathfrak{M}=\langle W,R^+,R^-,v_1,v_2\rangle$ realises the premise of the rule, it also realises one of its conclusions.

We begin with $\blacksquare_1\!\!\gtrsim$, assume w.l.o.g. that $\mathfrak{X}=w''\!:\!2\!:\!\psi$, and let $\mathfrak{M}$ realise $w\!:\!1\!:\!\blacksquare\phi\geqslant w''\!:\!2\!:\!\psi$. Now, since $R^+$ and $R^-$ are finitely branching, we have that $\min\limits_{w'\in W}\{w\mathsf{R}^+w'\rightarrow_\mathsf{G}v_1(\phi,w')\}\geq v_2(\psi,w)$, whence at each $w'\in W$ s.t. $wR^+w'>0$[Recall that if $u\mathsf{S}u'\notin\mathcal{B}$, we set $u\mathsf{S}u'=0$.], either $v_1(\phi,w')\geq v_2(\psi,w'')$ or $w\mathsf{R}^+w'\geq v_2(\psi,w'')$. Thus, at least one conclusion of the rule is satisfied.

For $\blacklozenge_2\!\!\gtrsim$ we proceed similarly. Let $\mathfrak{M}$ realise $w\!:\!1\!:\!\blacklozenge\phi\geqslant w''\!:\!2\!:\!\psi$. Again, by the finite branching, we have that $\min\limits_{w'\in W}\{wR^+w'\wedge_\mathsf{G}v_1(\phi,w')\}$. Hence, there is some fresh $w'\in W$ s.t. $wR^+w',v_1(\phi,w')\geq v_2(\psi,w'')$. Thus, the conclusion of the rule is satisfied, as desired.

For completeness, we reason by contraposition. We show by induction on formulas that every complete open branch is realised. The case of atomic constraints holds by the construction of the realising model (recall the proof of Theorem <ref>). We show that other constraints are satisfied. For that, we prove that if at least one conclusion of the rule is satisfied, then so is the premise. The propositional cases are straightforward and can be tackled in the same manner as in <cit.>. We consider only the cases of $\blacklozenge_2\!\gtrsim$ and $\blacksquare_1\!\!\gtrsim$ and assume w.l.o.g. that $\mathfrak{X}=w''\!:\!2\!:\!\psi$.

For $\blacksquare_1\!\!\gtrsim$, assume that for every $w'$ s.t. $w\mathsf{R}^+w'$ is on the branch, either $w'\!:\!1\!:\!\phi\geqslant w''\!:\!2\!:\!\psi$ or $w\mathsf{R}^+w'\leqslant w'\!:\!1\!:\!\phi$ is realisable. Thus, by the inductive hypothesis, for every $w'\in R^+(w)$, it holds that $v_1(\phi,w')\geq v_2(\psi,w'')$ or $wR^+w'\leq v_1(\phi,w')$. Hence, $v_1(\blacksquare\phi,w)\geq v_2(\psi,w'')$ and $w\!:\!1\!:\!\blacksquare\phi\geqslant w''\!:\!2\!:\!\psi$ is realised.

For $\blacklozenge_2\!\gtrsim$, let $w\mathsf{R}^-w''\geqslant w''\!:\!2\!:\!\psi$ and $w'\!:\!1\!:\!\phi\geqslant w''\!:\!2\!:\!\psi$ be realised for some $w''\in R(w)$. By the induction hypothesis, we have that $w\mathsf{R}^-w'',v_2(\phi,w')\geq v_2(\psi,w'')$, whence, $v_2(\blacklozenge\phi,w)\geq v_2(\psi,w'')$ and thus, $w\!:\!2\!:\!\blacklozenge\phi\geqslant w''\!:\!2\!:\!\psi$.

Other rules can be considered similarly.

§.§ Proof of Corollary <ref>

By theorem <ref>, if $\phi$ is not $\fbinfoGsquare$ valid, we can build a falsifying model using tableaux. It is also clear from the rules in Definition <ref> that the depth of the constructed model is bounded from above by the maximal number of nested modalities in $\phi$. The width of the model is bounded by the maximal number of modalities on the same level of nesting.

§.§ Proof of Theorem <ref>

We provide the decision algorithm that utilises the rewritten rules. The algorithm is essentially the same as in [9]. Note also that it is possible to use the original calculus as a decision procedure, although it is not optimal.

Let us show how to build a satisfying model for $\phi$ using polynomial space. We begin with $w_0\!:\!1\!:\phi\!=\!1$ (the algorithm for $w_0\!:\!1\!:\phi\!=\!0$ is the same) and start applying propositional rules (first, those that do not require branching). If we implement a branching rule, we pick one branch and work only with it: either until the branch is closed, in which case we pick another one; until no more rules are applicable (then, the model is constructed); or until we need to apply a modal rule to proceed. At this stage, we need to store only the subformulas of $\phi$ with labels denoting their value at $w_0$.

Now we guess a modal formula (say, $w_0\!:\!2\!:\!\blacklozenge\chi\!=\!\frac{1}{\#^\str}$) whose decomposition requires an introduction of a new state ($w_1$) and apply this rule. Then we apply all modal rules whose implementation requires that $w_0\mathsf{R}^-w_1$ occur on the branch (again, if those require branching, we guess only one branch) and start from the beginning with the propositional rules. If we reach a contradiction, the branch is closed. Again, the only new entries to store are subformulas of $\phi$ (now, with fewer modalities), their values at $w_1$, and a relational term $w_0\mathsf{R}^-w_1$ with its value. Since the depth of the model is $O(|\phi|)$ and since we work with modal formulas one by one, we need to store subformulas of $\phi$ with their values $O(|\phi|)$ times, so, we need only $O(|\phi|^2)$ space.

Finally, if no rule is applicable and there is no contradiction, we mark $w_0\!:\!2\!:\!\blacklozenge\chi\!=\!\frac{1}{\#^\str}$ as ‘safe’. Now we delete all entries of the tableau below it and pick another unmarked modal formula that requires an introduction of a new state. Dealing with these one by one allows us to construct the model branch by branch. But since the length of each branch of the model is bounded by $O(|\phi|)$ and since we delete branches of the model once they are shown to contain no contradictions, we need only polynomial space.