Repeatability of necessity: number restrictions?

[nomadreid]

The necessity quantifier (aka Provability quantifier, or ~◊~, or Belief, or... instead of the usual square I will be lazy and call it "N") is often allowed to be repeated as many (finite) times as one wishes, so NNNNNNψ is OK. Is it possible to somehow include into the axioms some restriction on the number of times it can be applied, or even for example outlawing an odd number of applications? My guess is that no, as one would need to have a sentence with too large a domain of the quantifier in the sentence, but I would like to see if my guess is correct.

 

[andrewkirk]

The necessity quantifier (aka Provability quantifier, or ~◊~, or Belief, or... instead of the usual square I will be lazy and call it "N") is often allowed to be repeated as many (finite) times as one wishes, so NNNNNNψ is OK. Is it possible to somehow include into the axioms some restriction on the number of times it can be applied, or even for example outlawing an odd number of applications? My guess is that no, as one would need to have a sentence with too large a domain of the quantifier in the sentence, but I would like to see if my guess is correct.

In modal logic, the axiom schema that is typically used to allow repeatability of the unary $\square$ operator is, labelled as:

$$\mathbf{4}:\ \ \square p\to\square\square p$$

with the schema consisting of one axiom for every well-formed formula (wff) $p$.

Using the standard labelling convention that is set out here, we get the logic S4, which is the version I have seen used most often, that adopts that axiom schema together with others (K, N, T).

The schema 4 allows unlimited numbers of $\square$ preceding a sub-wff in a wff.

If we wanted to limit the number of instances of $\square$ to say $n$, all we'd need to do is replace 4 by a different axiom schema of the form:

$$\mathbf{4}^*:s\ p\to\square s\ p$$

with the schema only including cases where $p$ is a formula that does not commence with $\square$ and $s$ is a sequence of between 1 and $n-1$ squares.

Such an axiom schema would allow us to increase the number of squares prefixing a non-squared wff from 1 up to any number up to and including $n$, but no further.

 

[nomadreid]

Thank you, Andrewkirk. That makes sense, and the idea can be extended to other types of restrictions. Very helpful.