2021

[1]Xinyu Wang

[1]School of Computer Science, Japan Advanced Institute of Science and
Technology, Asahidai 1–1, Nomi City, 923–1211, Ishikawa Prefecture, Japan

# Transfinite Modal Logic: a Semi-quantitative Explanation for Bayesian
Reasoning

<EMAIL_ADDRESS>*

###### Abstract

Bayesian reasoning plays a significant role both in human rationality and in
machine learning. In this paper, we introduce transfinite modal logic, which
combines modal logic with ordinal arithmetic, in order to formalize Bayesian
reasoning semi-quantitatively. Technically, we first investigate some
nontrivial properties of ordinal arithmetic, which then enable us to expand
normal modal logic’s semantics naturally and elegantly onto the novel
transfinite modal logic, while still keeping the ordinary definition of Kripke
models totally intact. Despite all the transfinite mathematical definition, we
argue that in practice, this logic can actually fit into a completely finite
interpretation as well. We suggest that transfinite modal logic captures the
essence of Bayesian reasoning in a rather clear and simple form, in
particular, it provides a perfect explanation for Sherlock Holmes’ famous
saying, “When you have eliminated the impossible, whatever remains, however
improbable, must be the truth.” We also prove a counterpart of finite model
property theorem for our logic.

###### keywords:

modal logic, ordinal arithmetic, Bayesian reasoning, Kripke model, regular
cardinal, Sherlock Holmes

##  1 Introduction

Bayes’ theorem, in spite of its seemingly simple mathematical form, not only
is undoubtedly one of the most essential foundations of statistics, but also
possesses extremely profound influence onto every corner of modern science
Freedman07 . The rule itself establishes one of the most popular philosophical
interpretations of probability, namely Bayesian probability, together with the
associative approach of Bayesian statistics deFinetti17 ; it has been
successfully applied so as to construct a universal science theory, the
Bayesian philosophy of science Sprenger19 ; and the recent boost of machine
learning in AI indispensably relies on Bayes’ rule as both theoretical basis
and practical guidance Bishop06 .

Logic, on the other hand, classically deals with prescribed truth values
without any room for randomness vanDalen04 . It may seem totally irrelevant to
probability. Nonetheless, if we admit that both probability and logic — or
even only either one out of them — is a universal feature of human being’s
intelligence, then these two flows of theories must intersect at some point
Audi98 . Admittedly, nowadays various types of probabilistic logics already
exist Nilsson86 ; Gilio05 ; Ognjanovic08 ; Nguyen19 , which extrinsically
merge the notion of probability into logical systems, for instance, by
extending the possible space of a formula’s truth value from only True and
False to ranging upon all the real numbers between $0$ and $1$ Nilsson93 ;
Biacino02 ; Dautovic21 . These kinds of logics could indisputably become
useful for their own purposes in practice, though from a metaphysical
perspective, they do not seem adequate for drawing a solid conclusion upon
fundamental relation between logic and probability. Ontologically, if logic
and probability are not two absolutely separated noumena, but instead
constitutionally connected with each other, then we should reasonably expect
that one notion can intrinsically arise from the other, without the need to
externally introduce any new concept Fitting04 .

After all, logic and probability are merely relevant to each other, but not
inclusive by any means, thus generally speaking, we cannot precisely capture
one concept entirely within the other Hodges97 . Indeed from the technical
aspect, the ordinary Kolmogorov probability axioms Durrett19 , which
comprehensively regulate every quantitative property of probability, do not
seem very feasible to be fully deduced out solely based on some usual logical
system. In this paper, however, we expand normal modal logic through
combination with ordinal arithmetic and yield a novel kind of transfinite
modal logic, whose interpretation provides a very interesting semi-
quantitative explanation for Bayesian reasoning. Our model still keeps exactly
the same as the traditional Kripke model, hence nothing new gets added
substantially and thus we actually succeed in characterizing a fragment of the
notion of probability internally from modal logic. Quite roughly speaking,
probability may also be viewed as a sort of modality, which essentially embeds
itself inside normal modal logic Pleasants09 : most commonly, $\Box\phi$ reads
as “$\phi$ is necessary”, but strictly speaking nothing is $100\%$ necessary
and so the reading may sound closer to “$\phi$ is almost necessary with
possibility near to $1$” Fan14 . We shall further elaborate on our whole
intuition in the rest of this paper.

Technically speaking, our transfinite modal logic depends on a few nontrivial
results about ordinal arithmetic, which we will detailedly develop and prove
in Section 5 as mathematical preliminaries before we introduce the whole
definition in Section 6. Later on we will also prove a counterpart of finite
model property theorem in Section 8, which further consummates and justifies
our logic. Although as its name suggests, transfinite modal logic involves
infinite ordinals, we argue that practically it can also be interpreted in a
finite manner. In Section 7 we will demonstrate how transfinite modal logic is
able to naturally explain Bayesian reasoning through a vivid example of
Sherlock Holmes.

The rest of this paper is organized as follows: Section 2 stipulates relevant
notational conventions throughout this paper; Section 3 introduces simple
transfinite modal logic as a sublanguage and then applies it to interpret
probability; Section 4 analyzes in detail how we should expand the modal
language so as to express dynamic Bayesian reasoning; Section 5 develops a few
nontrivial mathematical results about ordinal arithmetic, as a preparation for
defining duplex transfinite modal logic in the following Section 6; Section 7
demonstrates how Bayesian reasoning gets semi-quantitatively formalized by
transfinite modal logic with a well known example about Sherlock Holmes;
Section 8 proves a counterpart of finite model property theorem for the logic,
which also solidly guarantees a coherent theoretical background; Section 9 at
last briefly concludes the entire paper. Besides rigorous mathematical proofs
for those pivotal theorems, a handful of vivid examples as well as careful
remarks also scatter throughout this paper. Just as a piece of friendly
advice, we think examples and remarks are extremely helpful for explaining our
intuition behind the logic as clearly as possible, therefore, particular
attention on those texts is recommended for the sake of a smooth
understanding.

##  2 Notational Conventions

In this paper, we assume ZFC set theory Jech03  and adopt the following
notations:

  * •

$\subseteq$ is for subset (subclass) and $\subset$ is for proper subset
(subclass).

  * •

Ord is the class of ordinals.

  * •

Card is the class of cardinals. $\text{\bf Card}\subset\text{\bf Ord}$.

  * •

$\text{\bf InfCard}\subset\text{\bf Card}$ is the class of infinite cardinals.
InfCard is isomorphic to Ord, therefore, each $\aleph_{\alpha}\in\text{\bf
InfCard}$ is uniquely indexed by each $\alpha\in\text{\bf Ord}$.

  * •

Lowercase Greek letters
$\alpha,\beta,\gamma,\zeta,\eta,\theta,\rho,\sigma,\tau$ are used for
representing ordinals; $\kappa,\lambda$ for representing cardinals;
$\phi,\psi$ for representing formulae.

  * •

All kinds of arithmetic, including addition ($+$), multiplication ($\cdot$)
and exponentiation, are ordinal arithmetic. (i.e., they should never be
understood as cardinal arithmetic, even if both operands are cardinals.)

##  3 Simple Transfinite Modal Logic

To start with, we define simple transfinite modal logic in this section.
Syntactically, simple transfinite modal logic bears exactly the same language
as normal modal logic, while semantically its only modification is that, when
evaluating formula $\Box\phi$ on a Kripke model, cardinality gets taken into
consideration just by the most natural way that readers could possibly think
of.

######  Definition 1 (Language STML).

Let P be a non-empty set of propositions. Language STML is recursively defined
by the following Backus-Naur form, where $p\in\text{\bf P}$:

$\displaystyle\phi::=p\mid\neg\phi\mid(\phi\land\phi)\mid\Box\phi$

######  Definition 2 (Kripke Model).

A Kripke model $\mathcal{M}$ is a triple $(S,R,V)$ where:

  * •

$S$ is a non-empty set of possible worlds.

  * •

$R\subseteq S\times S$ is a binary relation over $S$.

  * •

$V:\text{\bf P}\to\mathcal{P}(S)$ is the valuation function.

A pointed (Kripke) model $\mathcal{M},s$ is a Kripke model $\mathcal{M}$ with
a possible world $s\in S$.

######  Definition 3 (Successor Cardinality of Pointed Model).

For any pointed model $\mathcal{M},s$, we define its successor cardinality as
$\kappa_{s}=\mid\\{t\in S:sRt\\}\mid$.

######  Remark 1.

Intuitively, “successor cardinality of pointed model $\mathcal{M},s$” in
Definition 3 is just the cardinality of successors of $s$.

######  Definition 4 (Semantics of STML).

For any pointed model $\mathcal{M},s$, semantics of language STML is
recursively defined as the following:

$\displaystyle\mathcal{M},s\vDash p\iff$ $\displaystyle s\in V(p)$
$\displaystyle\mathcal{M},s\vDash\neg\phi\iff$ $\displaystyle\text{not
}\mathcal{M},s\vDash\phi$ $\displaystyle\mathcal{M},s\vDash\phi\land\psi\iff$
$\displaystyle\mathcal{M},s\vDash\phi\text{ and }\mathcal{M},s\vDash\psi$
$\displaystyle\mathcal{M},s\vDash\Box\phi\iff$
$\displaystyle\left\\{\begin{array}[]{llll}\mid\\{t\in
S:sRt\land(\mathcal{M},t\vDash\phi)\\}\mid>&\\\ \mid\\{t\in
S:sRt\land\neg(\mathcal{M},t\vDash\phi)\\}\mid,&&&\text{if
}\kappa_{s}\in\text{\bf InfCard}\\\ \\\ \forall t\in S\text{ such that
}sRt,\mathcal{M},t\vDash\phi,&&&\text{otherwise}\end{array}\right.$

Readers should easily reason out that intuitively, semantics of $\Box\phi$ in
Definition 4 just says that when $s$ has infinite many successors, $\Box\phi$
holds on $s$ if and only if successors on which $\phi$ holds are more than
successors on which $\phi$ does not hold, namely, $\phi$ holds on almost all
the successors and so is almost necessary. The following Example 1 concisely
demonstrates such a case.

######  Example 1.

In this Kripke model $\mathcal{M}_{\ref{ex.sim}}$, from $s$ there is only one
successor on which $\neg p$ holds but $\aleph_{0}$ many successors on which
$p$ holds. Therefore we have $\mathcal{M}_{\ref{ex.sim}},s\vDash\Box p$,
simply ignoring the existence of that single $\neg p$ successor as it is
almost impossible.

$\textstyle{\mathcal{M}_{\ref{ex.sim}}}$$\textstyle{s\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\neg
p}$$\textstyle{p}$$\textstyle{p}$$\textstyle{\cdots}$$\textstyle{\aleph_{0}}$$\textstyle{\cdots}$$\textstyle{p}$$\textstyle{p}$

######  Remark 2.

A finitist might argue that in reality, every physical object is finite and
thus such a model in Example 1 should not be acceptable Ye11 . However, this
paper does not intend to survey on metaphysical problems in mathematical
philosophy, and here we make use of infinite cardinality simply as a
convenient tool for theoretical beauty; in fact as for practical usage, we
think it is perfectly okay to interpret $\aleph_{0}$ as certain sufficiently
large natural number $N\in\omega$, such that any common natural number, for
example $5$, $10$ or even $100$, is much smaller than $N$. Of course, it
depends on the specific situation in application to determine the actual upper
range of a “common” natural number, as well as how large $N$ must be in order
to be counted as “sufficiently” large. Furthermore, if $\aleph_{1}$ also
appears in the Kripke model, then it can be interpreted as an even larger
natural number $N^{\prime}\in\omega$, such that the result of any common
elementary arithmetic on $N$, for example $2N(=N+N)$ or $N^{2}(=N\cdot N)$, is
still much smaller than $N^{\prime}$.

As an analogy, readers are also suggested to recall the big O notation, which
is now commonly used for denoting the computational complexity of an algorithm
Sipser06 . Although in principal, the input scale of any computer algorithm
must be finite during a single run, the big O notation well captures the
algorithm’s approximate behaviour as long as the input scale is large enough
so as to be reasonably considered as almost infinite. Our idea here simply
resembles such an intuition. In short, we would recommend just freely choosing
to understand $\aleph_{0}$ in this paper at the ontological aspect either as
actual infinity or as certain sufficiently large natural number, whichever
could make readers more comfortable.

##  4 Toward Modal Logic for Bayesian Reasoning

Now that we have defined simple transfinite modal logic in Section 3, where
$\Box\phi$ holds on a possible world $s$ with infinite many successors if and
only if $\phi$ holds on almost all the successors of $s$, in other words, the
set of successors of $s$ on which $\phi$ does not hold must be smaller in
cardinality and thus comparatively negligible. Literally, this intuition is so
simple. Nevertheless, our final goal is to explain Bayesian reasoning with
modal logic, indicating that we have to deal with something like dynamic
belief revision Baltag08 ; vanBenthem09 , for instance, $\Box\phi$ holds a
priori and hence $\phi$ is almost necessary as the prior probability
distribution, but then upon obtaining new evidence, the posterior probability
distribution gets calculated according to Bayes’ rule and so $\Box\phi$ may
not hold any more. To provide a more specific context, suppose you have bought
a lottery and $\phi$ stands for that you do not win the first prize, then a
priori assertion of $\Box\phi$ could be reasonably drawn, but if you later
check the result and (very luckily!) find out that you really do win the first
prize, then the default $\Box\phi$ should now be rationally abandoned by
Bayesian reasoning.

Hence here follows the natural question: how should we model the dynamics of
Bayesian reasoning? Readers might quickly think of public announcement logic,
where update of information is achieved through deleting unwanted possible
worlds form the original Kripke model vanDitmarsch08 . Nevertheless, such kind
of approach now faces a serious endogenous difficulty: by deleting possible
worlds, the Kripke model inevitably gets smaller and smaller, but more
complicated new structures can never emerge. This feature may not present to
be a big problem for public announcement logic, which is intended to deal with
knowledge about the ultimately certain truth, however, it does not seem to fit
in well with Bayesian belief that could arbitrarily invert for (potentially)
infinite many times.

Therefore, we perceive that another natural approach is more plausible: just
like temporal logic for discrete time Goldblatt92 , the Kripke model is
generally stratified as a tree, and exploration over the next layer
corresponds to receiving new information and then adjusting the posterior
probability distribution by Bayesian reasoning. Intuitively, such modelling
indeed sounds quite similar to human being’s natural reasoning process. The
following Example 2 demonstrates such intuition with a very simple finite
model:

######  Example 2.

In this Kripke model $\mathcal{M}_{\ref{ex.fin}}$, by default namely among
children of $s$, there exist two possible worlds $t_{1}$ and $t_{2}$ on which
$p$ holds but only one possible world $t_{0}$ on which $\neg p$ holds, hence
representing that the prior probability distribution is $\Pr[p]=\frac{2}{3}$
and $\Pr[\neg p]=\frac{1}{3}$. However among grandchildren of $s$, namely
after one round of Bayesian update, we find out that there exist four
evidences to support $t_{0}$ but for either $t_{1}$ or $t_{2}$ there is only
one evidence, therefore, the posterior probability distribution should be
$\Pr_{\text{post}}[p]=\frac{2}{6}=\frac{1}{3}$ and $\Pr_{\text{post}}[\neg
p]=\frac{4}{6}=\frac{2}{3}$. The intuitive explanation being such in natural
language, however as a clarification, we do not expect our transfinite modal
logic expressive enough to be able to calculate out specific numerical values
of probability such as $\frac{1}{3}$ or $\frac{2}{3}$.

$\textstyle{\mathcal{M}_{\ref{ex.fin}}}$$\textstyle{s\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{t_{0}:\neg
p\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{t_{1}:p\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{t_{2}:p\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\neg
p}$$\textstyle{\neg p}$$\textstyle{\neg p}$$\textstyle{\neg
p}$$\textstyle{p}$$\textstyle{p}$

Take Example 2 as a reference, we are tempted to analogize that for
transfinite modal logic, since formula $\Box\phi$ expresses that $\phi$ is
almost necessary as of the prior probability distribution, that $\phi$ is
almost necessary as of the posterior probability distribution should then be
expressed by formula $\Box\Box\phi$ or something alike. This overall direction
does not seem too problematic, however, there remain a few essential technical
details with complexity, which require our very careful examination. Firstly
let us consider the following Example 3:

######  Example 3.

In this Kripke model $\mathcal{M}_{\ref{ex.inf}}$, the prior probability
distribution is that there are $\aleph_{0}$ many successors that satisfy $p$
while $\neg p$ only holds on a single successor $t_{0}$, hence $p$ is a priori
almost necessary, namely $\mathcal{M}_{\ref{ex.inf}},s\vDash\Box p$. However
later on, we newly acquire as many as $\aleph_{0}$ subsequent evidences to
support exactly the very branch of possibility $t_{0}$, while for any other
successor of $s$ only one following evidence gets provided. Hence intuitively,
by Bayesian reasoning we should infer that based on current information, the
posterior probability of $\neg p$ has now become comparable to probability of
$p$ and thus the possibility of $\neg p$ can no longer be neglected as almost
impossible.

$\textstyle{\mathcal{M}_{\ref{ex.inf}}}$$\textstyle{s\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{t_{0}:\neg
p\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{t_{1}:p\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{t_{3}:p\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\cdots}$$\textstyle{\aleph_{0}}$$\textstyle{\cdots}$$\textstyle{t_{4}:p\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{t_{2}:p\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\neg
p}$$\textstyle{\neg
p}$$\textstyle{\cdots}$$\textstyle{\aleph_{0}}$$\textstyle{\cdots}$$\textstyle{\neg
p}$$\textstyle{\neg
p}$$\textstyle{p}$$\textstyle{p}$$\textstyle{\cdots}$$\textstyle{\cdots}$$\textstyle{p}$$\textstyle{p}$

Such an intuition sounds quite plausible, but then how may we formally express
the above analysis by a modal logic formula? Notice that however, according to
the semantics defined in Definition 4, now we still have
$\mathcal{M}_{\ref{ex.inf}},s\vDash\Box\Box p$; in fact from the viewpoint of
$s$, $\Box\Box p$ differs from $\Box p$ in no way at all, as actually for any
successor $t\in S$ such that $sRt$, $\mathcal{M}_{\ref{ex.inf}},t\vDash\Box p$
if and only if $\mathcal{M}_{\ref{ex.inf}},t\vDash p$. If we take a closer
look into this issue, we may be able to recognize that roughly speaking, what
we really want to mean is not $\Box\Box p$, which essentially means $\Box(\Box
p)$ as its standard valuating order; instead, we want to mean $(\Box\Box)p$,
that is to say, firstly view $(\Box\Box)$ as an integrated modality
corresponding to the combined relation $(R\circ R)$. In fact, this exchange of
valuating order does not make any difference for normal modal logic, but here
it matters. For the sake of clarity, we shall denote this bundled modality as
a single notation $\boxbox$ in the rest of this paper. We would also like to
suggest denoting $\boxbox$ alternatively as $\Box^{2}$, a notation that can be
naturally generalized onto $\Box^{3}$ and so on, which are capable of
describing multiple steps of Bayesian reasoning. In this paper nevertheless,
we prefer neatly focusing on the general characters of transfinite modal logic
rather than diving into cumbersome details, so we shall restrict our following
discussion in the rest of this paper only up to $\Box^{2}$, i.e., $\boxbox$.
The technique for $\Box^{3}$ and others is simply similar in principle.

In a word, we conclude that in Example 3, we should have
$\mathcal{M}_{\ref{ex.inf}},s\vDash\neg\boxbox p$, although semantics of the
new modality $\boxbox$ still remains undefined, which constitutes our major
task at present. As suggested in Example 3, $\boxbox$ is meant nearly as
$(\Box\Box)$ for the combined relation $(R\circ R)$, whose semantics might
then be defined in the same way as Definition 4. Such definition approach,
however, causes serious flaws in philosophy, as the following Example 4
reveals:

######  Example 4.

In this Kripke model $\mathcal{M}_{\ref{ex.flaw}}$, the root $s$ is connected
to $\aleph_{0}$ many successors, each of which is just the same copy of the
pointed model $\mathcal{M}_{\ref{ex.sim}},s$ in Example 1. By symmetry, there
is no reason for us to anticipate an outcome different from Example 1, namely,
we should expect that $\mathcal{M}_{\ref{ex.flaw}},s\vDash\boxbox p$. However,
simply counting the cardinality of grandchildren of $s$ would lead to the
opposite statement $\mathcal{M}_{\ref{ex.flaw}},s\vDash\neg\boxbox p$, since
both grandchildren on which $p$ holds and grandchildren on which $\neg p$
holds are equally $\aleph_{0}$ in terms of cardinality. This conclusion is not
acceptable, as apparently there are much “more” chances of $p$ than $\neg p$
just from harmless intuition. An alternative viewpoint results into a very
strong objection as well: as discussed in Remark 2, suppose in practice,
$\aleph_{0}$ is actually interpreted as a synonym of certain natural number
$N\in\omega$ such that $N$ is far greater than $1$, but then $N^{2}$ should
also be far greater than $N$, thus the case of $p$ still bears much greater
possibility than the case of $\neg p$ and so is indeed almost necessary.

$\textstyle{\mathcal{M}_{\ref{ex.flaw}}}$$\textstyle{s\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{t_{0}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{t_{1}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\cdots}$$\textstyle{\aleph_{0}}$$\textstyle{\cdots}$$\textstyle{\neg
p}$$\textstyle{p}$$\textstyle{p}$$\textstyle{\cdots}$$\textstyle{\aleph_{0}}$$\textstyle{\cdots}$$\textstyle{p}$$\textstyle{p}$$\textstyle{\neg
p}$$\textstyle{p}$$\textstyle{p}$$\textstyle{\cdots}$$\textstyle{\aleph_{0}}$$\textstyle{\cdots}$$\textstyle{p}$$\textstyle{p}$$\textstyle{\cdots}$

Example 4 warns us that, essentially, flaws occur because cardinals are too
coarse-grained, so that cardinal-arithmetic square of $\aleph_{\alpha}$ still
equals $\aleph_{\alpha}$ for any $\aleph_{\alpha}\in\text{\bf InfCard}$
Kunen80 . Immediately, we get reminded of ordinals, which are finer-grained
than cardinals since $\alpha^{2}\neq\alpha$ for any $\alpha\in\text{\bf Ord}$
such that $\alpha>1$. It seems that ordinals are good candidate of replacement
for cardinals, but beware. Unlike cardinals, which can always yield an
absolute value for any fixed set, ordinals rely on well orders, which
originally do not exist in a Kripke model and we have never planned to extra
introduce from elsewhere, either. Such fact raises the major hurdle. Later on
in Section 6, we shall rigorously define the semantics of modality $\boxbox$,
and the accordingly expanded modal language is called duplex transfinite modal
logic. Notably, the Kripke model still keeps its original basic form as in
Definition 2. No extra well orders are introduced into the Kripke model, but
we manage to resolve the flaw in Example 4 with ingenious ordinal arithmetic.
Before introducing this duplex transfinite modal logic, nonetheless, several
crucial nontrivial results on ordinal arithmetic have to be firstly
established in the following Section 5.

##  5 Ordinal Arithmetic

###  5.1 Ordinal Logarithm

######  Lemma 1.

For any $\alpha,\beta\in\text{\bf Ord}$, if $0<\beta<\aleph_{\alpha}$, then
$\beta+\aleph_{\alpha}=\beta\cdot\aleph_{\alpha}=\aleph_{\alpha}$.

Proof: Since $\beta>0$, namely $\beta\geqslant 1$, obviously
$\beta+\aleph_{\alpha}\geqslant\aleph_{\alpha}$ and
$\beta\cdot\aleph_{\alpha}\geqslant\aleph_{\alpha}$.

To a contradiction suppose $\beta+\aleph_{\alpha}>\aleph_{\alpha}$, namely
$\aleph_{\alpha}\in\beta+\aleph_{\alpha}$. As $\aleph_{\alpha}$ is an infinite
cardinal, it is a limit ordinal, so
$\beta+\aleph_{\alpha}=\bigcup\limits_{\gamma<\aleph_{\alpha}}(\beta+\gamma)$,
and thus there exists $\gamma<\aleph_{\alpha}$ such that
$\aleph_{\alpha}\in\beta+\gamma$, namely $\beta+\gamma>\aleph_{\alpha}$, hence
$\mid\beta+\gamma\mid\geqslant\aleph_{\alpha}$. However, since
$\aleph_{\alpha}$ is a cardinal and $\beta,\gamma<\aleph_{\alpha}$,
$\mid\beta\mid,\mid\gamma\mid<\aleph_{\alpha}$, so
$\mid\beta+\gamma\mid=\max\\{\mid\beta\mid,\mid\gamma\mid\\}<\aleph_{\alpha}$,
a contradiction. Therefore $\beta+\aleph_{\alpha}=\aleph_{\alpha}$.

The case for multiplication is just similar.

######  Definition 5 (Relation $\sim_{\alpha}$).

Let $\alpha\in\text{\bf Ord}$ be fixed. For any $\beta,\gamma\in\text{\bf
Ord}$ such that $\beta>0\lor\gamma>0$, define $\beta\sim_{\alpha}\gamma$ iff
$\beta<\gamma\cdot\aleph_{\alpha}\land\gamma<\beta\cdot\aleph_{\alpha}$.
Besides, let $0\sim_{\alpha}0$.

######  Proposition 2.

For any fixed $\alpha\in\text{\bf Ord}$, $\sim_{\alpha}$ is an equivalence
relation over Ord.

Proof: Both reflexivity and symmetry of relation $\sim_{\alpha}$ are quite
straightforward to check. Cases concerning about $0$ are also rather trivial.
So focusing on transitivity, take arbitrary three ordinals
$\beta,\gamma,\zeta\neq 0$ such that
$\beta\sim_{\alpha}\gamma\land\gamma\sim_{\alpha}\zeta$. Thus
$\beta<\gamma\cdot\aleph_{\alpha}$ and $\gamma<\zeta\cdot\aleph_{\alpha}$, so
there exist $\eta,\theta<\aleph_{\alpha}$ such that $\beta<\gamma\cdot\eta$
and that $\gamma<\zeta\cdot\theta$, hence
$\beta<\zeta\cdot\theta\cdot\eta<\zeta\cdot\aleph_{\alpha}$. Similarly
$\zeta<\beta\cdot\aleph_{\alpha}$, therefore $\beta\sim_{\alpha}\zeta$.

######  Definition 6 (Equivalence Class ${[\beta]_{\alpha}}$ and Relation
$<$).

Let $\alpha\in\text{\bf Ord}$ be fixed. For any $\beta\in\text{\bf Ord}$, we
denote its corresponding equivalence class over Ord derived from relation
$\sim_{\alpha}$ as $[\beta]_{\alpha}=\\{\gamma\in\text{\bf
Ord}:\gamma\sim_{\alpha}\beta\\}$. We then naturally define relation $<$ over
the class of equivalence classes $\text{\bf Ord}/\sim_{\alpha}$: for any
$\beta,\gamma\in\text{\bf Ord}$, $[\beta]_{\alpha}<[\gamma]_{\alpha}$ iff
$\neg(\beta\sim_{\alpha}\gamma)\land\beta<\gamma$.

######  Proposition 3.

Relation $<$ is well defined in Definition 6, and is also a well order.

Proof: Obviously, this relation $<$ over $\text{\bf Ord}/\sim_{\alpha}$ just
reflects the original relation $<$ over Ord.

######  Lemma 4.

For any $\alpha,\beta\in\text{\bf Ord}$ such that $\alpha\geqslant 1$,
$\beta>1$, there uniquely exists a group of three ordinals
$\gamma,\zeta,\eta\in\text{\bf Ord}$ such that
$\alpha=\beta^{\gamma}\cdot\zeta+\eta$, $1\leqslant\zeta<\beta$,
$\eta<\beta^{\gamma}$.

Proof: For existence. Since $\beta>1$, power of $\beta$ has no upper bound.
Hence let $\gamma$ be the minimal ordinal such that $\alpha<\beta^{\gamma+1}$,
and as $\beta>1$, $\beta^{\gamma}\geqslant 1$. Then by ordinal division, there
uniquely exists a group of two ordinals $\zeta,\eta$ such that
$\alpha=\beta^{\gamma}\cdot\zeta+\eta$, $\eta<\beta^{\gamma}$. Suppose
$\zeta\geqslant\beta$, then
$\alpha=\beta^{\gamma}\cdot\zeta+\eta\geqslant\beta^{\gamma}\cdot\zeta\geqslant\beta^{\gamma}\cdot\beta=\beta^{\gamma+1}$,
a contradiction, so $\zeta<\beta$. Suppose $\zeta=0$, then
$\alpha=\beta^{\gamma}\cdot\zeta+\eta=\eta<\beta^{\gamma}$, and as
$\alpha\geqslant 1$, $\gamma>0$. If $\gamma$ is a successor ordinal, namely
there exists an ordinal $\theta$ such that $\gamma=\theta+1$, then
$\alpha<\beta^{\theta+1}$ but $\theta<\gamma$, a contradiction. If $\gamma$ is
a limit ordinal, then
$\alpha\in\beta^{\gamma}=\bigcup\limits_{\rho<\gamma}\beta^{\rho}$, so there
exists an ordinal $\theta<\gamma$ such that $\alpha\in\beta^{\theta}$, then
$\alpha<\beta^{\theta}<\beta^{\theta+1}$, a contradiction. So $\zeta\neq 0$,
therefore $1\leqslant\zeta<\beta$.

For uniqueness. Suppose there exist two groups of three ordinals
$\gamma_{1},\zeta_{1},\eta_{1}$ and $\gamma_{2},\zeta_{2},\eta_{2}$, such that
$\alpha=\beta^{\gamma_{1}}\cdot\zeta_{1}+\eta_{1}=\beta^{\gamma_{2}}\cdot\zeta_{2}+\eta_{2}$,
$1\leqslant\zeta_{1},\zeta_{2}<\beta$, $\eta_{1}<\beta^{\gamma_{1}}$,
$\eta_{2}<\beta^{\gamma_{2}}$. Hence
$\beta^{\gamma_{1}}\leqslant\alpha=\beta^{\gamma_{1}}\cdot\zeta_{1}+\eta_{1}<\beta^{\gamma_{1}}\cdot\zeta_{1}+\beta^{\gamma_{1}}=\beta^{\gamma_{1}}\cdot(\zeta_{1}+1)\leqslant\beta^{\gamma_{1}}\cdot\beta=\beta^{\gamma_{1}+1}$,
and similarly $\beta^{\gamma_{2}}\leqslant\alpha<\beta^{\gamma_{2}+1}$, so it
is easy to see $\gamma_{1}=\gamma_{2}$. Then by ordinal division,
$\zeta_{1}=\zeta_{2}$ and $\eta_{1}=\eta_{2}$.

######  Definition 7 (Ordinal Logarithm).

For any $\alpha,\beta\in\text{\bf Ord}$ such that $\alpha\geqslant 1$,
$\beta>1$, referring to Lemma 4, there unique exists $\gamma\in\text{\bf
Ord}$, which we denote as $\gamma=\log_{\beta}\alpha$.

######  Theorem 5.

Let $\alpha\in\text{\bf Ord}$ be fixed. For any $\beta,\gamma\in\text{\bf
Ord}$ such that $\beta,\gamma\geqslant 1$,
$[\beta]_{\alpha}<[\gamma]_{\alpha}\iff\log_{\aleph_{\alpha}}\beta<\log_{\aleph_{\alpha}}\gamma$.

Proof: By Lemma 4, there uniquely exist two groups of three ordinals
$\zeta,\eta,\theta$ and $\rho,\sigma,\tau$, such that
$\beta=\aleph_{\alpha}^{\zeta}\cdot\eta+\theta$,
$\gamma=\aleph_{\alpha}^{\rho}\cdot\sigma+\tau$,
$1\leqslant\eta,\sigma<\aleph_{\alpha}$, $\theta<\aleph_{\alpha}^{\zeta}$,
$\tau<\aleph_{\alpha}^{\rho}$. Therefore by also making use of Lemma 1:

$\displaystyle[\beta]_{\alpha}<[\gamma]_{\alpha}\iff$
$\displaystyle\beta\cdot\aleph_{\alpha}\leqslant\gamma$ $\displaystyle\iff$
$\displaystyle(\aleph_{\alpha}^{\zeta}\cdot\eta+\theta)\cdot\aleph_{\alpha}\leqslant\aleph_{\alpha}^{\rho}\cdot\sigma+\tau$
$\displaystyle\iff$
$\displaystyle\aleph_{\alpha}^{\zeta+1}\leqslant\aleph_{\alpha}^{\rho}\cdot\sigma+\tau$
$\displaystyle\iff$ $\displaystyle\zeta+1\leqslant\rho$ $\displaystyle\iff$
$\displaystyle\zeta<\rho$ $\displaystyle\iff$
$\displaystyle\log_{\aleph_{\alpha}}\beta<\log_{\aleph_{\alpha}}\gamma$

###  5.2 Transfinite Ordinal Addition

######  Definition 8 (Transfinite Ordinal Addition).

Let $\alpha\in\text{\bf Ord}$ be fixed, and $f_{\alpha}:\alpha\to\text{\bf
Ord}$ be a fixed function. For any $\beta\in\text{\bf Ord}$ such that
$\beta\leqslant\alpha$, we define $\sum\limits_{\beta}f_{\alpha}$ by
transfinite induction as the following:

  * •

If $\beta=0$, then let $\sum\limits_{0}f_{\alpha}=0$.

  * •

If $\beta$ is a successor ordinal, namely there exists an ordinal $\gamma$
such that $\beta=\gamma+1$, since $\beta\leqslant\alpha$, we have
$\gamma<\alpha$, namely $\gamma\in\alpha$, so let
$\sum\limits_{\beta}f_{\alpha}=(\sum\limits_{\gamma}f_{\alpha})+f_{\alpha}(\gamma)$.

  * •

If $\beta$ is a limit ordinal, then let
$\sum\limits_{\beta}f_{\alpha}=\bigcup\limits_{\gamma<\beta}(\sum\limits_{\gamma}f_{\alpha})$.

Finally, we denote $\sum\limits_{\alpha}f_{\alpha}$ simply as $\sum
f_{\alpha}$.

######  Definition 9 (Relation $<$).

Let $\alpha\in\text{\bf Ord}$ be fixed, and $f_{\alpha}:\alpha\to\text{\bf
Ord}$ be a fixed function. Define relation $<$ over the set
$\\{(\beta,\gamma):\beta\in\alpha,\gamma\in f_{\alpha}(\beta)\\}$ as the
following: for any
$(\beta_{1},\gamma_{1}),(\beta_{2},\gamma_{2})\in\\{(\beta,\gamma):\beta\in\alpha,\gamma\in
f_{\alpha}(\beta)\\}$, if $\beta_{1}\neq\beta_{2}$, then
$(\beta_{1},\gamma_{1})<(\beta_{2},\gamma_{2})$ iff $\beta_{1}<\beta_{2}$;
otherwise, $(\beta_{1},\gamma_{1})<(\beta_{2},\gamma_{2})$ iff
$\gamma_{1}<\gamma_{2}$.

######  Lemma 6.

Relation $<$ defined in Definition 9 is a well order isomorphic to $\sum
f_{\alpha}$.

Proof: It is not difficult to see that relation $<$ over the set
$\\{(\beta,\gamma):\beta\in\alpha,\gamma\in f_{\alpha}(\beta)\\}$ is a total
order. To show that it is also well founded, for any non-empty subset
$A\subseteq\\{(\beta,\gamma):\beta\in\alpha,\gamma\in f_{\alpha}(\beta)\\}$
such that $A\neq\emptyset$, let $A_{\beta}=\\{\beta\in\alpha:\exists\gamma\in
f_{\alpha}(\beta),(\beta,\gamma)\in A\\}$. Obviously
$A_{\beta}\subseteq\alpha$ and $A_{\beta}\neq\emptyset$, since ordinals are
well ordered, let $\beta_{0}\in A_{\beta}$ be the minimal element in
$A_{\beta}$, and let $A_{\gamma}=\\{\gamma\in
f_{\alpha}(\beta_{0}):(\beta_{0},\gamma)\in A\\}$. Obviously
$A_{\gamma}\subseteq f_{\alpha}(\beta_{0})$ and $A_{\gamma}\neq\emptyset$,
since ordinals are well ordered, let $\gamma_{0}\in A_{\gamma}$ be the minimal
element in $A_{\gamma}$. Then $(\beta_{0},\gamma_{0})\in A$, and it is easy to
reason that $(\beta_{0},\gamma_{0})$ is the minimal element in $A$. Hence
relation $<$ over the set $\\{(\beta,\gamma):\beta\in\alpha,\gamma\in
f_{\alpha}(\beta)\\}$ is well founded, so it is a well order.

In the following we show that the ordinal of well order relation $<$ over the
set $\\{(\beta,\gamma):\beta\in\alpha,\gamma\in f_{\alpha}(\beta)\\}$ is $\sum
f_{\alpha}$, by transfinite induction on $\alpha$:

  * •

If $\alpha=0$, namely $\alpha=\emptyset$ so obviously the set
$\\{(\beta,\gamma):\beta\in\alpha,\gamma\in f_{\alpha}(\beta)\\}=\emptyset$
and $\sum f_{\alpha}=0$.

  * •

If $\alpha$ is a successor ordinal, namely there exists an ordinal $\zeta$
such that $\alpha=\zeta+1$, let $g_{\zeta}:\zeta\to\text{\bf
Ord}=\\{(\beta,f_{\alpha}(\beta)):\beta\in\zeta\\}\subset f_{\alpha}$ be
another function, and by induction hypothesis we know that the ordinal of well
order relation $<$ over the set $\\{(\beta,\gamma):\beta\in\zeta,\gamma\in
g_{\zeta}(\beta)\\}$ is $\sum g_{\zeta}$. As the intuitive picture of addition
between two ordinals is just to put one well order after the other one so as
to together form a new well order, we know that the ordinal of well order
relation $<$ over the set $\\{(\beta,\gamma):\beta\in\alpha,\gamma\in
f_{\alpha}(\beta)\\}$ is $(\sum
g_{\zeta})+f_{\alpha}(\zeta)=(\sum\limits_{\zeta}f_{\alpha})+f_{\alpha}(\zeta)=\sum\limits_{\alpha}f_{\alpha}=\sum
f_{\alpha}$.

  * •

If $\alpha$ is a limit ordinal, for any ordinal $\zeta<\alpha$, let
$g_{\zeta}:\zeta\to\text{\bf
Ord}=\\{(\beta,f_{\alpha}(\beta)):\beta\in\zeta\\}\subset f_{\alpha}$ be
another function, and by induction hypothesis we know that the ordinal of well
order relation $<$ over the set $\\{(\beta,\gamma):\beta\in\zeta,\gamma\in
g_{\zeta}(\beta)\\}$ is $\sum g_{\zeta}$. As $\alpha$ is a limit ordinal, we
have the set $\\{(\beta,\gamma):\beta\in\alpha,\gamma\in
f_{\alpha}(\beta)\\}=\bigcup\limits_{\zeta<\alpha}\\{(\beta,\gamma):\beta\in\zeta,\gamma\in
f_{\alpha}(\beta)\\}=\bigcup\limits_{\zeta<\alpha}\\{(\beta,\gamma):\beta\in\zeta,\gamma\in
g_{\zeta}(\beta)\\}$, so the ordinal of well order relation $<$ over this set
is $\bigcup\limits_{\zeta<\alpha}(\sum
g_{\zeta})=\bigcup\limits_{\zeta<\alpha}(\sum\limits_{\zeta}f_{\alpha})=\sum\limits_{\alpha}f_{\alpha}=\sum
f_{\alpha}$.

######  Lemma 7.

Let $\aleph_{\alpha}$ be a fixed infinite regular cardinal. Let $\beta$ be any
fixed ordinal such that $\beta\leqslant\aleph_{\alpha}$, and
$f_{\beta}:\beta\to\aleph_{\alpha}$ be a fixed function. Then $\sum
f_{\beta}\leqslant\aleph_{\alpha}$.

Proof: It suffices to prove this statement only when $\beta$ is a limit
ordinal. To a contradiction suppose $\sum
f_{\beta}=\sum\limits_{\beta}f_{\beta}=\bigcup\limits_{\gamma<\beta}(\sum\limits_{\gamma}f_{\beta})>\aleph_{\alpha}$,
since ordinals are well ordered, there exists the minimal ordinal
$\gamma_{0}<\beta\leqslant\aleph_{\alpha}$ such that
$\sum\limits_{\gamma_{0}}f_{\beta}\geqslant\aleph_{\alpha}$. Obviously
$\gamma_{0}\neq 0$. If $\gamma_{0}$ is a successor ordinal, namely there
exists an ordinal $\zeta$ such that $\gamma_{0}=\zeta+1$, then
$\sum\limits_{\zeta}f_{\beta}<\aleph_{\alpha}$ and
$f_{\beta}(\zeta)<\aleph_{\alpha}$ but
$\sum\limits_{\gamma_{0}}f_{\beta}=(\sum\limits_{\zeta}f_{\beta})+f_{\beta}(\zeta)\geqslant\aleph_{\alpha}$,
a contradiction. If $\gamma_{0}$ is a limit ordinal, then
$\gamma_{0}<\aleph_{\alpha}$, and $\forall\zeta<\gamma_{0}$,
$\sum\limits_{\zeta}f_{\beta}<\aleph_{\alpha}$, but
$\sum\limits_{\gamma_{0}}f_{\beta}=\bigcup\limits_{\zeta<\gamma_{0}}(\sum\limits_{\zeta}f_{\beta})\geqslant\aleph_{\alpha}$,
contradicting that $\aleph_{\alpha}$ is a regular cardinal. Therefore $\sum
f_{\beta}\leqslant\aleph_{\alpha}$.

######  Theorem 8.

Let $\aleph_{\alpha}$ be a fixed infinite regular cardinal. Let $\beta$ be any
fixed ordinal such that $\beta\leqslant\aleph_{\alpha}$, and
$f_{\beta}:\beta\to(\aleph_{\alpha}+1)$ be a fixed function. Then $\sum
f_{\beta}=\aleph_{\alpha}^{2}$ iff
$\mid\\{\gamma\in\beta:f_{\beta}(\gamma)=\aleph_{\alpha}\\}\mid=\aleph_{\alpha}$.

Proof: Let $g_{\beta}:\beta\to(\aleph_{\alpha}+1)$ be another function such
that $\forall\gamma\in\beta$, $g_{\beta}(\gamma)=\aleph_{\alpha}\geqslant
f_{\beta}(\gamma)$. Then obviously $\sum f_{\beta}\leqslant\sum
g_{\beta}=\aleph_{\alpha}\cdot\beta\leqslant\aleph_{\alpha}^{2}$.

For the direction from right to left. As
$\\{\gamma\in\beta:f_{\beta}(\gamma)=\aleph_{\alpha}\\}\subseteq\beta$, we
have
$\mid\beta\mid\geqslant\mid\\{\gamma\in\beta:f_{\beta}(\gamma)=\aleph_{\alpha}\\}\mid=\aleph_{\alpha}$,
and because $\beta\leqslant\aleph_{\alpha}$, $\beta=\aleph_{\alpha}$. Relation
$<$ over the subset
$\\{\gamma\in\beta:f_{\beta}(\gamma)=\aleph_{\alpha}\\}\subseteq\beta$ is also
a well order with ordinal less than or equal to $\beta$, namely
$\aleph_{\alpha}$, and because
$\mid\\{\gamma\in\beta:f_{\beta}(\gamma)=\aleph_{\alpha}\\}\mid=\aleph_{\alpha}$,
the ordinal of well order relation $<$ over this set is $\aleph_{\alpha}$,
too. Thus consider the subset
$\\{(\gamma,\zeta):\gamma\in\beta,f_{\beta}(\gamma)=\aleph_{\alpha},\zeta\in
f_{\beta}(\gamma)\\}\subseteq\\{(\gamma,\zeta):\gamma\in\beta,\zeta\in
f_{\beta}(\gamma)\\}$, over which relation $<$ is also a well order with
ordinal $\aleph_{\alpha}^{2}$, hence by Lemma 6, $\sum f_{\beta}$ is the
ordinal of well order relation $<$ over the whole set
$\\{(\gamma,\zeta):\gamma\in\beta,\zeta\in f_{\beta}(\gamma)\\}$ and so $\sum
f_{\beta}\geqslant\aleph_{\alpha}^{2}$. Therefore $\sum
f_{\beta}=\aleph_{\alpha}^{2}$.

For the direction from left to right. To a contradiction suppose
$\mid\\{\gamma\in\beta:f_{\beta}(\gamma)=\aleph_{\alpha}\\}\mid<\aleph_{\alpha}$,
since $\aleph_{\alpha}$ is a regular cardinal, there exists an upper bound
ordinal $\eta\leqslant\beta\land\eta<\aleph_{\alpha}$ such that
$\forall\eta\leqslant\gamma<\beta$, $f_{\beta}(\gamma)<\aleph_{\alpha}$. By
Lemma 6, $\sum f_{\beta}$ is the ordinal of well order relation $<$ over the
set $\\{(\gamma,\zeta):\gamma\in\beta,\zeta\in
f_{\beta}(\gamma)\\}=\\{(\gamma,\zeta):\gamma<\eta,\zeta\in
f_{\beta}(\gamma)\\}\cup\\{(\gamma,\zeta):\eta\leqslant\gamma<\beta,\zeta\in
f_{\beta}(\gamma)\\}$, then by Lemma 7 and the intuitive picture of addition
between two ordinals, $\sum
f_{\beta}\leqslant\aleph_{\alpha}\cdot\eta+\aleph_{\alpha}=\aleph_{\alpha}\cdot(\eta+1)<\aleph_{\alpha}^{2}$,
a contradiction. Therefore
$\mid\\{\gamma\in\beta:f_{\beta}(\gamma)=\aleph_{\alpha}\\}\mid=\aleph_{\alpha}$.

######  Remark 3.

As a concluding remark of this section, the intuitive meaning of Theorem 8
says that, let $\aleph_{\alpha}$ be a fixed infinite regular cardinal, then in
order to reach $\aleph_{\alpha}^{2}$ in total sum by transfinitely adding no
more than $\aleph_{\alpha}$ many ordinals all of which are no greater than
$\aleph_{\alpha}$, on the one hand apparently, just adding together
$\aleph_{\alpha}$ many $\aleph_{\alpha}$s will work; on the other hand, this
is actually an indispensable requirement, namely, there must exist
$\aleph_{\alpha}$ many $\aleph_{\alpha}$s among all the addenda. Recall
Example 4, readers may speculate that Theorem 8 will play the crucial role of
converting between statements about cardinal $\aleph_{\alpha}$ and those about
ordinal $\aleph_{\alpha}^{2}$, while the former is absolute regardless of well
orders and the latter can be testified via ordinal logarithm by Theorem 5.
These mathematical results developed within this section will soon get
utilized in the following Section 6 so as to strictly define the semantics of
modality $\boxbox$ for duplex transfinite modal logic.

##  6 Duplex Transfinite Modal Logic

######  Assumption 1 (Regular Cardinality).

In the rest of this paper, we additionally assume that all the infinite
cardinals which we talk about are regular.

######  Remark 4.

Readers of course immediately notice that, the above Assumption 1 so obviously
aims at accommodating to Theorem 8, that at first glance it probably seems
abruptly artificial. Nevertheless, a while of calm analysis will convince
readers that such an assumption is actually reasonable and solid. In fact,
simply because the smallest irregular cardinal is $\aleph_{\omega}$, even
restricting our consideration about infinite cardinals only within this set
$\\{\aleph_{n}:n\in\omega\\}$ still provides us with countably many successive
infinite cardinals, which are already sufficient for any practical usage. From
another perspective, for now readers are suggested simply to put down this
concern anyway, because later on in Section 8, we shall be devoted to
mathematical work for showing Theorem 14 together with its following Corollary
15, which is a counterpart of regular finite model property theorem and
actually provides a pretty convincing explanation just for this Assumption 1.

######  Definition 10 (Language DTML).

Let P be a non-empty set of propositions. Language DTML is recursively defined
as the following Backus-Naur form, where $p\in\text{\bf P}$:

$\displaystyle\phi::=p\mid\neg\phi\mid(\phi\land\phi)\mid\Box\phi\mid\boxbox\phi$

Hence, STML is a sublanguage of DTML. Kripke models keep exactly the same as
originally defined in Definition 2. Therefore, we only have to supplement
semantics definition of the new modality $\boxbox$.

######  Definition 11 (Live Successor Cardinality of Pointed Model).

For any pointed model $\mathcal{M},s$, we define its live successor
cardinality as $\lambda_{s}=\mid\\{t\in S:sRt,\exists u\in S,tRu\\}\mid$.

######  Remark 5.

Intuitively, “live successor cardinality of pointed model $\mathcal{M},s$” in
Definition 11 in just the cardinality of live successors of $s$, i.e.,
successors which are not dead ends and possess some successor on their own. In
contrast with $\kappa_{s}$ in Definition 3 and Remark 1, here as for
$\lambda_{s}$, we must reasonably ignore those dummy successors which are no
longer succeeded by any of their own successors, because they have already
been ruled out as absolutely impossible in our posterior probability
distribution and thus will never be allocated any support of evidence, just
like explained in Example 3.

######  Definition 12 (Semantics of DTML).

Semantics of DTML extends semantics of STML in Definition 4 with the new
modality $\boxbox$. First, for any pointed model $\mathcal{M},s$, arbitrarily
fix a bijective function $f_{s}:\lambda_{s}\to\\{t\in S:sRt,\exists u\in
S,tRu\\}$. Next, for each possible world $t\in\\{t\in S:sRt,\exists u\in
S,tRu\\}$, arbitrarily fix a bijective function $g_{t}:\kappa_{t}\to\\{u\in
S:tRu\\}$. Define the following functions:

  * •

$h:\lambda_{s}\to\text{\bf Ord}$, $\forall\gamma\in\lambda_{s}$,
$h(\gamma)=\kappa_{f_{s}(\gamma)}$.

  * •

$h^{+}:\lambda_{s}\to\text{\bf Ord}$, $\forall\gamma\in\lambda_{s}$,
$h^{+}(\gamma)=$ the ordinal of well order relation under $g_{f_{s}(\gamma)}$
over the subset $\\{u\in
S:f_{s}(\gamma)Ru\land(\mathcal{M},u\vDash\phi)\\}\subseteq\\{u\in
S:f_{s}(\gamma)Ru\\}$.

  * •

$h^{-}:\lambda_{s}\to\text{\bf Ord}$, $\forall\gamma\in\lambda_{s}$,
$h^{-}(\gamma)=$ the ordinal of well order relation under $g_{f_{s}(\gamma)}$
over the subset $\\{u\in
S:f_{s}(\gamma)Ru\land\neg(\mathcal{M},u\vDash\phi)\\}\subseteq\\{u\in
S:f_{s}(\gamma)Ru\\}$.

The semantics of modality $\boxbox$ in language DTML is then defined as the
following:

$\displaystyle\mathcal{M},s\vDash\boxbox\phi\iff$
$\displaystyle\left\\{\begin{array}[]{llll}{[\sum h^{+}]}_{\zeta}>[\sum
h^{-}]_{\zeta},&&&\text{if }\mid\sum h\mid=\aleph_{\zeta}\in\text{\bf
InfCard}\\\ \\\ \forall t,u\in S\text{ s.t. }sRt\land
tRu,\mathcal{M},u\vDash\phi,&&&\text{otherwise}\end{array}\right.$

In Definition 12, functions $f_{s}$ and $g_{t}$ are allowed to be chosen
arbitrarily, hence we have to prove that Definition 12 is indeed well defined,
independent of choices on $f_{s}$ and $g_{t}$. But first let us briefly
explain the intuition. Complex as its form might seem, Definition 12
essentially manages to distinguish between finer-grained ordinals within the
classical Kripke model, where no information about any kind of well order
among successors of $s$ exists at all and thus only coarser-grained
cardinality is absolute. The serious philosophical flaw mentioned in Example 4
can then get favourably dissolved under our logic’s currently more advanced
resolution, which is able to achieve with the help of Theorem 5 and Theorem 8,
as readers will surely come to realize the whole vital mechanism through
rigorous proof for the following Proposition 9:

######  Proposition 9.

The semantics of modality $\boxbox$ is well defined in Definition 12, i.e., it
does not matter at all how we arbitrarily fix bijective functions $f_{s}$ and
$g_{t}$.

Proof: We only need to pay attention to the nontrivial case when $\mid\sum
h\mid=\aleph_{\zeta}$ and $\sum h^{+},\sum h^{-}\geqslant 1$. As
$\kappa_{t}\geqslant 1$ for all $t\in\\{t\in S:sRt,\exists u\in S,tRu\\}$, we
obviously have $\lambda_{s},\kappa_{t}\leqslant\aleph_{\zeta}$, thus $\sum
h,\sum h^{+},\sum h^{-}\leqslant\aleph_{\zeta}^{2}$, so
$\log_{\aleph_{\zeta}}(\sum h^{+}),\log_{\aleph_{\zeta}}(\sum h^{-})\leqslant
2$. By Theorem 5, $[\sum h^{+}]_{\zeta}>[\sum h^{-}]_{\zeta}$ iff
$\log_{\aleph_{\zeta}}(\sum h^{+})>\log_{\aleph_{\zeta}}(\sum h^{-})$. If
$\log_{\aleph_{\zeta}}(\sum h^{+})=1\land\log_{\aleph_{\zeta}}(\sum h^{-})=0$,
then $\mid\sum h^{+}\mid=\aleph_{\zeta}>\mid\sum h^{-}\mid$, and cardinality
will not vary with different functions $f_{s}$ and $g_{t}$. If
$\log_{\aleph_{\zeta}}(\sum h^{+})=2\land\log_{\aleph_{\zeta}}(\sum h^{-})<2$,
then by Theorem 8,
$\mid\\{\gamma\in\lambda_{s}:h^{+}(\gamma)=\aleph_{\zeta}\\}\mid=\aleph_{\zeta}\land\mid\\{\gamma\in\lambda_{s}:h^{-}(\gamma)=\aleph_{\zeta}\\}\mid<\aleph_{\zeta}$.
Similarly, cardinality will not vary with different functions $f_{s}$ and
$g_{t}$. Therefore, the semantics of modality $\boxbox$ in Definition 12 is
well defined. Now from Proposition 9 we know that $\boxbox$ is indeed a well
defined modality, but after all is it really a new modality? In fact in
Example 3, we have analyzed the close similarity on intuitions of modality
$\boxbox$ and two consecutive modalities $\Box\Box$, nevertheless, the
following Proposition 10 clearly claims their difference:

######  Proposition 10.

Generally speaking, neither of the following two formulae is valid:

$\displaystyle\boxbox\phi\to\Box\Box\phi$
$\displaystyle\Box\Box\phi\to\boxbox\phi$

Proof: Please cf. the following Example 5 and Example 6.

######  Example 5.

In this Kripke model $\mathcal{M}_{\ref{ex.2to11}}$, possible successor
$t_{1}$ gets a posteriori supported by $\aleph_{0}$ many new evidences, on all
of which $p$ holds. Now we have $\mathcal{M}_{\ref{ex.2to11}},s\vDash\boxbox
p\land\neg\Box\Box p$.

$\textstyle{\mathcal{M}_{\ref{ex.2to11}}}$$\textstyle{s\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{t_{0}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{t_{1}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\neg
p}$$\textstyle{p}$$\textstyle{p}$$\textstyle{\cdots}$$\textstyle{\aleph_{0}}$$\textstyle{\cdots}$$\textstyle{p}$$\textstyle{p}$

######  Example 6.

This Kripke model $\mathcal{M}_{\ref{ex.11to2}}$ is a reexamination of the
Kripke model $\mathcal{M}_{\ref{ex.inf}}$ in Example 3. Now we have
$\mathcal{M}_{\ref{ex.11to2}},s\vDash\neg\boxbox p\land\Box\Box p$.

$\textstyle{\mathcal{M}_{\ref{ex.11to2}}}$$\textstyle{s\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{t_{0}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{t_{1}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{t_{3}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\cdots}$$\textstyle{\aleph_{0}}$$\textstyle{\cdots}$$\textstyle{t_{4}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{t_{2}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\neg
p}$$\textstyle{\neg
p}$$\textstyle{\cdots}$$\textstyle{\aleph_{0}}$$\textstyle{\cdots}$$\textstyle{\neg
p}$$\textstyle{\neg
p}$$\textstyle{p}$$\textstyle{p}$$\textstyle{\cdots}$$\textstyle{\cdots}$$\textstyle{p}$$\textstyle{p}$

At last, we conclude this section by showing that this new modality $\boxbox$
successfully solves our target problem proposed in Example 4, as the following
Example 7 illustrates:

######  Example 7.

This Kripke model $\mathcal{M}_{\ref{ex.fix}}$ is a reexamination of the
Kripke model $\mathcal{M}_{\ref{ex.flaw}}$ in Example 4. Now we have
$\mathcal{M}_{\ref{ex.fix}},s\vDash\boxbox p\land\Box\Box p$, therefore, the
flaw in Example 4 has gotten fixed satisfactorily.

$\textstyle{\mathcal{M}_{\ref{ex.fix}}}$$\textstyle{s\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{t_{0}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{t_{1}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\cdots}$$\textstyle{\aleph_{0}}$$\textstyle{\cdots}$$\textstyle{\neg
p}$$\textstyle{p}$$\textstyle{p}$$\textstyle{\cdots}$$\textstyle{\aleph_{0}}$$\textstyle{\cdots}$$\textstyle{p}$$\textstyle{p}$$\textstyle{\neg
p}$$\textstyle{p}$$\textstyle{p}$$\textstyle{\cdots}$$\textstyle{\aleph_{0}}$$\textstyle{\cdots}$$\textstyle{p}$$\textstyle{p}$$\textstyle{\cdots}$

##  7 Sherlock Holmes’ Saying

We are now ready for an exciting application of transfinite modal logic as
explanation for Bayesian Reasoning: a perfect formalization of Sherlock
Holmes’ famous saying, “When you have eliminated the impossible, whatever
remains, however improbable, must be the truth.” Intuitively, in this scenario
a radical conversion happens: we drastically revise our belief from originally
thinking something improbable to finally assuring it as the only necessary
truth. Such intensive vibration does not seem usual in logic, but it does take
place so naturally in our daily life even if we are not a detective, for
instance as we have demonstrated, winning the first prize of a lottery. We
shall see that in transfinite modal logic, even stronger evidence is required
in order for the improbable as of the prior probability to become the
necessary as of the posterior probability, which definitely fits pretty well
with our intuition about how we overthrow an existing belief and establish the
opposite one.

######  Example 8.

In this Kripke model $\mathcal{M}_{\ref{ex.det}}$, where $i,j\in\omega$, for
the prior probability distribution there are $\aleph_{i}$ many supports for
$\neg p$ but only one support for $p$, hence by default $p$ is improbable,
namely $\mathcal{M}_{\ref{ex.det}},s\vDash\Box\neg p$. However at the next
time point, $\aleph_{j}$ many new evidences for $p$ are discovered while each
possible $\neg p$ branch is only assigned with one evidence, thus now it
settles on the comparison of magnitude between $i$ and $j$.

For one case suppose $i<j$, namely the new evidence is even stronger so as to
deny our a priori assumption, and accordingly by our Bayesian reasoning, we a
posteriori have $\mathcal{M}_{\ref{ex.det}},s\vDash\boxbox p$ in contrast.

$\textstyle{\mathcal{M}_{\ref{ex.det}}}$$\textstyle{s\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{p\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\neg
p\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\neg
p\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\cdots}$$\textstyle{\aleph_{i}}$$\textstyle{\cdots}$$\textstyle{\neg
p\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\neg
p\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{p\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{p\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\cdots}$$\textstyle{\aleph_{j}}$$\textstyle{\cdots}$$\textstyle{p\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{p\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\neg
p\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\neg
p\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\cdots}$$\textstyle{\cdots}$$\textstyle{\neg
p\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\neg
p\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\cdots}$$\textstyle{\cdots}$$\textstyle{\cdots}$

For another case suppose $i=j$, namely the new evidence is approximately of
the same weight as our default bias, then it is able to shock our original
belief but yet not strong enough to establish its own, hence we have
$\mathcal{M}_{\ref{ex.det}},s\vDash\neg\boxbox\neg p\land\neg\boxbox p$.
Nonetheless, as we indicate with dotted line in Kripke model
$\mathcal{M}_{\ref{ex.det}}$, if later on we continue obtaining more and more
new evidences supporting for $p$, we shall finally turn our belief completely
over. As mentioned in Example 3, although in this paper we do not formally
introduce more generalized modalities such as $\Box^{3}$ or $\Box^{4}$,
readers should be able to reasonably imagine that in such a condition we may
end with $\mathcal{M}_{\ref{ex.det}},s\vDash\Box^{3}p$. Of course on the other
hand, depending on the actual situation, it may also turn out that we later on
obtain more new evidences supporting for $\neg p$ and thus result in
$\mathcal{M}_{\ref{ex.det}},s\vDash\Box^{3}\neg p$.

For the final case suppose $i>j$, namely the new evidence is still too weak to
currently impose any visible impact, and so we keep holding
$\mathcal{M}_{\ref{ex.det}},s\vDash\boxbox\neg p$. Nevertheless, those
$\aleph_{j}$ many new evidences are never utterly useless: we may also imagine
that if in the next dotted round, so many possibilities for $\neg p$ even
become dead end that the total amount of evidences for $\neg p$ decreases to
$\aleph_{j}$ or even fewer, then these $\aleph_{j}$ many new evidences for $p$
will start to play their own role regarding $\Box^{3}$ formulae.

As a conclusion, we have fully learnt from the above Example 8 that it is the
relative magnitude between cardinals or ordinals, rather than their absolute
value, that ultimately matters to transfinite modal logic’s formulae.
Different relative magnitudes stand for different levels of strength of
evidence and can be quantitatively calculated and compared by modal formulae.
Therefore, although as mentioned in Example 2, transfinite modal logic is not
expressible enough for arbitrary specific value of probability between $0$ and
$1$, it is after all expressible to some extent for a certain degree of
quantitative computation on probability and thus we view it as a semi-
quantitative explanation for Bayesian reasoning.

##  8 “Finite” Model Property

We have already largely justified our transfinite modal logic’s soundness as
well as usefulness, through both conceptual analysis and specific examples.
Nevertheless just in case, extremely careful readers might still wonder that
our Assumption 1 looks more or less artificial anyway. Now in this section, we
offer a reconsideration of such an issue, and decide to settle on solving this
problem permanently via strict mathematical argument, as we have previously
forecast in Remark 4. In detail, we shall show that transfinite modal logic
enjoys a counterpart of finite model property: for any DTML formula $\phi$, if
$\phi$ is satisfiable in some Kripke model, then $\phi$ is also satisfiable in
a Kripke model with fewer than $\aleph_{\omega}$ many possible worlds. Of
course, since here infinity plays a crucial role in our logic, we do not
expect that $\phi$ can always be satisfied in some really finite Kripke model;
however, we shall prove that $\phi$ can always be satisfied in an
$\aleph_{n}$-large Kripke model, where $n\in\omega$, and as explained in
Remark 2, this may be understood simply as a counterpart of ordinary finite
model property theorem Libkin04 . Hence all in all, readers should be anyhow
convinced that Assumption 1 is actually reasonable, innocent and self-
consistent.

######  Definition 13 (Degree of Formula).

For any DTML formula $\phi$, its degree $\deg(\phi)\in\omega$ is recursively
defined as the following:

$\displaystyle\deg(p)=$ $\displaystyle 0$ $\displaystyle\deg(\neg\phi)=$
$\displaystyle\deg(\phi)$ $\displaystyle\deg(\phi\land\psi)=$
$\displaystyle\max\\{\deg(\phi),\deg(\psi)\\}$ $\displaystyle\deg(\Box\phi)=$
$\displaystyle\deg(\phi)+1$ $\displaystyle\deg(\boxbox\phi)=$
$\displaystyle\deg(\phi)+2$

######  Definition 14 (Walk in Kripke Model).

Let $\mathcal{M},s$ be a fixed pointed model. A walk starting from $s$ with
length $n\in\omega$ is a function $w_{n}:n\to S$ such that $sRw_{n}(0)$ if
$n>0$, and that for any $k\in\omega\land 0\leqslant k<n-1$,
$w_{n}(k)Rw_{n}(k+1)$.

######  Definition 15 (Unravelled Pointed Model).

Let $\mathcal{M},s$ be a fixed pointed model. For any $k\in\omega$, the
unravelled pointed model until depth $k$ is a pointed model
$\mathcal{M}_{k},\emptyset$, where $\mathcal{M}_{k}=(S_{k},R_{k},V_{k})$ and:

  * •

$S_{k}=\\{w_{n}:w_{n}$ is a walk starting from $s$ with length
$n\in\omega,n\leqslant k\\}$. $w_{0}=\emptyset\in S_{k}$.

  * •

For any $w_{m},w_{n}\in S_{k}$, where $m,n\in\omega\land m,n\leqslant k$,
$w_{m}R_{k}w_{n}$ iff $m+1=n\land w_{m}\subset w_{n}$.

  * •

For any $p\in\text{\bf P}$ and any $w_{n}\in S_{k}$, where $n\in\omega\land
n\leqslant k$, if $n=0$, then $w_{n}\in V_{k}(p)$ iff $s\in V(p)$; otherwise,
$w_{n}\in V_{k}(p)$ iff $w_{n}(n-1)\in V(p)$.

######  Proposition 11.

Let $\mathcal{M},s$ be a fixed pointed model. For any $k\in\omega$, the
unravelled pointed model $\mathcal{M}_{k},\emptyset$ is a tree with root
$\emptyset$ and maximal depth $k$, moreover, for any DTML formula $\phi$ such
that $\deg(\phi)\leqslant k$,
$\mathcal{M},s\vDash\phi\iff\mathcal{M}_{k},\emptyset\vDash\phi$.

Proof: Obvious. Therefore by Proposition 11, $\phi$ is satisfiable in some
Kripke model if and only if $\phi$ is satisfiable in some tree-like Kripke
model with maximal depth $\deg(\phi)$. Till now, our reasoning is no different
from usual standard proof of normal modal logic’s finite model property
Blackburn01 . However, presently this finite-depth tree-like Kripke model may
still bear arbitrarily large width, hence requiring our further treatment.

######  Proposition 12.

If P is finite, then for any $k\in\omega$, there exist only finite many
nonequivalent DTML formulae $\phi$ such that $\deg(\phi)\leqslant k$.

Proof: By induction on $k$, obvious.

######  Definition 16 (Modal Equivalence).

For any $k\in\omega$ and any $\alpha,\beta\in\text{\bf Ord}$, any two pointed
models $\mathcal{M},s$ and $\mathcal{N},w$ are $(k,\alpha,\beta)$-modal-
equivalent iff:

  * •

For any DTML formula $\phi$ such that $\deg(\phi)\leqslant k$,
$\mathcal{M},s\vDash\phi\iff\mathcal{N},w\vDash\phi$.

  * •

For any DTML formula $\phi$ such that $\deg(\phi)<k$, either one of the
following two cases holds:

    1. 1.

$\neg\exists t$, $t$ is a successor of $s$ and $\mathcal{M},t\vDash\phi$,
$\neg\exists v$, $v$ is a successor of $w$ and $\mathcal{N},v\vDash\phi$.

    2. 2.

$\exists t$, $t$ is a successor of $s$ and $\mathcal{M},t\vDash\phi$, $\exists
v$, $v$ is a successor of $w$ and $\mathcal{N},v\vDash\phi$, furthermore,
$\log_{\aleph_{\alpha}}\mid\\{t$ is a successor of
$s:\mathcal{M},t\vDash\phi\\}\mid=\log_{\aleph_{\beta}}\mid\\{v$ is a
successor of $w:\mathcal{N},v\vDash\phi\\}\mid$.

######  Lemma 13.

For any tree-like pointed models $\mathcal{M},s$ and $\mathcal{N},w$ and any
fixed $k\in\omega$, suppose $\mid\\{u:u$ is a successor of a successor of
$s\\}\mid=\aleph_{\alpha}\in\text{\bf InfCard}$, $\mid\\{r:r$ is a successor
of a successor of $w\\}\mid=\aleph_{\beta}\in\text{\bf InfCard}$, where
$\alpha,\beta\in\text{\bf Ord}$, for any successor $t_{0}$ of $s$,
$\log_{\aleph_{\alpha}}\mid\\{t$ is a successor of $s:\mathcal{M},t_{0}$ and
$\mathcal{M},t$ are $(k+1,\alpha,\alpha)$-modal-
equivalent$\\}\mid=\log_{\aleph_{\beta}}\mid\\{v$ is a successor of
$w:\mathcal{M},t_{0}$ and $\mathcal{N},v$ are $(k+1,\alpha,\beta)$-modal-
equivalent$\\}\mid$, and for any successor $v_{0}$ of $w$, vice versa. Then
for any DTML formula $\phi$ such that $\deg(\phi)\leqslant k$,
$\mathcal{M},s\vDash\boxbox\phi\iff\mathcal{N},w\vDash\boxbox\phi$.

Proof: This result is not difficult to observe from Definition 12.

######  Theorem 14.

If P is finite, then for any tree-like pointed model $\mathcal{M},s$, any
$k\in\omega$ and any $\alpha\in\text{\bf Ord}$, if $\mid\\{t\in
S:sRt\\}\mid\leqslant\aleph_{\alpha}$, then there exists $m\in\omega$ so that
for any $n\in\omega\land n\geqslant m$, there exists a tree-like pointed model
$\mathcal{N}_{n},w$ such that $\mathcal{M},s$ and $\mathcal{N}_{n},w$ are
$(k,\alpha,n)$-modal-equivalent and that size of Kripke model
$\mathcal{N}_{n}$ is smaller than $\aleph_{\omega}$.

Proof: By induction on $k$. When $k=0$, apparently keeping the single possible
world $s$ is enough for modal equivalence, so we focus on the inductive step
when $k>0$.

For one case, if $\mid\sum h\mid=\mid\\{u\in S:\exists t\in S,sRt\land
tRu\\}\mid=\aleph_{\beta}\in\text{\bf InfCard}$, where $\beta\in\text{\bf
Ord}$ and $h$ is defined as in Definition 12, then for any $t\in\\{t\in
S:sRt,\exists u\in S,tRu\\}$, we have $\\{u\in S:tRu\\}\subseteq\\{u\in
S:\exists t\in S,sRt\land tRu\\}$ so $\mid\\{u\in
S:tRu\\}\mid\leqslant\aleph_{\beta}$ and thus
$\log_{\aleph_{\beta}}\mid\\{u\in S:tRu\\}\mid\leqslant 1$. Therefore by
Proposition 12, there exist only finite many $(k-1,\beta,\beta)$-modal-
equivalence classes over the set $\\{\mathcal{M},t:t\in S,sRt\\}$. For every
such equivalence class, by induction hypothesis, there exists $m\in\omega$
with respect to arbitrary $\mathcal{M},t$ in this equivalence class,
$(k-1)\in\omega$ and $\beta\in\text{\bf Ord}$. Since there are only finite
many equivalence classes, we can take the largest $m_{0}\in\omega$ and so for
any $l\in\omega\land l\geqslant m_{0}$, any equivalence class and arbitrary
$\mathcal{M},t$ in the class, there exists a tree-like pointed model
$\mathcal{L}_{l},v$ such that $\mathcal{M},t$ and $\mathcal{L}_{l},v$ are
$(k-1,\beta,l)$-modal-equivalent and that size of Kripke model
$\mathcal{L}_{l}$ is smaller than $\aleph_{\omega}$.

Now we claim that $(m_{0}+3)\in\omega$ just satisfies this theorem regardless
of $\alpha$, hence for any fixed $\alpha\in\text{\bf Ord}$ such that
$\aleph_{\alpha}\geqslant\mid\\{t\in S:sRt\\}\mid$ and any fixed
$n\in\omega\land n\geqslant m_{0}+3$, we have to construct our target tree-
like pointed model $\mathcal{N}_{n},w$. To start with, there is only one
possible world $w$ as the tree root in Kripke model $\mathcal{N}_{n}$, with
the same propositional valuation as $s$. For each equivalence class, since
$\emptyset\subset\\{t\in S:\mathcal{M},t$ is in the equivalence
class$\\}\subseteq\\{t\in S:sRt\\}$, cardinality of this equivalence class
taking logarithm with respect to base $\aleph_{\alpha}$ will only result in
either $0$ or $1$. Moreover when $k>1$, it is easy to see that an equivalence
class contains either all live possible worlds (i.e. with some successor) or
all dead possible worlds (i.e. without any successor), and in the former case
since $\mid\\{t\in S:sRt,\exists u\in S,tRu\\}\mid\leqslant\mid\\{u\in
S:\exists t\in S,sRt\land tRu\\}\mid=\aleph_{\beta}$, cardinality of this
equivalence class taking logarithm with respect to base $\aleph_{\beta}$ will
only result in either $0$ or $1$, too. Let $l=n+1$ if $\alpha<\beta$, $l=n$ if
$\alpha=\beta$, $l=n-2$ if $\alpha>\beta$, in any case, $l\in\omega\land
l\geqslant m_{0}+1$. We then modify Kripke model $\mathcal{N}_{n}$ through the
following sequent procedure:

  1. 1.

Firstly, for each equivalence class whose logarithm with respect to
$\aleph_{\alpha}$ is $1$, we add $\aleph_{n}$ many independent copies of the
corresponding pointed model $\mathcal{L}_{l},v$ into Kripke model
$\mathcal{N}_{n}$ as the children of $w$.

  2. 2.

Secondly, if $k>1$, then for each remaining equivalence class such that it
contains live possible worlds and that its logarithm with respect to
$\aleph_{\beta}$ is $1$, we add $\aleph_{l}$ many independent copies of the
corresponding pointed model $\mathcal{L}_{l},v$ into Kripke model
$\mathcal{N}_{n}$ as the children of $w$. Temporarily take $c\in\omega$ just
for recording an ad hoc variable, if some equivalence class gets processed
within this step, we either let $c=l$ if this equivalence class has the same
cardinality as $\\{t\in S:sRt\\}$, or let $c=l+1$ otherwise; if no equivalence
class gets processed within this step, we let $c=m_{0}$.

  3. 3.

Thirdly, if $\\{t\in S:sRt\\}$ is infinite, then for each remaining
equivalence class whose cardinality is the same as $\\{t\in S:sRt\\}$, we add
$\aleph_{c}$ many independent copies of the corresponding pointed model
$\mathcal{L}_{l},v$ into Kripke model $\mathcal{N}_{n}$ as the children of
$w$.

  4. 4.

Finally, for each remaining equivalence class, we add only $1$ copy of the
corresponding pointed model $\mathcal{L}_{l},v$ into Kripke model
$\mathcal{N}_{n}$ as the child of $w$.

Obviously in the end, size of Kripke model $\mathcal{N}_{n}$ still keeps
smaller than $\aleph_{\omega}$. The whole constructive procedure may seem a
bit complex, nonetheless with particular carefulness and also using Lemma 13,
there actually does not present any principled difficulty in checking that
pointed models $\mathcal{M},s$ and $\mathcal{N}_{n},w$ are indeed
$(k,\alpha,n)$-modal-equivalent.

For another case, if $\\{u\in S:\exists t\in S,sRt\land tRu\\}$ is finite, the
construction is similar but even simpler, so we omit it here.

######  Corollary 15.

For any DTML formula $\phi$, $\phi$ is satisfiable in some Kripke model if and
only if $\phi$ is satisfiable in some Kripke model that is smaller than
$\aleph_{\omega}$.

######  Remark 6.

We conclude this section with a brief remark on the intuition of proof. As
explained in Example 3, modality $\boxbox$ is in fact “non-associative” from
consecutive $\Box\Box$, therefore in Definition 16, modal equivalence between
a pair of pointed models not only requires total agreement on truth values of
formulae as usual, but also demands further constraints so that such
equivalence relation is able to get preserved between their predecessors as
well. Such definition leads to Theorem 14, where kind of like downward
Löwenheim-Skolem theorem Marker02 , we manage to compress the Kripke model
into the scope smaller than $\aleph_{\omega}$. Essentially, since a fixed
finite formula has only finite length and finite many propositions in it, its
resolution should also be restricted within a finite level, hence it can
always be expressed inside the room below $\aleph_{\omega}$, a space vast
enough so as to dwell all the first countably many infinite regular cardinals.
In a word, although the Kripke model still has to be infinite most of the
time, from our discussion in Remark 2 readers can get enlightened that, if we
choose to interpret infinite cardinals as very large natural numbers instead
of actual infinity, it then sounds definitely plausible just to call Corollary
15 as “finite” model property. And therefore, readers could finally feel
completely relieved about our Assumption 1 with overall harmony.

##  9 Conclusions

In this paper, we introduce transfinite modal logic, which combines modal
logic with ordinal arithmetic, and apply it as a semi-quantitative explanation
for Bayesian reasoning through bountiful examples, especially including a
though formalization of the well-known Sherlock Holmes’ saying. The
philosophical intuition is rather clear and straightforward while the
technical details are quite nontrivial, and through proving a counterpart of
finite model property theorem we in turn justifies the philosophical
playground of our transfinite modal logic. As directions of future work, more
aspects of mathematical properties of this logic are to be considered, and we
may also compare it with other existing logics about cardinals and ordinals
Ding20 .

## Acknowledgments

The author would like to thank Satoshi Tojo for help on notations, Yang Song
for philosophical inspiration, and Hiroakira Ono for suggestions on
composition.

## References

  *   * (1) Freedman, D., Pisani, R. & Purves, R.  _Statistics_ (W.W. Norton & Company, New York & London, 2007).
  * (2) de Finetti, B.  _Theory of Probability: A critical introductory treatment_ (John Wiley & Sons Ltd, Chichester, 2017).
  * (3) Sprenger, J. & Hartmann, S.  _Bayesian Philosophy of Science_ (Oxford University Press, Oxford, 2019).
  * (4) Bishop, C. M.  _Pattern Recognition and Machine Learning_ (Springer Science+Business Media, New York, 2006).
  * (5) van Dalen, D.  _Logic and Structure_ (Springer-Verlag, Berlin, 2004).
  * (6) Audi, R.  _Epistemology: a comtemporary introduction to the theory of knowledge_ (Routledge, New York, 1998).
  * (7) Nilsson, N. J.  Probabilistic logic.  _Artificial Intelligence_ 28 (1), 71–87 (1986).  10.1016/0004-3702(86)90031-7 .
  * (8) Gilio, A.  Probabilistic logic under coherence, conditional interpretations, and default reasoning.  _Synthese_ 146 (1), 139–152 (2005).  10.1007/s11229-005-9080-y .
  * (9) Ognjanović, Z., Perović, A. & Rašković, M.  Logics with the qualitative probability operator.  _Logic Journal of the IGPL_ 16 (2), 105–120 (2008).  10.1093/jigpal/jzm031 .
  * (10) Nguyen, H. N. & Rakib, A.  Kraus, S. (ed.) _A probabilistic logic for resource-bounded multi-agent systems_.  (ed.Kraus, S.) _Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence, IJCAI-19_ , Vol. 28, 521–527 (International Joint Conferences on Artificial Intelligence Organization, Macao, 2019).
  * (11) Nilsson, N. J.  Probabilistic logic revisited.  _Artificial Intelligence_ 59 (1), 39–42 (1993).  10.1016/0004-3702(93)90167-A .
  * (12) Biacino, L. & Gerla, G.  Fuzzy logic, continuity and effectiveness.  _Archive for Mathematical Logic_ 41 (7), 643–667 (2002).  10.1007/s001530100128 .
  * (13) Šejla Dautović, Doder, D. & Ognjanović, Z.  Faber, W., Friedrich, G., Gebser, M. & Morak, M. (eds) _An epistemic probabilistic logic with conditional probabilities_.  (eds Faber, W., Friedrich, G., Gebser, M. & Morak, M.) _Proceedings of the 17th European Conference on Logics in Artificial Intelligence, JELIA 2021_ , Vol. 17, 279–293 (Springer Nature Switzerland AG, Klagenfurt, 2021).
  * (14) Fitting, M.  First-order intensional logic.  _Annals of Pure and Applied Logic_ 127 (1), 171–193 (2004).  10.1016/j.apal.2003.11.014 .
  * (15) Hodges, W.  _A shorter model theory_ (Cambridge University Press, Cambridge, 1997).
  * (16) Durrett, R.  _Probability: Theory and Examples_ (Cambridge University Press, Cambridge, 2019).
  * (17) Pleasants, N.  Wittgenstein and basic moral certainty.  _Philosophia_ 37 (4), 669 (2009).  10.1007/s11406-009-9198-0 .
  * (18) Fan, J., Wang, Y. & van Ditmarsch, H.  Goré, R., Kooi, B. & Kurucz, A. (eds) _Almost necessary_.  (eds Goré, R., Kooi, B. & Kurucz, A.) _Proceedings of the Tenth Conference on Advances in Modal Logic, AiML 2014_ , Vol. 10, 178–196 (College Publications, Groningen, 2014).
  * (19) Jech, T.  _Set Theory_ (Springer-Verlag, Berlin, 2003).
  * (20) Ye, F.  _Strict Finitism and the Logic of Mathematical Applications_ (Springer Science+Business Media, Dordrecht, 2011).
  * (21) Sipser, M.  _Introduction to the Theory of Computation_ (Thomson Course Technology, Boston, 2006).
  * (22) Baltag, A. & Smets, S.  Probabilistic dynamic belief revision.  _Synthese_ 165 (2), 179 (2008).  10.1007/s11229-008-9369-8 .
  * (23) van Benthem, J., Gerbrandy, J. & Kooi, B.  Dynamic update with probabilities.  _Studia Logica_ 93 (1), 67 (2009).  10.1007/s11225-009-9209-y .
  * (24) van Ditmarsch, H., van der Hoek, W. & Kooi, B.  _Dynamic Epistemic Logic_ (Springer, Dordrecht, 2008).
  * (25) Goldblatt, R.  _Logics of Time and Computation_ (Center for the Study of Language and Information, Stanford, 1992).
  * (26) Kunen, K.  _Set Theory: An Introduction to Independent Proofs_ (Elsevier Science B.V., Amsterdam, 1980).
  * (27) Libkin, L.  _Elements of Finite Model Theory_ (Springer-Verlag, Berlin, 2004).
  * (28) Blackburn, P., de Rijke, M. & Venema, Y.  _Modal Logic_ (Cambridge University Press, Cambridge, 2001).
  * (29) Marker, D.  _Model Theory: An Introduction_ (Springer-Verlag, New York, 2002).
  * (30) Ding, Y., Harrison-Trainor, M. & Holliday, W. H.  The logic of comparative cardinality.  _The Journal of Symbolic Logic_ 85 (3), 972–1005 (2020).  10.1017/jsl.2019.67 .