{'fraction_non_alphanumeric': 0.057639036863413595, 'fraction_numerical': 0.010547624121031324, 'mean_word_length': 3.723079503522308, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 14, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Monadicity of Non-deterministic Logical Matrices is Undecidable

The notion of non-deterministic logical matrix (where connectives are interpreted as multi-functions) preserves many good properties of traditional semantics based on logical matrices (where connectives are interpreted as functions) whilst finitely characterizing a much wider class of logics, and has proven to be decisive in a myriad of recent compositional results in logic. Crucially, when a finite non-deterministic matrix satisfies monadicity (distinct truth-values can be separated by unary formulas) one can automatically produce an axiomatization of the induced logic. Furthermore, the resulting calculi are analytical and enable algorithmic proof-search and symbolic counter-model generation. For finite (deterministic) matrices it is well known that checking monadicity is decidable. We show that, in the presence of non-determinism, the property becomes undecidable. As a consequence, we conclude that there is no algorithm for computing the set of all multi-functions expressible in a given finite Nmatrix. The undecidability result is obtained by reduction from the halting problem for deterministic counter machines.


Introduction
Logical matrices are arguably the most widespread semantic structures for propositional logics [17,11]. After Łukasiewicz, a logical matrix consists in an underlying algebra, functionally interpreting logical connectives over a set of truth-values, together with a designated set of truth-values. The logical models (valuations) are obtained by considering homomorphisms from the free-algebra in the matrix similarity type into the algebra, and formulas that hold in the model are the ones that take designated values.
However, in recent years, it has become clear that there are advantages in departing from semantics based on logical matrices, by adopting a non-deterministic generalization of the standard notion. Nondeterministic logical matrices (Nmatrices) were introduced in the beginning of this century by Avron and his collaborators [3,4], and interpret connectives by multi-functions instead of functions. The central idea is that a connective can non-deterministically pick from a set of possible values instead of its value being completely determined by the input values. Logical semantics based on Nmatrices are very malleable, allowing not only for finite characterizations of logics that do not admit finite semantics based on logical matrices, but also for general recipes for various practical problems in logic [13]. Further, Nmatrices still permit, whenever the underlying logical language is sufficiently expressive, to extend from logical matrices general techniques for effectively producing analytic calculi for the induced logics, over which a series of reasoning activities in a purely symbolic fashion can be automated, including proof-search and counter-model generation [16,3,4,2,9,14,7]. In its simplest form, the sufficient expressiveness requirement mentioned above corresponds to monadicity [16,14,7]. A Nmatrix is monadic when pairs of distinct truth-values can be separated by unary formulas of the logic. This crucial property is decidable, in a straightforward way, for finite logical matrices, as one can simply compute the set of all unary functions expressible in a given finite matrix. However, the computational character of monadicity with respect to Nmatrices has not been studied before.
In this paper we show that, in fact, monadicity is undecidable for Nmatrices. Our proof is obtained by means of a suitable reduction from the halting problem for counter machines, well known to be undecidable [15]. Several details of the construction are inspired by results about the inclusion of infectious values in Nmatrices [8], and also by undecidability results concerning term-dag-automata (a computational model that bears some interesting connections with Nmatrices) [1]. As a consequence, we conclude that the set of all unary multi-functions expressible in a given finite Nmatrix is not computable.
The paper is organized as follows. In Section 2 we introduce and illustrate our objects of study, namely logical matrices and Nmatrices, the logics they induce, and the monadicity property. Section 3 recalls the counter machine model of computation, and shows how its computations can be encoded into suitable Nmatrices. Finally, Section 4 establishes our main results, namely the undecidability of monadicity for Nmatrices, and as a corollary the uncomputability of expressible multi-functions. We conclude, in Section 5, with a discussion of the importance of the results obtained and several topics for further research.

Preliminaries
In this section we recall the notion of logical matrix, non-deterministic matrix, and their associated logics. We also introduce, exemplify and discuss the notion of monadicity.
Matrices, Nmatrices and their logics A signature Σ is a family of connectives indexed by their arity, Σ = {Σ (k) : k ∈ N}. The set of formulas over Σ based on a set of propositional variables P is denoted by L Σ (P). The set of subformulas (resp, variables) of a formula ϕ ∈ L Σ (P) is denoted by Sub(ϕ) (resp.,Var(ϕ)). There are two subsets of L Σ (P) that will be of particular interest to us: the set of closed formulas, denoted by L Σ ( / 0), and the set of unary (or monadic) formulas, denoted by L Σ ({p}). A Σ-Nmatrix, is a tuple M = A, · M , D where A is the set of truth-values, D ⊆ A is the set of designated truth-values, and for each © ∈ Σ (k) , the function © M : A k → ℘(A) \ { / 0} interprets the connective ©. A Σ-Nmatrix M is finite if it contains only a finite number of truth-values and Σ is finite. Clearly, this definition generalizes the usual definition of logical matrix, which is recovered when, for every © ∈ Σ (k) and a 1 , . . . , a k ∈ A, © M (a 1 , . . . , a k ) is a singleton. In this case we will sometimes refer to © M simply as a function. A valuation over M is a function v : and is said to falsify ϕ, otherwise. Note that every formula ϕ ∈ L Σ (P), with Var(ϕ) = {p 1 , . . . , p k }, defines a multi-function ϕ M : The multi-function ϕ M is said to be represented, or expressed, by the formula ϕ in M. Furthermore, we say that a multi-function f is expressible in an Nmatrix M if there is a formula ϕ such that ϕ M = f . The logic induced by an Nmatrix M is the Tarskian consequence relation ⊢ M ⊆ ℘(L Σ (P)) × L Σ (P) defined as Γ ⊢ M ϕ whenever, for every v ∈ Val(M), if v(Γ) ⊆ D then v(ϕ) ∈ D. This definition generalizes the usual logical matrix semantics [17,11]. As usual, a formula ϕ is said to be a theorem of M if / 0 ⊢ M ϕ. M Ł is monadic with {p, ¬p} as a set of separators. Indeed, p separates 1 from 0, and also 1 from 1 2 , whereas ¬p separates 0 and 1 2 . One may wonder, though, whether one could separate 0 and 1 2 without using negation. △ Remark 2.2. Notice that we can decide if a given matrix M is monadic by algorithmically generating every unary function expressible in M, as it is usually done when calculating clones over finite algebras [12]. This procedure is, however, quite expensive, since there are, at most, n n unary formulas from a set with n values to itself. The next example illustrates this procedure.  (1)). The formulas p, p ∨ p and p ∧ p define the same function (0, 1 2 , 1) and the formula p → p defines the constant function (1, 1, 1). It is easy to see that we cannot obtain new functions by further applying connectives, so (0, 1 2 , 1) and (1, 1, 1) are the only expressible unary functions. For example, ((p → p) → (p → p)) M ′ Ł = (1, 1, 1). We conclude that 0 cannot be separated from 1 2 , and so M ′ Ł is not monadic. △

Monadicity in Nmatrices
In the presence of non-determinism, we cannot follow the strategy described in Remark 2.2 and Example 2.3. A fundamental difference from the deterministic case is that the multifunctions represented by formulas in a Nmatrix are sensitive to the syntax since, even if there are multiple choices for the value of a subformula, all its occurrences need to have the same value. Crucially, on an Nmatrix M, the multi-function ©(ϕ 1 , . . . , ϕ k ) M does not depend only on the multi-functions © M and (ϕ 1 ) M , . . . , (ϕ k ) M , as we shall see in the next example. Hence, contrarily to what happens in the deterministic case, when generating the expressible multifunctions in an Nmatrix M (to find if M is monadic, or for any other purpose), we cannot just keep the information about the multi-functions themselves but also about the formulas that produce them. Otherwise, we might generate a non-expressible function (as every occurrence of a subformula must have the same value) or miss some multi-functions that are still expressible.
With the intent of making the notation lighter, when representing the interpretation of the connectives using tables, we drop the curly brackets around the elements of an output set. For example, in the table of Example 2.4 we simply write a, c instead of {a, c}.
These functions can easily be shown to be valuations over M for every choice of x and so, for every unary formula ϕ = p, we have that c ∈ ϕ M (a) ∩ ϕ M (b) ∩ ϕ M (c). We conclude that, apart from p, no unary formula can separate elements of {a, b, c}, and so M is not monadic, for any choice of D.

Counter machines and Nmatrices
In this section we recall the essentials of counter machines, and define a suitable finite Nmatrix representing the computations of any given counter machine.

Counter machines
A (deterministic) counter machine is a tuple C = n, Q, q init , δ , where n ∈ N is the number of counters, Q is a finite set of states, q init ∈ Q is the initial state, and δ is a partial transition function δ : Q → ({i ++ : where q is a state, and x = x 1 , . . . , x n are the values of the counters. Let Conf(C ) be the set of all configurations. C ∈ Conf(C ) is said to be the initial configuration if q = q init and x = 0. C is said to be a halting configuration if q ∈ H.
When (q, y) is not a halting configuration, the transition function δ completely determines the next configuration nxt(q, y) as follows: The computation of C is a finite or infinite sequence of configurations C i i<η , where η ∈ N 0 ∪ {ω} such that C 0 is the initial configuration, and for each i < η, either C i is a halting configuration and i + 1 = η is the length of the computation, or else C i+1 = nxt(C i ).
The intuition behind the transitions of a counter machine is clear from the underlying notion of computation, and in particular the definition of the next configuration. Clearly, δ (q) = i ++ , r results in incrementing the i-th counter and moving to state r, whereas δ (q) = i test , r, s either moves to state r, leaving the counters unchanged, when the value of the i-th counter is zero, or moves to state s, and decrements the i-th counter, when its value is not zero. As usual in counter machine models (see [15]), and also for the sake of simplicity, we are assuming that in the initial configuration all counters have value 0. This is well known not to hinder the computational power of the model, as a machine can always start by setting the counters to other desired input values. We will base our undecidability result on the following well known result about counter machines. In what follows, given x ∈ A n and f : For a given counter machine C = n, Q, q init , δ , we define the signature Σ C such that Σ As usual, zero and suc allow us to encode every k ∈ N 0 as the closed formula enc(k) = suc k (zero). Moreover, we can encode every finite sequence of configurations C 0 , . . . ,C k as a sequence formula in the following way: • seq( ) = ε, and seq( C 0 , . . . ,C k−1 , (q, y) ) = step q (seq( C 0 , . . . ,C k−1 ), enc( y)).
We will construct a finite Nmatrix M C over Σ C that recognizes as a theorem precisely the finite computation of C , if it exists. This means that M C can only falsify a formula ϕ if it is not a sequence formula, or if ϕ = seq( C 0 , . . . ,C k ) but C 0 is not the initial configuration of C , or C k is not a halting configuration of C , or nxt(

From counter machines to Nmatrices
For a given counter machine C = n, Q, q init , δ let where, s ∈ Q represents an arbitrary state.
M C is conceived as a finite way of representing the behavior of C . For that purpose, it is useful to understand the operations zero and suc as means of representing the natural number values of the counters. Their interpretation, however, is finitely defined over the abstract values Rm. In fact, in order to check if some formula ϕ encodes a sequence of computations respecting nxt, it is not essential to distinguish all natural values. Indeed, it is easy to conclude from the definition of counter machine that in each computation step its counters either retain their previous values, or else they are incremented or decremented. As we set the initial configuration with all counters set to zero and the effect of test transitions also depends on detecting zero values, it is sufficient to being able to characterize unambiguously the value 0 and, additionally, being able to recognize pairs of values whose difference is larger than one. This is successfully accomplished with the proposed non-deterministic interpretation of suc, as shall be made clear below. The ε and step operations are then meant to represent sequences of configurations, whereas their interpretation over the abstract values Conf ∪ {init} guarantees that consecutive configurations respect nxt. Of course, the designated values of M C are those corresponding to halting configurations. The error value is absorbing with respect to the interpretation of all operations, and gathers all meaningless situations. Overall, as we will show, M C induces a logic that has at most one theorem, corresponding to the computation of C , if it is halting.

The inner workings of the construction
In the next examples we will illustrate the way the Nmatrix M C encodes the computations of C . Proofs of the general statements are postponed to the next section.
In order for ⊢ M C to have, at most, the formula representing the computation of C as theorem, Val(M C ) must contain enough valuations to refute every formula not representing the computation of C . These valuations are presented in the following example Example 3.2. By definition of seq, it is clear that no formula containing variables corresponds to a sequence of configurations. Furthermore, no formula containing variables can be a theorem of M C since these formulas are easily refuted by any valuation sending the variables to the truth value error, as this value is absorbing (aka infectious), that is, suc M C (x) = error whenever x = error and (step q ) M C (x, z) = error whenever x = error or z i = error. Because of this, from here onwards, we concern ourselves only with the truth-values assigned to closed formulas.
We do not have much freedom left, but it will be enough. The interpretations of the connectives are all deterministic, except in the case of zero M C and suc M C (r ≥0 ). This means that, if v ∈ Val(M C ) and v(zero) = r =0 , then there is no choice left for the values assigned by v to the remaining closed formulas. Consider, therefore, the following valuation (1), otherwise.
If v(zero) = r ≥0 , however, we can still loop the truth values assigned to formulas of the form enc( j).
The amount of loops could be infinite or finite, though the infinite case is of no interest to us, since it does not allow us to falsify any of the formulas that we want to falsify.
As previously discussed, it is crucial for the valuations in Val(M C ) to be able to identify whenever two given numbers a, b ∈ N 0 are not consecutive, or different. To this aim, for every pair a, b ∈ (N 0 ) 2 , we denote by µ + a,b , µ − a,b , µ = a,b the valuations determined by the following conditions Remark 3.3. The following properties can be easily checked by inspecting the corresponding definition: (enc(a)). In the following two examples we consider two different machines that should make clear the soundness of our construction. In the first one, we show how every valuation validates the formula encoding a finite computation. We also see how sequences of configurations can fail to respect nxt in different ways and how we can use the valuations presented in Example 3.2 to falsify formulas encoding them. In the second example, we show a counter machine that never halts. Example 3.4. Consider the counter machine C = 1, Q, q init , δ with Q = {q init , q 1 , q 2 , q 3 } and δ as defined in the following table q q init q 1 q 2 q 3 δ (q) 1 ++ , q 1 1 test , q 3 , q 2 1 test , q 3 , q 3 undefined The only halting state of C is q 3 and the machine C has the following finite computation (q init , 0), (q 1 , 1), (q 2 , 0), (q 3 , 0) .
Finally, consider ξ = step q 3 (ϕ 2 , enc(1)) encoding the sequence resulting from appending (q 3 , 1) to the sequence encoded by ϕ 2 . As the value in the first counter was incremented, while the transition δ (q 2 ) = 1 test , q 3 , q 3 required it to remain unchanged we obtain µ = 0,1 (ξ ) = v = 0 (ξ ) = error. △ Example 3.5. Consider the counter machine C = 2, Q, q init , δ with Q = {q init , q 1 , q 2 , q 3 , q 4 } and δ as defined in following table This machine does not have a finite computation, and its infinite computation loops indefinitely in the following cycle consisting of 4 transitions. It starts by incrementing both counters. Then it tests if the first counter has the value 0. As the counter has just been incremented, the test is bound to fail and hence that counter is decremented. It then increments the same counter, and returns to the initial state. The halting state q 4 could only be reached if at a certain point the test would succeed, but this never happens since, at the point the tests are made, the value of the first counter is never 0. Thus, the machine C has the following infinite computation (q init , 0, 0), (q 1 , 1, 0), (q 2 , 1, 1), (q 3 , 0, 1), (q init , 1, 1), (q 1 , 2, 1), (q 2 , 2, 2), (q 3 , 1, 2), (q init , 2, 2), . . .
As we show in the next section, since C has no finite computations, M C has no theorems. Let k ≥ 1 and consider the sequence resulting from adding (q 3 , k − 1, k + 1) to the prefix of the infinite computation of C with 4(k − 1) + 3 elements, and let ϕ k encode this sequence. In this case, the value of the second counter is increased, when it should have remained the same, and we have

Monadicity of Nmatrices is undecidable
In this section we show that M C really does what is intended. The main result of the paper then follows, after we additionally introduce a construction connecting the existence of a theorem with monadicity.

M C validates the finite computation of C
In the following propositions we show that M C is interpreting computations of C as it should. Thus, formulas encoding computations of C that do not end in a halting state can be falsified, whilst the one encoding the finite computation of C is always designated.
In all the three cases we conclude (1) directly by the definition of (step q ′ ) M C .

M C can falsify everything else
The following propositions deal with all the possible ways in which a formula can fail to represent a halting computation of C . Proposition 4.3. Let C = n, Q, q init , δ be a deterministic n-counter machine. If ϕ ∈ L Σ C ( / 0) does not represent a sequence of configurations of C then v(ϕ) = conf q, y for all v ∈ Val C , q ∈ Q and y ∈ Rm n .
Proof. The proof follows by induction on the structure of the formula ϕ ∈ L Σ C ( / 0). In the base case we have ϕ ∈ {zero, ε}. The statement then holds since, for all v ∈ Val C , v(ϕ) ∈ {zero, init}.
Proof. Assume nxt(q, y) = (q ′ , z) and notice that, if δ (q) concerns the ith counter and y j = z j , for some j = i, then µ = y j ,z j (enc(y j )) = µ = y j ,z j (enc(z j )), by remark 3.3. Therefore, equality (2) holds for v = µ = y j ,z j . Because of this, throughout the rest of the proof, we assume that, y j = z j , for every j = i, and concern ourselves only with the values taken by y i and z i . We have to consider three cases, depending on δ (q).
If δ (q) = i ++ , s , for some machine state s. Then either q ′ = s, in which case equality (2) holds for every v ∈ Val(M C ), or z i = y i + 1. In this later case, also by remark 3.3, we have µ + y i ,z i (enc(z i )) / ∈ suc M C (µ + y i ,z i (enc(y i ))), so equality (2) holds for v = µ + y i ,z i . Otherwise, δ (q) = i test , s 1 , s 2 for some machine states s 1 and s 2 . If y i = 0, then either q ′ = s 1 or z i = y i . Consider the valuation µ = , the second condition concerning i test , in the definition of (step q ′ ) M C , is not satisfied whenever v = µ = y i ,z i . The first condition is also not satisfied if q ′ = s 1 , directly, or if z i = y i , since in this case µ = y i ,z i (z i ) = µ = y i ,z i (y i ), by remark 3.3. We conclude that equality (2) holds for v = µ = y i ,z i . If y i = 0, then either q ′ = s 2 or z i = y i − 1. Note that, in any case, µ − y i ,z i (enc(y i )) / ∈ {r =0 , r ≥0 }, which can easily be checked using the definition of µ − y i ,z i . Therefore, the first condition concerning i test , in the definition of (step q ′ ) M C , is not satisfied whenever Proposition 4.5. Given a deterministic counter machine C = n, Q, q init , δ and ϕ ∈ L Σ C ( / 0) such that ϕ = seq( C 0 , . . . ,C k ). If C 0 , . . . ,C k is not the computation of C then / 0 ⊢ M C ϕ.
Proof. If C 0 , . . . ,C k is not the computation of C , then one of the following must hold: (i) C 0 is not the initial configuration of C , (ii) C k is not a halting configuration of C , or (iii) there is some 1 ≤ i < k such that nxt(C i ) = C i+1 . We deal with each situation separately. If (i) holds and C 0 = (q, y) then either q = q init or y j = 0, for some 1 ≤ j ≤ n. In the first case, for all v ∈ Val(M C ), we have (step q ) M C (init, v(enc( y))) = error. In the second case, v y j −1 (enc(y j )) / ∈ {r =0 , r ≥0 } and (step q init ) M C (init, v y j −1 (enc( y))) = error.
If (ii) holds and C k = (q, y) then q is not a halting state and v(ϕ) ∈ {error, conf q,v( y) } ⊆ A \ D, for all v ∈ Val(M C ).
In any of the cases, there is some Having seen how to refute any formula not representing a computation of C we conclude M C does exactly what we intended.
Theorem 4.6. Let C = n, Q, q init , δ be a deterministic counter machine. For any formula ϕ ∈ L Σ C (P) we have / 0 ⊢ M C ϕ if and only if ϕ = seq( C 0 , . . . ,C k ) and C 0 , . . . ,C k is a finite computation of C .
Proof. From right to left, if C 0 , . . . ,C k is a finite computation of C and ϕ = seq( C 0 , . . . ,C k ) then, by theorem 4.2, we have that / 0 ⊢ M C ϕ. In the other direction, suppose / 0 ⊢ M C ϕ then, as discussed in example 3.2, ϕ must be a closed formula. By proposition 4.3, ϕ = seq( C 0 , . . . ,C k ) for some sequence of configurations seq( C 0 , . . . ,C k ), and, by proposition 4.5, seq( C 0 , . . . ,C k ) must be the computation of C .

From theoremhood to monadicity
In order to obtain the announced undecidability result we need one last construction. We will show how to build an Nmatrix M m from an Nmatrix M, under certain conditions, such that M m is monadic if and only if ⊢ M has theorems.
Given a finite Σ-Nmatrix M = A, · M , D , let Σ m be such that Σ and, for every a ∈ A, The following theorem targets Nmatrices with infectious values. Recall that * is infectious in M if for every connective © in the signature of M we have © M (x 1 , . . . , x k ) = * whenever * ∈ {x 1 , . . . , x k }. Proof. Let us denote the infectious non-designated value of M by * . Clearly, * ceases to be infectious in M m as ( f a ) M m does not necessarily output * when it receives it as input. The value 1 is also not infectious in M m , quite the opposite, when given as input to any connective the output can take any value. That is, for every connective © ∈ Σ m we have © M m (x 1 , . . . , x k ) = A m whenever 1 ∈ {x 1 , . . . , x k }. This immediately implies that if ψ ∈ Sub(ϕ) \ {ϕ} and 1 ∈ ψ M m (x) then ϕ M m (x) = A m for any x ∈ A m .
If / 0 ⊢ M ϕ then ϕ must be a closed formula due to the presence of * . Hence, for v ∈ Val(M m ) we have v(ϕ) ∈ D. Thus, {p} ∪ { f a (p, ϕ) : a ∈ A} is a set of monadic separators for M m , as p separates 1 from the elements in A, and f a (p, ϕ) separates a from every b ∈ A.
If instead there are no theorems in ⊢ M , let us consider an arbitrary monadic formula ϕ ∈ L Σ m ({p}) and show it cannot separate * from the other elements of A. We need to consider two cases.
• If ϕ ∈ L Σ ({p}) then ϕ M m (a) = ϕ M (a) ⊆ A ∋ 1 for every a ∈ A. In which case ϕ cannot separate any pair of distinct elements of A and, in particular, cannot separate * from any other element of A.
As we are assuming that A has at least two elements, we conclude that M m is not monadic.
Finally, we get to the main result of this paper.
Theorem 4.8. The problem of determining if a given finite Σ-Nmatrix is monadic is undecidable.
Proof. For every counter machine C , the Nmatrix M C is in the conditions of Theorem 4.7, as it has more than two truth-values and error is infectious. Therefore, by applying successively Theorem 4.6 and 4.7, we reduce the halting problem for counter machines to the problem of checking if a finite Nmatrix is monadic. Indeed, for a given counter machine C , C halts if and only if ⊢ M C has theorems if and only if (M C ) m is monadic. Furthermore, the presented constructions are all computable and (M C ) m is always finite since, if C has m states and n counters, then M C has m × 4 n + 6 truth-values and Σ C has 3 + m connectives. Therefore, (M C ) m has m × 4 n + 7 truth-values and (Σ C ) m has m × 4 n + m + 9 connectives. We can therefore conclude the proof just by invoking Theorem 3.1.
As a simple corollary we obtain that following result about Nmatrices, or better, about their underlying multi-algebras. Proof. Just note that if we could compute the set of all expressible unary multi-functions, as the set is necessarily finite, we could test each of them for the separation of values, as illustrated in the case of matrices in Example 2.3.

Conclusion
In this paper we have shown that, contrarily to the most common case of logical matrices, the monadicity property is undecidable for non-deterministic matrices. As a consequence, we conclude that the set of all multi-functions expressible in a given finite Nmatrix is not computable, in general. These results, of course, do not spoil the usefulness of the techniques for obtaining axiomatizations, analytical calculi and automated proof-search for monadic non-deterministic matrices. This is especially the case since, for a given Nmatrix, one can always define a monadic Nmatrix over an enriched signature, such that its logic is a conservative extension of the logic of the previous Nmatrix, as described in [14]. The results show, however, that tool support for logics based on non-deterministic matrices must necessarily have its limitations.
On a closer perspective, the reduction we have obtained from counter machines to Nmatrices (of which non-determinism is a fundamental ingredient) just adds to the initial perception that allowing for non-determinism brings a substantial amount of expressive power to logical matrices. Concretely, it opens the door for studying the computational hardness of other fundamental meta-theoretical questions regarding logics defined by Nmatrices. In particular, we will be interested in studying the problem of deciding whether two given finite Nmatrices define the same logic, a fundamental question raised by Zohar and Avron in [5], for which only necessary or sufficient conditions are known.
Additionally, we deem it important to further explore the connections between Nmatrices and termdag-automata (an interesting computational model for term languages [10,1]) and which informed our undecidability result. Another relevant direction for further investigation is the systematic study of infectious semantics, in the lines of [8,6], whose variable inclusion properties also played an important role in our results.