Paper deep dive
Better Understanding, Understanding Better
Yu Wei
Intelligence
Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 95%
Last extracted: 7/5/2026, 8:11:51 AM
Summary
The paper introduces a comparative epistemic logic of understanding (CELU) to formally distinguish 'knowing' from 'understanding' and to model the degree and comparison of understanding between agents. It utilizes a level-indexed modality (U^τ_i φ) and a comparative connective ((i ≻ j) φ) within a multi-agent epistemic framework enriched with agent-indexed graded explanation structures and a justification-style term algebra. The author establishes that understanding comes in degrees (minimal, ordinary, ideal) and provides a distinction between a finitary bounded-level calculus and an infinitary full-language system, proving soundness, strong completeness, and decidability for the finite-level fragments.
Entities (6)
Relation Signals (3)
Yu Wei → authored → Comparative Epistemic Logic of Understanding
confidence 100% · Yu Wei Department of Philosophy East China Normal University... Better Understanding, Understanding Better
Comparative Epistemic Logic of Understanding → uses → Justification-style Term Algebra
confidence 100% · Semantically, we enrich multi-agent epistemic models with agent-indexed graded explanation structures and a justification-style term algebra.
CELU → isatypeof → Epistemic Logic
confidence 90% · The framework remains an epistemic logic in the strict technical sense
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
Abstract:"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 level-indexed understanding modalities and a comparative connective for saying that one agent understands why a proposition better than another agent does. 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.
Tags
Links
- Source: https://arxiv.org/abs/2606.31892v1
- Canonical: https://arxiv.org/abs/2606.31892v1
Trouble viewing inline? Open PDF directly →
Full Text
65,906 characters extracted from source content.
Expand or collapse full text
M. Bílková, M. Gattinger, I. van der Giessen, M. Girlando, Y. Wang (Eds.): Advances in Modal Logic 2026 (AiML 2026) EPTCS 447, 2026, p. 750–769, doi:10.4204/EPTCS.447.42 © Y. Wei This work is licensed under the Creative Commons Attribution License. Better Understanding, Understanding Better Yu Wei Department of Philosophy East China Normal University Shanghai, China ywei@philo.ecnu.edu.cn “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 episte- mology, 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 modalitiesU τ i and a comparative connective(i≻j)φ for “iunderstands whyφbetter thanj”. 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 acomparativedimension. 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]. Y. Wei751 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 non- identity 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 epis- temology 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 em- phasizes, “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 con- temporary 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 of- ten 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. Wilken- feld 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 epis- temic accessibility with explanation terms. Intuitively, agentiknows whypwheniknows thatpand has a uniform explanation witness that works across alli-accessible worlds. In this sense, knowing-why has an existential explanation profile, which can be rendered schematically as∃tK i (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 asunderstanding 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. 752Better Understanding, Understanding Better metalanguage. Philosophically inspired by [21] and technically by [35], Wei [31] models understanding- why via higher-order explanation, schematically∃t 1 ∃t 2 K i t 2 :(t 1 :φ) , wheret 1 :φmeans thatt 1 is an explanation forφ, andt 2 :(t 1 :φ)means thatt 2 is ahigher-orderexplanation of “t 1 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 un- derstanding 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 agentiunderstands whyφbetter thanj. Comparative modal work such as [9] already includes a comparative operatori⪰jto express that, locally at a given world, all formulas known by agentiare also known by agentj. In that framework, the global axiom schemeK i ψ→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 op- erator+, 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+sis available as an explanation ofφwhenever eithertorsis available. The compression perspective mentioned above explains why this operation should be treated with care. It does not re- quire 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 stan- dard justification logic: the object language has no formulas of the formt:φ. Explanation terms enter only semantically, as graded witnesses governed by the agent-indexed functionsE i 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 level- indexed 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. Wei753 the conceptual level, we take finite indicesτto range overN + =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 U 1 i φ,U 2 i φ,U m i φ,U ω i φ. 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 levelm>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 limit by requiring every finite level: V n∈N + U n i φ. The numerical levels are a formal idealization. Finite indices on the understanding operators repre- sent 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 fea- tures 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 complete- ness. 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 setsPof proposition letters andIof agents, and a nonempty understanding-level domainL⊆N + ∪ω, whereN + :=1,2,3, . . ., the comparative epistemic lan- guage of understandingCELU(L)is defined by (wherep∈P,i,j∈I,τ∈L): φ::=p|¬φ|(φ∧φ)|K i φ|U τ i φ|(i≻j)φ. We use only these two instances in what follows: CELU:=CELU(N + ∪ω),CELU κ :=CELU(1, . . . ,κ) (κ⩾2). Hereτis anunderstanding-level index. As explained above, finite indices onU τ i are intended to distinguish explanatory standards of different strength. ThusU n i φsays that agentimeets thenth such standard for understanding whyφ. Note that we setKy i φin [35, 31] asU 1 i φnow, which can be read as minimal understanding. 4 The formulaU ω i φexpresses ideal understanding and is interpreted as “for all 4 It may be tempting to setK i φ:=U 0 i φ, i.e., knowledge is just level-0 understanding. However, our philosophical point is that understanding is more than knowledge, which does not require thatK i φitself is already a very minimal form of understanding. 754Better Understanding, Understanding Better finite levelsn,U n i φ”. By abuse of notation, we writeUfor the family of modalitiesU τ i . The comparative understanding formula(i≻j)φindicates that agentiunderstands whyφbetter than agentjdoes. Informally, the bounded languageCELU κ keeps comparatives but restricts all understanding-level indices to1, . . . ,κ, 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 un- derstanding (knowledge why) of that tautology. A special set of “self-evident” tautologiesΛis intro- duced, 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 forUin general. Definition 2.2.Fix a level domainLand the associated languageCELU(L). A graded explanatory epistemicCELU(L)-modelMis a tuple(W,R i |i∈I,V,E,gr,E i |i∈I)where(W,R i |i∈I,V) is a standard multi-agent epistemic model, i.e. for eachi∈I,R i is an equivalence relation onW, and: •Eis a nonempty set of explanations, closed under·,+, and !, and containing the constantc. • gr :E→Nis a grade map. For eachn∈N, letE n :=t∈E|gr(t)⩾n. The grade map satisfies: –gr(t·s)⩾mingr(t),gr(s); –if mingr(t),gr(s)=0 then gr(t+s) =0; if mingr(t),gr(s)⩾1 then gr(t+s)<mingr(t),gr(s). –gr(!t) =0 if gr(t) =0, and gr(!t) =2 if gr(t)⩾1; –gr(c) =1. •E i |i∈Iis a family of admissible explanation functions, eachE i :E×CELU(L)→2 W satisfies: Explanation ApplicationE i (t,φ→ψ)∩E i (s,φ)⊆E i (t·s,ψ). Explanation SumE i (t,φ)∪E i (s,φ)⊆E i (t+s,φ). Constant SpecificationIfφ∈Λ, thenE i (c,φ) =W. Epistemic IntrospectionFor allt∈E,E i (t,K i φ)⊆E i (!t,K i φ). The term operations·,+, !, and the constantcare standard in justification logic. Application· combines explanations,+has the usual disjunctive or choice reading, ! represents positive introspection, and the constantcserves 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 termtand formulaφthe worlds at whichtexplainsφ. Here we replace that single function with an agent-indexed familyE i i∈I . Thusw∈E i (t,φ)means that, atw,tis available as an explanation ofφfor agenti. 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 onE i . The Sum condition preserves availability: if eithertorsexplainsφfor agentiat a world, thent+sdoes too. But the sum termt+sis less specific than either input, since it does not by itself specify whethertorsis 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 toE 0 , but not to any positive-grade classE n =t∈E|gr(t)⩾nwithn⩾1. As the truth conditions below make explicit, grade-0 terms cannot support positive-level understanding claims. The first three conditions onE i are standard. The fourth condition,E i (t,K i φ)⊆E i (!t,K i φ), requires a separate reading. Its source is the positive-introspection principle from justification logic. In standard Y. Wei755 justification logic,t:φ→!t:(t:φ)says that iftis a justification forφ, then !tis a justification for the claim thattjustifiesφ[12]. Intuitively, !trecords a reflective confirmation of the justificatory status oft. The introspection condition uses this idea only for knowledge claims about the same agent. Suppose p orb says that the Earth orbits the Sun. A request to explain why agentiknowsp orb is normally a request fori’s reasons or evidence for believingp orb , 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 ofK i φgives the agent’s reasons or evidence for believingφ. The condition above says that whenever, at a worldw,tis available to agentias an explanation of K i φ, the reflected term !tis also available toiatwas an explanation of the same knowledge claim. The point is not that !tadds another explanation ofφitself. Rather, !tmakes explicit thatican citetas 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 toK i φ, it means that agentihas an explanation of why she knowsφ. The term !trepresents 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 principleU 1 i K i φ→U 2 i K i φ: it is not a general mechanism for producing ever higher levels, does not validateU n i K i φ→U n+1 i K i φ, and does not apply toU 1 i K j φ→U 2 i K j φforj̸=ior to non-epistemic formulas. Definition 2.3(Truth conditions).Fix a level domainL, aCELU(L)-modelM, and letL fin :=L∩N + . The satisfaction relation forCELU(L)is defined inductively as follows (forp∈P,i,j∈I, andn∈L fin ): M,w⊨p⇔w∈V(p) M,w⊨¬φ⇔M,w̸⊨φ M,w⊨φ∧ψ⇔M,w⊨φandM,w⊨ψ M,w⊨K i φ⇔M,v⊨φfor allvsuch thatwR i v M,w⊨U n i φ⇔(1) there existst∈E n such that for allv∈WwithwR i v,v∈E i (t,φ), (2) for allv∈WwithwR i v,M,v⊨φ M,w⊨U ω i φ⇔(ifω∈L) for alln∈L fin ,M,w⊨U n i φ M,w⊨(i≻j)φ⇔(1) deg i (w,φ)>deg j (w,φ), and (2)M,w⊨K j φ where theunderstanding degree functionis deg i (w,φ):=sup n∈L fin |M,w⊨U n i φ∪0 . Thus deg i (w,φ)is not a primitive measure, but the supremum of the finite levels at whichiunder- stands whyφatw. The existential quantifier inU n i φis a witness condition: a level-nclaim requires one and the same explanation term of grade at leastnto be available at everyi-accessible world. Ifω/∈L, as in the bounded languagesCELU κ , thenU ω i φis not a well-formed formula, so theU ω clause is absent. In the full languageCELU, whereL=N + ∪ω,U ω i φexpresses ideal understanding as the limit case requiringU n i φfor everyn∈N + . Equivalently,M,w⊨U ω i φiff deg i (w,φ) =ω. Although(i≻j)φis primitive in the syntax, its semantic value is fixed by two independently defined notions: the induced degrees deg i ,deg j and the epistemic conditionK j φ. The comparison is formula- relative: it compares agents only with respect to the sameφ, not globally. The truth condition statesK j φ explicitly because deg i (w,φ)>deg j (w,φ)⩾0 already impliesM,w⊨U 1 i φ, henceM,w⊨K i φ. (i≻j)φcovers both cases where both agents understandφbut at different levels, and cases where ihas minimal understanding whilejmerely knowsφ. The latter remains a comparison within a shared epistemic issue: having an explanation already supports the ordinary judgment “I understand it better”. 756Better Understanding, Understanding Better Accordingly, for finitemwithm,m+1∈L fin , the conjunctionU m i φ∧¬U m+1 i φisolates the exact finite understanding degreemof agentiwith respect toφ. Returning to the opening example, letp orb ∈Psay that the Earth orbits the Sun, and leti C ,i S ,i R ∈I denote the child, the student, and the researcher. In one natural formalization, a worldwmay satisfy 1⩽deg i C (w,p orb )<deg i S (w,p orb )<deg i R (w,p orb ). ThenM,w⊨(i S ≻i C )p orb andM,w⊨(i R ≻i S )p orb . If a bystanderi B merely knows thatp orb while deg i B (w,p orb ) =0, thenM,w⊨(i C ≻i B )p orb holds. Remark 2.4.(i≻j)φbecomes eliminable in the comparative-free fragment ofCELU κ . That is, for every model⟨M,w⟩over level domainL=1, . . . ,κ, M,w⊨(i≻j)φ⇐⇒M,w⊨K j φ∧ κ _ m=1 U m i φ∧¬U m j φ . Proposition 2.5.InCELU, 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 comparative- free formula. Sinceχcontains only finitely many finite understanding-level indices, letnbe 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 withptrue. All accessibility relations are reflexive, soK j pholds at both points. Specify the explanation functions by puttingw∈E i (t i ,p),w∈E j (t j ,p),w ′ ∈E ′ i (t i ,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 ofMandM ′ , respectively, and let the only relevant difference be the grades: gr(t i ) =n, gr ′ (t i ) =n+1, and gr(t j ) =gr ′ (t j ) =n. Choose the remaining grades so that all generated terms have bounded grade; hence everyU ω -formula is false at both points. Then deg i (w,p) =n, deg i (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 belown: this is proved by induction on formulas, with theU m k case using the same available witnesses, if any, for everym<n, and with theU ω case handled by the preceding boundedness observation. HenceM,w⊨χ⇐⇒M ′ ,w ′ ⊨χ. ButM,w̸⊨(i≻j)p, andM ′ ,w ′ ⊨(i≻j)p. Below we show that the full languageCELUis non-compact. Proposition 2.6.Fix distinct agents i̸=j and an atom p. LetΣ ≻ :=(i≻j)p ∪ U n j p|n∈N + . Then every finite subset ofΣ ≻ is satisfiable overCELU-models, butΣ ≻ itself is unsatisfiable. Proof sketch.For any finite∆⊆Σ ≻ , letmbe the largestnsuch thatU n j p∈∆. Then a one-state model withptrue, reflexive accessibility, and deg j (w,p) =m<m+1=deg i (w,p)satisfies∆and(i≻j)p. IfM,w⊨U n j pfor alln⩾1, then deg j (w,p) =sup n|M,w⊨U n j p∪0 =ω. SoM,w⊨(i≻j)p is impossible, since it requires deg i (w,p)>deg j (w,p) =ω. HenceΣ ≻ is unsatisfiable. Therefore, no finitary proof system overCELUcan 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 domainLand aCELU(L)-modelM. We say thatMhasexplanation factivity if wheneverw∈E i (t,φ)for somei∈Iandt∈E, thenM,w⊨φ. Given aCELU(L)-modelM= (W,R i |i∈I,V,E,gr,E i |i∈I), define its factive companion M F = (W,R i |i∈I,V,E,gr,E F i |i∈I)byE F i (t,φ) =E i (t,φ)\w|M,w̸⊨φ. By direct checking, M F is again aCELU(L)-model. The proposition below asserts thatCELU(L)-truth is invariant under this factive transformation. The proof is routine and omitted for reasons of space. Proposition 2.8.For anyCELU(L)-formulaφand any w∈W ,M,w⊨φ⇔M F ,w⊨φ. Y. Wei757 3 Axiomatization We present two related systems over two aligned languages: the bounded finitary calculusSCU κ for CELU κ , and the infinitary systemSCUforCELU. Definition 3.1(Finitary calculus).Fixκ⩾2. LetSCU κ be the finitary Hilbert system overCELU κ whose axiom schemas are (wherei,j,k∈I, and understanding-level indices range overL=1, . . . ,κ): (TAUT)Propositional tautologies (DISTK)K i (φ→ψ)→(K i φ→K i ψ) (T)K i φ→φ (4)K i φ→K i K i φ (5)¬K i φ→K i ¬K i φ (DISTU)U n i (φ→ψ)→(U n i φ→U n i ψ)(n∈L) (DEG)U n i φ→U m i φ(n,m∈L,n>m) (UYK)U n i φ→K i φ(n∈L) (4 ∗ )U n i φ→K i U n i φ(n∈L) (KYU)U 1 i K i φ→U 2 i K i φ (UYC0)U 1 i φ∧K j φ∧¬U 1 j φ→(i≻j)φ (UYC)U n i φ∧U m j φ∧¬U m+1 j φ→(i≻j)φ(n,m,m+1∈L,n>m) (CMPn) (i≻j)φ∧U n j φ→U n+1 i φ(n,n+1∈L) (CMP1) (i≻j)φ→U 1 i φ∧K j φ (CMPκ) (i≻j)φ→¬U κ j φ. The inference rules are: (MP)Modus Ponens(N)⊢φ/⊢K i φ(NE)φ∈Λ/⊢U 1 i φ The axiom(KYU)captures a restricted introspective step: from level-1 understanding of why agenti knowsφ, agentican 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 semanticepistemic introspection condition onE i . Axiom(CMPκ)records the upper bound of the finite languageCELU κ : ifiunderstands φbetter thanj, thenjcannot 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 systemSCUoverCELUis theω-companion ofSCU κ : it has the same finitary schemas/rules as Definition 3.1 with all finite level indices ranging overN + , 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: (DEG n ω )U ω i φ→U n i φ(n∈N + ), and the following infinitary rule schema: (ωI) χ→K j 1 (θ 1 →·K j m (θ m →U n i φ)·)|n∈N + χ→K j 1 (θ 1 →·K j m (θ m →U ω i φ)·) . 758Better Understanding, Understanding Better Herem⩾0,j 1 , . . . ,j m ∈I, andθ 1 , . . . ,θ m ∈CELU. Ifm=0, the rule is read without any outerK- operators, i.e.,χ→U n i φ|n∈N + /(χ→U ω i φ). Ifm=1 andθ 1 =⊤, the rule includes the instance χ→K j U n i φ|n∈N + /(χ→K j U ω i φ). That is, under the same assumptionχ, ifjknows thatihas understanding ofφat every finite level, thenjalso knows thatihas 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 systemSCUby well-founded proof trees, following the treatment of infinitary formal proofs in [18]. Definition 3.3(SCU-derivability).Aproof 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 aSCU-axiom), or is obtained by one of the following rules: •(MP): from children labeledψ→χandψ, concludeχ; •(NE): concludeU 1 i ψforψ∈Λ; •(N): from oneclosedchild labeledψ, concludeK i ψ; •(ωI): form∈N, from children labeledχ→K j 1 (θ 1 → ·K j m (θ m →U n i ψ)·), one for each n∈N + , conclude the corresponding formula withU ω i ψin place ofU n i ψ; 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ΣisSCU-consistentiffΣ⊬ 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Σ∪¬φisSCU-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 χ→B n (n∈N + )and its conclusion asχ→B ω , whereB ω is obtained fromB n by replacing the displayed U n i ψwithU ω i ψ. By the induction hypothesis,Σ⊢ SCU α→(χ→B n )for alln. HenceΣ⊢ SCU (α∧χ)→ B n for alln, 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 ∗ )¬U n i φ→K i ¬U n i φ(4 ∗ ω )U ω i φ→K i U ω i φ (5 ∗ ω )¬U ω i φ→K i ¬U ω i φ(IRREF)¬(i≻i)φ (TRANS) (i≻j)φ∧(j≻k)φ→(i≻k)φ(ASYM) (i≻j)φ→¬(j≻i)φ Here(5 ∗ ),(IRREF),(TRANS), and(ASYM)are provable in bothSCU κ andSCU; for(5 ∗ ), n∈1, . . . ,κ inSCU κ and n∈N + inSCU.(4 ∗ ω )and(5 ∗ ω )are provable inSCU. Y. Wei759 Proof.The derivation of(5 ∗ )is routine from(T),(5),(4 ∗ )together with classical reasoning. InSCU, (DEG n ω )and(4 ∗ )giveU ω i φ→K i U n i φfor everyn∈N + . By modal reasoning, these yield the premises U ω i φ→K i (⊤→U n i φ)of them=1 instance of(ωI), which givesU ω i φ→K i (⊤→U ω i φ), and hence (4 ∗ ω ). Then(5 ∗ ω )follows by the same argument as(5 ∗ ). Given(IRREF)and(TRANS), the derivation of (ASYM)is routine. For(IRREF)inSCU κ : (1) (i≻i)φ→U 1 i φ(CMP1) (2 m ) (i≻i)φ∧U m i φ→U m+1 i φ(CMPn) (1⩽m<κ) (3) (i≻i)φ→U κ i φ(1),(2 m ),induction onm(1⩽m<κ) (4) (i≻i)φ→¬U κ i φ(CMPκ) (5)¬(i≻i)φ(3),(4),classical reasoning For(TRANS)inSCU κ , writeA:= (i≻j)φ∧(j≻k)φandB:= (i≻k)φ. Then: (1)A→¬U κ k φ(CMPκ),propositional reasoning (2)A→U 1 i φ∧K k φ(CMP1),propositional reasoning (3)A∧¬U 1 k φ→B(2),(UYC0) (4 m ) (j≻k)φ∧U m k φ→U m+1 j φ(CMPn) (1⩽m<κ) (5 m )U m+1 j φ→U m j φ(DEG) (1⩽m<κ) (6 m ) (i≻j)φ∧U m j φ→U m+1 i φ(CMPn) (1⩽m<κ) (7 m )A∧U m k φ→U m+1 i φ(4 m ),(5 m ),(6 m ) (8 m )A∧U m k φ∧¬U m+1 k φ→B(7 m ),(UYC) (1⩽m<κ) (9 m )A∧¬B∧U m k φ→U m+1 k φ(8 m ),classical reasoning (10)A∧¬B→U κ k φ(3),(9 m ),induction onm (11)A→B(1),(10),classical reasoning For(IRREF)inSCU: (1) (i≻i)φ→U 1 i φ(CMP1) (2 m ) (i≻i)φ∧U m i φ→U m+1 i φ(CMPn) (m∈N + ) (3 n ) (i≻i)φ→U n i φ(1),(2 m ),induction onn (4) (i≻i)φ→U ω i φ(ωI)applied to(3 n ) n∈N + (5) (i≻i)φ→¬U ω i φ(CMPω) (6)¬(i≻i)φ(4),(5),classical reasoning For(TRANS)inSCU, use the same abbreviationsA:= (i≻j)φ∧(j≻k)φandB:= (i≻k)φ. Then: (1)A→¬U ω k φ(CMPω),propositional reasoning (2)A→U 1 i φ∧K k φ(CMP1),propositional reasoning (3)A∧¬U 1 k φ→B(2),(UYC0) (4 m ) (j≻k)φ∧U m k φ→U m+1 j φ(CMPn) (m∈N + ) (5 m )U m+1 j φ→U m j φ(DEG) (m∈N + ) (6 m ) (i≻j)φ∧U m j φ→U m+1 i φ(CMPn) (m∈N + ) (7 m )A∧U m k φ→U m+1 i φ(4 m ),(5 m ),(6 m ) (8 m )A∧U m k φ∧¬U m+1 k φ→B(7 m ),(UYC) (m∈N + ) (9 m )A∧¬B∧U m k φ→U m+1 k φ(8 m ),classical reasoning (10 n )A∧¬B→U n k φ(3),(9 m ),induction onn (11)A∧¬B→U ω k φ(ωI)applied to(10 n ) n∈N + (12)A→B(1),(11),classical reasoning 760Better Understanding, Understanding Better Theorem 3.7(Soundness forSCU κ ).Fixκ⩾2.SCU κ is sound overCELU κ -models. Proof sketch.Below we record only two representative nontrivial cases. For(KYU), assumeM,w⊨U 1 i K i φ, witnessed byt∈E 1 . Then gr(t)⩾1, so gr(!t) =2 and hence !t∈E 2 . For eachvwithwR i v, we havev∈E i (t,K i φ)andM,v⊨K i φ; by epistemic introspection ofE i , alsov∈E i (!t,K i φ). Thus !twitnessesM,w⊨U 2 i K i φ. For(CMPκ), ifM,w⊨(i≻j)φ∧U κ j φ, then deg j (w,φ) =κwhile overCELU κ always deg i (w,φ)⩽ κ, contradicting deg i (w,φ)>deg j (w,φ); henceM,w⊨¬U κ j φ. Theorem 3.8(Soundness forSCU).SCUis sound overCELUmodels. Proof sketch.By induction onSCUproof trees from Definition 3.3. The shared finitary axioms/rules are sound as in Theorem 3.7. For(DEG n ω ), assumeM,w⊨U ω i φ. By the semantic clause ofU ω , this meansM,w⊨U n i φfor everyn⩾1.(CMPω)is valid because(i≻j)φrequires deg i (w,φ)>deg j (w,φ), impossible ifU ω j φholds (then deg j (w,φ) =ω). For(ωI), assume all its premises are true atw. If M,w̸⊨χ, the conclusion is immediate. SupposeM,w⊨χ. Ifm=0, the premises giveM,w⊨U n i φ for everyn⩾1, henceM,w⊨U ω i φby the semantics. Ifm>0, take arbitrary worldsw 1 , . . . ,w m with wR j 1 w 1 , . . . ,w m−1 R j m w m . If there is a firstrsuch thatθ r fails atw r , the corresponding implication is true. If allθ r hold, then the premises giveM,w m ⊨U n i φfor everyn⩾1, soM,w m ⊨U ω i φ. Thus the conclusion is true atw. 4 Completeness and Bounded Decidability This section proves strong completeness for the bounded finitary and full infinitary calculi, and also es- tablishes 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 expla- nation 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 forSCU κ . LetΩbe the set of all maximalSCU κ - consistent sets ofCELU κ -formulas. Definition 4.1.The canonical model forSCU κ isM c = (W c ,R c i |i∈I,V c ,E c ,gr c ,E c i |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 gr c :E c →Nis defined inductively by: gr c (c) =1, gr c (φ n ) =n, gr c (t·s) =mingr c (t),gr c (s), gr c (!t) = ( 0,if gr c (t) =0, 2,if gr c (t)>0, gr c (t+s) = ( 0,if mingr c (t),gr c (s)=0, mingr c (t),gr c (s)−1,otherwise. For eachn∈N, letE c n :=t∈E c |gr c (t)⩾n. Y. Wei761 •W c is the set of all triples⟨Γ,F, ⃗ f⟩such thatΓ∈Ωand: – ⃗ f=f n i |i∈I,n∈1, . . . ,κwithf n i :φ|U n i φ∈Γ→t∈E c |gr c (t) =n; –F=F i |i∈I, where eachF i ⊆E c ×CELU κ is theagent-i explanation storesatisfying the following base and admissibility conditions relative toΓand ⃗ f: (Base i )⟨c,φ⟩|φ∈Λ⊆F i and⟨f n i (φ),φ⟩|U n i φ∈Γ⊆F i ; (App i )if⟨t,φ→ψ⟩,⟨s,φ⟩∈F i then⟨t·s,ψ⟩∈F i ; (Sum i )if⟨t,φ⟩∈F i or⟨s,φ⟩∈F i then⟨t+s,φ⟩∈F i ; (Int i )if⟨t,K i φ⟩∈F i , then⟨!t,K i φ⟩∈F i . •⟨Γ,F, ⃗ f⟩R c i ⟨∆,G,⃗g⟩iffφ|K i φ∈Γ⊆∆and∀n∈1, . . . ,κ(f n i =g n i ). • For eachi∈I,E c i :E c ×CELU κ →2 W c is defined byE c i (t,φ):=⟨Γ,F, ⃗ f⟩∈W c |⟨t,φ⟩∈F i . •V c (p):=⟨Γ,F, ⃗ f⟩∈W c |p∈Γ. In this construction, each canonical world⟨Γ,F, ⃗ f⟩∈W c packages exact-grade witnesses for theU- formulas inΓ. For eachU n i φ∈Γ, the mapf n i selects a termf n i (φ)∈E c with gr c (f n i (φ)) =n, and the pair⟨f n i (φ),φ⟩is placed into the base ofF i . EachF i is then closed under (App i ), (Sum i ), and (Int i ). The specific clauses in the canonical grading gr c 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.ForX⊆E c ×CELU κ andi∈I, define the one-step closure operatorcl i (X)⊆E c × CELU κ bycl i (X):=X∪cl app (X)∪cl sum (X)∪cl i int (X), where cl app (X):=⟨t·s,ψ⟩|∃χ(⟨t,χ→ψ⟩∈X∧ ⟨s,χ⟩∈X), cl sum (X):=⟨t+s,φ⟩|⟨t,φ⟩∈Xor⟨s,φ⟩∈X, cl i int (X):=⟨!t,K i φ⟩|⟨t,K i φ⟩∈X. GivenS⊆E c ×CELU κ , letS 0 i :=SandS k+1 i :=cl i (S k i )fork∈N. DefineS ∞ i := S k∈N S k i . Lemma 4.3.For every maximalSCU κ -consistent setΓ∈Ω, there existF=F i |i∈Iand a witness family ⃗ f such that⟨Γ,F, ⃗ f⟩∈W c . In particular, W c ̸=/0. Proof.For eachi∈Iandn∈1, . . . ,κ, definef n i (φ):=φ n forφwithU n i φ∈Γ. This is well-typed since gr c (φ n ) =n. For each fixedi∈I, let S Γ, ⃗ f,i :=⟨c,φ⟩|φ∈Λ ∪ ⟨f n i (φ),φ⟩|n∈1, . . . ,κ,U n i φ∈Γ. Using the notation of Definition 4.2, setS 0 Γ, ⃗ f,i :=S Γ, ⃗ f,i ,S k+1 Γ, ⃗ f,i :=cl i (S k Γ, ⃗ f,i ),F i :=S ∞ Γ, ⃗ f,i . LetF:= F i |i∈I. Then eachF i is base-extending and closed under (App i ), (Sum i ), and (Int i ) by construction. Hence⟨Γ,F, ⃗ f⟩∈W c . For nonemptiness, take any theorem⊤ofSCU κ . Then⊤isSCU κ -consistent, so by Lindenbaum there existsΓ∈Ω. Applying the first part to thisΓgives⟨Γ,F, ⃗ f⟩∈W c . HenceW c ̸=/0. Lemma 4.4.For each i∈I, R c i is an equivalence relation on W c . We omit the proof. RegardingE c i in canonical models, it is obvious to check the following: 762Better Understanding, Understanding Better Lemma 4.5.For each i∈I, the functionE c i 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 aCELU κ -model (equivalently, aCELU(L)-model with L=1, . . . ,κ). Proof. E c is nonempty and closed under·,+,! by its BNF generation. The clauses defining gr c satisfy all grade constraints in Definition 2.2. By Lemma 4.3,W c ̸=/0. By Lemma 4.4, eachR c i is an equivalence relation onW c . By Lemma 4.5, eachE c i satisfies the required admissibility clauses. We now establish the existence ingredients for the Truth Lemma. Lemma 4.7(K i -Existence Lemma).For any canonical world w=⟨Γ,F, ⃗ f⟩∈W c , if¬K i φ∈Γ, then there exists a canonical world w ′ =⟨∆,G,⃗g⟩∈W c such that wR c i w ′ and¬φ∈∆. Proof.Fixw=⟨Γ,F, ⃗ f⟩∈W c with¬K i φ∈Γ. Let∆ − :=ψ|K i ψ∈Γ ∪ ¬φ. It is routine to show that∆ − isSCU κ -consistent, by(N)and(DISTK). Extend∆ − to a maximalSCU κ -consistent set ∆∈Ω. Thenψ|K i ψ∈Γ⊆∆and¬φ∈∆. For eachn∈1, . . . ,κand formulaχ, we haveU n i χ∈Γ⇔U n i χ∈∆. Indeed, ifU n i χ∈Γ, then (4 ∗ )givesK i U n i χ∈Γ, soU n i χ∈∆. Conversely, ifU n i χ/∈Γ, then¬U n i χ∈Γby maximality; by theorem (5 ∗ ),K i ¬U n i χ∈Γ, hence¬U n i χ∈∆, soU n i χ/∈∆. Thus settingg n i :=f n i is type-correct for the∆-domain requirement inW c . Define⃗g=g n j |j∈I,n∈1, . . . ,κby: forj=i, letg n i :=f n i ; forj̸=i, letg n j (ψ):=ψ n whenever U n j ψ∈∆. This is well-defined becauseψ n ∈E c and gr c (ψ n ) =n. To constructG=G j |j∈I, for eachj∈Idefine S ∆,⃗g,j :=⟨c,φ⟩|φ∈Λ ∪ ⟨g n j (ψ),ψ⟩|n∈1, . . . ,κ,U n j ψ∈∆, and then letS 0 ∆,⃗g,j :=S ∆,⃗g,j ,S m+1 ∆,⃗g,j :=cl j (S m ∆,⃗g,j ),S ∞ ∆,⃗g,j := S m∈N S m ∆,⃗g,j , andG j :=S ∞ ∆,⃗g,j . EachG j is base- extending and closed under (App j ), (Sum j ), and (Int j ). SetG:=G j |j∈Iand letw ′ :=⟨∆,G,⃗g⟩. Thenw ′ ∈W c . By the definition ofR c i , sinceψ|K i ψ∈Γ⊆∆andf n i =g n i for alln∈1, . . . ,κ, we havewR c i w ′ . Finally,¬φ∈∆by construction. Lemma 4.8(U n i -Existence Lemma).Let w=⟨Γ,F, ⃗ f⟩∈W c , fix i∈I and n∈1, . . . ,κ, and assume U n i φ/∈Γand⟨t,φ⟩∈F i for some t∈E c n . There exists w ′ =⟨∆,G,⃗g⟩∈W c such that wR c i w ′ and⟨t,φ⟩/∈G i . Proof.Fixw=⟨Γ,F, ⃗ f⟩. Define, for this proof: C 0 :=⟨c,φ⟩|φ∈Λ ∪ ⟨f m i (ψ),ψ⟩|m∈1, . . . ,κ,U m i ψ∈Γ, andC k+1 :=cl i (C k ),C ∞ := S k∈N C k . ThusC ∞ is the least agent-iexplanation store generated fromΓand the witness maps ⃗ fby the admissibility conditions. Claim 1.If⟨t,φ⟩∈C ∞ and gr c (t)⩾n⩾1, thenU n i φ∈Γ. Claim 2.Given the fixedw=⟨Γ,F, ⃗ f⟩∈W c ,i∈Iandt∈E c , if⟨t,φ⟩/∈C ∞ , then there exists w ′ =⟨∆,G,⃗g⟩∈W c such thatwR c i w ′ and⟨t,φ⟩/∈G i . Proof of Claim 1.We prove by induction onk∈Nthat each pair inC k has, inΓ, all positive understanding formulas up to the grade of its term: P(k):∀⟨u,ψ⟩∈C k ∀ℓ(1⩽ℓ⩽gr c (u)⇒U ℓ i ψ∈Γ). Y. Wei763 Fork=0, there are two kinds of pairs inC 0 . If⟨u,ψ⟩=⟨c,λ⟩withλ∈Λ, then gr c (c) =1 andU 1 i λ is derivable by(NE), hence belongs toΓ. If⟨u,ψ⟩=⟨f m i (ψ),ψ⟩, thenU m i ψ∈Γby definition of the domain off m i ; for any 1⩽ℓ⩽m,(DEG)yieldsU ℓ i ψ∈Γ. For the induction step, take⟨u,ψ⟩∈C k+1 =cl i (C k )and 1⩽ℓ⩽gr c (u). If⟨u,ψ⟩∈C k , apply IH. Otherwise: (App)u=r·swith⟨r,χ→ψ⟩,⟨s,χ⟩∈C k . Leta:=gr c (r),b:=gr c (s), andh:=mina,b; then gr c (u) =h. By IH and(DEG),U h i (χ→ψ),U h i χ∈Γ. By(DISTU),U h i ψ∈Γ, and then(DEG)yields U ℓ i ψ∈Γ. (Sum)u=r+sand either⟨r,ψ⟩∈C k or⟨s,ψ⟩∈C k . Assume⟨r,ψ⟩∈C k . Seta:=gr c (r)andh:=gr c (u). Since 1⩽ℓ⩽h, we haveh⩾1. By the grade definition for+, this yieldsh<a, henceℓ <a. By IH,U a i ψ∈Γ, and then(DEG)givesU ℓ i ψ∈Γ. (Int)u=!rwith⟨r,K i ψ⟩∈C k . If gr c (r) =0, then gr c (u) =0, impossible since 1⩽ℓ⩽gr c (u). If gr c (r)⩾1, then gr c (u) =2. By IH,U 1 i K i ψ∈Γ. By(KYU),U 2 i K i ψ∈Γ, and then(DEG)yields U ℓ i K i ψ∈Γ. SoP(k+1)holds. HenceP(k)holds for allk. If⟨t,φ⟩∈C ∞ , then⟨t,φ⟩∈C k for somek, and applying P(k)withℓ:=n(since 1⩽n⩽gr c (t)) yieldsU n i φ∈Γ. Proof of Claim 2.Set∆:=Γ, and for eachm∈1, . . . ,κletg m i :=f m i . Forj̸=i, defineg m j (ψ):=ψ m forU m j ψ∈∆. Then⃗gsatisfies the typing condition in the definition ofW c , andg m i =f m i for allm. LetG i :=C ∞ . By hypothesis,⟨t,φ⟩/∈G i . For eachj̸=i, let S ∆,⃗g,j :=⟨c,φ⟩|φ∈Λ ∪ ⟨g m j (ψ),ψ⟩|m∈1, . . . ,κ,U m j ψ∈∆, and defineS 0 ∆,⃗g,j :=S ∆,⃗g,j ,S k+1 ∆,⃗g,j :=cl j (S k ∆,⃗g,j ),S ∞ ∆,⃗g,j := S k∈N S k ∆,⃗g,j , andG j :=S ∞ ∆,⃗g,j . LetG:=G j |j∈I and definew ′ :=⟨∆,G,⃗g⟩. Forj=i,G i =C ∞ is base-extending and closed under (App i ), (Sum i ), (Int i ) by construction. Forj̸=i, eachG j has the same closure properties by the iterative construction above. Hencew ′ ∈W c . Also,ψ|K i ψ∈Γ⊆∆andf m i =g m i for allm, sowR c i w ′ . Finally,⟨t,φ⟩/∈G i . Now we conclude the lemma. If⟨t,φ⟩∈C ∞ , then Claim 1 givesU n i φ∈Γ, contradiction. Hence ⟨t,φ⟩/∈C ∞ . By Claim 2 there exists ani-successorw ′ =⟨∆,G,⃗g⟩∈W c with⟨t,φ⟩/∈G i . With these existence lemmas in place, we prove the bounded Truth Lemma. Lemma 4.9(Truth Lemma forCELU κ ).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φ=K i ψ: • AssumeK i ψ∈Γ, and letw ′ =⟨∆,G,⃗g⟩satisfywR c i w ′ . By definition ofR c i ,χ|K i χ∈Γ⊆∆, henceψ∈∆. By IH,M c ,w ′ ⊨ψ. SoM c ,w⊨K i ψ. • AssumeM c ,w⊨K i ψ. IfK i ψ/∈Γ, then¬K i ψ∈Γby maximality. By Lemma 4.7, there is w ′ =⟨∆,G,⃗g⟩withwR c i w ′ and¬ψ∈∆. By IH,M c ,w ′ ̸⊨ψ, contradiction. HenceK i ψ∈Γ. Forφ=U n i ψ: • AssumeU n i ψ∈Γ. Lett:=f n i (ψ); then gr c (t) =n, sot∈E c n . We show thattwitnessesU n i ψatw. Letw ′ =⟨∆,G,⃗g⟩satisfywR c i w ′ . By the definition ofR c i ,g n i =f n i . Sinceψ∈dom(f n i ), we have ψ∈dom(g n i ), henceU n i ψ∈∆. The base condition forG i gives⟨g n i (ψ),ψ⟩∈G i , and therefore ⟨t,ψ⟩∈G i . Thusw ′ ∈E c i (t,ψ). From(UYK)andU n i ψ∈Γ, we getK i ψ∈Γ. By theK i -case already proved,M c ,w⊨K i ψ. ThereforeM c ,w⊨U n i ψ. 764Better Understanding, Understanding Better • AssumeM c ,w⊨U n i ψ. Then there existst∈E c n such that∀v∈W c (wR c i v⇒v∈E c i (t,ψ)). Since R c i is reflexive,w∈E c i (t,ψ), i.e.⟨t,ψ⟩∈F i . IfU n i ψ/∈Γ, then Lemma 4.8 givesw ′ =⟨∆,G,⃗g⟩with wR c i w ′ and⟨t,ψ⟩/∈G i . Hencew ′ /∈E c i (t,ψ), contradiction. ThereforeU n i ψ∈Γ. Forφ= (i≻j)ψ. First handle the special casei=j. By theorem(IRREF), noΓcontains(i≻i)ψ. Semantically,M c ,w⊨(i≻i)ψis impossible since it would require deg i (w,ψ)>deg i (w,ψ). Hence, M c ,w⊨(i≻i)ψ⇔(i≻i)ψ∈Γ. Now assumei̸=j. • Assume(i≻j)ψ∈Γ. From(CMP1),K j ψ∈ΓandU 1 i ψ∈Γ. From(CMPκ),¬U κ j ψ∈Γ. By IH, M c ,w⊨K j ψ. LetS j :=n⩽κ|U n j ψ∈Γ. By(DEG),S j is downward closed. Since¬U κ j ψ∈Γ, we haveS j ̸=1, . . . ,κ. IfS j =/0, then deg j (w,ψ) =0, whileU 1 i ψ∈Γgives deg i (w,ψ)⩾1 by IH. IfS j ̸=/0, letm+1⩽κbe the least not inS j . Thenm⩽κ−1 andS j =1, . . . ,m. Hence U m j ψ∈ΓandU m+1 j ψ/∈Γ; then¬U m+1 j ψ∈Γ, and by(CMPn),U m+1 i ψ∈Γ. By IH, deg j (w,ψ) =m and deg i (w,ψ)⩾m+1. In either case, deg i (w,ψ)>deg j (w,ψ). SoM c ,w⊨(i≻j)ψ. • AssumeM c ,w⊨(i≻j)ψ. ThenM c ,w⊨K j ψ, soK j ψ∈Γby IH. If deg j (w,ψ) =0, then deg i (w,ψ)⩾1, henceM c ,w⊨U 1 i ψ, andM c ,w⊨¬U 1 j ψ; by IH, both belong toΓ, hence(i≻ j)ψ∈Γby(UYC0). If deg j (w,ψ) =m⩾1, then necessarilym⩽κ−1. ThenM c ,w⊨U m j ψ∧ ¬U m+1 j ψandM c ,w⊨U m+1 i ψ. By IH these formulas are inΓ, and(UYC)yields(i≻j)ψ∈Γ. Theorem 4.10(Completeness forSCU κ ).Fixκ⩾2. ForΣ∪φ⊆CELU κ ,Σ|=φimpliesΣ⊢ SCU κ φ. Proof.AssumeΣ⊬ SCU κ φ. ThenΣ∪¬φisSCU κ -consistent. Extend it to a maximalSCU κ -consistent setΓ∈Ω. By Lemma 4.3, chooseF, ⃗ fwithw:=⟨Γ,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κ-effectiveif the following can be done effectively. Given finiteC⊆CELU κ , finiteJ⊆I, and finite setsX i (i∈J)of pairs⟨s,ψ⟩, withsa graded explanation term andψ∈C, one can decide, for eachi∈J, eachφ∈C, and each 1⩽m⩽κ, whether there exists a termtsuch that gr(t)⩾mand⟨t,φ⟩∈ X i ∪⟨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κ⩾2and assume thatΛisκ-effective. Then satisfiability and validity overCELU κ are decidable. Proof sketch.We prove an effective finite-model property. Givenφ∈CELU κ , form the finite clo- sureCofφunder subformulas, negation, downward closure for understanding levels (U m+1 i ψbrings inU m i ψ), theK i ψassociated withU m i ψ, and, for each comparative subformula(i≻j)ψ, the formulas K j ψ,U m i ψ,U m j ψfor 1⩽m⩽κ. Only proposition letters and agents occurring inCare relevant. CallX⊆Ca completeC-type if it decides every formula inCand respects the Boolean connectives. Enumerate finite structures whose states are completeC-types, with equivalence relationsR i matching the K i -formulas. ForU-formulas, require class-uniformity: ifX R i Y, thenXandYcontain the same formulas U m i ψfromC. Letδ i (X,ψ)be the largest suchm, or 0 if none exists. For eachδ i (X,ψ)>0, add one fresh witnesse i,[X] i ,ψ of that grade, shared across theR i -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. Wei765 exactly those structures in which theU m i ψ-labels match this generated-witness condition and the truth of ψthroughout the relevantR i -class, and in which(i≻j)ψ∈Xiffδ i (X,ψ)>δ j (X,ψ)andK j ψ∈X. Filtration of any model satisfyingφthroughCyields an accepted finite structure, and any accepted structure is realized as a finite model with its states, relations, atom valuation, and least generated expla- nation stores. Induction on formulas inCgives agreement between truth and membership in the corre- sponding 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 systemSCU, 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 wit- nesses, along the lines of [10]. Lemma 4.12(ω-Lindenbaum extension).EverySCU-consistent set extends to a maximalSCU-consistent set that is closed under allω-introduction instances. Proof.AssumeΣisSCU-consistent. Note thatCELUand the set ofω-introduction instances are count- able. Enumerate the formulas ofCELUas(θ s ) s∈N . LetRbe the set of allω-introduction instances, and fix a listingr:N→Rin which every instance occurs infinitely often. At stages, writer(s)as the rule with premisesχ s →B n s (n∈N + )and conclusionχ s →B ω s , whereB ω s is obtained fromB n s by replacing the displayedU n withU ω . We define the sequence(Γ s ) s∈N recursively byΓ 0 :=Σ, and, givenΓ s , first set H s := ( Γ s ∪θ s ,Γ s ∪θ s isSCU-consistent, Γ s ∪¬θ s ,otherwise. If¬(χ s →B ω s )∈H s , let Γ s+1 :=H s ∪¬(χ s →B n s s ), wheren s is the least positive integer such thatH s ∪¬(χ s →B n s s )isSCU-consistent. Otherwise let Γ s+1 :=H s . We first show that this recursion is well-defined and that everyΓ s isSCU-consistent. The basis is immediate. For the step, supposeΓ s is consistent. At least one ofΓ s ∪θ s andΓ s ∪¬θ s is consis- tent; 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. ThusH s is consistent. If no suchn s existed in this finite-failure-witness step, then for everyn∈N + ,H s ∪¬(χ s →B n s )would be inconsistent; by Lemma 3.5,H s ⊢ SCU χ s →B n s for alln, and theω-introduction instancer(s)would yieldH s ⊢ SCU χ s →B ω s , contradicting consistency ofH s . LetΓ ∗ := S s∈N Γ s . The construction has the following finite-failure property: if the conclusion χ→B ω of anω-introduction instance has its negation inΓ ∗ , then¬(χ→B n )∈Γ ∗ for somen∈N + . Indeed, once¬(χ→B ω )has entered the construction, choose a later stagesat whichr(s)is that same instance. Such a stage exists because every instance occurs infinitely often. The witness step at stages then adds¬(χ→B n )for somen. It remains to check thatΓ ∗ is a maximalSCU-consistent set and is closed under allω-introduction instances. First,Γ ∗ decides every formula: ifθ=θ s , then stages+1 puts eitherθor¬θintoΓ ∗ . EverySCU-theorem belongs toΓ ∗ . Otherwise, sinceΓ ∗ decides formulas,¬η∈Γ ∗ for some theorem η. Then¬η∈Γ s for somes, 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χ→B n of an instance are inΓ ∗ but the conclusionχ→B ω is not, then¬(χ→B ω )∈Γ ∗ . By 766Better Understanding, Understanding Better the finite-failure property,¬(χ→B n )∈Γ ∗ for somen. Since the construction is increasing, someΓ s contains bothχ→B n and its negation, contradicting consistency ofΓ s . Finally,Γ ∗ isSCU-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 somes, contradicting consistency ofΓ s . Now letΩ ∞ be the set of maximalSCU-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 byCELU, and every bounded index range1, . . . ,κreplaced byN + . For every Γ∈Ω ∞ , there existF=F i |i∈Iand a witness family ⃗ f such that⟨Γ,F, ⃗ f⟩∈W c ∞ . Proof.Exactly as in Lemma 4.3: definef n i (ψ):=ψ n onψ|U n i ψ∈Γ, and let eachF i be the least closure of the corresponding base under (App i ), (Sum i ), and (Int i ). The construction is purely syntactic and independent of whetherΓ∈ΩorΓ∈Ω ∞ . LetM c ∞ = (W c ∞ ,R c i i∈I ,V c ,E c ,gr c ,E c i i∈I )be the canonical model overΩ ∞ obtained in this way. Lemma 4.14(FullK i -Existence Lemma).If w=⟨Γ,F, ⃗ f⟩∈W c ∞ and¬K i φ∈Γ, then there exists w ′ = ⟨∆,G,⃗g⟩∈W c ∞ such that wR c i w ′ and¬φ∈∆. Proof.Let∆ − :=ψ|K i ψ∈Γ∪¬φ. We first show that∆ − isSCU-consistent. Suppose otherwise. Let a proof tree of⊥from∆ − be given. We claim, by induction on this tree, that for every node labelα, K i (¬φ→α)∈Γ. For assumption leaves, eitherα=ψwithK i ψ∈Γ, orα=¬φ. In the first case, normal modal rea- soning givesK i (¬φ→ψ)∈ΓfromK i ψ∈Γ; in the second,K i (¬φ→¬φ)∈Γfollows by necessitation. Axiom leaves,(NE)-nodes, and closed(N)-nodes are theorems, so the desired formulaK i (¬φ→α)also follows by necessitation. The(MP)case is standard. For anω-introduction node, write its premises asχ→B n (n∈N + )and its conclusion asχ→B ω . By the induction hypothesis,K i (¬φ→(χ→B n ))∈Γfor everyn. Equivalently, by normal modal reasoning,K i ((¬φ∧χ)→B n )∈Γfor everyn. By propositional reasoning, these give the premises⊤→ K i ((¬φ∧χ)→B n )of the corresponding(ωI)-instance, whose conclusion is⊤→K i ((¬φ∧χ)→B ω ). SinceΓis closed under allω-introduction instances, we obtain⊤→K i ((¬φ∧χ)→B ω )∈Γ, hence K i ((¬φ∧χ)→B ω )∈Γ, and thereforeK i (¬φ→(χ→B ω ))∈Γ. At the root we obtainK i (¬φ→⊥)∈Γ, and henceK i φ∈Γ, contradicting¬K i φ∈Γ. Thus∆ − is consistent. By Lemma 4.12, extend∆ − to some∆∈Ω ∞ . For everyn∈N + and formulaχ,U n i χ∈ΓiffU n i χ∈∆: the forward direction uses(4 ∗ ), and the backward direction uses(5 ∗ ), exactly as in the boundedK i -Existence Lemma. Hence we may setg n i :=f n i for alln. Forj̸=i, letg n j (ψ):=ψ n wheneverU n j ψ∈∆. BuildG=G j |j∈Ifrom∆and⃗gby the same base-and-closure construction used in Lemma 4.13. Thenw ′ :=⟨∆,G,⃗g⟩belongs toW c ∞ . Since ψ|K i ψ∈Γ⊆∆andg n i =f n i for alln, we havewR c i w ′ . Finally,¬φ∈∆by construction. Lemma 4.15.Let w=⟨Γ,F, ⃗ f⟩∈W c ∞ , fix i∈I and n∈N + , and assumeU n i φ/∈Γand⟨t,φ⟩∈F i for some t∈E c n . There exists w ′ =⟨∆,G,⃗g⟩∈W c ∞ such that wR c i w ′ and⟨t,φ⟩/∈G i . Proof.It is the same as Lemma 4.8, withN + in place of1, . . . ,κ.ω-introduction is not used. Y. Wei767 Lemma 4.16(Truth Lemma forCELU).Forφ∈CELUand w=⟨Γ,F, ⃗ f⟩∈W c ∞ :M c ∞ ,w⊨φiffφ∈Γ. Proof.Induction onφ. The Boolean cases are standard. TheK i case uses Lemma 4.14. The finite-level U n i case is the same as in Lemma 4.9, using Lemma 4.15 for the refutation direction. Forφ=U ω i ψ. • IfU ω i ψ∈Γ, then by(DEG n ω ),U n i ψ∈Γfor everyn⩾1. By IH,M c ∞ ,w⊨U n i ψfor everyn⩾1, henceM c ∞ ,w⊨U ω i ψ. • IfM c ∞ ,w⊨U ω i ψ, then by semanticsM c ∞ ,w⊨U n i ψfor alln⩾1, so by the finite-levelU-case U n i ψ∈Γfor alln⩾1. By closure under the basicω-introduction instance,U ω i ψ∈Γ. Forφ= (i≻j)ψ. The casei=jis the same as in Lemma 4.9. Assumei̸=j. • Assume(i≻j)ψ∈Γ. By(CMP1)and(CMPω),K j ψ,U 1 i ψ,¬U ω j ψ∈Γ; henceM c ∞ ,w⊨K j ψby the precedingK-case. LetS j :=n⩾1|U n j ψ∈Γ. By(DEG),S j is downward closed andS j ̸= N + ; otherwise the basicω-introduction instance would contradict¬U ω j ψ∈Γ. IfS j =/0, then deg j (w,ψ) =0, whileU 1 i ψ∈Γgives deg i (w,ψ)⩾1 by the finite-levelU-case. IfS j ̸=/0, letm+1 be the least not inS j . Thenm⩾1 andS j =1, . . . ,m. HenceU m j ψ,¬U m+1 j ψ∈Γand, by(CMPn), U m+1 i ψ∈Γ. By the finite-levelU-case, deg j (w,ψ) =mand deg i (w,ψ)⩾m+1. In either case, deg i (w,ψ)>deg j (w,ψ), soM c ∞ ,w⊨(i≻j)ψ. • AssumeM c ∞ ,w⊨(i≻j)ψ. ThenK j ψ∈Γby theK-case. The degree inequality also gives deg j (w,ψ)̸=ω. If deg j (w,ψ) =0, then deg i (w,ψ)⩾1 andU 1 j ψis false. By the finite-level U-case,U 1 i ψ,¬U 1 j ψ∈Γ; hence(i≻j)ψ∈Γby(UYC0). If deg j (w,ψ) =m⩾1, then deg i (w,ψ)⩾ m+1. By the finite-levelU-case,U m j ψ,¬U m+1 j ψ,U m+1 i ψ∈Γ; then(UYC)yields(i≻j)ψ∈Γ. Theorem 4.17(Strong completeness forSCU).For allΣ∪φ⊆CELU,Σ|=φimpliesΣ⊢ SCU φ. Proof.AssumeΣ⊬ SCU φ. By Lemmas 3.5 and 4.12, chooseΓ ∞ ∈Ω ∞ withΣ∪¬φ ⊆Γ ∞ . By Lemma 4.13, chooseF, ⃗ fsuch thatw:=⟨Γ ∞ ,F, ⃗ f⟩∈W c ∞ . LetM c ∞ be the corresponding canonical model overΩ ∞ . By Lemma 4.16,M c ∞ ,w⊨ΣandM 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, communica- tion, 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. 768Better Understanding, Understanding Better References [1] Sergei Artemov (2008):The logic of justification.The Review of Symbolic Logic1(4), p. 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.Con- ceptus40(98), p. 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, p. 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.Theoria66(2), p. 129–144, doi:10.1111/j.1755- 2567.2000.tb01159.x. [8] Felipe Morales Carbonell (2025):Compressing Graphs: a Model for the Content of Understanding.Erken- ntnis90, p. 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), p. 955–960. [10] D. Doder & Z. Ognjanovi ́ c (2024):Probabilistic Temporal Logic with Countably Additive Semantics.Annals of Pure and Applied Logic175, p. 103389, doi:10.1016/j.apal.2023.103389. [11] Miguel Egler (2021):Why Understanding-Why Is Contrastive.Synthese199(3–4), p. 6061–6083, doi:10.1007/s11229-021-03059-x. [12] Melvin Fitting (2004):A logic of explicit knowledge.Logica Yearbook, p. 11–22. [13] Melvin Fitting (2005):The logic of proofs, semantically.Annals of Pure and Applied Logic132(1), p. 1–25, doi:10.1016/j.apal.2004.04.009. [14] Emma C Gordon (2012):Is there propositional understanding?Logos & Episteme3(2), p. 181–192, doi:10.5840/logos-episteme20123234. [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, p. 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), p. 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 Science64(1), p. 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.Synthese196(11), p. 4583–4603, doi:10.1007/s11229-017-1672-9. Y. Wei769 [22] Rachel McKinnon (2012):How do you know that ‘how do you know?’Challenges a speaker’s knowledge? Pacific Philosophical Quarterly93(1), p. 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 America120(13), p. e2215907120, doi:10.1073/pnas.2215907120. [24] Duncan Pritchard (2014):Knowledge and understanding. In:Virtue Epistemology Naturalized, Springer, p. 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 Society115(1, Part 1), p. 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 A44(3), p. 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 Intel- ligence, Springer International Publishing, Cham, p. 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, p. 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, p. 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. Synthese191(14), p. 3367–3391, doi:10.1007/s11229-014-0452-z. [33] Daniel A. Wilkenfeld (2019):Understanding as Compression.Philosophical Studies176(10), p. 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.Synthese198(2), p. 1259– 1285, doi:10.1007/s11229-019-02104-0.