Better Understanding, Understanding Better Yu Wei Department of Philosophy East China Normal University Shanghai, China [email protected]
“Any fool can know; the point is to understand.” A well-known remark often attributed to Einstein captures a widely shared intuition: understanding is more than merely knowing. Yet epistemic logic has paid relatively little attention to understanding, despite its central role in contemporary epistemology, philosophy of science, and recent debates about AI. A recurring theme in the philosophical literature is that, unlike knowledge, understanding comes in degrees: one may understand something more or less well, and one’s understanding may be better than another’s. We introduce a comparative epistemic logic of understanding with graded modalities Uτi and a comparative connective (i ≻ j)ϕ for “i understands why ϕ better than j”. Semantically, we enrich multi-agent epistemic models with agent-indexed graded explanation structures and a justification-style term algebra. This yields a unified framework for representing minimal, ordinary, more demanding, and ideal understanding, together with comparisons between agents with respect to the same formula at issue. We distinguish a finitary bounded-level calculus from an infinitary full-language companion system. We establish soundness and strong completeness, and show that each fixed finite-level fragment is decidable.
1
Introduction
Why does the Earth orbit the Sun? This question can be simple enough for a classroom. A child may be credited with understanding why by giving a basic gravity story (e.g., “the Sun’s gravity keeps the Earth going around”); in another context, say in an undergraduate astrophysics seminar, that attribution may be withdrawn once stricter explanatory standards are imposed.1 The withdrawal does not mean “no understanding at all”: it means the required explanatory standard has shifted. The same pattern repeats at higher levels. An undergraduate physics student may count as understanding in a seminar, yet not in a panel of astrophysics experts discussing nearby phenomena. Again, the point is not that the student’s understanding evaporates. The point is that what it takes to qualify as understanding in that context is more epistemically demanding. This is exactly the phenomenon of understanding coming in degrees. As noted in [26], one prominent reason for distinguishing understanding from knowledge is that understanding is widely taken to admit degrees, whereas knowledge is typically not treated in this way. It already reveals the core logical issue of the present work. Besides, the same example also displays a comparative dimension. It is natural to say that some people understand why something is the case better than others. Two agents may both explain why the Earth orbits the Sun, yet one explanation can be deeper, more integrated, or more counterfactually robust. We therefore need to express not only whether an agent understands why a proposition holds, but also whether one agent understands it better than another. Modern epistemic logic has rich tools for knowledge and belief, but much less machinery for these two features taken together: degree-sensitive understanding and comparative understanding. This logical gap mirrors a deeper epistemological distinction: standard philosophical cases separate knowing from understanding. A child may know via testimony that faulty wiring caused a fire while 1 We borrow this example from [11].
M. Bílková, M. Gattinger, I. van der Giessen, M. Girlando, Y. Wang (Eds.): Advances in Modal Logic 2026 (AiML 2026) EPTCS 447, 2026, pp. 750–769, doi:10.4204/EPTCS.447.42
© Y. Wei This work is licensed under the Creative Commons Attribution License.
Y. Wei
751
lacking the ability to explain the relevant mechanism. A scientist may identify oxygen as a decisive factor in a reaction yet still lack understanding of why that dependence holds [24, 21]. These stories support, in particular, the contrast between knowing why and understanding why. They suggest not only a nonidentity claim: understanding is often taken to require explanatory grasp beyond merely possessing true information, and is therefore a richer epistemic achievement than bare knowing. Given this distinction and its epistemic significance, understanding is now a central topic in contemporary epistemology and philosophy of science rather than a marginal one [19, 4, 15]. The issue is equally salient in AI-facing debates. In the wake of large language models, disputes about whether, and in what sense, AI genuinely understands have moved to the center of discussion [23, 5]. Yet the pressure is not new: well before the recent LLM wave, authors had already noted that “understanding” is often invoked operationally without a stable theoretical account [29]. If formal epistemology is to contribute here, it must represent not only knowledge but also comparative understanding. There is also a historical reason to revisit the topic. Understanding was not alien to earlier logical traditions: medieval epistemic logic treated it as an epistemic mode in its own right [6, 7]. As Boh emphasizes, “the epistemic modality of understanding seems to be treated as even more basic than knowing or believing” [6, p. 100]. Our aim is to recover understanding as a formally disciplined notion within contemporary epistemic logic, while keeping close contact with current philosophical discussions. Formally, we build on [31, 35] by moving to a graded and comparative setting that integrates an epistemic base, a justification-style explanation algebra, and an explicit comparative connective within one framework.
1.1
Background and Related Work
Philosophers distinguish multiple uses of “understanding”: understanding-that, understanding-wh, and objectual understanding [14, 3]. Among these, understanding-wh (especially understanding-why) is often treated as the central case [20]. We follow this line and focus on understanding-why. A central philosophical thesis is that understanding is explanation-involving. Understanding why is widely characterized as “explanatory understanding”,2 which already signals this connection. Wilkenfeld argues that explanations are the kinds of things that bring about understanding [32], and Strevens puts the point succinctly: “No understanding without explanation” [27]. At the same time, theories of explanation differ sharply over what counts as explanans and explanatory support [17, 16, 25, 34]. For a logic with broad applicability, this suggests a methodological stance: explanatory structure should be represented abstractly enough to avoid commitment to any one substantive theory, but concretely enough for logical analysis. A nearby line treats understanding as involving compression: understanding is not a matter of storing a long list of disconnected facts, but of having a compact representation of relevant structure that can be used to recover relevant information about the target phenomenon [33, 8]. This point fits the present project well: useful compression must still retain enough information to support explanation, and the formal framework below will distinguish more specific explanations from coarser explanatory resources that may provide weaker support than their more specific counterparts. Recent epistemic logic has extensively studied non-standard knowledge operators (what/how/why, etc.); see [30]. A key predecessor for our setting is the logic of knowing why [35], which combines epistemic accessibility with explanation terms. Intuitively, agent i knows why p when i knows that p and has a uniform explanation witness that works across all i-accessible worlds. In this sense, knowing-why has an existential explanation profile, which can be rendered schematically as ∃t Ki (t : p) in a justification-style 2 For example, see [4, 20] and the bibliographies therein. We do not treat the “why” in “understanding why” as restrictive:
some cases are more naturally phrased as understanding how [20]. For example, one may say “understanding how the dinosaurs went extinct” rather than “understanding why they went extinct,” without intending any substantial difference.
752
Better Understanding, Understanding Better
metalanguage. Philosophically inspired by [21] and technically by [35], Wei [31] models understandingwhy via higher-order explanation, schematically ∃t1 ∃t2 Ki t2 : (t1 : ϕ) , where t1 : ϕ means that t1 is an explanation for ϕ, and t2 : (t1 : ϕ) means that t2 is a higher-order explanation of “t1 explains ϕ”. This logic thereby embodies the philosophical idea that understanding why requires at least two explanations at different levels, beyond what standard knowing-why requires. The present paper builds directly on this line. The predecessor captures the key insight that understanding requires higher-order explanatory support, but its formal architecture remains too coarse for a full hierarchy of explanatory depth and lacks an explicit comparative connective with a unified meta-theory. We therefore replace the packed operator with a level-indexed family, add a comparative connective, and use graded explanations in the semantics. Intuitively, higher grades mark explanations as eligible to support higher-level, and hence more demanding, understanding claims. This work is best read as a synthesis of epistemic, comparative, and justification-style ideas. At its base, the framework remains an epistemic logic in the strict technical sense: its semantics is based on multi-agent epistemic models, and modal interaction principles are developed inside that setting. In this respect, the project continues the “beyond knowing that” line in contemporary epistemic logic, but shifts the focus to understanding-why and comparative understanding. The language is also genuinely comparative, because it contains an explicit connective (i ≻ j)ϕ stating that agent i understands why ϕ better than j. Comparative modal work such as [9] already includes a comparative operator i ⪰ j to express that, locally at a given world, all formulas known by agent i are also known by agent j. In that framework, the global axiom scheme Ki ψ → K j ψ is replaced by a local inference-rule treatment. Our approach follows this local-comparative spirit, but with a different semantic source. The comparative clause is not a primitive relation-inclusion postulate; it is induced by explanation-sensitive understanding levels and evaluated relative to the formula at issue, with an epistemic side condition. This design has substantial technical consequences, developed in detail later. The semantic machinery also borrows core ingredients from justification logic: explanation terms, algebraic term operations, and admissibility constraints [13, 1, 2]. Earlier logics [35, 31] omit the sum operator +, understandably: a disjunctive or choice term can be too indeterminate to serve as a determinate “reason-why” witness in ordinary knowledge-why ascriptions. 3 The present framework nevertheless includes the full term algebra (·, +, !, c). For present purposes, + has a natural explanation-theoretic reading: t + s is available as an explanation of ϕ whenever either t or s is available. The compression perspective mentioned above explains why this operation should be treated with care. It does not require us to exclude +; rather, it shows that a sum term preserves only the fact that some explanation is available, while losing the information about which explanation supplies the support. For this reason, + is included, but it is strictly grade-downgrading. Thus the system is justification-style, but not a standard justification logic: the object language has no formulas of the form t : ϕ. Explanation terms enter only semantically, as graded witnesses governed by the agent-indexed functions Ei and the epistemic accessibility relations used for knowledge and comparison.
1.2
Framework and Contributions
We propose a comparative epistemic logic of understanding with two operator families: Uτi ϕ for levelindexed understanding-why and (i ≻ j)ϕ for comparative understanding with respect to a formula. At 3 For example, in a simple finite case, the agent may consider several possible causes of a forest fire: lightning, arson, an
unattended campfire, or a power-line fault. If each alternative has its own explanation term, repeated use of + can combine these terms into one disjunctive witness. This may provide a uniform witness across these alternatives, but the combined term no longer specifies which cause explains the fire at the actual world. See Xu et al. [35].
Y. Wei
753
the conceptual level, we take finite indices τ to range over N+ = {1, 2, 3, . . .}. This already lets the language capture the spectrum emphasized in [20]: minimal understanding < everyday understanding < typical scientist’s understanding < ideal understanding. Schematically, these may be represented by ω U1i ϕ, U2i ϕ, Um i ϕ, Ui ϕ. Level 1 is intended to model a minimal explanatory foothold (a necessary but not yet typical notion of understanding), while level 2 is intended to capture ordinary or everyday explanatory understanding in a higher-order sense [21, 31]. Some finite level m > 2 can then be used to represent typical scientific understanding. Higher levels correspond to explanations that are more systematically organized and more deeply integrated into scientific understanding. This level-sensitive hierarchy fits Khalifa’s spectrum picture, in which ideal understanding is a limit notion [20]. Formally, we capture that V limit by requiring every finite level: n∈N+ Uni ϕ. The numerical levels are a formal idealization. Finite indices on the understanding operators represent an ordered family of explanatory standards fixed in a model; a larger index marks a more demanding standard for the same formula. Depending on the application, such standards may concern specificity, systematic integration, or counterfactual robustness. The logic does not decide which substantive features make one standard stronger than another in every application; it only provides a framework for representing such standards once fixed. Meeting a stronger standard entails meeting weaker standards for the same formula, not possessing every particular explanation that might satisfy a weaker standard. Our main technical contributions are fourfold. First, we give a graded semantics for level-indexed and comparative understanding, with comparisons always relative to the formula at issue. Second, for each fixed finite understanding-level domain, we introduce a finitary calculus and establish soundness, strong completeness, and decidability. Third, for the full language, we move to an infinitary extension of the finitary calculus, reflecting the ideal-understanding level, and prove soundness and strong completeness. Fourth, we isolate the boundary between the bounded and full languages: in each fixed finite-level fragment the comparative connective is eliminable, while in the full language it is not; moreover, the full language is non-compact, so no sound finitary proof system can be strongly complete for it. The rest follows this architecture. Section 2 introduces syntax and semantics. Section 3 presents the calculi and soundness. Section 4 proves bounded and full completeness and gives a bounded decidability result. Section 5 concludes.
2
Syntax and Semantics
Definition 2.1. Given nonempty countable sets P of proposition letters and I of agents, and a nonempty understanding-level domain L ⊆ N+ ∪ {ω}, where N+ := {1, 2, 3, . . . }, the comparative epistemic language of understanding CELU(L) is defined by (where p ∈ P, i, j ∈ I, τ ∈ L): ϕ ::= p | ¬ϕ | (ϕ ∧ ϕ) | Ki ϕ | Uτi ϕ | (i ≻ j)ϕ. We use only these two instances in what follows: CELU := CELU(N+ ∪ {ω}),
CELUκ := CELU({1, . . . , κ}) (κ ⩾ 2).
Here τ is an understanding-level index. As explained above, finite indices on Uτi are intended to distinguish explanatory standards of different strength. Thus Uni ϕ says that agent i meets the nth such standard for understanding why ϕ. Note that we set Kyi ϕ in [35, 31] as U1i ϕ now, which can be read as minimal understanding.4 The formula Uω i ϕ expresses ideal understanding and is interpreted as “for all 4 It may be tempting to set K ϕ := U0 ϕ, i.e., knowledge is just level-0 understanding. However, our philosophical point is that i i understanding is more than knowledge, which does not require that Ki ϕ itself is already a very minimal form of understanding.
754
Better Understanding, Understanding Better
finite levels n, Uni ϕ”. By abuse of notation, we write U for the family of modalities Uτi . The comparative understanding formula (i ≻ j)ϕ indicates that agent i understands why ϕ better than agent j does. Informally, the bounded language CELUκ keeps comparatives but restricts all understanding-level indices to {1, . . . , κ}, so ideal and unbounded distinctions are not expressible. Technically, CELUκ is the base language for both the finitary calculus and the bounded decidability analysis. We accept the view in [35] that although something is a tautology, one may still lack minimal understanding (knowledge why) of that tautology. A special set of “self-evident” tautologies Λ is introduced, which the agent is assumed to minimally understand. For example, we can let all the instances of ϕ ∧ ψ → ϕ and ϕ ∧ ψ → ψ be Λ. Such simple choices will behave well in the bounded decidability argument below. At present, we do not suppose any necessitation rule for U in general. Definition 2.2. Fix a level domain L and the associated language CELU(L). A graded explanatory epistemic CELU(L)-model M is a tuple (W, {Ri | i ∈ I},V, E, gr, {Ei | i ∈ I}) where (W, {Ri | i ∈ I},V ) is a standard multi-agent epistemic model, i.e. for each i ∈ I, Ri is an equivalence relation on W , and: • E is a nonempty set of explanations, closed under ·, +, and !, and containing the constant c. • gr : E → N is a grade map. For each n ∈ N, let En := {t ∈ E | gr(t) ⩾ n}. The grade map satisfies: – gr(t · s) ⩾ min{gr(t), gr(s)}; – if min{gr(t), gr(s)} = 0 then gr(t + s) = 0; if min{gr(t), gr(s)} ⩾ 1 then gr(t + s) < min{gr(t), gr(s)}. – gr(!t) = 0 if gr(t) = 0, and gr(!t) = 2 if gr(t) ⩾ 1; – gr(c) = 1. • {Ei | i ∈ I} is a family of admissible explanation functions, each Ei : E × CELU(L) → 2W satisfies: Explanation Application Ei (t, ϕ → ψ) ∩ Ei (s, ϕ) ⊆ Ei (t · s, ψ). Explanation Sum Ei (t, ϕ) ∪ Ei (s, ϕ) ⊆ Ei (t + s, ϕ). Constant Specification If ϕ ∈ Λ, then Ei (c, ϕ) = W . Epistemic Introspection For all t ∈ E, Ei (t, Ki ϕ) ⊆ Ei (!t, Ki ϕ). The term operations ·, +, !, and the constant c are standard in justification logic. Application · combines explanations, + has the usual disjunctive or choice reading, ! represents positive introspection, and the constant c serves as a self-evident explanation for formulas in Λ. Unlike the models in [35, 31], every explanation term here also carries a grade. There is another generalization. In [35, 31], a single admissible explanation function, not indexed by agents, records for each term t and formula ϕ the worlds at which t explains ϕ. Here we replace that single function with an agent-indexed family {Ei }i∈I . Thus w ∈ Ei (t, ϕ) means that, at w, t is available as an explanation of ϕ for agent i. In this respect, the present model is more general: explanatory support can vary with the subject whose understanding is at issue. The grade constraint on + works together with the Sum condition on Ei . The Sum condition preserves availability: if either t or s explains ϕ for agent i at a world, then t + s does too. But the sum term t + s is less specific than either input, since it does not by itself specify whether t or s is the available explanation at that world. For this reason, + is strictly grade-lowering whenever the input minimum is positive. Grade-0 terms are allowed as closure-generated explanation terms. They belong to E0 , but not to any positive-grade class En = {t ∈ E | gr(t) ⩾ n} with n ⩾ 1. As the truth conditions below make explicit, grade-0 terms cannot support positive-level understanding claims. The first three conditions on Ei are standard. The fourth condition, Ei (t, Ki ϕ) ⊆ Ei (!t, Ki ϕ), requires a separate reading. Its source is the positive-introspection principle from justification logic. In standard
Y. Wei
755
justification logic, t : ϕ →!t : (t : ϕ) says that if t is a justification for ϕ, then !t is a justification for the claim that t justifies ϕ [12]. Intuitively, !t records a reflective confirmation of the justificatory status of t. The introspection condition uses this idea only for knowledge claims about the same agent. Suppose porb says that the Earth orbits the Sun. A request to explain why agent i knows porb is normally a request for i’s reasons or evidence for believing porb , not a request to explain why the Earth orbits the Sun. This is in line with the view that requests to justify knowledge claims commonly ask for the agent’s reasons or evidence [22]. In such cases, these reasons can play a justification-like explanatory role: an explanation of Ki ϕ gives the agent’s reasons or evidence for believing ϕ. The condition above says that whenever, at a world w, t is available to agent i as an explanation of Ki ϕ, the reflected term !t is also available to i at w as an explanation of the same knowledge claim. The point is not that !t adds another explanation of ϕ itself. Rather, !t makes explicit that i can cite t as the support for knowing ϕ. This should be read together with the grading rule for !: if gr(t) = 0 then gr(!t) = 0, while if gr(t) ⩾ 1 then gr(!t) = 2. Level 1 is minimal understanding, corresponding to knowing why; applied to Ki ϕ, it means that agent i has an explanation of why she knows ϕ. The term !t represents reflecting on that reason as her reason, so for own-knowledge claims level 2 marks this reflective grasp. Thus the semantic condition validates only the restricted introspection principle U1i Ki ϕ → U2i Ki ϕ: it is not a general mechanism for producing ever higher levels, does not validate Uni Ki ϕ → Un+1 Ki ϕ, and does not i apply to U1i K j ϕ → U2i K j ϕ for j ̸= i or to non-epistemic formulas. Definition 2.3 (Truth conditions). Fix a level domain L, a CELU(L)-model M , and let Lfin := L ∩ N+ . The satisfaction relation for CELU(L) is defined inductively as follows (for p ∈ P, i, j ∈ I, and n ∈ Lfin ): M ,w ⊨ p M , w ⊨ ¬ϕ M ,w ⊨ ϕ ∧ψ M , w ⊨ Ki ϕ M , w ⊨ Uni ϕ
⇔ ⇔ ⇔ ⇔ ⇔
M , w ⊨ Uω i ϕ M , w ⊨ (i ≻ j)ϕ
⇔ ⇔
w ∈ V (p) M , w ̸⊨ ϕ M , w ⊨ ϕ and M , w ⊨ ψ M , v ⊨ ϕ for all v such that wRi v (1) there exists t ∈ En such that for all v ∈ W with wRi v, v ∈ Ei (t, ϕ), (2) for all v ∈ W with wRi v, M , v ⊨ ϕ (if ω ∈ L) for all n ∈ Lfin , M , w ⊨ Uni ϕ (1) degi (w, ϕ) > deg j (w, ϕ), and (2) M , w ⊨ K j ϕ
where the understanding degree function is degi (w, ϕ) := sup {n ∈ Lfin | M , w ⊨ Uni ϕ} ∪ {0} . Thus degi (w, ϕ) is not a primitive measure, but the supremum of the finite levels at which i understands why ϕ at w. The existential quantifier in Uni ϕ is a witness condition: a level-n claim requires one and the same explanation term of grade at least n to be available at every i-accessible world. ω If ω ∈ / L, as in the bounded languages CELUκ , then Uω i ϕ is not a well-formed formula, so the U + ω clause is absent. In the full language CELU, where L = N ∪ {ω}, Ui ϕ expresses ideal understanding as the limit case requiring Uni ϕ for every n ∈ N+ . Equivalently, M , w ⊨ Uω i ϕ iff degi (w, ϕ) = ω. Although (i ≻ j)ϕ is primitive in the syntax, its semantic value is fixed by two independently defined notions: the induced degrees degi , deg j and the epistemic condition K j ϕ. The comparison is formularelative: it compares agents only with respect to the same ϕ, not globally. The truth condition states K j ϕ explicitly because degi (w, ϕ) > deg j (w, ϕ) ⩾ 0 already implies M , w ⊨ U1i ϕ, hence M , w ⊨ Ki ϕ. (i ≻ j)ϕ covers both cases where both agents understand ϕ but at different levels, and cases where i has minimal understanding while j merely knows ϕ. The latter remains a comparison within a shared epistemic issue: having an explanation already supports the ordinary judgment “I understand it better”.
756
Better Understanding, Understanding Better
m+1 Accordingly, for finite m with m, m + 1 ∈ Lfin , the conjunction Um ϕ isolates the exact i ϕ ∧ ¬Ui finite understanding degree m of agent i with respect to ϕ. Returning to the opening example, let porb ∈ P say that the Earth orbits the Sun, and let iC , iS , iR ∈ I denote the child, the student, and the researcher. In one natural formalization, a world w may satisfy 1 ⩽ degiC (w, porb ) < degiS (w, porb ) < degiR (w, porb ). Then M , w ⊨ (iS ≻ iC )porb and M , w ⊨ (iR ≻ iS )porb . If a bystander iB merely knows that porb while degiB (w, porb ) = 0, then M , w ⊨ (iC ≻ iB )porb holds.
Remark 2.4. (i ≻ j)ϕ becomes eliminable in the comparative-free fragment of CELUκ . That is, for every model ⟨M , w⟩ over level domain L = {1, . . . , κ}, M , w ⊨ (i ≻ j)ϕ ⇐⇒ M , w ⊨ K j ϕ ∧
κ _
m Um i ϕ ∧ ¬U j ϕ .
m=1
Proposition 2.5. In CELU, the (i ≻ j)ϕ is in general not eliminable by any comparative-free formula. Proof. It suffices to show non-eliminability for one instance, say (i ≻ j)p. Suppose χ is a comparativefree formula. Since χ contains only finitely many finite understanding-level indices, let n be greater than all those indices. Take two pointed models (M , w) and (M ′ , w′ ), each with just one world, with the same valuation, in particular with p true. All accessibility relations are reflexive, so K j p holds at both points. Specify the explanation functions by putting w ∈ Ei (ti , p), w ∈ E j (t j , p), w′ ∈ Ei′ (ti , p), and w′ ∈ E j′ (t j , p), and by adding only what is required by the admissibility clauses. Write gr and gr′ for the grade maps of M and M ′ , respectively, and let the only relevant difference be the grades: gr(ti ) = n, gr′ (ti ) = n + 1, and gr(t j ) = gr′ (t j ) = n. Choose the remaining grades so that all generated terms have bounded grade; hence every Uω -formula is false at both points. Then degi (w, p) = n, degi (w′ , p) = n + 1, and deg j (w, p) = deg j (w′ , p) = n. The two points satisfy the same comparative-free formulas whose finite indices are below n: this is proved by induction on formulas, with the Um k case using the same ω available witnesses, if any, for every m < n, and with the U case handled by the preceding boundedness observation. Hence M , w ⊨ χ ⇐⇒ M ′ , w′ ⊨ χ. But M , w ̸⊨ (i ≻ j)p, and M ′ , w′ ⊨ (i ≻ j)p. Below we show that the full language CELU is non-compact. Proposition 2.6. Fix distinct agents i ̸= j and an atom p. Let Σ≻ := {(i ≻ j)p} ∪ {Unj p | n ∈ N+ }. Then every finite subset of Σ≻ is satisfiable over CELU-models, but Σ≻ itself is unsatisfiable. Proof sketch. For any finite ∆ ⊆ Σ≻ , let m be the largest n such that Unj p ∈ ∆. Then a one-state model with p true, reflexive accessibility, and deg j (w, p) = m < m + 1 = degi (w, p) satisfies ∆ and (i ≻ j)p. If M , w ⊨ Unj p for all n ⩾ 1, then deg j (w, p) = sup {n | M , w ⊨ Unj p}∪{0} = ω. So M , w ⊨ (i ≻ j)p is impossible, since it requires degi (w, p) > deg j (w, p) = ω. Hence Σ≻ is unsatisfiable. Therefore, no finitary proof system over CELU can be both sound and strongly complete. As in [35, 31], explanation factivity, defined below, is not built into the model definition. Definition 2.7. Fix a level domain L and a CELU(L)-model M . We say that M has explanation factivity if whenever w ∈ Ei (t, ϕ) for some i ∈ I and t ∈ E, then M , w ⊨ ϕ. Given a CELU(L)-model M = (W, {Ri | i ∈ I},V, E, gr, {Ei | i ∈ I}), define its factive companion M F = (W, {Ri | i ∈ I},V, E, gr, {EiF | i ∈ I}) by EiF (t, ϕ) = Ei (t, ϕ)\{w | M , w ̸⊨ ϕ}. By direct checking, M F is again a CELU(L)-model. The proposition below asserts that CELU(L)-truth is invariant under this factive transformation. The proof is routine and omitted for reasons of space. Proposition 2.8. For any CELU(L)-formula ϕ and any w ∈ W , M , w ⊨ ϕ ⇔ M F , w ⊨ ϕ.
Y. Wei
3
757
Axiomatization
We present two related systems over two aligned languages: the bounded finitary calculus SCUκ for CELUκ , and the infinitary system SCU for CELU. Definition 3.1 (Finitary calculus). Fix κ ⩾ 2. Let SCUκ be the finitary Hilbert system over CELUκ whose axiom schemas are (where i, j, k ∈ I, and understanding-level indices range over L = {1, . . . , κ}): (TAUT) Propositional tautologies (DISTK) Ki (ϕ → ψ) → (Ki ϕ → Ki ψ) (T) Ki ϕ → ϕ (4) Ki ϕ → Ki Ki ϕ (5) ¬Ki ϕ → Ki ¬Ki ϕ (DISTU) Uni (ϕ → ψ) → (Uni ϕ → Uni ψ) (DEG) (UYK) ∗
(4 ) (KYU) (UYC0) (UYC) (CMPn) (CMP1) (CMPκ)
Uni ϕ → Um i ϕ n Ui ϕ → Ki ϕ Uni ϕ → Ki Uni ϕ U1i Ki ϕ → U2i Ki ϕ U1i ϕ ∧ K j ϕ ∧ ¬U1j ϕ → (i ≻ j)ϕ Uni ϕ ∧ Umj ϕ ∧ ¬Um+1 ϕ → (i ≻ j)ϕ j n n+1 (i ≻ j)ϕ ∧ U j ϕ → Ui ϕ (i ≻ j)ϕ → U1i ϕ ∧ K j ϕ (i ≻ j)ϕ → ¬Uκj ϕ.
(n ∈ L) (n, m ∈ L, n > m) (n ∈ L) (n ∈ L)
(n, m, m + 1 ∈ L, n > m) (n, n + 1 ∈ L)
The inference rules are: (MP) Modus Ponens (N) ⊢ ϕ/ ⊢ Ki ϕ (NE) ϕ ∈ Λ/ ⊢ U1i ϕ The axiom (KYU) captures a restricted introspective step: from level-1 understanding of why agent i knows ϕ, agent i can move to level-2 understanding of that same knowledge claim by reflecting on her own reason for knowing ϕ. It is the proof-theoretic counterpart of the semantic epistemic introspection condition on Ei . Axiom (CMPκ) records the upper bound of the finite language CELUκ : if i understands ϕ better than j, then j cannot already satisfy the top available level κ.In the full system below, it is replaced by (CMPω), which plays the same role for ideal understanding. Definition 3.2 (Full calculus). The system SCU over CELU is the ω-companion of SCUκ : it has the same finitary schemas/rules as Definition 3.1 with all finite level indices ranging over N+ , except that the finite-language upper-bound axiom (CMPκ) is replaced by (CMPω) (i ≻ j)ϕ → ¬Uωj ϕ, and it additionally includes the following axiom schema: n + (DEGnω ) Uω i ϕ → Ui ϕ (n ∈ N ),
and the following infinitary rule schema: (ωI)
{χ → K j1 (θ1 → · · · K jm (θm → Uni ϕ) · · · ) | n ∈ N+ } . χ → K j1 (θ1 → · · · K jm (θm → Uω i ϕ) · · · )
758
Better Understanding, Understanding Better
Here m ⩾ 0, j1 , . . . , jm ∈ I, and θ1 , . . . , θm ∈ CELU. If m = 0, the rule is read without any outer Koperators, i.e., {χ → Uni ϕ | n ∈ N+ }/(χ → Uω i ϕ). If m = 1 and θ1 = ⊤, the rule includes the instance n + ω {χ → K j Ui ϕ | n ∈ N }/(χ → K j Ui ϕ). That is, under the same assumption χ, if j knows that i has understanding of ϕ at every finite level, then j also knows that i has ideal understanding of ϕ. Thus m > 0 makes the same limit step available inside epistemic implication contexts. Since ω-introduction is an infinitary rule with countably many premises, we represent derivability of system SCU by well-founded proof trees, following the treatment of infinitary formal proofs in [18]. Definition 3.3 (SCU-derivability). A proof tree from Σ is a well-founded tree whose nodes are labeled by formulas. Each node is either an assumption leaf (label in Σ), an axiom leaf (instance of a SCU-axiom), or is obtained by one of the following rules: • (MP): from children labeled ψ → χ and ψ, conclude χ; • (NE): conclude U1i ψ for ψ ∈ Λ; • (N): from one closed child labeled ψ, conclude Ki ψ; • (ωI): for m ∈ N, from children labeled χ → K j1 (θ1 → · · · K jm (θm → Uni ψ) · · · ), one for each n n ∈ N+ , conclude the corresponding formula with Uω i ψ in place of Ui ψ; where “closed” means that the corresponding subtree has no assumption leaves. We write Σ ⊢SCU ϕ iff there exists such a proof tree with root label ϕ. A set Σ is SCU-consistent iff Σ ⊬SCU ⊥. Lemma 3.4. If Σ ⊢SCU ψ and Σ ∪ {ψ} ⊢SCU χ, then Σ ⊢SCU χ. Proof. Graft a fresh copy of a proof tree of ψ from Σ onto each assumption leaf labeled ψ in a proof tree of χ from Σ ∪ {ψ}, leaving all other nodes unchanged and preserving the original rule applications. The result is a proof tree from Σ. The only point requiring checking is the requirement in (N) that its premise child be closed: this is preserved because a closed child subtree contains no assumption leaves, so no grafting takes place inside it. Well-foundedness is also preserved: any descending chain either stays in the original tree or eventually enters a single grafted copy, both of which are well-founded. Lemma 3.5. If Σ ⊬SCU ϕ, then Σ ∪ {¬ϕ} is SCU-consistent. Proof. Suppose that Σ ∪ {¬ϕ} ⊢SCU ⊥. By induction on proof trees, we first obtain: if Σ ∪ {α} ⊢SCU β , then Σ ⊢SCU α → β . The finitary cases are standard. For an ω-introduction instance, write its premises as χ → Bn (n ∈ N+ ) and its conclusion as χ → Bω , where Bω is obtained from Bn by replacing the displayed Uni ψ with Uω i ψ. By the induction hypothesis, Σ ⊢SCU α → (χ → Bn ) for all n. Hence Σ ⊢SCU (α ∧ χ) → Bn for all n, so (ωI) gives Σ ⊢SCU (α ∧ χ) → Bω , and therefore Σ ⊢SCU α → (χ → Bω ). Then we get Σ ⊢SCU ¬ϕ → ⊥, therefore Σ ⊢SCU ϕ, contradicting the hypothesis. So Σ ∪ {¬ϕ} is consistent. The next derived principles are useful later in the completeness proofs. They also show that the formula (i ≻ j)ϕ behaves like a strict comparison: irreflexivity, transitivity, and asymmetry follow from the axioms connecting comparison with level-indexed understanding. For the full system, we also derive the ideal-level analogues of the epistemic principles for understanding formulas. Proposition 3.6. The following principles are provable in the indicated systems: (5∗ ) ¬Uni ϕ → Ki ¬Uni ϕ ω (5∗ω ) ¬Uω i ϕ → Ki ¬Ui ϕ
(TRANS) (i ≻ j)ϕ ∧ ( j ≻ k)ϕ → (i ≻ k)ϕ
ω (4∗ω ) Uω i ϕ → Ki Ui ϕ
(IRREF) ¬(i ≻ i)ϕ (ASYM) (i ≻ j)ϕ → ¬( j ≻ i)ϕ
Here (5∗ ), (IRREF), (TRANS), and (ASYM) are provable in both SCUκ and SCU; for (5∗ ), n ∈ {1, . . . , κ} in SCUκ and n ∈ N+ in SCU. (4∗ω ) and (5∗ω ) are provable in SCU.
Y. Wei
759
Proof. The derivation of (5∗ ) is routine from (T), (5), (4∗ ) together with classical reasoning. In SCU, n + (DEGnω ) and (4∗ ) give Uω i ϕ → Ki Ui ϕ for every n ∈ N . By modal reasoning, these yield the premises n ω ω Uω i ϕ → Ki (⊤ → Ui ϕ) of the m = 1 instance of (ωI), which gives Ui ϕ → Ki (⊤ → Ui ϕ), and hence ∗ ∗ ∗ (4ω ). Then (5ω ) follows by the same argument as (5 ). Given (IRREF) and (TRANS), the derivation of (ASYM) is routine. For (IRREF) in SCUκ : (i ≻ i)ϕ → U1i ϕ m+1 (i ≻ i)ϕ ∧ Um ϕ i ϕ → Ui κ (i ≻ i)ϕ → Ui ϕ (i ≻ i)ϕ → ¬Uκi ϕ ¬(i ≻ i)ϕ
(1) (2m ) (3) (4) (5)
(CMP1) (CMPn) (1 ⩽ m < κ) (1), (2m ), induction on m (1 ⩽ m < κ) (CMPκ) (3), (4), classical reasoning
For (TRANS) in SCUκ , write A := (i ≻ j)ϕ ∧ ( j ≻ k)ϕ and B := (i ≻ k)ϕ. Then: (1) (2) (3)
A → ¬Uκk ϕ A → U1i ϕ ∧ Kk ϕ A ∧ ¬U1k ϕ → B
(CMPκ), propositional reasoning (CMP1), propositional reasoning (2), (UYC0)
(4m ) (5m ) (6m ) (7m ) (8m ) (9m )
m+1 ( j ≻ k)ϕ ∧ Um ϕ k ϕ → Uj m+1 m Uj ϕ → Uj ϕ (i ≻ j)ϕ ∧ Umj ϕ → Um+1 ϕ i m+1 m A ∧ Uk ϕ → Ui ϕ m+1 A ∧ Um ϕ →B k ϕ ∧ ¬Uk m A ∧ ¬B ∧ Uk ϕ → Um+1 ϕ k
(CMPn) (1 ⩽ m < κ) (DEG) (1 ⩽ m < κ) (CMPn) (1 ⩽ m < κ) (4m ), (5m ), (6m ) (7m ), (UYC) (1 ⩽ m < κ) (8m ), classical reasoning
(10) A ∧ ¬B → Uκk ϕ (11) A → B
(3), (9m ), induction on m (1), (10), classical reasoning
For (IRREF) in SCU: (1) (2m ) (3n ) (4) (5) (6)
(i ≻ i)ϕ → U1i ϕ m+1 (i ≻ i)ϕ ∧ Um ϕ i ϕ → Ui n (i ≻ i)ϕ → Ui ϕ (i ≻ i)ϕ → Uω i ϕ (i ≻ i)ϕ → ¬Uω i ϕ ¬(i ≻ i)ϕ
(CMP1) (CMPn) (m ∈ N+ ) (1), (2m ), induction on n (ωI) applied to (3n )n∈N+ (CMPω) (4), (5), classical reasoning
For (TRANS) in SCU, use the same abbreviations A := (i ≻ j)ϕ ∧ ( j ≻ k)ϕ and B := (i ≻ k)ϕ. Then: (1) (2) (3)
A → ¬Uω kϕ 1 A → Ui ϕ ∧ Kk ϕ A ∧ ¬U1k ϕ → B
(CMPω), propositional reasoning (CMP1), propositional reasoning (2), (UYC0)
(4m ) (5m ) (6m ) (7m ) (8m ) (9m )
m+1 ( j ≻ k)ϕ ∧ Um ϕ k ϕ → Uj m+1 m Uj ϕ → Uj ϕ (i ≻ j)ϕ ∧ Umj ϕ → Um+1 ϕ i m+1 m A ∧ Uk ϕ → Ui ϕ m+1 A ∧ Um ϕ →B k ϕ ∧ ¬Uk m A ∧ ¬B ∧ Uk ϕ → Um+1 ϕ k
(CMPn) (m ∈ N+ ) (DEG) (m ∈ N+ ) (CMPn) (m ∈ N+ ) (4m ), (5m ), (6m ) (7m ), (UYC) (m ∈ N+ ) (8m ), classical reasoning
(10n ) A ∧ ¬B → Unk ϕ (11) A ∧ ¬B → Uω kϕ (12) A → B
(3), (9m ), induction on n (ωI) applied to (10n )n∈N+ (1), (11), classical reasoning
760
Better Understanding, Understanding Better
Theorem 3.7 (Soundness for SCUκ ). Fix κ ⩾ 2. SCUκ is sound over CELUκ -models. Proof sketch. Below we record only two representative nontrivial cases. For (KYU), assume M , w ⊨ U1i Ki ϕ, witnessed by t ∈ E1 . Then gr(t) ⩾ 1, so gr(!t) = 2 and hence !t ∈ E2 . For each v with wRi v, we have v ∈ Ei (t, Ki ϕ) and M , v ⊨ Ki ϕ; by epistemic introspection of Ei , also v ∈ Ei (!t, Ki ϕ). Thus !t witnesses M , w ⊨ U2i Ki ϕ. For (CMPκ), if M , w ⊨ (i ≻ j)ϕ ∧ Uκj ϕ, then deg j (w, ϕ) = κ while over CELUκ always degi (w, ϕ) ⩽ κ, contradicting degi (w, ϕ) > deg j (w, ϕ); hence M , w ⊨ ¬Uκj ϕ. Theorem 3.8 (Soundness for SCU). SCU is sound over CELU models. Proof sketch. By induction on SCU proof trees from Definition 3.3. The shared finitary axioms/rules ω are sound as in Theorem 3.7. For (DEGnω ), assume M , w ⊨ Uω i ϕ. By the semantic clause of U , this n means M , w ⊨ Ui ϕ for every n ⩾ 1. (CMPω) is valid because (i ≻ j)ϕ requires degi (w, ϕ) > deg j (w, ϕ), impossible if Uωj ϕ holds (then deg j (w, ϕ) = ω). For (ωI), assume all its premises are true at w. If M , w ̸⊨ χ, the conclusion is immediate. Suppose M , w ⊨ χ. If m = 0, the premises give M , w ⊨ Uni ϕ for every n ⩾ 1, hence M , w ⊨ Uω i ϕ by the semantics. If m > 0, take arbitrary worlds w1 , . . . , wm with wR j1 w1 , . . . , wm−1 R jm wm . If there is a first r such that θr fails at wr , the corresponding implication is true. If all θr hold, then the premises give M , wm ⊨ Uni ϕ for every n ⩾ 1, so M , wm ⊨ Uω i ϕ. Thus the conclusion is true at w.
4
Completeness and Bounded Decidability
This section proves strong completeness for the bounded finitary and full infinitary calculi, and also establishes bounded decidability. We therefore use two canonical-model constructions: a bounded one, following the witness-based strategy of [35, 31] but adapted to graded witnesses, agent-indexed explanation stores, and comparative formulas, and a full-language construction based on maximal consistent sets closed under the infinitary rule. We first construct the bounded canonical model for SCUκ . Let Ω be the set of all maximal SCUκ consistent sets of CELUκ -formulas. Definition 4.1. The canonical model for SCUκ is M c = (W c , {Rci | i ∈ I},V c , E c , grc , {Eic | i ∈ I}), where: • E c is generated by the BNF: t ::= c | ϕ n | (t · t) | (t + t) |!t, where ϕ ∈ CELUκ , n ∈ {1, . . . , κ}. • The canonical grade map grc : E c → N is defined inductively by: grc (c) = 1, grc (ϕ n ) = n, grc (t · s) = min{grc (t), grc (s)}, ( 0, if grc (t) = 0, grc (!t) = c (2, if gr (t) > 0, grc (t + s) =
0, if min{grc (t), grc (s)} = 0, min{grc (t), grc (s)} − 1, otherwise.
For each n ∈ N, let Enc := {t ∈ E c | grc (t) ⩾ n}.
Y. Wei
761
• W c is the set of all triples ⟨Γ, F , ⃗f ⟩ such that Γ ∈ Ω and: – ⃗f = { f n | i ∈ I, n ∈ {1, . . . , κ}} with f n : {ϕ | Un ϕ ∈ Γ} → {t ∈ E c | grc (t) = n}; i
i
i
– F = {Fi | i ∈ I}, where each Fi ⊆ E c × CELUκ is the agent-i explanation store satisfying the following base and admissibility conditions relative to Γ and ⃗f : (Basei ) {⟨c, ϕ⟩ | ϕ ∈ Λ} ⊆ Fi and {⟨ fin (ϕ), ϕ⟩ | Uni ϕ ∈ Γ} ⊆ Fi ; (Appi )
if ⟨t, ϕ → ψ⟩, ⟨s, ϕ⟩ ∈ Fi then ⟨t · s, ψ⟩ ∈ Fi ;
(Sumi )
if ⟨t, ϕ⟩ ∈ Fi or ⟨s, ϕ⟩ ∈ Fi then ⟨t + s, ϕ⟩ ∈ Fi ;
(Inti )
if ⟨t, Ki ϕ⟩ ∈ Fi , then ⟨!t, Ki ϕ⟩ ∈ Fi .
• ⟨Γ, F , ⃗f ⟩Rci ⟨∆, G ,⃗g⟩ iff {ϕ | Ki ϕ ∈ Γ} ⊆ ∆ and ∀n ∈ {1, . . . , κ} ( fin = gni ). c • For each i ∈ I, E c : E c × CELUκ → 2W is defined by E c (t, ϕ) := {⟨Γ, F , ⃗f ⟩ ∈ W c | ⟨t, ϕ⟩ ∈ Fi }.
i c • V (p) := {⟨Γ, F , ⃗f ⟩ ∈ W c | p ∈ Γ}.
i
In this construction, each canonical world ⟨Γ, F, ⃗f ⟩ ∈ W c packages exact-grade witnesses for the Uformulas in Γ. For each Uni ϕ ∈ Γ, the map fin selects a term fin (ϕ) ∈ E c with grc ( fin (ϕ)) = n, and the pair ⟨ fin (ϕ), ϕ⟩ is placed into the base of Fi . Each Fi is then closed under (Appi ), (Sumi ), and (Inti ). The specific clauses in the canonical grading grc are chosen so that the canonical model still satisfies the original semantic constraints and, at the same time, supports the later technical arguments. We next define the closure operation used to build explanation stores from their base pairs. It adds exactly the pairs forced by the admissibility conditions for application, sum, and epistemic introspection. Definition 4.2. For X ⊆ E c × CELUκ and i ∈ I, define the one-step closure operator cl i (X) ⊆ E c × i CELUκ by cl i (X) := X ∪ clapp (X) ∪ clsum (X) ∪ clint (X), where clapp (X) := {⟨t · s, ψ⟩ | ∃χ (⟨t, χ → ψ⟩ ∈ X ∧ ⟨s, χ⟩ ∈ X)}, clsum (X) := {⟨t + s, ϕ⟩ | ⟨t, ϕ⟩ ∈ X or ⟨s, ϕ⟩ ∈ X}, i clint (X) := {⟨!t, Ki ϕ⟩ | ⟨t, Ki ϕ⟩ ∈ X}.
Given S ⊆ E c × CELUκ , let Si0 := S and Sik+1 := cl i (Sik ) for k ∈ N. Define Si∞ :=
k k∈N Si .
S
Lemma 4.3. For every maximal SCUκ -consistent set Γ ∈ Ω, there exist F = {Fi | i ∈ I} and a witness family ⃗f such that ⟨Γ, F , ⃗f ⟩ ∈ W c . In particular, W c ̸= 0. / Proof. For each i ∈ I and n ∈ {1, . . . , κ}, define fin (ϕ) := ϕ n for ϕ with Uni ϕ ∈ Γ. This is well-typed since grc (ϕ n ) = n. For each fixed i ∈ I, let SΓ,⃗f ,i := {⟨c, ϕ⟩ | ϕ ∈ Λ} ∪ {⟨ fin (ϕ), ϕ⟩ | n ∈ {1, . . . , κ}, Uni ϕ ∈ Γ}. i k k+1 0 ∞ Using the notation of Definition 4.2, set SΓ, ⃗f ,i := SΓ,⃗f ,i , SΓ,⃗f ,i := cl (SΓ,⃗f ,i ), Fi := SΓ,⃗f ,i . Let F := {Fi | i ∈ I}. Then each Fi is base-extending and closed under (Appi ), (Sumi ), and (Inti ) by construction. Hence ⟨Γ, F , ⃗f ⟩ ∈ W c . For nonemptiness, take any theorem ⊤ of SCUκ . Then {⊤} is SCUκ -consistent, so by Lindenbaum there exists Γ ∈ Ω. Applying the first part to this Γ gives ⟨Γ, F , ⃗f ⟩ ∈ W c . Hence W c ̸= 0. /
Lemma 4.4. For each i ∈ I, Rci is an equivalence relation on W c . We omit the proof. Regarding Eic in canonical models, it is obvious to check the following:
762
Better Understanding, Understanding Better
Lemma 4.5. For each i ∈ I, the function Eic satisfies all conditions in Definition 2.2 for L = {1, . . . , κ}. We conclude that the canonical model is well-defined, based on the above lemmas. Proposition 4.6. M c is a CELUκ -model (equivalently, a CELU(L)-model with L = {1, . . . , κ}). Proof. E c is nonempty and closed under ·, +, ! by its BNF generation. The clauses defining grc satisfy all grade constraints in Definition 2.2. By Lemma 4.3, W c ̸= 0. / By Lemma 4.4, each Rci is an equivalence relation on W c . By Lemma 4.5, each Eic satisfies the required admissibility clauses. We now establish the existence ingredients for the Truth Lemma. Lemma 4.7 (Ki -Existence Lemma). For any canonical world w = ⟨Γ, F , ⃗f ⟩ ∈ W c , if ¬Ki ϕ ∈ Γ, then there exists a canonical world w′ = ⟨∆, G ,⃗g⟩ ∈ W c such that wRci w′ and ¬ϕ ∈ ∆. Proof. Fix w = ⟨Γ, F , ⃗f ⟩ ∈ W c with ¬Ki ϕ ∈ Γ. Let ∆− := {ψ | Ki ψ ∈ Γ} ∪ {¬ϕ}. It is routine to show that ∆− is SCUκ -consistent, by (N) and (DISTK). Extend ∆− to a maximal SCUκ -consistent set ∆ ∈ Ω. Then {ψ | Ki ψ ∈ Γ} ⊆ ∆ and ¬ϕ ∈ ∆. For each n ∈ {1, . . . , κ} and formula χ, we have Uni χ ∈ Γ ⇔ Uni χ ∈ ∆. Indeed, if Uni χ ∈ Γ, then (4∗ ) gives Ki Uni χ ∈ Γ, so Uni χ ∈ ∆. Conversely, if Uni χ ∈ / Γ, then ¬Uni χ ∈ Γ by maximality; by theorem ∗ n n n (5 ), Ki ¬Ui χ ∈ Γ, hence ¬Ui χ ∈ ∆, so Ui χ ∈ / ∆. Thus setting gni := fin is type-correct for the ∆-domain c requirement in W . Define ⃗g = {gnj | j ∈ I, n ∈ {1, . . . , κ}} by: for j = i, let gni := fin ; for j ̸= i, let gnj (ψ) := ψ n whenever n U j ψ ∈ ∆. This is well-defined because ψ n ∈ E c and grc (ψ n ) = n. To construct G = {G j | j ∈ I}, for each j ∈ I define S∆,⃗g, j := {⟨c, ϕ⟩ | ϕ ∈ Λ} ∪ {⟨gnj (ψ), ψ⟩ | n ∈ {1, . . . , κ}, Unj ψ ∈ ∆}, j m m+1 0 m ∞ ∞ and then let S∆,⃗ g, j := S∆,⃗g, j , S∆,⃗g, j := cl (S∆,⃗g, j ), S∆,⃗g, j := m∈N S∆,⃗g, j , and G j := S∆,⃗g, j . Each G j is baseextending and closed under (App j ), (Sum j ), and (Int j ). Set G := {G j | j ∈ I} and let w′ := ⟨∆, G ,⃗g⟩. Then w′ ∈ W c . By the definition of Rci , since {ψ | Ki ψ ∈ Γ} ⊆ ∆ and fin = gni for all n ∈ {1, . . . , κ}, we have wRci w′ . Finally, ¬ϕ ∈ ∆ by construction.
S
Lemma 4.8 (Uni -Existence Lemma). Let w = ⟨Γ, F , ⃗f ⟩ ∈ W c , fix i ∈ I and n ∈ {1, . . . , κ}, and assume Uni ϕ ∈ / Γ and ⟨t, ϕ⟩ ∈ Fi for some t ∈ Enc . There exists w′ = ⟨∆, G ,⃗g⟩ ∈ W c such that wRci w′ and ⟨t, ϕ⟩ ∈ / Gi . Proof. Fix w = ⟨Γ, F , ⃗f ⟩. Define, for this proof: C0 := {⟨c, ϕ⟩ | ϕ ∈ Λ} ∪ {⟨ fim (ψ), ψ⟩ | m ∈ {1, . . . , κ}, Um i ψ ∈ Γ}, and Ck+1 := cl i (Ck ), C∞ := k∈N Ck . Thus C∞ is the least agent-i explanation store generated from Γ and the witness maps ⃗f by the admissibility conditions. Claim 1. If ⟨t, ϕ⟩ ∈ C∞ and grc (t) ⩾ n ⩾ 1, then Uni ϕ ∈ Γ. Claim 2. Given the fixed w = ⟨Γ, F , ⃗f ⟩ ∈ W c , i ∈ I and t ∈ E c , if ⟨t, ϕ⟩ ∈ / C∞ , then there exists w′ = ⟨∆, G ,⃗g⟩ ∈ W c such that wRci w′ and ⟨t, ϕ⟩ ∈ / Gi . S
Proof of Claim 1. We prove by induction on k ∈ N that each pair in Ck has, in Γ, all positive understanding formulas up to the grade of its term: P(k) : ∀⟨u, ψ⟩ ∈ Ck ∀ℓ (1 ⩽ ℓ ⩽ grc (u) ⇒ Uℓi ψ ∈ Γ).
Y. Wei
763
For k = 0, there are two kinds of pairs in C0 . If ⟨u, ψ⟩ = ⟨c, λ ⟩ with λ ∈ Λ, then grc (c) = 1 and U1i λ is derivable by (NE), hence belongs to Γ. If ⟨u, ψ⟩ = ⟨ fim (ψ), ψ⟩, then Um i ψ ∈ Γ by definition of the m ℓ domain of fi ; for any 1 ⩽ ℓ ⩽ m, (DEG) yields Ui ψ ∈ Γ. For the induction step, take ⟨u, ψ⟩ ∈ Ck+1 = cl i (Ck ) and 1 ⩽ ℓ ⩽ grc (u). If ⟨u, ψ⟩ ∈ Ck , apply IH. Otherwise: (App) u = r · s with ⟨r, χ → ψ⟩, ⟨s, χ⟩ ∈ Ck . Let a := grc (r), b := grc (s), and h := min{a, b}; then grc (u) = h. By IH and (DEG), Uhi (χ → ψ), Uhi χ ∈ Γ. By (DISTU), Uhi ψ ∈ Γ, and then (DEG) yields Uℓi ψ ∈ Γ. (Sum) u = r +s and either ⟨r, ψ⟩ ∈ Ck or ⟨s, ψ⟩ ∈ Ck . Assume ⟨r, ψ⟩ ∈ Ck . Set a := grc (r) and h := grc (u). Since 1 ⩽ ℓ ⩽ h, we have h ⩾ 1. By the grade definition for +, this yields h < a, hence ℓ < a. By IH, Uai ψ ∈ Γ, and then (DEG) gives Uℓi ψ ∈ Γ. (Int) u =!r with ⟨r, Ki ψ⟩ ∈ Ck . If grc (r) = 0, then grc (u) = 0, impossible since 1 ⩽ ℓ ⩽ grc (u). If grc (r) ⩾ 1, then grc (u) = 2. By IH, U1i Ki ψ ∈ Γ. By (KYU), U2i Ki ψ ∈ Γ, and then (DEG) yields Uℓi Ki ψ ∈ Γ. So P(k + 1) holds. Hence P(k) holds for all k. If ⟨t, ϕ⟩ ∈ C∞ , then ⟨t, ϕ⟩ ∈ Ck for some k, and applying P(k) with ℓ := n (since 1 ⩽ n ⩽ grc (t)) yields Uni ϕ ∈ Γ. m m m Proof of Claim 2. Set ∆ := Γ, and for each m ∈ {1, . . . , κ} let gm i := f i . For j ̸= i, define g j (ψ) := ψ m for Umj ψ ∈ ∆. Then ⃗g satisfies the typing condition in the definition of W c , and gm i = f i for all m. ∞ Let Gi := C . By hypothesis, ⟨t, ϕ⟩ ∈ / Gi . For each j ̸= i, let
S∆,⃗g, j := {⟨c, ϕ⟩ | ϕ ∈ Λ} ∪ {⟨gmj (ψ), ψ⟩ | m ∈ {1, . . . , κ}, Umj ψ ∈ ∆}, j k k+1 0 ∞ k ∞ and define S∆,⃗ g, j := S∆,⃗g, j , S∆,⃗g, j := cl (S∆,⃗g, j ), S∆,⃗g, j := k∈N S∆,⃗g, j , and G j := S∆,⃗g, j . Let G := {G j | j ∈ I} ′ ∞ and define w := ⟨∆, G ,⃗g⟩. For j = i, Gi = C is base-extending and closed under (Appi ), (Sumi ), (Inti ) by construction. For j ̸= i, each G j has the same closure properties by the iterative construction above. c ′ Hence w′ ∈ W c . Also, {ψ | Ki ψ ∈ Γ} ⊆ ∆ and fim = gm / Gi . i for all m, so wRi w . Finally, ⟨t, ϕ⟩ ∈ ∞ n Now we conclude the lemma. If ⟨t, ϕ⟩ ∈ C , then Claim 1 gives Ui ϕ ∈ Γ, contradiction. Hence ⟨t, ϕ⟩ ∈ / C∞ . By Claim 2 there exists an i-successor w′ = ⟨∆, G ,⃗g⟩ ∈ W c with ⟨t, ϕ⟩ ∈ / Gi .
S
With these existence lemmas in place, we prove the bounded Truth Lemma. Lemma 4.9 (Truth Lemma for CELUκ ). For ϕ ∈ CELUκ and w = ⟨Γ, F , ⃗f ⟩ ∈ W c , M c , w ⊨ ϕ iff ϕ ∈ Γ. Proof. We use induction on formula structure. The Boolean cases are standard. For ϕ = Ki ψ: • Assume Ki ψ ∈ Γ, and let w′ = ⟨∆, G ,⃗g⟩ satisfy wRci w′ . By definition of Rci , {χ | Ki χ ∈ Γ} ⊆ ∆, hence ψ ∈ ∆. By IH, M c , w′ ⊨ ψ. So M c , w ⊨ Ki ψ. • Assume M c , w ⊨ Ki ψ. If Ki ψ ∈ / Γ, then ¬Ki ψ ∈ Γ by maximality. By Lemma 4.7, there is w′ = ⟨∆, G ,⃗g⟩ with wRci w′ and ¬ψ ∈ ∆. By IH, M c , w′ ̸⊨ ψ, contradiction. Hence Ki ψ ∈ Γ. For ϕ = Uni ψ: • Assume Uni ψ ∈ Γ. Let t := fin (ψ); then grc (t) = n, so t ∈ Enc . We show that t witnesses Uni ψ at w. Let w′ = ⟨∆, G ,⃗g⟩ satisfy wRci w′ . By the definition of Rci , gni = fin . Since ψ ∈ dom( fin ), we have ψ ∈ dom(gni ), hence Uni ψ ∈ ∆. The base condition for Gi gives ⟨gni (ψ), ψ⟩ ∈ Gi , and therefore ⟨t, ψ⟩ ∈ Gi . Thus w′ ∈ Eic (t, ψ). From (UYK) and Uni ψ ∈ Γ, we get Ki ψ ∈ Γ. By the Ki -case already proved, M c , w ⊨ Ki ψ. Therefore M c , w ⊨ Uni ψ.
764
Better Understanding, Understanding Better • Assume M c , w ⊨ Uni ψ. Then there exists t ∈ Enc such that ∀v ∈ W c (wRci v ⇒ v ∈ Eic (t, ψ)). Since / Γ, then Lemma 4.8 gives w′ = ⟨∆, G ,⃗g⟩ with Rci is reflexive, w ∈ Eic (t, ψ), i.e. ⟨t, ψ⟩ ∈ Fi . If Uni ψ ∈ wRci w′ and ⟨t, ψ⟩ ∈ / Gi . Hence w′ ∈ / Eic (t, ψ), contradiction. Therefore Uni ψ ∈ Γ.
For ϕ = (i ≻ j)ψ. First handle the special case i = j. By theorem (IRREF), no Γ contains (i ≻ i)ψ. Semantically, M c , w ⊨ (i ≻ i)ψ is impossible since it would require degi (w, ψ) > degi (w, ψ). Hence, M c , w ⊨ (i ≻ i)ψ ⇔ (i ≻ i)ψ ∈ Γ. Now assume i ̸= j. • Assume (i ≻ j)ψ ∈ Γ. From (CMP1), K j ψ ∈ Γ and U1i ψ ∈ Γ. From (CMPκ), ¬Uκj ψ ∈ Γ. By IH, M c , w ⊨ K j ψ. Let S j := {n ⩽ κ | Unj ψ ∈ Γ}. By (DEG), S j is downward closed. Since ¬Uκj ψ ∈ Γ, we have S j ̸= {1, . . . , κ}. If S j = 0, / then deg j (w, ψ) = 0, while U1i ψ ∈ Γ gives degi (w, ψ) ⩾ 1 by IH. If S j ̸= 0, / let m + 1 ⩽ κ be the least not in S j . Then m ⩽ κ − 1 and S j = {1, . . . , m}. Hence m U j ψ ∈ Γ and Um+1 ψ∈ / Γ; then ¬Um+1 ψ ∈ Γ, and by (CMPn), Um+1 ψ ∈ Γ. By IH, deg j (w, ψ) = m j j i and degi (w, ψ) ⩾ m + 1. In either case, degi (w, ψ) > deg j (w, ψ). So M c , w ⊨ (i ≻ j)ψ. • Assume M c , w ⊨ (i ≻ j)ψ. Then M c , w ⊨ K j ψ, so K j ψ ∈ Γ by IH. If deg j (w, ψ) = 0, then degi (w, ψ) ⩾ 1, hence M c , w ⊨ U1i ψ, and M c , w ⊨ ¬U1j ψ; by IH, both belong to Γ, hence (i ≻ j)ψ ∈ Γ by (UYC0). If deg j (w, ψ) = m ⩾ 1, then necessarily m ⩽ κ − 1. Then M c , w ⊨ Umj ψ ∧ ¬Um+1 ψ and M c , w ⊨ Um+1 ψ. By IH these formulas are in Γ, and (UYC) yields (i ≻ j)ψ ∈ Γ. j i
Theorem 4.10 (Completeness for SCUκ ). Fix κ ⩾ 2. For Σ ∪ {ϕ} ⊆ CELUκ , Σ |= ϕ implies Σ ⊢SCUκ ϕ. Proof. Assume Σ ⊬SCUκ ϕ. Then Σ ∪ {¬ϕ} is SCUκ -consistent. Extend it to a maximal SCUκ -consistent set Γ ∈ Ω. By Lemma 4.3, choose F , ⃗f with w := ⟨Γ, F , ⃗f ⟩ ∈ W c . By Lemma 4.9, M c , w ⊨ Σ and M c , w ⊨ ¬ϕ. So Σ ̸|= ϕ. Before stating decidability, we isolate the effective assumption on Λ used in the finite search below. As in the finitary-model strategy of justification logic, what is needed is effective control of generated evidence, not merely decidable membership in the constant specification [28]. Say that Λ is κ-effective if the following can be done effectively. Given finite C ⊆ CELUκ , finite J ⊆ I, and finite sets Xi (i ∈ J) of pairs ⟨s, ψ⟩, with s a graded explanation term and ψ ∈ C, one can decide, for each i ∈ J, each ϕ ∈ C, and ∞ each 1 ⩽ m ⩽ κ, whether there exists a term t such that gr(t) ⩾ m and ⟨t, ϕ⟩ ∈ Xi ∪ {⟨c, λ ⟩ | λ ∈ Λ} i , where the iterated closure is as in Definition 4.2. Simple effective finite-schema choices of Λ satisfy this condition; for example, Λ may be generated by the schemata ϕ ∧ ψ → ϕ and ϕ ∧ ψ → ψ. Theorem 4.11 (Decidability of fixed-level fragments). Fix κ ⩾ 2 and assume that Λ is κ-effective. Then satisfiability and validity over CELUκ are decidable. Proof sketch. We prove an effective finite-model property. Given ϕ ∈ CELUκ , form the finite closure C of ϕ under subformulas, negation, downward closure for understanding levels (Um+1 ψ brings i m m in Ui ψ), the Ki ψ associated with Ui ψ, and, for each comparative subformula (i ≻ j)ψ, the formulas m K j ψ, Um i ψ, U j ψ for 1 ⩽ m ⩽ κ. Only proposition letters and agents occurring in C are relevant. Call X ⊆ C a complete C-type if it decides every formula in C and respects the Boolean connectives. Enumerate finite structures whose states are complete C-types, with equivalence relations Ri matching the Ki -formulas. For U-formulas, require class-uniformity: if XRiY , then X and Y contain the same formulas Um i ψ from C. Let δi (X, ψ) be the largest such m, or 0 if none exists. For each δi (X, ψ) > 0, add one fresh witness ei,[X]i ,ψ of that grade, shared across the Ri -class [X]i . Using κ-effectiveness, decide whether the least store generated from Λ and these shared witness pairs contains a pair ⟨t, ψ⟩ with gr(t) ⩾ m. Accept
Y. Wei
765
exactly those structures in which the Um i ψ-labels match this generated-witness condition and the truth of ψ throughout the relevant Ri -class, and in which (i ≻ j)ψ ∈ X iff δi (X, ψ) > δ j (X, ψ) and K j ψ ∈ X. Filtration of any model satisfying ϕ through C yields an accepted finite structure, and any accepted structure is realized as a finite model with its states, relations, atom valuation, and least generated explanation stores. Induction on formulas in C gives agreement between truth and membership in the corresponding type. Hence ϕ is satisfiable iff some accepted finite structure contains ϕ. Since finitely many such structures are checked and all checks are effective, satisfiability is decidable. Validity follows. For the system SCU, the remaining key step is to build maximal consistent sets closed under all ω-introduction instances. We use a countable Lindenbaum–Henkin construction with finite failure witnesses, along the lines of [10]. Lemma 4.12 (ω-Lindenbaum extension). Every SCU-consistent set extends to a maximal SCU-consistent set that is closed under all ω-introduction instances. Proof. Assume Σ is SCU-consistent. Note that CELU and the set of ω-introduction instances are countable. Enumerate the formulas of CELU as (θs )s∈N . Let R be the set of all ω-introduction instances, and fix a listing r : N → R in which every instance occurs infinitely often. At stage s, write r(s) as the rule ω n with premises χs → Bns (n ∈ N+ ) and conclusion χs → Bω s , where Bs is obtained from Bs by replacing the displayed Un with Uω . We define the sequence (Γs )s∈N recursively by Γ0 := Σ, and, given Γs , first set ( Γs ∪ {θs }, Γs ∪ {θs } is SCU-consistent, Hs := Γs ∪ {¬θs }, otherwise. If ¬(χs → Bω s ) ∈ Hs , let
Γs+1 := Hs ∪ {¬(χs → Bns s )},
where ns is the least positive integer such that Hs ∪ {¬(χs → Bns s )} is SCU-consistent. Otherwise let Γs+1 := Hs . We first show that this recursion is well-defined and that every Γs is SCU-consistent. The basis is immediate. For the step, suppose Γs is consistent. At least one of Γs ∪ {θs } and Γs ∪ {¬θs } is consistent; otherwise, Lemma 3.5 gives Γs ⊢SCU θs , while inconsistency of Γs ∪ {θs } implies inconsistency of Γs ∪ {¬¬θs } by tautology and Lemma 3.4, so another application of Lemma 3.5 gives Γs ⊢SCU ¬θs , contradiction. Thus Hs is consistent. If no such ns existed in this finite-failure-witness step, then for every n ∈ N+ , Hs ∪ {¬(χs → Bns )} would be inconsistent; by Lemma 3.5, Hs ⊢SCU χs → Bns for all n, and the ω-introduction instance r(s) would yield Hs ⊢SCU χs → Bω s , contradicting consistency of Hs . S Let Γ∗ := s∈N Γs . The construction has the following finite-failure property: if the conclusion χ → Bω of an ω-introduction instance has its negation in Γ∗ , then ¬(χ → Bn ) ∈ Γ∗ for some n ∈ N+ . Indeed, once ¬(χ → Bω ) has entered the construction, choose a later stage s at which r(s) is that same instance. Such a stage exists because every instance occurs infinitely often. The witness step at stage s then adds ¬(χ → Bn ) for some n. It remains to check that Γ∗ is a maximal SCU-consistent set and is closed under all ω-introduction instances. First, Γ∗ decides every formula: if θ = θs , then stage s + 1 puts either θ or ¬θ into Γ∗ . Every SCU-theorem belongs to Γ∗ . Otherwise, since Γ∗ decides formulas, ¬η ∈ Γ∗ for some theorem η. Then ¬η ∈ Γs for some s, and the theorem proof of η together with the tautology η → (¬η → ⊥) makes Γs inconsistent. The set Γ∗ is closed under (MP) in the usual way. It is also closed under ω-introduction: if all premises χ → Bn of an instance are in Γ∗ but the conclusion χ → Bω is not, then ¬(χ → Bω ) ∈ Γ∗ . By
766
Better Understanding, Understanding Better
the finite-failure property, ¬(χ → Bn ) ∈ Γ∗ for some n. Since the construction is increasing, some Γs contains both χ → Bn and its negation, contradicting consistency of Γs . Finally, Γ∗ is SCU-consistent. Otherwise take a proof tree of ⊥ from Γ∗ . By induction on the tree, every node label belongs to Γ∗ : assumptions by definition; axioms and (NE)-nodes because theorems belong to Γ∗ ; (MP)- and ω-introduction nodes by the closure just proved; and (N)-nodes because their premise subtrees are closed and hence prove theorems. Thus ⊥ ∈ Γ∗ , so ⊥ ∈ Γs for some s, contradicting consistency of Γs . Now let Ω∞ be the set of maximal SCU-consistent sets closed under all ω-introduction instances. Lemma 4.13. Let W∞c be the world set obtained by rebuilding Definition 4.1 with Ω replaced by Ω∞ , CELUκ replaced by CELU, and every bounded index range {1, . . . , κ} replaced by N+ . For every Γ ∈ Ω∞ , there exist F = {Fi | i ∈ I} and a witness family ⃗f such that ⟨Γ, F , ⃗f ⟩ ∈ W∞c . Proof. Exactly as in Lemma 4.3: define fin (ψ) := ψ n on {ψ | Uni ψ ∈ Γ}, and let each Fi be the least closure of the corresponding base under (Appi ), (Sumi ), and (Inti ). The construction is purely syntactic and independent of whether Γ ∈ Ω or Γ ∈ Ω∞ . Let M∞c = (W∞c , {Rci }i∈I ,V c , E c , grc , {Eic }i∈I ) be the canonical model over Ω∞ obtained in this way. Lemma 4.14 (Full Ki -Existence Lemma). If w = ⟨Γ, F , ⃗f ⟩ ∈ W∞c and ¬Ki ϕ ∈ Γ, then there exists w′ = ⟨∆, G ,⃗g⟩ ∈ W∞c such that wRci w′ and ¬ϕ ∈ ∆. Proof. Let ∆− := {ψ | Ki ψ ∈ Γ} ∪ {¬ϕ}. We first show that ∆− is SCU-consistent. Suppose otherwise. Let a proof tree of ⊥ from ∆− be given. We claim, by induction on this tree, that for every node label α, Ki (¬ϕ → α) ∈ Γ. For assumption leaves, either α = ψ with Ki ψ ∈ Γ, or α = ¬ϕ. In the first case, normal modal reasoning gives Ki (¬ϕ → ψ) ∈ Γ from Ki ψ ∈ Γ; in the second, Ki (¬ϕ → ¬ϕ) ∈ Γ follows by necessitation. Axiom leaves, (NE)-nodes, and closed (N)-nodes are theorems, so the desired formula Ki (¬ϕ → α) also follows by necessitation. The (MP) case is standard. For an ω-introduction node, write its premises as χ → Bn (n ∈ N+ ) and its conclusion as χ → Bω . By the induction hypothesis, Ki (¬ϕ → (χ → Bn )) ∈ Γ for every n. Equivalently, by normal modal reasoning, Ki ((¬ϕ ∧ χ) → Bn ) ∈ Γ for every n. By propositional reasoning, these give the premises ⊤ → Ki ((¬ϕ ∧ χ) → Bn ) of the corresponding (ωI)-instance, whose conclusion is ⊤ → Ki ((¬ϕ ∧ χ) → Bω ). Since Γ is closed under all ω-introduction instances, we obtain ⊤ → Ki ((¬ϕ ∧ χ) → Bω ) ∈ Γ, hence Ki ((¬ϕ ∧ χ) → Bω ) ∈ Γ, and therefore Ki (¬ϕ → (χ → Bω )) ∈ Γ. At the root we obtain Ki (¬ϕ → ⊥) ∈ Γ, and hence Ki ϕ ∈ Γ, contradicting ¬Ki ϕ ∈ Γ. Thus ∆− is consistent. By Lemma 4.12, extend ∆− to some ∆ ∈ Ω∞ . For every n ∈ N+ and formula χ, Uni χ ∈ Γ iff Uni χ ∈ ∆: the forward direction uses (4∗ ), and the backward direction uses (5∗ ), exactly as in the bounded Ki -Existence Lemma. Hence we may set gni := fin for all n. For j ̸= i, let gnj (ψ) := ψ n whenever Unj ψ ∈ ∆. Build G = {G j | j ∈ I} from ∆ and ⃗g by the same base-and-closure construction used in Lemma 4.13. Then w′ := ⟨∆, G ,⃗g⟩ belongs to W∞c . Since {ψ | Ki ψ ∈ Γ} ⊆ ∆ and gni = fin for all n, we have wRci w′ . Finally, ¬ϕ ∈ ∆ by construction. Lemma 4.15. Let w = ⟨Γ, F , ⃗f ⟩ ∈ W∞c , fix i ∈ I and n ∈ N+ , and assume Uni ϕ ∈ / Γ and ⟨t, ϕ⟩ ∈ Fi for some t ∈ Enc . There exists w′ = ⟨∆, G ,⃗g⟩ ∈ W∞c such that wRci w′ and ⟨t, ϕ⟩ ∈ / Gi . Proof. It is the same as Lemma 4.8, with N+ in place of {1, . . . , κ}. ω-introduction is not used.
Y. Wei
767
Lemma 4.16 (Truth Lemma for CELU). For ϕ ∈ CELU and w = ⟨Γ, F , ⃗f ⟩ ∈ W∞c : M∞c , w ⊨ ϕ iff ϕ ∈ Γ. Proof. Induction on ϕ. The Boolean cases are standard. The Ki case uses Lemma 4.14. The finite-level Uni case is the same as in Lemma 4.9, using Lemma 4.15 for the refutation direction. For ϕ = Uω i ψ. ω • If Ui ψ ∈ Γ, then by (DEGnω ), Uni ψ ∈ Γ for every n ⩾ 1. By IH, M∞c , w ⊨ Uni ψ for every n ⩾ 1, hence M∞c , w ⊨ Uω i ψ. c n • If M∞c , w ⊨ Uω i ψ, then by semantics M∞ , w ⊨ Ui ψ for all n ⩾ 1, so by the finite-level U-case n Ui ψ ∈ Γ for all n ⩾ 1. By closure under the basic ω-introduction instance, Uω i ψ ∈ Γ. For ϕ = (i ≻ j)ψ. The case i = j is the same as in Lemma 4.9. Assume i ̸= j. • Assume (i ≻ j)ψ ∈ Γ. By (CMP1) and (CMPω), K j ψ, U1i ψ, ¬Uωj ψ ∈ Γ; hence M∞c , w ⊨ K j ψ by the preceding K-case. Let S j := {n ⩾ 1 | Unj ψ ∈ Γ}. By (DEG), S j is downward closed and S j ̸= N+ ; otherwise the basic ω-introduction instance would contradict ¬Uωj ψ ∈ Γ. If S j = 0, / then 1 deg j (w, ψ) = 0, while Ui ψ ∈ Γ gives degi (w, ψ) ⩾ 1 by the finite-level U-case. If S j ̸= 0, / let m + 1 m+1 m be the least not in S j . Then m ⩾ 1 and S j = {1, . . . , m}. Hence U j ψ, ¬U j ψ ∈ Γ and, by (CMPn), Um+1 ψ ∈ Γ. By the finite-level U-case, deg j (w, ψ) = m and degi (w, ψ) ⩾ m + 1. In either case, i degi (w, ψ) > deg j (w, ψ), so M∞c , w ⊨ (i ≻ j)ψ.
• Assume M∞c , w ⊨ (i ≻ j)ψ. Then K j ψ ∈ Γ by the K-case. The degree inequality also gives deg j (w, ψ) ̸= ω. If deg j (w, ψ) = 0, then degi (w, ψ) ⩾ 1 and U1j ψ is false. By the finite-level U-case, U1i ψ, ¬U1j ψ ∈ Γ; hence (i ≻ j)ψ ∈ Γ by (UYC0). If deg j (w, ψ) = m ⩾ 1, then degi (w, ψ) ⩾ m + 1. By the finite-level U-case, Umj ψ, ¬Um+1 ψ, Um+1 ψ ∈ Γ; then (UYC) yields (i ≻ j)ψ ∈ Γ. j i Theorem 4.17 (Strong completeness for SCU). For all Σ ∪ {ϕ} ⊆ CELU, Σ |= ϕ implies Σ ⊢SCU ϕ. Proof. Assume Σ ⊬SCU ϕ. By Lemmas 3.5 and 4.12, choose Γ∞ ∈ Ω∞ with Σ ∪ {¬ϕ} ⊆ Γ∞ . By Lemma 4.13, choose F , ⃗f such that w := ⟨Γ∞ , F , ⃗f ⟩ ∈ W∞c . Let M∞c be the corresponding canonical model over Ω∞ . By Lemma 4.16, M∞c , w ⊨ Σ and M∞c , w ⊨ ¬ϕ. Thus Σ ̸|= ϕ.
5
Conclusion
We have developed a comparative epistemic logic of understanding. On the semantic side, the framework is based on agent-indexed graded explanations; on the proof-theoretic side, it separates a bounded finitary layer from a full infinitary layer. In this way, the logic captures understanding in degrees and comparative understanding with respect to the same formula at issue, while also supporting strong completeness for the intended calculi and decidability for each fixed finite-level fragment. The framework also suggests several natural directions for further work. On the technical side, it would be worth studying richer proof-theoretic presentations for the full language. On the dynamic side, one may ask how graded and comparative understanding behaves under information change, communication, or learning. More broadly, the present logic invites closer comparison both with other comparative epistemic frameworks and with neighboring formal accounts of explanation and understanding. Acknowledgements. The author thanks the anonymous reviewers for their helpful suggestions that led to many improvements. The author also thanks Qiang Wang for commenting on a very early draft of this paper. This work is supported by the grant 24CZX085 from the National Social Science Fund of China.
768
Better Understanding, Understanding Better
References [1] Sergei Artemov (2008): The logic of justification. The Review of Symbolic Logic 1(4), pp. 477–513, doi:10.1017/S1755020308090060. [2] Sergei Artemov & Melvin Fitting (2019): Justification Logic: Reasoning with Reasons. 216, Cambridge University Press. [3] Christoph Baumberger (2014): Types of understanding: Their nature and their relation to knowledge. Conceptus 40(98), pp. 67–88, doi:10.1515/cpt-2014-0002. [4] Christoph Baumberger, Claus Beisbart & Georg Brun (2017): What is Understanding? An Overview of Recent Debates in Epistemology and Philosophy of Science. In Stephen Grimm, Christoph Baumberger & Sabine Ammon, editors: Explaining Understanding: New Perspectives from Epistemology and Philosophy of Science, Routledge, pp. 1–34, doi:10.4324/9781315686110. [5] Pierre Beckmann & Matthieu Queloz (2025): Mechanistic Indicators of Understanding in Large Language Models, doi:10.48550/arXiv.2507.08017. Preprint. [6] Ivan Boh (1993): Epistemic logic in the later middle ages. Routledge. [7] Ivan Boh (2000): Four phases of medieval epistemic logic. Theoria 66(2), pp. 129–144, doi:10.1111/j.17552567.2000.tb01159.x. [8] Felipe Morales Carbonell (2025): Compressing Graphs: a Model for the Content of Understanding. Erkenntnis 90, pp. 187–215, doi:10.1007/s10670-023-00694-3. [9] Hans van Ditmarsch, Wiebe van der Hoek & Barteld Kooi (2009): Knowing More — From Global to Local Correspondence. In: Proceedings of the Twenty-First International Joint Conference on Artificial Intelligence (IJCAI 2009), pp. 955–960. [10] D. Doder & Z. Ognjanović (2024): Probabilistic Temporal Logic with Countably Additive Semantics. Annals of Pure and Applied Logic 175, p. 103389, doi:10.1016/j.apal.2023.103389. [11] Miguel Egler (2021): Why Understanding-Why Is Contrastive. doi:10.1007/s11229-021-03059-x.
Synthese 199(3–4), pp. 6061–6083,
[12] Melvin Fitting (2004): A logic of explicit knowledge. Logica Yearbook, pp. 11–22. [13] Melvin Fitting (2005): The logic of proofs, semantically. Annals of Pure and Applied Logic 132(1), pp. 1–25, doi:10.1016/j.apal.2004.04.009. [14] Emma C Gordon (2012): Is there propositional understanding? doi:10.5840/logos-episteme20123234.
Logos & Episteme 3(2), pp. 181–192,
[15] Stephen R. Grimm (2017): Understanding and Transparency. In Stephen Grimm, Christoph Baumberger & Sabine Ammon, editors: Explaining Understanding: New Perspectives from Epistemology and Philosophy of Science, Routledge, pp. 212–229, doi:10.4324/9781315686110. [16] Carl Hempel (1965): Aspects of Scientific Explanation and Other Essays in the Philosophy of Science. The Free Press. [17] Carl Gustav Hempel & Paul Oppenheim (1948): Studies in the Logic of Explanation. Philosophy of Science 15(2), pp. 135–175, doi:10.1086/286983. [18] Carol Karp (1964): Languages with Expressions of Infinite Length. North-Holland. [19] Kareem Khalifa (2013): The role of explanation in understanding. The British Journal for the Philosophy of Science 64(1), pp. 161–187, doi:10.1093/bjps/axr057. [20] Kareem Khalifa (2017): Understanding, Explanation, and Scientific Knowledge. Cambridge University Press, Cambridge, UK, doi:10.1017/9781108164276. [21] Insa Lawler (2019): Understanding why, knowing why, and cognitive achievements. Synthese 196(11), pp. 4583–4603, doi:10.1007/s11229-017-1672-9.
Y. Wei
769
[22] Rachel McKinnon (2012): How do you know that ‘how do you know?’Challenges a speaker’s knowledge? Pacific Philosophical Quarterly 93(1), pp. 65–83, doi:10.1111/j.1468-0114.2011.01416.x. [23] Melanie Mitchell & David C. Krakauer (2023): The Debate Over Understanding in AI’s Large Language Models. Proceedings of the National Academy of Sciences of the United States of America 120(13), p. e2215907120, doi:10.1073/pnas.2215907120. [24] Duncan Pritchard (2014): Knowledge and understanding. In: Virtue Epistemology Naturalized, Springer, pp. 315–327, doi:10.1007/978-3-319-04672-3_18. [25] Wesley C. Salmon (1985): Scientific Explanation and the Causal Structure of the World. Princeton University Press. [26] Paulina Sliwa (2015): IV—Understanding and knowing. Proceedings of the Aristotelian Society 115(1, Part 1), pp. 57–74, doi:10.1111/j.1467-9264.2015.00384.x. [27] Michael Strevens (2013): No Understanding Without Explanation. Studies in History and Philosophy of Science Part A 44(3), pp. 510–515, doi:10.1016/j.shpsa.2012.12.005. [28] Thomas Studer (2012): Lectures on Justification Logic. Lecture notes, University of Bern. [29] Kristinn R. Thórisson, David Kremelberg, Bas R. Steunebrink & Eric Nivel (2016): About Understanding. In Bas Steunebrink, Pei Wang & Ben Goertzel, editors: International Conference on Artificial General Intelligence, Springer International Publishing, Cham, pp. 106–117, doi:10.1007/978-3-319-41649-6_11. [30] Yanjing Wang (2018): Beyond knowing that: a new generation of epistemic logics. In: Jaakko Hintikka on Knowledge and Game-Theoretical Semantics, Springer, pp. 499–533, doi:10.1007/978-3-319-62864-6_21. [31] Yu Wei (2024): A Logical Framework for Understanding Why. In Alexandra Pavlova, Mina Young Pedersen & Raffaella Bernardi, editors: Selected Reflections in Language, Logic, and Information, Springer Nature Switzerland, Cham, pp. 203–220, doi:10.1007/978-3-031-50628-4_13. [32] Daniel A. Wilkenfeld (2014): Functional Explaining: A New Approach to the Philosophy of Explanation. Synthese 191(14), pp. 3367–3391, doi:10.1007/s11229-014-0452-z. [33] Daniel A. Wilkenfeld (2019): Understanding as Compression. Philosophical Studies 176(10), pp. 2807– 2831, doi:10.1007/s11098-018-1152-1. [34] James Woodward & Lauren Ross (2021): Scientific Explanation. In Edward N. Zalta, editor: The Stanford Encyclopedia of Philosophy, Summer 2021 edition, Metaphysics Research Lab, Stanford University. [35] Chao Xu, Yanjing Wang & Thomas Studer (2021): A Logic of Knowing Why. Synthese 198(2), pp. 1259– 1285, doi:10.1007/s11229-019-02104-0.