Abstract
Taking an intuitionistic stance and regarding proof theory as methodologically basic for semantics and logic, we develop, building on previous work (J. Log. Comput. 31(3): 704-770, 2021; Bull. Symb. Log. 32(1): 136-196, 2026), a proof-theoretic framework for the study of the inferential interaction between counterfactuals and belief/knowledge. Relying on the technical results obtained for this framework (preservation, normalization, the subexpression property), we give a proof-theoretic semantics for elementary constructions which combine (counter)factuals, belief, knowledge, disbelief, and ignorance.
Similar content being viewed by others
1 Introduction
In reasoning in which counterfactuals and doxastic attitude verbs (specifically, ‘believes that’ and ‘knows that’) interact, three kinds of construction, two of which are basic, play a central role. Firstly, constructions which embed a doxastic attitude in the antecedent and/or consequent of a counterfactual. An example of this kind is (1.1). We shall call constructions of this basic kind conditional embeddings. They subsume both counterfactually conditionalizing belief/knowledge (the attitude governs the antecedent) and counterfactually conditionalized belief/knowledge (the attitude governs the consequent). Secondly, constructions which prefix a doxastic attitude to a counterfactual like, for example, (1.2). We shall call constructions of this basic kind doxastic prefixings. Finally, constructions which do both, for instance (1.3), possibly stacking the embedding and/or the prefixing.
-
(1.1)
If (agent) a knew that A, a would [might] believe that B.
-
(1.2)
a knows that if A were the case, B would [might] be the case.
-
(1.3)
a knows that if a knew that A, a would [might] believe that B.
Although reasoning with such constructions is naturally construed as an inferential process, in which one passes from assumptions to conclusions, and although the tools and techniques of structural proof theory (cf. Negri and von Plato (2001), Troelstra and Schwichtenberg (2000)) make it a natural framework for the formal study of inference, structural proof-theoretic research on the interaction of counterfactuals and belief/knowledge is scarce. A rare example is, perhaps, Girlando et al. (2018), where a labelled (or external) sequent calculus for the logic of conditional belief (CDL, conditional doxastic logic; cf. Baltag and Smets (2006, 2008)) which aims at modeling revisable belief is developed. I write ‘perhaps’, because ‘interaction’ is here presumably not the right word. Specifically, belief is here formally rendered in terms of a conditional belief operator, where a formula of the form \(B^{P}_{a}(Q)\) is understood as a counterfactual construction: “if the agent would learn P, then (after learning) he would come to believe that Q was the case in the current state (before the learning)” ( Baltag and Smets (2006): 13) or, simpler, “a would come to believe that Q, if a learned that P”. The operator for knowledge is then defined by \(K_{a}(P) =_{def} B^{\lnot P}_{a}(\bot )\) or \(K_{a}(P) =_{def} B^{\lnot P}_{a}(P)\) (cf. Baltag and Smets (2006): 15). Thus, in CDL, counterfactuals and belief/knowledge can be seen as merged rather than as interacting.
The merge reading is not mandatory, though. It is common to read \(B^{P}_{a}(Q)\) as “after learning that P, a comes to believe that Q”. On this reading, we cannot even speak of a merge, let alone of an interaction between the counterfactual and belief/knowledge, as it removes any counterfactual connotation from the conditional belief operator. What, at bottom, is counterfactual about that operator is the fact that the explanation of its meaning (e.g., Baltag and Smets (2006): 8) draws on the model-theoretic semantics in the tradition of Stalnaker and Lewis (e.g., Lewis (1973), Nute and Cross (2001), Stalnaker (1968)) that is used to explain the meaning of counterfactuals (or maybe, more adequately, that of comparative possibility statements). If these observations are correct, we cannot necessarily view (Girlando et al., 2018) as a contribution to the proof-theoretic study of the interaction between counterfactuals and belief/knowledge.
This said, we note that conditional beliefs of the form of “a would come to believe that Q, if a learned that P” are not covered by our conditional embeddings, since such beliefs crucially involve the component ‘learn that’, not taken into account here, in the antecedent. (The phenomena attached to conditional belief are closely related to those concerning hypothetical knowledge studied in the context of game theory, e.g., Arló-Costa and Bicchieri (2007), Halpern (1999), Samet (1996), Stalnaker (1996).)
Furthermore, as the subtitle “From Neighbourhood Semantics to Sequent Calculus” of Girlando et al. (2018) suggests, the authors take a perspective on the logic and the semantics of counterfactuals and belief/knowledge on which model-theoretic structure is methodologically fundamental. Specifically, the model-theoretic semantics of CDL is, in effect, incorporated into the labelled proof system for it. Moreover, since that proof system is designed for CDL, it also incorporates classical logic.
In what follows, we take a proof-theoretic perspective on counterfactuals (cf. Więckowski (2024a, 2026)) and belief/knowledge (cf. Więckowski (2021b)) rather than a model-theoretic one. On our perspective, proof-theoretic structure, more specifically, the structure of agent-relative derivations from counterfactual assumptions will be methodologically fundamental. And, importantly, we take an intutionistic stance. We shall explain the meaning of combinations such as (1.1)-(1.3)—and their factual analogues—such as
-
(1.4)
Since a knows that A, a believes [might believe] that B.
-
(1.5)
a knows that since A is the case, B is [might be] the case.
-
(1.6)
a knows that since A is the case, a believes [might believe] that B.
proof-theoretically on the basis of canonical derivations in suitably defined intuitionistic proof systems. (For an overview of proof-theoretic semantics see Francez (2015), Schroeder-Heister (2024).) The contrast is that in the causal (or reason giving) ‘since’-sentences (factuals) involved in (1.4)-(1.6) the antecedents are, intuitively, true, whereas they are not true in the counterfactuals contained in (1.1)-(1.3).
On our perspective, the fundamental notions for the study of the logic of the aforementioned combinations will be the notions of derivation and proof in such systems rather than the notion of a model-theoretically defined consequence relation (paradigmatically, “all (intuitionistic) models of the premisses are models of the conclusion”) and validity (“truth in all models”). Completeness will be understood as an internal property of a proof system (cf. Więckowski (2026)), rather than as an external one (that is shown to hold for that system “with respect to” structures such as intuitionistic models; typically, external completeness is established by appeal to classical reasoning in the metatheory (e.g., van Dalen (2002)), something that is not appealing from a foundational intuitionistic point of view).
The intuitionistic proof systems which we shall develop to make the above ideas precise, will be systems of doxastic modal subatomic natural deduction which combine the doxastic components of the systems for intuitionistic belief/knowledge presented in Więckowski (2021b) with the modal components of the systems for (counter)factuals studied in detail in Więckowski (2026). The resulting systems are doxastic, since they construe knowledge as a special case of belief. And they are modal, because they make use of assumption modes for formulae. These modes are sensitive to the factuality status (e.g., factual, counterfactual) of the formula that is to be assumed, where that status is determined by a doxastic reference proof system on top of which the doxastic modal proof system is defined.
In order to make the structural elements of our proof-theoretic approach to the study of the inferential interaction between (counter)factuals and belief/knowledge perspicuous, we shall consider only very elementary doxastic modal systems. They will comprise essentially only the relevant forms of implication (specifically, factual and counterfactual) in addition to the operators for belief and knowledge, and resources for the analysis of simple constructions which deal with doubt (‘does not believe’) and ignorance (‘does not know’).
Before embarking on the study of the interaction between the (counter)factual and the doxastic/epistemic by means of doxastic modal proof systems, we give an informal description of the workings of these systems and provide a roadmap of that project in the next section.
2 Preparations
Consider the following scenario that draws on Otfried Preußler’s stories about the adventures of Kasperl and Seppel with the robber Hotzenplotz. Hotzenplotz, the renowned robber with seven knives, robbed Kasperl’s grandmother of her beloved coffee grinder. Taking the minutes for this misdeed, the clumsy village policeman Alois Dimpfelmoser says:
-
(2.1)
If I knew that Hotzenplotz observes Grandmother, I would believe that he is going to rob her.
Dimpfelmoser’s reasoning by which he arrives at this counterfactual embedding is naturally construed as an inference, inside his system of beliefs, by which he derives the consequent (formally: \(\textsf {B}_{\underline{d}}(Rhg)\)) of (2.1) from the counterfactual assumption of its antecedent (\(\textsf {K}_{\underline{d}}(Ohg)\)). Roughly, the derivation process can be illustrated as follows: Dimpfelmoser makes the counterfactual assumption that \(\textsf {K}_{\underline{d}}(Ohg)\). Intuitively, he is entitled to do so, because he does not consider \(\textsf {K}_{\underline{d}}(Ohg)\) to be a fact. To be more precise, (2.1) is here construed narrowly as a contrary-to-fact conditional. Specifically, the intuition is that “counterfactuals are subjunctive conditionals whose antecedents are assumed to be not settled” (cf. Więckowski (2026): 137). Dimpfelmoser then infers, inside the context of the counterfactual assumption, that Ohg. Next, he uses the information that he associates with ‘robs’ (R), ‘Hotzenplotz’ (h), and ‘Grandmother’ (g) to infer, still inside the context of his counterfactual assumption, that Rhg. From this he infers \(\textsf {B}_{\underline{d}}(Rhg)\) in the next step, making his belief that Rhg explicit. In the last step, he discharges the counterfactual assumption of \(\textsf {K}_{\underline{d}}(Ohg)\) and concludes that (2.1) holds, given that \(\textsf {B}_{\underline{d}}(Rhg)\) occurs in a factual context after the discharge.
Now, for an only slightly different example. Seppel, Karperl’s buddy, knows that Dimpfelmoser is afraid of Hotzenplotz and thinks that Kasperl is determined to bring back the stolen coffee grinder to Grandmother. Seppel thinks to himself:
-
(2.2)
Since I know that Dimpfelmoser is afraid of Hotzenplotz, I might believe that Kasperl will seek Hotzenplotz.
Seppel arrives at this factual embedding by way of deriving its consequent, \(\textsf {B}_{\underline{s}}(Skh)\), from the factual assumption of its antecedent, \(\textsf {K}_{\underline{s}}(Adh)\), inside his belief system. Here, the inferential process can be described as follows: Seppel makes the factual assumption that \(\textsf {K}_{\underline{s}}(Adh)\). Intuitively, he is entitled to do so, because he does consider \(\textsf {K}_{\underline{s}}(Adh)\) a fact. From this he infers, inside a factual context, that Adh. After that, Seppel makes use of the information that he associates with ‘seek’ (S), ‘Kasperl’ (k), and ‘Hotzenplotz’ (h) to infer, still inside the context of his factual assumption, that Skh. In the next step, he makes this belief explicit inferring \(\textsf {B}_{\underline{d}}(Skh)\). Finally, he discharges the factual assumption of \(\textsf {K}_{\underline{s}}(Adh)\) and concludes that (2.2) holds, given that \(\textsf {B}_{\underline{d}}(Skh)\) occurs in a counterfactual context after the discharge.
Sentence (2.1) is an instance of (1.1) and sentence (2.2) an instance of (1.4). In the first derivation, the antecedent of (2.1) is assumed in the counterfactual mode by the agent, as it is not considered settled by him. By contrast, in the second derivation, the antecedent of (2.2) is assumed in the factual mode by the agent, as the agent considers it an established fact. Intuitively, the agent has to make up his mind concerning the factuality status of the formula that is to be assumed. In the framework we shall study, the agent determines this status within his doxastic reference proof system on which his modal proof system is based. Section 3 explains what a doxastic reference proof system is. Section 4 defines doxastic modal proof systems. It is these systems which we shall apply to the reasoning in the above and other cases.
Sections 5 and 6 establish results for these systems (specifically, preservation, normalization, subexpression/subformula property) which are important for an approach to semantics and logic that takes proof theory to be methodologically fundamental. (In particular, normalization guarantees, e.g., computational tractability, whereas the subformula property ensures, e.g., consistency and internal completeness.) In other words, Sections 4-6 suggest, how the inferential interaction between belief/knowledge and (counter)factuals can be made precise proof-theoretically.
Among the benefits of the aforementioned results is the fact that in doxastic modal proof systems (and in the reference proof systems they incorporate), the meaning of a formula can be explained in terms of canonical derivations. Such derivations use an introduction rule in the last inference step. Following Gentzen’s well-known suggestion (cf. Gentzen (1934): 189), we take introduction rules to be meaning determining. Once its formal structure is made explicit, the derivation for (2.1) turns out to be canonical, since it derives (2.1) according to the meaning of its main operator, the ‘would’-counterfactual, in the last step. Similarly, the derivation for (2.2) is a canonical one, as it derives (2.2) according to the meaning of the ‘might’-factual in the last step. It is the purpose of Section 7 to formulate a proof-theoretic semantics for elementary constructions which combine (counter)factuals, belief, knowledge, disbelief, and ignorance that is intuitionistically acceptable. Section 8 illustrates this semantics, applying it, among other things, to (2.1), (2.2), and further examples.
After a short digression on CDL’s “after learning that P, a comes to believe that Q” in Section 9, the paper closes with a couple of remarks.
3 Doxastic reference proof systems
The purpose of a doxastic reference proof system is, very roughly, to explain formally what a doxastic agent considers to be a fact.
3.1 The language L0
Doxastic reference proof systems are defined for the base language L0.
Definition 3.1
L0 comprises the following primitive symbols:
-
1.
denumerably many individual (or nominal) constants (metavariables: \(\alpha \), \(\alpha _{i}\));
-
2.
denumerably many n-ary predicate constants (metavariables: \(\varphi ^{n}\), \(\varphi ^{n}_{i}\));
-
3.
the one-place operators − (predication failure), \(\textsf {B}_{\underline{a}}\) (belief), \(\textsf {K}_{\underline{a}}\) (knowledge);
-
4.
the two-place operator \(\supset \) (implication);
-
5.
the logical constant \(\bot \) (absurdity);
-
6.
brackets (, ).
\(\mathcal {C}\) is the set of nominal constants, \(\mathcal {P}\) is the set of predicate constants, and \(\mathcal {C}\cup \mathcal {P}\) is the set of non-logical constants (metavariables: \(\tau \), \(\tau _{i}\)).
Definition 3.2
A prime formula of L0 is either an atomic sentence (\(\varphi ^{n}\alpha _{1}... \alpha _{n}\)), a negative predication (\(-\varphi ^{n}\alpha _{1}... \alpha _{n}\)), or \(\bot \). The notion of a formula (of L0) is defined inductively by:
-
1.
Any prime formula is a formula.
-
2.
If A and B are formulae, then so are \(\textsf {B}_{\underline{a}}(A)\), \(\textsf {K}_{\underline{a}}(A)\), and \(A \supset B\).
Atm is the set of atomic sentences. \(Atm(\alpha ) =_{def} \{A \in Atm: A\) contains at least one occurrence of \(\alpha \in \mathcal {C}\}\) and \(Atm(\varphi ^{n}) =_{def} \{A \in Atm: A\) contains an occurrence of \(\varphi ^{n} \in \mathcal {P}\}\). \(Fml_{0}\) is the set of formulae of L0.
Definition 3.3
Defined operators of L0:
-
1.
\(\lnot A =_{def} A \supset \bot \) (negation);
-
2.
\(A \leftrightarrow B =_{def} (A \supset B)\) & \( (B \supset A)\) (bi-implication).
Remark 3.1
In L0, we may, thus, distinguish between sentential negation ‘it is not the case that A’ (in symbols: \(\lnot A\)) and predicate denial ‘\(\alpha \) isn’t \(\varphi \)’ (in symbols: \(-\varphi \alpha \)). Unlike the defined \(\lnot \)-operator, the primitive −-operator for predication failure (cf. Więckowski (2023)) can be prefixed only to atomic sentences and is sensitive to the internal structure of the formula to which it is applied. (We note in parentheses that predicate denial must not be confused with predicate term negation ‘\(\alpha \) is non-\(\varphi \)’; see Więckowski (2021a).)
3.2 Doxastic reference proof systems
The systems which we shall use as our doxastic reference proof systems (DR-systems, for short) are systems of intuitionistic subatomic natural deduction for belief and knowledge (cf. Więckowski (2021b)) that are single-agent and modified so as to manipulate L0-formulae.
Any DR-system integrates a subatomic system that is relativized to a single agent \({{\varvec{a}}}\).
Definition 3.4
An agent-relative subatomic system \(\mathcal {S}_{{{\varvec{a}}}}\) is a pair \(\langle \mathcal {I}_{{{\varvec{a}}}}, \mathcal {R}_{{{\varvec{a}}}}\rangle \), where \(\mathcal {I}_{{{\varvec{a}}}} = \langle \mathcal {C}, \mathcal {P}, v_{{{\varvec{a}}}}\rangle \) is an agent-relative subatomic base with \(\mathcal {C}\), \(\mathcal {P}\) as above, and \(v_{{{\varvec{a}}}}\) such that:
-
1.
For any \(\alpha \in \mathcal {C}\), \(v_{{{\varvec{a}}}}: \mathcal {C}\rightarrow \wp (Atm)\), where \(v_{{{\varvec{a}}}}(\alpha )\subseteq Atm(\alpha )\).
-
2.
For any \(\varphi ^{n}\in \mathcal {P}\), \(v_{{{\varvec{a}}}}: \mathcal {P}\rightarrow \wp (Atm)\), where \(v_{{{\varvec{a}}}}(\varphi ^{n})\subseteq Atm(\varphi ^{n})\).
For any \(\tau \in \mathcal {C}\cup \mathcal {P}\): \(\tau \Gamma ^{{{\varvec{a}}}} =_{def} v_{{{\varvec{a}}}}(\tau )\). \(\tau \Gamma ^{{{\varvec{a}}}}\) is the set of agent-relative term assumptions for \(\tau \). \(\mathcal {R}_{{{\varvec{a}}}}\) is a set of I/E-rules for atomic sentences (as) and negative predications (\(-as\)):
Side conditions:
asI: \(\varphi ^{n}_{0}\alpha _{1} ... \alpha _{n} \in \varphi ^{n}_{0}\Gamma ^{{{\varvec{a}}}} \cap \alpha _{1}\Gamma ^{{{\varvec{a}}}} \cap ... \cap \alpha _{n}\Gamma ^{{{\varvec{a}}}}\).
\(-as\)I: \(\varphi ^{n}_{0}\alpha _{1} ... \alpha _{n} \not \in \varphi ^{n}_{0}\Gamma ^{{{\varvec{a}}}} \cap \alpha _{1}\Gamma ^{{{\varvec{a}}}} \cap ... \cap \alpha _{n}\Gamma ^{{{\varvec{a}}}}\).
\(as \textrm{E}_{i}\) and \(-as\) \(\textrm{E}_{i}\): \(i \in \{0, ..., n\}\) and \(\tau _{i} \in \{\varphi ^{n}_{0}, \alpha _{1}, ..., \alpha _{n}\}\).
Terminology: We say that \(-\varphi ^{n}_{0}\alpha _{1}... \alpha _{n}\) is negatively contained in \(\varphi ^{n}_{0}\Gamma ^{{{\varvec{a}}}} \cap \alpha _{1}\Gamma ^{{{\varvec{a}}}} \cap ... \cap \alpha _{n}\Gamma ^{{{\varvec{a}}}}\), in case the side condition on \(-as\)I is satisfied.
Remark 3.2
Intuitively, a term assumption can be seen as the unevaluated atomic information that an agent associates with a non-logical constant. The agent may conclude that an atomic sentence is true, in case the term assumptions for the non-logical constants of which that atomic sentence is composed match with respect to that sentence (cf. Więckowski (2021b)). In case there is no match, the agent may conclude that the corresponding negative predication holds (cf. Więckowski (2023)). Due to the presence of rules for two kinds of predication (i.e., as, \(-as\)), these subatomic systems are bipredicational.
We now define the intended DR-systems by stating what a derivation in such a system is. Informal explanations of the rules involved in that definition are given in remarks that follow it.
Definition 3.5
Derivations in \(\textsf {DR}\)-systems.
Basic step. Any term assumption \(\tau \Gamma ^{{{\varvec{a}}}}\) and any L0-formula A assumed by agent \({{\varvec{a}}}\) (i.e., a derivation from the open assumption of A written \(\langle A\rangle _{{{\varvec{a}}}}\)) is a \(\textsf {DR}\)-derivation.
Induction step. If \(\mathcal {D}_{0}\), ..., \(\mathcal {D}_{n}\) are \(\textsf {DR}\)-derivations, then a \(\textsf {DR}\)-derivation can be constructed by means the I/E-rules for as, \(-as\) (Definition 3.4), and the following agent-relative rules:
-
1.
Agent-relative rules for predication conflicts:
Side condition: \(A \in Atm(\alpha )\) for some \(\alpha \in \mathcal {C}\).
-
2.
Agent-relative absurdity rule:
Side condition: \(\bot \) is not a conclusion of c1a.
-
3.
Agent-relative rules for implication:
-
4.
Agent-relative rules for belief:
-
5.
Agent-relative rules for knowledge:
Side condition on \(\textsf {K}_{\underline{a}}\)I: A does not depend on an undischarged formula assumption.
Remark 3.3
1. The rule c1a is maintained in \(\textsf {DR}\)-systems for the purpose of modeling certain natural language constructions considered in Section 8. c1a is one of the c-rules for handling predication conflicts introduced in Więckowski (2023). It is intuitively plausible, but proof-theoretically cumbersome, as \(\bot \) is not a subformula of \(-A\). Due to this fact, \(\bot \)i comes with a side condition which secures the subformula property. For example, this side condition is violated in (1a) and (1b):
In (1a) and (1b), \(\bot \) is neither a subformula of one of the undischarged assumptions nor of the conclusion (cf. Więckowski (2023): Remark 3.43(2)). As we shall stress in Section 6, the terminology of negative containment (not used in Więckowski (2023)) becomes relevant to the formulation of the subformula property in the presence of c-rules.
2. The rules for intuitionistic absurdity and implication are as usual, except that each inference step and assumption is marked by an agent.
3. The \(\textsf {B}_{\underline{a}}\)-rules make an agent’s belief attitudes explicit and model them by means of derivations in that agent’s belief system. The I-rule for belief is very permissive (cf. Więckowski (2021b)). It allows one to introduce a belief formula \(\textsf {B}_{\underline{a}}(A)\) in case its premiss A (i) depends on an undischarged assumption (or is itself an assumption), or (ii) in case it has the form of an atomic sentence or a negative predication that has been derived from term assumptions, or (iii) in case it has been derived as a theorem (Definition 3.6(3) below). In this way, the structure of the derivation of the \(\textsf {B}_{\underline{a}}\)I-premiss allows one to distinguish various kinds of belief ranging from mere belief that is based on a mere assumption of that premiss, to factual belief that is based on atomic facts, to logical belief that is based on proof (cf. Więckowski (2021b): Remark 5.9). \(\textsf {B}_{\underline{a}}\)E is defined to be inverting.
4. The reference proof systems are called “doxastic” rather than “epistemic”, because knowledge is construed as a special case of belief. The side condition on \(\textsf {K}_{\underline{a}}\)I says, in effect, that \(\textsf {K}_{\underline{a}}(A)\) can be introduced in case A has been derived as a theorem, or (unlike in Więckowski (2021b) also) in case A has the form of an atomic sentence or a negative predication that has been derived from term assumption leaves. In other words, an agent can claim to have knowledge of A, only in case A does not depend on assumptions (of formulae)—including assumptions of knowledge. (As a consequence, e.g., \(\textsf {K}_{\underline{a}}(A \supset B) \supset (\textsf {K}_{\underline{a}}(A) \supset \textsf {K}_{\underline{a}}(B))\) is not a theorem of the present \(\textsf {DR}\)-systems; Więckowski (2021b): Theorem 7.2).
Remark 3.4
We mention that normalization and the subexpression (incl. subformula) property hold for our \(\textsf {DR}\)-systems. These results are obtained by combining the relevant parts of the corresponding proofs in Więckowski (2021b, 2023). Indeed, they are special cases of the results presented in Sections 5 and 6 below.
Definition 3.6
-
1.
A derivation \(\mathcal {D}\) of a formula A in a \(\textsf {DR}\)-system is a canonical derivation iff it derives A by means of an I-rule in the last step of \(\mathcal {D}\).
-
2.
A canonical derivation \(\mathcal {D}\) of A in a \(\textsf {DR}\)-system is a canonical proof of A in that system iff there are no applications of rules for as, \(-as\), and no undischarged assumptions in \(\mathcal {D}\).
-
3.
The conclusions of canonical \(\textsf {DR}\)-derivations are \(\textsf {DR}\)-theses and the conclusions of \(\textsf {DR}\)-proofs are also \(\textsf {DR}\)-theorems.
We may now state what an agent counts as a fact.
Definition 3.7
An established thesis (or fact) for the agent of a \(\textsf {DR}\)-system is an L0-formula for which a canonical derivation in that \(\textsf {DR}\)-system has been constructed. \(\Theta _{\textsf {DR}}\) is the set of so far established theses of that system.
Remark 3.5
A consequence of this definition is that an agent may consider an L0-formula an established thesis, even in case the formula derived canonically in the agent’s \(\textsf {DR}\)-system depends on an undischarged assumption. The definition, thus, allows for conditional facts in addition to unconditional ones.
4 Doxastic modal proof systems
Doxastic modal proof systems give formal expression to doxastic reasoning from factual and counterfactual assumptions.
4.1 The language L1
Doxastic modal proof systems are defined for the language L1 which extends L0.
Definition 4.1
Formula of L1:
-
1.
Any formula of L0 is a formula of L1.
-
2.
If A, B are formulae of L1, then so are \(A \supset _{f} B\) (factual implication), \(A \supset _{c} B\) (counterfactual implication), \(A \supset _{*} B\) (mode-sensitive implication), \(\textsf {B}_{\underline{a}*}(A)\) (mode-sensitive belief), and \(\textsf {K}_{\underline{a}*}(A)\) (mode-sensitive knowledge).
\(Fml_{1}\) is the set of formulae of L1. Metalinguistic notation: \(\star ^{i} \in \{\supset , \supset _{f}, \supset _{c}, \supset _{*}\}\).
Notational convention: In case a compound L0-formula A is used as a formula of L1, we write \(\supset _{*}\) [\(\textsf {B}_{\underline{a}*}\), \(\textsf {K}_{\underline{a}*}\)] for occurrences of \(\supset \) [\(\textsf {B}_{\underline{a}}\), \(\textsf {K}_{\underline{a}}\)] in A.
Definition 4.2
Defined operators of L1:
-
1.
\(\lnot _{*} A =_{def} A \supset _{*} \bot \) (mode-sensitive negation);
-
2.
\( A \leftrightarrow _{*} B =_{def} (A \supset _{*} B) \& _{*} (B \supset _{*} A)\) (mode-sensitive bi-implication).
Definition 4.3
-
1.
Any non-logical constant and any formula of L1 is an expression (metavariables: \(\epsilon \), \(\epsilon ^{\prime }\)).
-
2.
Let \(\epsilon \) be an expression (of L1). Subexpressions of \(\epsilon \) are defined by:
-
(a)
\(\epsilon \) is a subexpression of \(\epsilon \).
-
(b)
If \(\varphi ^{n}\alpha _{1}... \alpha _{n}\) is a subexpression of A, then so is \(\varphi ^{n}, \alpha _{1},..., \alpha _{n}\).
-
(c)
If \(-\varphi ^{n}\alpha _{1}... \alpha _{n}\) is a subexpression of A, then so is \(\varphi ^{n}\alpha _{1}... \alpha _{n}\).
-
(d)
If \(\textsf {B}_{\underline{a}*}(B)\), \(\textsf {K}_{\underline{a}*}(B)\), is a subexpression of A, then so is B.
-
(e)
If \(B \star ^{i} C\) is a subexpression of A, then so are B and C.
-
(a)
Special cases of subexpressions:
Definition 4.4
Let A be a formula (of L1). Subformulae of A are defined by:
-
1.
A is a subformula of A.
-
2.
If \(-\varphi ^{n}\alpha _{1}... \alpha _{n}\) is a subformula of A, then so is \(\varphi ^{n}\alpha _{1}... \alpha _{n}\).
-
3.
If \(\textsf {B}_{\underline{a}*}(B)\), \(\textsf {K}_{\underline{a}*}(B)\) is a subformula of A, then so is B.
-
4.
If \(B \star ^{i} C\) is a subformula of A, then so are B and C.
4.2 Doxastic modal proof systems
Doxastic modal proof systems (DM-systems, for short) are modal, because they maintain modes of making assumptions.
Definition 4.5
Assumption modes. There are three modes in which a formula can be assumed by an agent in a DM-system:
-
1.
\(\langle |A|\rangle _{{{\varvec{a}}}}\) indicates that A is assumed by \({{\varvec{a}}}\) in the factual mode, given that \(A \in Fml_{0}\) and \(A\in \Theta _{\textsf {DR}}\).
-
2.
\(\langle \wr A\wr \rangle _{{{\varvec{a}}}}\) indicates that A is assumed by \({{\varvec{a}}}\) in the counterfactual mode, given that \(A \in Fml_{0}\) and \(A \in \Theta _{\textsf {DR}}^{c}\), where \(\Theta _{\textsf {DR}}^{c} =_{def} Fml_{0}\setminus \Theta _{\textsf {DR}}\).
-
3.
\(\langle (A)\rangle _{{{\varvec{a}}}}\) indicates that A is assumed by \({{\varvec{a}}}\) in the independent mode, where \(A \in Fml_{1}\). Specifically, in case A is also an L0-formula, A is assumed independently of whether it is contained in \(\Theta _{\textsf {DR}}\) or \(\Theta _{\textsf {DR}}^{c}\).
\(\langle /A/\rangle _{{{\varvec{a}}}}\) indicates that A is assumed by \({{\varvec{a}}}\) in one of the three modes.
Definition 4.6
Modal status: Formulae. A formula A in a derivation \(\mathcal {D}\) in a DM-system may have three different kinds of modal status:
-
1.
A has factual status in \(\mathcal {D}\), if it depends on no counterfactual assumption, and either
-
(a)
A depends on at least one factual assumption (special case: \(\langle | A|\rangle _{{{\varvec{a}}}}\)), or
-
(b)
A has been derived by means of term assumptions, or
-
(c)
A is a conclusion of a canonical derivation in \(\textsf {DR}\).
-
(a)
-
2.
A has counterfactual status in \(\mathcal {D}\), if it depends on at least one counterfactual assumption (special case: \(\langle \wr A\wr \rangle _{{{\varvec{a}}}}\)).
-
3.
A has independent (or neutral) status in \(\mathcal {D}\), if it has no factual or counterfactual status (special case: \(\langle ( A)\rangle _{{{\varvec{a}}}}\)).
Definition 4.7
Modal status: Term assumptions. Any term assumption \(\tau \Gamma ^{{{\varvec{a}}}}\) in a derivation \(\mathcal {D}\) in a DM-system has factual status.
Definition 4.8
Modal status: Further notation.
-
1.
\(|\mathcal {D}|\) [\(\wr \mathcal {D}\wr \), \((\mathcal {D})\)] indicates that the conclusion of \(\mathcal {D}\) has factual [counterfactual, independent] status.
-
2.
\(/\mathcal {D}/\) indicates that the conclusion of \(\mathcal {D}\) has one of the three kinds of status (factual, counterfactual, independent).
-
3.
Negated status markers: means either or \((\mathcal {D})\), means either \(| \mathcal {D}|\) or \((\mathcal {D})\), and means either \(| \mathcal {D}|\) or .
Definition 4.9
Modal status: Derivations with conclusions and assumptions made explicit. We use \([\langle / A/\rangle _{{{\varvec{a}}}}]^{(u)}\) to denote a set (possibly, a singleton) of agent-relative undischarged assumptions of occurrences of A marked by u. Three of the following derivations are illegitimate, the rest (basic cases) is legitimate:
The illegitimate combinations are (b), (g), (h). Convention: (\(\dagger \)) covers only the basic cases.
We now define the intended DM-systems by defining the notion of a derivation in such systems. We first state the precise definition and give informal explanations of the rules involved in DM-systems in subsequent remarks.
Definition 4.10
Derivations in \(\textsf {DM}\)-systems.
Basic step. Any derivation in the \(\textsf {DR}\)-system (Definition 3.5) of a \(\textsf {DM}\)-system, any L0-formula A assumed by agent \({{\varvec{a}}}\) in the factual (resp. counterfactual) mode \(\langle |A|\rangle _{{{\varvec{a}}}}\) (resp. \(\langle \wr A\wr \rangle _{{{\varvec{a}}}}\)) and any L1-formula A assumed by \({{\varvec{a}}}\) in the independent mode \(\langle (A)\rangle _{{{\varvec{a}}}}\) is a derivation in that \(\textsf {DM}\)-system.
Induction step. If \(/\mathcal {D}_{0}/\), ..., \(/\mathcal {D}_{n}/\) are \(\textsf {DM}\)-derivations then a \(\textsf {DM}\)-derivation can be constructed by means of the following rules:
-
1.
Modal agent-relative rules for atomic sentences:
Side conditions:
asI: \(\varphi ^{n}_{0}\alpha _{1} ... \alpha _{n} \in \varphi ^{n}_{0}\Gamma ^{{{\varvec{a}}}} \cap \alpha _{1}\Gamma ^{{{\varvec{a}}}} \cap ... \cap \alpha _{n}\Gamma ^{{{\varvec{a}}}}\). \(as\) \(\textrm{E}_{i}\): \(i \in \{0, ..., n\}\) and \(\tau _{i} \in \{\varphi ^{n}_{0}, \alpha _{1}, ..., \alpha _{n}\}\).
-
2.
Modal agent-relative rules for negative predications:
Side conditions:
\(-as\)I: \(\varphi ^{n}_{0}\alpha _{1} ... \alpha _{n} \not \in \varphi ^{n}_{0}\Gamma ^{{{\varvec{a}}}} \cap \alpha _{1}\Gamma ^{{{\varvec{a}}}} \cap ... \cap \alpha _{n}\Gamma ^{{{\varvec{a}}}}\). \(-as\) \(\textrm{E}_{i}\): \(i \in \{0, ..., n\}\) and \(\tau _{i} \in \{\varphi ^{n}_{0}, \alpha _{1}, ..., \alpha _{n}\}\).
(Like in Definition 3.4, the terminology of negative containment applies.)
-
3.
Modal agent-relative rule for predication conflicts:
Side condition: \(A \in Atm(\alpha )\) for some \(\alpha \in \mathcal {C}\).
-
4.
Modal agent-relative absurdity rule:
Side condition: \(\bot \) is not a conclusion of \(c_{*}\)1a.
-
5.
Modal agent-relative rules for implications:
Side conditions:
- sc1.:
-
\(\supset _{f}\)I: No empty discharge; and no empty discharge in \(\mathcal {D}_{1}\).
- sc2.:
-
\(\supset _{c}\)I: Like sc1.
- sc3.:
-
\(\supset _{c}\)E: In case A and B are distinct formulae, the conclusion of \(\supset _{c}\)E must not be the minor premiss of an application of another application of \(\supset _{c}\)E or of \(\supset _{*}\)E (break formula, for short).
-
6.
Modal agent-relative rules for belief:
-
7.
Modal agent-relative rules for knowledge:
Side conditions on \(\textsf {K}_{\underline{a}*}\)I:
- sc4.:
-
In case = \((\mathcal {D}_{1})\): A does neither depend on a term assumption nor on an undischarged formula assumption.
- sc5.:
-
In case = \(|\mathcal {D}_{1}|\): A does not depend on an undischarged formula assumption.
Assumption principles: The following principles are respected by any derivation \(\mathcal {D}\) in a \(\textsf {DM}\)-system:
- ap1.:
-
No formula is assumed in more than one mode in \(\mathcal {D}\).
- ap2.:
-
The mode in which an antecedent A is assumed in \(\star ^{i}\)I-applications in \(\mathcal {D}\) determines the modal status of all antecedent A-nodes (i.e., minor premisses of \(\star ^{i}\)E-applications) in \(\mathcal {D}\).
Remark 4.1
1. The rules \(as_{*}\)I/E, \(-as_{*}\)I/E, \(c_{*}\)1a, \(\bot _{*}\)i, and \(\textsf {B}_{\underline{a}*}\)I/E are like the corresponding rules in \(\textsf {DR}\)-systems, except that they apply to formulae and term assumptions that come with a modal status.
2. \(\supset _{f}\)I/E and \(\supset _{c}\)I/E: These rules may involve a nesting of status markers. In general, if \(/\mathcal {D}/\) is a derivation of the form (\(\dagger \)), we write \(//\mathcal {D}//\) for the new derivation resulting from the application of an \(\star ^{i}\)I-rule which discharges the members of \([/ A/]^{(u)}\):
In \(//\mathcal {D}//\) the (optional) inner slashes indicate the status of B and the outer ones the status of \(A \star ^{i} B\) after the discharge by \(\star ^{i}\)I. sc1 [sc2] blocks weakening, and thus monotonicity for factuals [counterfactuals]. \(\supset _{f}\)E [\(\supset _{c}\)E] allows one to infer B from the premisses \(A \supset _{f} B\) [\(A \supset _{c} B\)] and A, in case the latter has factual [counterfactual] status. sc3 blocks transitivity for counterfactuals. The side conditions imposed on \(\supset _{c}\)I/E are motivated by the familiar counterfactual fallacies (see Więckowski (2026) for further discussion).
3. \(\supset _{*}\)I/E: These rules turn the \(\supset \)I/E-rules of \(\textsf {DR}\)-systems into mode-sensitive rules and contain them as a special case. No side conditions are imposed on them. However, the rules for \(\supset _{*}\) are, like those for \(\supset _{f}\) and \(\supset _{c}\), subject to ap2 which passes on the status of the assumptions of the antecedents of \(A \star ^{i} B\)-formulae to all A-nodes in derivations in \(\textsf {DM}\)-systems.
4. \(\textsf {K}_{\underline{a}*}\)I/E: \(\textsf {K}_{\underline{a}*}\)I insists that knowledge must not rest on counterfactual assumptions. This granted, \(\textsf {K}_{\underline{a}*}(A)\) can be introduced, in case A has independent status (sc4); in this case A is a \(\textsf {DM}\)-theorem that is not a \(\textsf {DR}\)-theorem. Alternatively, \(\textsf {K}_{\underline{a}*}(A)\) can be introduced, in case A has factual status (sc5); in this case A is either derived from term assumption leaves (and possibly discharged formula assumptions), or a \(\textsf {DR}\)-theorem. \(\textsf {K}_{\underline{a}*}\)E is like \(\textsf {K}_{\underline{a}}\)E, but modal.
Definition 4.11
Canonical derivation, canonical proof, thesis, theorem (\(\textsf {DM}\)-systems). Analogous to Definition 3.6.
5 Preservation and normalization
In order to prove normalization for \(\textsf {DM}\)-systems, we shall adapt the familiar methods (cf. Prawitz (1965), Troelstra and Schwichtenberg (2000), van Dalen (2004)) taking also the issue of preservation (cf. Więckowski (2026)) into account.
Definition 5.1
An L1-formula which is the conclusion of an I-rule and at the same time the major premiss of an E-rule is a maximum (or cut) formula (or a maximum).
Definition 5.2
Rank, maximal cut formula, cut rank (\(\textsf {DM}\)-systems):
-
1.
The rank of a term assumption \(\tau \Gamma \) is defined by: \(r(\tau \Gamma )=0\).
-
2.
The rank of an atomic sentence \(\varphi ^{n}\alpha _{1}... \alpha _{n}\) is defined by: \(r(\varphi ^{n}\alpha _{1}... \alpha _{n}) = 1\).
-
3.
Let A, B be formulae and let \(\textsf {E}\in \{\textsf {B}_{\underline{a}}, \textsf {K}_{\underline{a}}, \textsf {B}_{\underline{a}*}, \textsf {K}_{\underline{a}*}\}\), \(\star ^{i}\in \{\supset , \supset _{f}, \supset _{c}, \supset _{*}\}\). The rank of \(\bot \) [\(\textsf {E}(A)\), \(A \star ^{i} B\)] is defined by: \(r(\bot ) = 0\) [\(r(\textsf {E}(A)) = r(A)+1\), \(r(A \star ^{i} B) = max(r(A), r(B))+1\)].
-
4.
A cut formula with maximal rank is a maximal cut formula.
-
5.
The cut rank of a \(\textsf {DM}\)-derivation \(/\mathcal {D}/\) is defined by: \(cr(/\mathcal {D}/) = \langle d, n\rangle \), where:
-
1.
\(d = max\{r(A)\): A is a cut formula in \(/\mathcal {D}/\}\); in case there is no cut formula, \(max\emptyset = 0\).
-
2.
n = number of maximal cut formulae in \(/\mathcal {D}/\).
-
1.
Definition 5.3
Derivations in \(\textsf {DM}\)-systems which do not contain cut formulae (or maxima) are said to be normal or in normal form.
Maximum formulae in derivations are removed by means of detour conversions.
Definition 5.4
Detour conversions (\(\textsf {DM}\)-systems):
-
1.
\(as_{*}\)-Conversions:
-
2.
\(-as_{*}\)-Conversions:
-
3.
\(\star ^{i}\)-Conversions:
-
4.
\(\textsf {B}_{\underline{a}*}\)-Conversion:
-
5.
\(\textsf {K}_{\underline{a}*}\)-Conversion:
Due to the presence of status markers, specific side conditions, and assumption principles in \(\textsf {DM}\)-systems the question arises whether it may happen that the detour conversions transform a derivation into a non-derivation (cf. Więckowski (2026)). By the preservation theorem, this is precluded.
Theorem 5.1
Preservation (DM-systems). The detour conversions do not transform derivations in DM-systems into non-derivations.
Proof
The proof is by exhaustion of cases. We need to check only conversions in which rules are applied which combine requirements concerning modal status with side conditions. These are the conversions for the \(\star ^{i}\)-operators (strictly speaking, only for \(\supset _{f}\) and \(\supset _{c}\)) and for \(\textsf {K}_{\underline{a}*}\). The proof comprises two parts.
-
Part A: preservation for \(\star ^{i}\)-conversions
-
Part B: preservation for \(\textsf {K}_{\underline{a}*}\)-conversion
We note that none of the remaining conversions (i.e., those for \(as_{*}\), \(-as_{*}\), \(\textsf {B}_{\underline{a}*}\)) involves rules with requirements concerning modal status. The rules for \(as_{*}\), \(-as_{*}\) impose only side conditions on term assumptions and thus do not affect the interaction with the other rules which operate exclusively on formulae. Also \(\textsf {B}_{\underline{a}*}\)-conversion cannot give rise to complications, as the \(\textsf {B}_{\underline{a}*}\)-rules are entirely unconstrained.
Part A: Preservation for \(\star ^{i}\)-conversions. Let , be legitimate derivations. We show: If these derivations can be combined into a legitimate derivation \(\mathcal {D}^{*}\), then the \(\star ^{i}\)-conversions transform \(\mathcal {D}^{*}\) into a legitimate derivation \(\mathcal {D}^{**}\); otherwise, the combination is illegitimate and an \(\star ^{i}\)-conversion is precluded:
In the proof we follow the top-down procedure described in Więckowski (2026). A combination is illegitimate, in case it gives rise to a violation (Figure 1), where, strictly speaking, VK1 is a special case of VK2.
(We note that \(\bot _{*}\)i comes with a side condition which affects the interaction of this rule with \(c_{*}\)1a. We may here rely on the observation mentioned in Remark 3.3(1) which applies also to \(\supset _{*}\)I/E of which \(\supset _{f}\)I/E and \(\supset _{c}\)I/E are restricted versions.)
Part A of the proof is condensed in preservation tables A.1-4 below. Each table is characterized by three letters in brackets each of which indicates the kind of operator (I for \(\star ^{i}\), K for \(\textsf {K}_{\underline{a}*}\)) involved in the construction of \(\mathcal {D}^{*}\): A.1. (III), A.2. (IIK), A.3. (IKI), A.4. (IKK). The first letter indicates the kind of main operator of the maximum formula, the second the kind of operator of the last rule used in \(\mathcal {D}^{a}\), and the third the kind of operator of the last rule used in \(\mathcal {D}^{b}\). In each A-table, the entries below \(\supset _{f}\)-c [\(\supset _{c}\)-c, \(\supset _{*}\)-c] indicate the results for \(\supset _{f}\) [\(\supset _{c}\), \(\supset _{*}\)]-conversion; \(\bullet \) [\(\circ \)] indicates that the combination \(\mathcal {D}^{*}\) is legitimate [illegitimate] and its the \(\star ^{i}\)-conversion into \(\mathcal {D}^{**}\) successful [precluded]. In case of illegitimacy, the kind of violation is indicated. For each kind of conversion, the number of illegitimate derivations (I-number) is listed.
In table A.1 (cf. Więckowski (2026)), there are two entries, since \(\mathcal {D}^{a}\) ends with \(\star ^{i}\)E. The first [second] entry in the (c)- and (d)-cases indicates the result for the construction in which the \(\star ^{i}\)-maximum is introduced discharging an assumption which is used to derive the major [minor] premiss of that \(\star ^{i}\)E-application.
Example 5.1
-
1.
Case A.1.1.b. \(\alpha \): \(\mathcal {D}^{a}\) ends with \(\supset _{f}\)I, \(\mathcal {D}^{b}\) ends with \(\supset _{f}\)E: \(\bullet \)
(3) -
2.
Case A.1.2.d2. \(\beta \): \(\mathcal {D}^{a}\) ends with \(\supset _{f}\)E, \(\mathcal {D}^{b}\) ends with \(\supset _{c}\)E: \(\circ ^{3, 6}\)
(4) -
3.
Case A.2.1.d1. \(\beta \): \(\mathcal {D}^{a}\) ends with \(\supset _{f}\)E, \(\mathcal {D}^{b}\) ends with \(\textsf {K}_{\underline{a}*}\)E: \(\bullet \)
(5)
-
4.
Case A.3.2.a. \(\beta \): \(\mathcal {D}^{a}\) ends with \(\textsf {K}_{\underline{a}*}\)I, \(\mathcal {D}^{b}\) ends with \(\supset _{c}\)I: \(\circ ^{1, K1, K2}\)
(6) -
5.
Case A.4.1.c. \(\beta \): \(\mathcal {D}^{a}\) ends with \(\textsf {K}_{\underline{a}*}\)E, \(\mathcal {D}^{b}\) ends with \(\textsf {K}_{\underline{a}*}\)I: \(\circ ^{2a, 4}\)
(7)
A.1 (III) | \(\mathcal {D}^{a}\): | \(\mathcal {D}^{b}\): | \(\alpha \): \(\supset _{f}\)-c | \(\beta \): \(\supset _{c}\)-c | \(\gamma \): \(\supset _{*}\)-c |
|---|---|---|---|---|---|
A.1.1.a | \(\supset _{f}\)I | \(\supset _{f}\)I | \(\circ ^{1}\) | \(\circ ^{1}\) | \(\bullet \) |
A.1.1.b | \(\supset _{f}\)I | \(\supset _{f}\)E | \(\bullet \) | \(\bullet \) | \(\bullet \) |
A.1.1.c | \(\supset _{f}\)E | \(\supset _{f}\)I | \(\circ ^{1}\) | \(\circ ^{1}\) | \(\circ ^{1}\) | \(\circ ^{1, 3}\) | \(\bullet \) | \(\bullet \) |
A.1.1.d | \(\supset _{f}\)E | \(\supset _{f}\)E | \(\bullet \) | \(\bullet \) | \(\bullet \) | \(\circ ^{3}\) | \(\bullet \) | \(\bullet \) |
A.1.2.a | \(\supset _{f}\)I | \(\supset _{c}\)I | \(\circ ^{1}\) | \(\circ ^{1}\) | \(\bullet \) |
A.1.2.b | \(\supset _{f}\)I | \(\supset _{c}\)E | \(\circ ^{2a, 3}\) | \(\circ ^{6}\) | \(\circ ^{6}\) |
A.1.2.c | \(\supset _{f}\)E | \(\supset _{c}\)I | \(\circ ^{1}\) | \(\circ ^{1}\) | \(\circ ^{1}\) | \(\circ ^{1, 3}\) | \(\bullet \) | \(\bullet \) |
A.1.2.d | \(\supset _{f}\)E | \(\supset _{c}\)E | \(\circ ^{2a, 3}\) | \(\circ ^{2a, 3}\) | \(\circ ^{6}\) | \(\circ ^{3, 6}\) | \(\circ ^{6}\) | \(\circ ^{2a, 6}\) |
A.1.3.a | \(\supset _{f}\)I | \(\supset _{*}\)I | \(\bullet \) | \(\bullet \) | \(\bullet \) |
A.1.3.b | \(\supset _{f}\)I | \(\supset _{*}\)E | \(\bullet \) | \(\bullet \) | \(\bullet \) |
A.1.3.c | \(\supset _{f}\)E | \(\supset _{*}\)I | \(\bullet \) | \(\bullet \) | \(\bullet \) | \(\circ ^{3}\) | \(\bullet \) | \(\bullet \) |
A.1.3.d | \(\supset _{f}\)E | \(\supset _{*}\)E | \(\bullet \) | \(\bullet \) | \(\bullet \) | \(\circ ^{3}\) | \(\bullet \) | \(\bullet \) |
A.1.4.a | \(\supset _{c}\)I | \(\supset _{f}\)I | \(\circ ^{1}\) | \(\circ ^{1}\) | \(\bullet \) |
A.1.4.b | \(\supset _{c}\)I | \(\supset _{f}\)E | \(\bullet \) | \(\bullet \) | \(\bullet \) |
A.1.4.c | \(\supset _{c}\)E | \(\supset _{f}\)I | \(\circ ^{1}\) | \(\circ ^{1}\) | \(\circ ^{1}\) | \(\circ ^{1}\) | \(\bullet \) | \(\bullet \) |
A.1.4.d | \(\supset _{c}\)E | \(\supset _{f}\)E | \(\bullet \) | \(\bullet \) | \(\bullet \) | \(\bullet \) | \(\bullet \) | \(\bullet \) |
A.1.5.a | \(\supset _{c}\)I | \(\supset _{c}\)I | \(\circ ^{1}\) | \(\circ ^{1}\) | \(\bullet \) |
A.1.5.b | \(\supset _{c}\)I | \(\supset _{c}\)E | \(\circ ^{2a, 3}\) | \(\circ ^{6}\) | \(\circ ^{6}\) |
A.1.5.c | \(\supset _{c}\)E | \(\supset _{c}\)I | \(\circ ^{1}\) | \(\circ ^{1}\) | \(\circ ^{1}\) | \(\circ ^{1}\) | \(\bullet \) | \(\bullet \) |
A.1.5.d | \(\supset _{c}\)E | \(\supset _{c}\)E | \(\circ ^{2a, 3}\) | \(\circ ^{2a, 3}\) | \(\circ ^{6}\) | \(\circ ^{6}\) | \(\circ ^{6}\) | \(\circ ^{6}\) |
A.1.6.a | \(\supset _{c}\)I | \(\supset _{*}\)I | \(\bullet \) | \(\bullet \) | \(\bullet \) |
A.1.6.b | \(\supset _{c}\)I | \(\supset _{*}\)E | \(\bullet \) | \(\bullet \) | \(\bullet \) |
A.1.6.c | \(\supset _{c}\)E | \(\supset _{*}\)I | \(\bullet \) | \(\bullet \) | \(\bullet \) | \(\bullet \) | \(\bullet \) | \(\bullet \) |
A.1.6.d | \(\supset _{c}\)E | \(\supset _{*}\)E | \(\bullet \) | \(\bullet \) | \(\bullet \) | \(\bullet \) | \(\bullet \) | \(\bullet \) |
A.1.7.a | \(\supset _{*}\)I | \(\supset _{f}\)I | \(\circ ^{1}\) | \(\circ ^{1}\) | \(\bullet \) |
A.1.7.b | \(\supset _{*}\)I | \(\supset _{f}\)E | \(\bullet \) | \(\bullet \) | \(\bullet \) |
A.1.7.c | \(\supset _{*}\)E | \(\supset _{f}\)I | \(\circ ^{1}\) | \(\circ ^{1}\) | \(\circ ^{1}\) | \(\circ ^{1}\) | \(\bullet \) | \(\bullet \) |
A.1.7.d | \(\supset _{*}\)E | \(\supset _{f}\)E | \(\bullet \) | \(\bullet \) | \(\bullet \) | \(\bullet \) | \(\bullet \) | \(\bullet \) |
A.1.8.a | \(\supset _{*}\)I | \(\supset _{c}\)I | \(\circ ^{1}\) | \(\circ ^{1}\) | \(\bullet \) |
A.1.8.b | \(\supset _{*}\)I | \(\supset _{c}\)E | \(\circ ^{2a, 3}\) | \(\circ ^{6}\) | \(\circ ^{6}\) |
A.1.8.c | \(\supset _{*}\)E | \(\supset _{c}\)I | \(\circ ^{1}\) | \(\circ ^{1}\) | \(\circ ^{1}\) | \(\circ ^{1}\) | \(\bullet \) | \(\bullet \) |
A.1.8.d | \(\supset _{*}\)E | \(\supset _{c}\)E | \(\circ ^{2a, 3}\) | \(\circ ^{2a, 3}\) | \(\circ ^{6}\) | \(\circ ^{6}\) | \(\circ ^{6}\) | \(\circ ^{6}\) |
A.1.9.a | \(\supset _{*}\)I | \(\supset _{*}\)I | \(\bullet \) | \(\bullet \) | \(\bullet \) |
A.1.9.b | \(\supset _{*}\)I | \(\supset _{*}\)E | \(\bullet \) | \(\bullet \) | \(\bullet \) |
A.1.9.c | \(\supset _{*}\)E | \(\supset _{*}\)I | \(\bullet \) | \(\bullet \) | \(\bullet \) | \(\bullet \) | \(\bullet \) | \(\bullet \) |
A.1.9.d | \(\supset _{*}\)E | \(\supset _{*}\)E | \(\bullet \) | \(\bullet \) | \(\bullet \) | \(\bullet \) | \(\bullet \) | \(\bullet \) |
I27 | I30 | I9 |
A.2 (IIK) | \(\mathcal {D}^{a}\): | \(\mathcal {D}^{b}\): | \(\alpha \): \(\supset _{f}\)-c | \(\beta \): \(\supset _{c}\)-c | \(\gamma \): \(\supset _{*}\)-c |
|---|---|---|---|---|---|
A.2.1.a | \(\supset _{f}\)I | \(\textsf {K}_{\underline{a}*}\)I | \(\bullet \) | \(\circ ^{2a, 4}\) | \(\bullet \) |
A.2.1.b | \(\supset _{f}\)I | \(\textsf {K}_{\underline{a}*}\)E | \(\bullet \) | \(\bullet \) | \(\bullet \) |
A.2.1.c | \(\supset _{f}\)E | \(\textsf {K}_{\underline{a}*}\)I | \(\bullet \) | \(\bullet \) | \(\circ ^{2a, 4}\) | \(\circ ^{2a, 3, 4}\) | \(\bullet \) | \(\bullet \) |
A.2.1.d | \(\supset _{f}\)E | \(\textsf {K}_{\underline{a}*}\)E | \(\bullet \) | \(\bullet \) | \(\bullet \) | \(\circ ^{3}\) | \(\bullet \) | \(\bullet \) |
A.2.2.a | \(\supset _{c}\)I | \(\textsf {K}_{\underline{a}*}\)I | \(\bullet \) | \(\circ ^{2a, 4}\) | \(\bullet \) |
A.2.2.b | \(\supset _{c}\)I | \(\textsf {K}_{\underline{a}*}\)E | \(\bullet \) | \(\bullet \) | \(\bullet \) |
A.2.2.c | \(\supset _{c}\)E | \(\textsf {K}_{\underline{a}*}\)I | \(\bullet \) | \(\bullet \) | \(\circ ^{2a, 4}\) | \(\circ ^{2a, 4}\) | \(\bullet \) | \(\bullet \) |
A.2.2.d | \(\supset _{c}\)E | \(\textsf {K}_{\underline{a}*}\)E | \(\bullet \) | \(\bullet \) | \(\bullet \) | \(\bullet \) | \(\bullet \) | \(\bullet \) |
A.2.3.a | \(\supset _{*}\)I | \(\textsf {K}_{\underline{a}*}\)I | \(\bullet \) | \(\circ ^{2a, 4}\) | \(\bullet \) |
A.2.3.b | \(\supset _{*}\)I | \(\textsf {K}_{\underline{a}*}\)E | \(\bullet \) | \(\bullet \) | \(\bullet \) |
A.2.3.c | \(\supset _{*}\)E | \(\textsf {K}_{\underline{a}*}\)I | \(\bullet \) | \(\bullet \) | \(\circ ^{2a, 4}\) | \(\circ ^{2a, 4}\) | \(\bullet \) | \(\bullet \) |
A.2.3.d | \(\supset _{*}\)E | \(\textsf {K}_{\underline{a}*}\)E | \(\bullet \) | \(\bullet \) | \(\bullet \) | \(\bullet \) | \(\bullet \) | \(\bullet \) |
I0 | I10 | I0 | |||
A.3 (IKI) | \(\mathcal {D}^{a}\): | \(\mathcal {D}^{b}\): | \(\alpha \): \(\supset _{f}\)-c | \(\beta \): \(\supset _{c}\)-c | \(\gamma \): \(\supset _{*}\)-c |
A.3.1.a | \(\textsf {K}_{\underline{a}*}\)I | \(\supset _{f}\)I | \(\circ ^{1}\) | \(\circ ^{1, K1, K2}\) | \(\circ ^{K2}\) |
A.3.1.b | \(\textsf {K}_{\underline{a}*}\)I | \(\supset _{f}\)E | \(\circ ^{K2}\) | \(\circ ^{K1, K2}\) | \(\circ ^{K2}\) |
A.3.1.c | \(\textsf {K}_{\underline{a}*}\)E | \(\supset _{f}\)I | \(\circ ^{1}\) | \(\circ ^{1}\) | \(\bullet \) |
A.3.1.d | \(\textsf {K}_{\underline{a}*}\)E | \(\supset _{f}\)E | \(\bullet \) | \(\bullet \) | \(\bullet \) |
A.3.2.a | \(\textsf {K}_{\underline{a}*}\)I | \(\supset _{c}\)I | \(\circ ^{1}\) | \(\circ ^{1, K1, K2}\) | \(\circ ^{K2}\) |
A.3.2.b | \(\textsf {K}_{\underline{a}*}\)I | \(\supset _{c}\)E | \(\circ ^{2a, 3}\) | \(\circ ^{6, K1, K2}\) | \(\circ ^{6, K1, K2}\) |
A.3.2.c | \(\textsf {K}_{\underline{a}*}\)E | \(\supset _{c}\)I | \(\circ ^{1}\) | \(\circ ^{1}\) | \(\bullet \) |
A.3.2.d | \(\textsf {K}_{\underline{a}*}\)E | \(\supset _{c}\)E | \(\circ ^{2a, 3}\) | \(\circ ^{6}\) | \(\circ ^{6}\) |
A.3.3.a | \(\textsf {K}_{\underline{a}*}\)I | \(\supset _{*}\)I | \(\circ ^{K2}\) | \(\circ ^{K1, K2}\) | \(\circ ^{K2}\) |
A.3.3.b | \(\textsf {K}_{\underline{a}*}\)I | \(\supset _{*}\)E | \(\circ ^{K2}\) | \(\circ ^{K1, K2}\) | \(\circ ^{K2}\) |
A.3.3.c | \(\textsf {K}_{\underline{a}*}\)E | \(\supset _{*}\)I | \(\bullet \) | \(\bullet \) | \(\bullet \) |
A.3.3.d | \(\textsf {K}_{\underline{a}*}\)E | \(\supset _{*}\)E | \(\bullet \) | \(\bullet \) | \(\bullet \) |
I9 | I9 | I7 | |||
A.4 (IKK) | \(\mathcal {D}^{a}\): | \(\mathcal {D}^{b}\): | \(\alpha \): \(\supset _{f}\)-c | \(\beta \): \(\supset _{c}\)-c | \(\gamma \): \(\supset _{*}\)-c |
A.4.1.a | \(\textsf {K}_{\underline{a}*}\)I | \(\textsf {K}_{\underline{a}*}\)I | \(\circ ^{K2}\) | \(\circ ^{2a, 4, K1, K2}\) | \(\circ ^{K2}\) |
A.4.1.b | \(\textsf {K}_{\underline{a}*}\)I | \(\textsf {K}_{\underline{a}*}\)E | \(\circ ^{K2}\) | \(\circ ^{K1, K2}\) | \(\circ ^{K2}\) |
A.4.1.c | \(\textsf {K}_{\underline{a}*}\)E | \(\textsf {K}_{\underline{a}*}\)I | \(\bullet \) | \(\circ ^{2a, 4}\) | \(\bullet \) |
A.4.1.d | \(\textsf {K}_{\underline{a}*}\)E | \(\textsf {K}_{\underline{a}*}\)E | \(\bullet \) | \(\bullet \) | \(\bullet \) |
I2 | I3 | I2 |
We get V5a, in case in \(\mathcal {D}^{*}\) is \(\langle / B/\rangle _{{{\varvec{a}}}}\) for \(\star ^{i} \in \{\supset _{f}, \supset _{c}\}\).
Part B: Preservation for \(\textsf {K}_{\underline{a}*}\)-conversions. Let be a legitimate derivation. We show: If this derivation can be combined into a legitimate derivation \(\mathcal {D}^{*}\), then the \(\textsf {K}_{\underline{a}*}\)-conversion transforms \(\mathcal {D}^{*}\) into a legitimate derivation \(\mathcal {D}^{**}\); otherwise, the combination is illegitimate and a \(\textsf {K}_{\underline{a}*}\)-conversion is precluded.
(Concerning the side condition on \(\bot _{*}\)i, we note that, by sc4 and sc5, A = \(\bot \) concluded by \(c_{*}\)1a in can never be a premiss to \(\textsf {K}_{\underline{a}*}\)I; thus, a situation in which the I/E-rule in \(\mathcal {D}^{*}\) is replaced by \(\bot _{*}\)i cannot arise.)
Part B of the proof is summarized in the preservation tables B.1. (KII), B.2. (KIK), B.3. (KKI), and B.4. (KKK) below. In the B-tables, the first and second letters are analogous to those in the A-tables, whereas the third one indicates the operator of the last rule applied in \(\mathcal {D}^{*}\).
In table B.1 there are two entries in the (b)-, (c)-, and (d)-cases, due to the presence of an \(\star ^{i}\)E-application in \(\mathcal {D}^{*}\). In the (b)-cases, the first [second] entry indicates the result for the construction of \(\mathcal {D}^{*}\) in which the last rule applied in \(\mathcal {D}^{a}\) is \(\star ^{i}\)I and the \(\textsf {K}_{\underline{a}*}\)-maximum appears above the major [minor] premiss of the last rule applied in \(\mathcal {D}^{*}\) which is an \(\star ^{i}\)E-rule. (In the (b)-cases, the first entry is \(\boxtimes \), in case the \(\star ^{i}\)-operator in \(\star ^{i}\)I and \(\star ^{i}\)E is not the same.) In the (c)-cases, the last rule applied in \(\mathcal {D}^{a}\) above the \(\textsf {K}_{\underline{a}*}\)-maximum is an \(\star ^{i}\)E-rule and the last rule applied in \(\mathcal {D}^{*}\) is an \(\star ^{i}\)I-rule; here, the first [second] entry indicates the result for the construction of \(\mathcal {D}^{*}\) in which the assumption discharged by \(\star ^{i}\)I appears above the major [minor] premiss of the \(\star ^{i}\)E-application. (In the (c)-cases the results never come apart.) Finally, in the (d)-cases, the first [second] entry indicates the result for the construction of \(\mathcal {D}^{*}\) in which the last rule applied in \(\mathcal {D}^{a}\) is \(\star ^{i}\)E and the \(\textsf {K}_{\underline{a}*}\)-maximum appears above the major [minor] premiss of the last rule applied in \(\mathcal {D}^{*}\) which is an \(\star ^{i}\)E-rule.
In table B.3, there are two entries in the (b)- and (d)-cases, as \(\star ^{i}\)E-rules are applied in \(\mathcal {D}^{*}\). In the (b)-cases, the first [second] entry indicates the result for the construction of \(\mathcal {D}^{*}\) in which the last rule applied in \(\mathcal {D}^{a}\) is \(\textsf {K}_{\underline{a}*}\)I and the \(\textsf {K}_{\underline{a}*}\)-maximum appears above the major [minor] premiss of the last rule applied in \(\mathcal {D}^{*}\) which is an \(\star ^{i}\)E-rule. (In the (b)-cases, the first entry is always \(\boxtimes \), since a \(\textsf {K}_{\underline{a}*}\)-formula cannot be a major premiss of an \(\star ^{i}\)E-application.) In the (d)-cases, the first [second] entry indicates the result for the construction of \(\mathcal {D}^{*}\) in which the last rule applied in \(\mathcal {D}^{a}\) is \(\textsf {K}_{\underline{a}*}\)E and the \(\textsf {K}_{\underline{a}*}\)-maximum appears above the major [minor] premiss of the last rule applied in \(\mathcal {D}^{*}\), that is, \(\star ^{i}\)E.
B.1 (KII) | \(\mathcal {D}^{a}\): | \(\mathcal {D}^{*}\): | \(\textsf {K}_{\underline{a}*}\)-c |
|---|---|---|---|
B.1.1.a | \(\supset _{f}\)I | \(\supset _{f}\)I | \(\circ ^{K2}\) |
B.1.1.b | \(\supset _{f}\)I | \(\supset _{f}\)E | \(\bullet \) | \(\bullet \) |
B.1.1.c | \(\supset _{f}\)E | \(\supset _{f}\)I | \(\circ ^{K2}\) | \(\circ ^{K2}\) |
B.1.1.d | \(\supset _{f}\)E | \(\supset _{f}\)E | \(\bullet \) | \(\bullet \) |
B.1.2.a | \(\supset _{f}\)I | \(\supset _{c}\)I | \(\circ ^{K1, K2}\) |
B.1.2.b | \(\supset _{f}\)I | \(\supset _{c}\)E | \(\boxtimes \) | \(\circ ^{4}\) |
B.1.2.c | \(\supset _{f}\)E | \(\supset _{c}\)I | \(\circ ^{K1, K2}\) | \(\circ ^{3, K1, K2}\) |
B.1.2.d | \(\supset _{f}\)E | \(\supset _{c}\)E | \(\bullet \) | \(\circ ^{4}\) |
B.1.3.a | \(\supset _{f}\)I | \(\supset _{*}\)I | \(\circ ^{K2}\) |
B.1.3.b | \(\supset _{f}\)I | \(\supset _{*}\)E | \(\boxtimes \) | \(\bullet \) |
B.1.3.c | \(\supset _{f}\)E | \(\supset _{*}\)I | \(\circ ^{K2}\) | \(\circ ^{K2}\) |
B.1.3.d | \(\supset _{f}\)E | \(\supset _{*}\)E | \(\bullet \) | \(\bullet \) |
B.1.4.a | \(\supset _{c}\)I | \(\supset _{f}\)I | \(\circ ^{K2}\) |
B.1.4.b | \(\supset _{c}\)I | \(\supset _{f}\)E | \(\boxtimes \) | \(\bullet \) |
B.1.4.c | \(\supset _{c}\)E | \(\supset _{f}\)I | \(\circ ^{K1, K2}\) | \(\circ ^{K1, K2}\) |
B.1.4.d | \(\supset _{c}\)E | \(\supset _{f}\)E | \(\circ ^{K1}\) | \(\circ ^{3, K1}\) |
B.1.5.a | \(\supset _{c}\)I | \(\supset _{c}\)I | \(\circ ^{K1, K2}\) |
B.1.5.b | \(\supset _{c}\)I | \(\supset _{c}\)E | \(\bullet \) | \(\circ ^{4}\) |
B.1.5.c | \(\supset _{c}\)E | \(\supset _{c}\)I | \(\circ ^{K1, K2}\) | \(\circ ^{K1, K2}\) |
B.1.5.d | \(\supset _{c}\)E | \(\supset _{c}\)E | \(\circ ^{K1}\) | \(\circ ^{6, K1}\) |
B.1.6.a | \(\supset _{c}\)I | \(\supset _{*}\)I | \(\circ ^{K2}\) |
B.1.6.b | \(\supset _{c}\)I | \(\supset _{*}\)E | \(\boxtimes \) | \(\bullet \) |
B.1.6.c | \(\supset _{c}\)E | \(\supset _{*}\)I | \(\circ ^{K1, K2}\) | \(\circ ^{K1, K2}\) |
B.1.6.d | \(\supset _{c}\)E | \(\supset _{*}\)E | \(\circ ^{K1}\) | \(\circ ^{6, K1}\) |
B.1.7.a | \(\supset _{*}\)I | \(\supset _{f}\)I | \(\circ ^{K2}\) |
B.1.7.b | \(\supset _{*}\)I | \(\supset _{f}\)E | \(\boxtimes \) | \(\bullet \) |
B.1.7.c | \(\supset _{*}\)E | \(\supset _{f}\)I | \(\circ ^{K2}\) | \(\circ ^{K2}\) |
B.1.7.d | \(\supset _{*}\)E | \(\supset _{f}\)E | \(\bullet \) | \(\bullet \) |
B.1.8.a | \(\supset _{*}\)I | \(\supset _{c}\)I | \(\circ ^{K1, K2}\) |
B.1.8.b | \(\supset _{*}\)I | \(\supset _{c}\)E | \(\boxtimes \) | \(\circ ^{4}\) |
B.1.8.c | \(\supset _{*}\)E | \(\supset _{c}\)I | \(\circ ^{K1, K2}\) | \(\circ ^{K1, K2}\) |
B.1.8.d | \(\supset _{*}\)E | \(\supset _{c}\)E | \(\bullet \) | \(\circ ^{4}\) |
B.1.9.a | \(\supset _{*}\)I | \(\supset _{*}\)I | \(\circ ^{K2}\) |
B.1.9.b | \(\supset _{*}\)I | \(\supset _{*}\)E | \(\bullet \) | \(\bullet \) |
B.1.9.c | \(\supset _{*}\)E | \(\supset _{*}\)I | \(\circ ^{K2}\) | \(\circ ^{K2}\) |
B.1.9.d | \(\supset _{*}\)E | \(\supset _{*}\)E | \(\bullet \) | \(\bullet \) |
I38 (\(\boxtimes \)6) |
B.2 (KIK) | \(\mathcal {D}^{a}\): | \(\mathcal {D}^{*}\): | \(\textsf {K}_{\underline{a}*}\)-c |
|---|---|---|---|
B.2.1.a | \(\supset _{f}\)I | \(\textsf {K}_{\underline{a}*}\)I | \(\bullet \) |
B.2.1.b | \(\supset _{f}\)I | \(\textsf {K}_{\underline{a}*}\)E | \(\boxtimes \) |
B.2.1.c | \(\supset _{f}\)E | \(\textsf {K}_{\underline{a}*}\)I | \(\bullet \) |
B.2.1.d | \(\supset _{f}\)E | \(\textsf {K}_{\underline{a}*}\)E | \(\bullet \) |
B.2.2.a | \(\supset _{c}\)I | \(\textsf {K}_{\underline{a}*}\)I | \(\bullet \) |
B.2.2.b | \(\supset _{c}\)I | \(\textsf {K}_{\underline{a}*}\)E | \(\boxtimes \) |
B.2.2.c | \(\supset _{c}\)E | \(\textsf {K}_{\underline{a}*}\)I | \(\circ ^{K1}\) |
B.2.2.d | \(\supset _{c}\)E | \(\textsf {K}_{\underline{a}*}\)E | \(\circ ^{K1}\) |
B.2.3.a | \(\supset _{*}\)I | \(\textsf {K}_{\underline{a}*}\)I | \(\bullet \) |
B.2.3.b | \(\supset _{*}\)I | \(\textsf {K}_{\underline{a}*}\)E | \(\boxtimes \) |
B.2.3.c | \(\supset _{*}\)E | \(\textsf {K}_{\underline{a}*}\)I | \(\bullet \) |
B.2.3.d | \(\supset _{*}\)E | \(\textsf {K}_{\underline{a}*}\)E | \(\bullet \) |
I2 (\(\boxtimes \)3) | |||
B.3 (KKI) | \(\mathcal {D}^{a}\): | \(\mathcal {D}^{*}\): | \(\textsf {K}_{\underline{a}*}\)-c |
B.3.1.a | \(\textsf {K}_{\underline{a}*}\)I | \(\supset _{f}\)I | \(\circ ^{K2}\) |
B.3.1.b | \(\textsf {K}_{\underline{a}*}\)I | \(\supset _{f}\)E | \(\boxtimes \) | \(\bullet \) |
B.3.1.c | \(\textsf {K}_{\underline{a}*}\)E | \(\supset _{f}\)I | \(\circ ^{K2}\) |
B.3.1.d | \(\textsf {K}_{\underline{a}*}\)E | \(\supset _{f}\)E | \(\bullet \) | \(\bullet \) |
B.3.2.a | \(\textsf {K}_{\underline{a}*}\)I | \(\supset _{c}\)I | \(\circ ^{K1, K2}\) |
B.3.2.b | \(\textsf {K}_{\underline{a}*}\)I | \(\supset _{c}\)E | \(\boxtimes \) | \(\circ ^{4}\) |
B.3.2.c | \(\textsf {K}_{\underline{a}*}\)E | \(\supset _{c}\)I | \(\circ ^{K1, K2}\) |
B.3.2.d | \(\textsf {K}_{\underline{a}*}\)E | \(\supset _{c}\)E | \(\bullet \) | \(\circ ^{4}\) |
B.3.3.a | \(\textsf {K}_{\underline{a}*}\)I | \(\supset _{*}\)I | \(\circ ^{K2}\) |
B.3.3.b | \(\textsf {K}_{\underline{a}*}\)I | \(\supset _{*}\)E | \(\boxtimes \) | \(\bullet \) |
B.3.3.c | \(\textsf {K}_{\underline{a}*}\)E | \(\supset _{*}\)I | \(\circ ^{K2}\) |
B.3.3.d | \(\textsf {K}_{\underline{a}*}\)E | \(\supset _{*}\)E | \(\bullet \) | \(\bullet \) |
I8 (\(\boxtimes \)3) | |||
B.4 (KKK) | \(\mathcal {D}^{a}\): | \(\mathcal {D}^{*}\): | \(\textsf {K}_{\underline{a}*}\)-c |
B.4.1.a | \(\textsf {K}_{\underline{a}*}\)I | \(\textsf {K}_{\underline{a}*}\)I | \(\bullet \) |
B.4.1.b | \(\textsf {K}_{\underline{a}*}\)I | \(\textsf {K}_{\underline{a}*}\)E | \(\bullet \) |
B.4.1.c | \(\textsf {K}_{\underline{a}*}\)E | \(\textsf {K}_{\underline{a}*}\)I | \(\bullet \) |
B.4.1.d | \(\textsf {K}_{\underline{a}*}\)E | \(\textsf {K}_{\underline{a}*}\)E | \(\bullet \) |
I0 |
Example 5.2
-
1.
Case B.1.2.d1: \(\mathcal {D}^{a}\) ends with \(\supset _{f}\)E, \(\mathcal {D}^{*}\) ends with \(\supset _{c}\)E: \(\bullet \)
(8) -
2.
Case B.1.4.b1: \(\mathcal {D}^{a}\) ends with \(\supset _{c}\)I, \(\mathcal {D}^{*}\) ends with \(\supset _{f}\)E: \(\boxtimes \)
(9) -
3.
Case B.1.4.d2: \(\mathcal {D}^{a}\) ends with \(\supset _{c}\)E, \(\mathcal {D}^{*}\) ends with \(\supset _{f}\)E: \(\circ ^{3, K1}\)
(10) -
4.
Case B.2.2.b: \(\mathcal {D}^{a}\) ends with \(\supset _{c}\)I, \(\mathcal {D}^{*}\) ends with \(\textsf {K}_{\underline{a}*}\)E: \(\boxtimes \)
(11) -
5.
Case B.3.2.d: \(\mathcal {D}^{a}\) ends with \(\textsf {K}_{\underline{a}*}\)E, \(\mathcal {D}^{*}\) ends with \(\supset _{c}\)E: (d1): \(\bullet \)
(12)(d2): \(\circ ^{4}\)
(13)
\(\square \)
We are now in the position to show the following to hold:
Theorem 5.2
Normalization (DM-systems). Any derivation \(/\mathcal {D}/\) in a DM-system can be transformed into a normal DM-derivation.
Proof
Relying on Theorem 5.1, we apply the detour conversions in the familiar way to remove maximum formulae from \(/\mathcal {D}/\) so as to obtain \(cr(/\mathcal {D}/) = \langle 0, 0\rangle \). \(\square \)
6 Some properties of normal doxastic modal derivations
Next, we consider the structure of normal derivations in \(\textsf {DM}\)-systems. We do so by combining the relevant parts of the adaptations of the familiar definitions and results (cf. Prawitz (1965), Troelstra and Schwichtenberg (2000)) presented in Więckowski (2021b, 2023, 2026).
Derivations in \(\textsf {DM}\)-systems are composed of units.
Definition 6.1
Let \(/\mathcal {D}/\) be a derivation in a \(\textsf {DM}\)-system.
-
1.
A unit in \(/\mathcal {D}/\) is either an occurrence of (i) a term assumption \(\tau \Gamma \), or (ii) a formula A in \(/\mathcal {D}/\). We use \(U, U^{\prime }\) (possibly subscripted) for units of \(\textsf {DM}\)-systems.
-
2.
In case U is a term assumption \(\tau \Gamma \) in \(/\mathcal {D}/\), \(\tau \) is the expression in U.
Units in \(\textsf {DM}\)-derivations are arranged in tracks.
Definition 6.2
A track of a derivation \(/\mathcal {D}/\) in a \(\textsf {DM}\)-system is a sequence of occurrences of units \(U_{0},..., U_{n}\) such that:
-
1.
\(U_{0}\) is either
-
(a)
a top formula occurrence \(/A_{0}/\) in \(/\mathcal {D}/\), or
-
(b)
a top occurrence of a term assumption \(\tau \Gamma _{0}\);
-
(a)
-
2.
\(U_{i}\) for \(i < n\) is either
-
(a)
a formula occurrence \(A_{i}\) which is not the minor premiss of an instance of \(\star ^{i}\)E, or
-
(b)
an occurrence of a term assumption \(\tau \Gamma _{i}\);
-
(a)
-
3.
\(U_{n}\) is either
-
(a)
a formula occurrence \(A_{n}\) which is either
-
i.
the minor premiss of an instance of \(\star ^{i}\)E, or
-
ii.
the conclusion of \(/\mathcal {D}/\), or
-
iii.
the premiss of an instance of \(c_{*}\)1a which is a conclusion of an application of \(as_{*}\)/\(-as_{*}\)I, or
-
i.
-
(b)
an occurrence of a term assumption \(\tau \Gamma _{n}\).
A \(c_{*}\)1a-premiss that satisfies condition (iii), a subatomically introduced c-premiss.
-
(a)
Remark 6.1
By Definition 3.4, there can be at most one subatomically introduced c-premiss in an application of \(c_{*}\)1a; such a premiss is negatively contained, in case it is introduced by \(-as_{*}\)I.
Example 6.1
In the derivation, more exactly, proof below the tracks are 1-9 (Track 1), 10, 4-9 (Track 2), and 11-12 (Track 3).
If lines 8 and 9 were deleted and if \(-B\) were subatomically introduced by \(-as_{*}\)I rather than assumed (B has to be atomic), \(-B\) would be negatively contained in the term assumptions for the terms of which B is composed and it would be an end unit of a track. This modification would turn this \(\textsf {DM}\)-proof into a \(\textsf {DM}\)-derivation of a thesis.
Tracks in normal \(\textsf {DM}\)-derivations can be divided into three parts.
Theorem 6.1
Let \(/\mathcal {D}/\) be a normal derivation in a \(\textsf {DM}\)-system, and let \(\pi \) be a track \(U_{0},..., U_{n}\) in \(/\mathcal {D}/\). There is a unit \(U_{i}\) in \(\pi \), the minimum part of \(\pi \), which separates the possibly empty parts of \(\pi \), called the elimination (or E-)part and the introduction (or I-)part of \(\pi \), such that:
-
1.
for each \(U_{j}\) in the E-part we have \(j < i\), \(U_{j}\) is a major premiss of an E-rule, and \(U_{j+1}\) is a subexpression of \(U_{j}\), and so each \(U_{j}\) is a subexpression of \(U_{0}\);
-
2.
for each \(U_{j}\) in the I-part we have \(i < j\), and if \(j < n\), then \(U_{j}\) is a premiss of an I-rule and a subexpression of \(U_{j+1}\), thus, each \(U_{j}\) is a subexpression of \(U_{n}\); otherwise \(U_{j}\) is a (possibly negatively contained) premiss of \(c_{*}\)1a, so \(j = n\), and a subexpression of \(U_{n}\);
-
3.
in case \(i \not = n\), \(U_{i}\) is a premiss of an I-rule or of \(\bot _{*}\)i (so \(U_{i}= \bot \)) and a subexpression of \(U_{0}\), or a conclusion of \(c_{*}\)1a (hence, \(U_{i}= \bot \)) and a subexpression of \(U_{n}\).
Proof
We use the fact that \(/\mathcal {D}/\) is normal and inspect the rules of \(\textsf {DM}\)-systems.
In case \(U_{i}\) is the first occurrence of a unit in \(\pi \) which is a premiss of an E-rule, all unit occurrences in \(\pi \) which are major premisses of E-rules precede all unit occurrences in \(\pi \) which are premisses of I-rules or of \(\bot _{*}\)i, and all unit occurrences in \(\pi \) which are not subatomically introduced c-premisses precede all unit occurrences in \(\pi \) which are premisses of the I-rules. Otherwise, \(/\mathcal {D}/\) would not be a normal derivation.
Next, let \(U_{i}\) be the first occurrence of a unit in \(\pi \) which is a premiss of an I-rule, \(\bot _{*}\)i, or of \(c_{*}\)1a. Put \(U_{i} = U_{n}\), in case there is no such unit. In these cases, \(U_{i}\) belongs to the minimum part of \(\pi \).
Since, given these observations, \(U_{i}\) satisfies clauses 1 and 3, every unit occurrence \(U_{j}\) (\(i< j < n\)) is a premiss of an I-rule, of \(\bot _{*}\)i, or of \(c_{*}\)1a. However, the case of \(\bot _{*}\)i is excluded, as the premiss of this rule is \(\bot \), a formula that can only be derived by an E-rule or by \(c_{*}\)1a. Hence, clause 2 is satisfied as well. \(\square \)
All expressions in a track \(\pi \) are, thus, (possibly negatively contained) subexpressions of \(U_{0}\) or \(U_{n}\). Tracks in derivations can be ordered.
Definition 6.3
Let \(/\mathcal {D}/\) be a normal derivation in a \(\textsf {DM}\)-system.
-
1.
A track of order 0 (a main track) in \(/\mathcal {D}/\) is a track ending in a conclusion of \(/\mathcal {D}/\).
-
2.
A track of order \(n+1\) in \(/\mathcal {D}/\) is a track ending either in
A main branch of a derivation in a \(\textsf {DM}\)-system is a branch \(\pi \) which passes only through premisses of (i) the I-rules, (ii) the major premisses of the E-rules, and (iii) premisses of \(c_{*}\)1a that are not subatomically introduced, beginning at a top-unit and ending in the conclusion of the derivation.
Remark 6.2
1. Applications of \(as_{*}\)I and \(-as_{*}\)I undermine the uniqueness of main branches, as do applications of \(c_{*}\)1a with no subatomically introduced c-premisses.
2. By Definition 4.11, no (canonical) proof in a \(\textsf {DM}\)-system contains a subatomically introduced \(c_{*}\)1a-premiss.
Theorem 6.2
In a normal derivation in a \(\textsf {DM}\)-system each occurrence of a unit belongs to a track.
Proof
Left out. \(\square \)
Example 6.2
Tracks 1 and 2 in Example 6.1 are main tracks and main branches. Track 3 is a track of order 1.
Theorem 6.3
Subexpression property (DM-systems). If \(/\mathcal {D}/\) is a normal DM-derivation of a unit U from a set of units \(\Gamma \), then each unit in \(/\mathcal {D}/\) is a subexpression of an expression in \(\Gamma \cup \{U\}\) or negatively contained.
Proof
The proof relies on Theorem 6.1 and proceeds by induction on the order of tracks n using Theorem 6.2. So let \(/\mathcal {D}/\) be a normal derivation of U from \(\Gamma \). Assume that the result holds for unit occurrences in tracks of order \(< n\), let \(\pi = U_{0},..., U_{n}\), and let \(U_{i}\) belong to the minimum part in \(\pi \). There are two cases.
Case 1. For \(U_{n}\) either \(U_{n} = U\) or \(U_{n}\) is (a) a minor premiss of \(\star ^{i}\)E with the major premiss of the form \(U_{n} \star ^{i} B\), or (b) a (possibly negatively contained) subatomically introduced premiss of \(c_{*}\)1a. In each of these cases these premisses appear in a track of order \(n-1\). Hence, the result follows for all \(U_{j}\) (\(i< j <n\)) by Theorem 6.1.
Case 2. Either \(U_{0} \in \Gamma \), or \(U_{0}\) is discharged by an application \({{\varvec{a}}}\) of \(\star ^{i}\)I such that the conclusion of \({{\varvec{a}}}\) has the form \(U_{0} \star ^{i} B\), is contained in the I-part of \(\pi \), or in some track of order \(< n\), and \(U_{0}\) is a subformula of the conditional. Hence, the result follows for all \(U_{j}\) (\(j \le i\)) by Theorem 6.1. \(\square \)
Corollary 6.1
Subformula property (DM-systems). If \(/\mathcal {D}/\) is a normal DM-derivation of formula A from a set of formulae \(\Gamma \), then each formula in \(/\mathcal {D}/\) is a subformula of a formula in \(\Gamma \cup \{A\}\) or negatively contained.
Remark 6.3
Unfortunately, in Więckowski (2023) the additional qualification ‘or negatively contained’ (cf. Definition 3.4) that becomes relevant to the formulation of the subexpression (and subformula) property in the presence of \(c_{*}\)1a (and the other c-rules discussed in Więckowski (2023)) has been left implicit (cf. Więckowski (2023): 124, (22)).
We can also make the following observation:
Corollary 6.2
DM-systems are internally complete by virtue of enjoying the subformula property (cf. Więckowski (2026): Sect. 5.3).
As a consequence of the subformula property, we obtain the following decision method for theoremhood also for DM-systems.
Definition 6.4
Method of counter-derivations (cf. Więckowski (2021b, 2024a, 2026)). Construct a candidate for a normal canonical DM-proof of formula A by proceeding bottom-up using the rules for the operators ignoring the side conditions on them. In case (i) the construction has been successful, check whether the candidate violates a side condition. If this is the case, (ia) we obtain a counter-derivation for A, otherwise (ib) we obtain a normal DM-proof of A. In case (ii) the construction of a candidate has not been successful, we may conclude that A cannot be derived as a theorem. Consequently, we get a decision concerning the DM-derivability of A as a theorem. It is derivable as a theorem in case (ib), and underivable in cases (ia) and (ii).
We shall use this method further below.
7 Proof-theoretic semantics
The results obtained above allow us to formulate an intuitionistically acceptable proof-theoretic semantics.
Definition 7.1
Meaning.
-
1.
The meaning of a non-logical constant \(\tau \) is given by the term assumptions \(\tau \Gamma \) for \(\tau \) which are determined by the subatomic base of the subatomic system of the reference proof system \(\textsf {DR}\) of \(\textsf {DM}\).
-
2.
The meaning of an L1-formula A is given by the set of canonical derivations of A in \(\textsf {DM}\).
Definition 7.2
A formula A of L1 is a truth [logical truth], in case A is the conclusion of a canonical derivation [proof] in an \(\textsf {DM}\)-system (cf. Więckowski (2024a, 2026)).
Remark 7.1
A truth that is not a logical truth may be a conditional one, that is, one that depends on an open formula assumption. In the present systems, conditional truths are precluded as objects of knowledge by the side conditions imposed on \(\textsf {K}_{\underline{a}*}\)I.
In order to investigate both would- and might-counterfactuals, we shall make use of the stereo implications introduced in Więckowski (2026) (Sect. 6.3). These implications are special cases of the mono implications discussed above. They owe their name to the fact that the rules for them are not only sensitive to the modal status of their antecedents, but also to the status of their consequents. The rules for stereo implications make this refinement explicit by means of two subscripts attached to the implication symbol (the left one indicating the status of the antecedent, the right one that of the consequent).
For present purposes it will suffice to consider only four implications of the stereo kind.
Definition 7.3
Rules for stereo implications. I-rules:
E-rules: Mutatis mutandis, like those for mono implications. Side conditions: Like for mono implications.
Remark 7.2
As the outermost status markers of the \(\mathcal {D}\)s in the I-rules for stereo implications make clear, what matters is the status of the consequent after the discharge of the antecedent.
Remark 7.3
We shall adopt the readings of stereo implications proposed in Więckowski (2026).
We may also adopt weaker versions of might-implications:
Definition 7.4
Weak might-implications. I-rules:
The second subscript c/i means that the consequent has either counterfactual or independent status after the discharge. The E-rules and the side conditions for weak implications are like in Definition 7.3. We shall use, somewhat sloppily, the readings proposed in Remark 7.3 also for them.
Remark 7.4
The results obtained for the mono implications (preservation, normalization, subexpression/subformula property) carry over to stereo implications (see Więckowski (2026) for more details). Moreover, the method of counter-derivations applies also to DM-systems that make use of stereo implications (see Section 8). Finally, meaning and truth for stereo implications are defined, mutatis mutandis, like in Definitions 7.1 and 7.2, respectively.
8 Applications: Doxastic attitudes, factuals, and counterfactuals
We now illustrate how our rudimentary DM-systems may contribute to the study of the inferential interaction of doxastic attitudes and (counter)factuals and to the semantics of elementary constructions which combine them from a proof-theoretic perspective.
8.1 Some elementary theorems
Example 8.1
On axioms for epistemic logics and conditional logics. For an assessment of familiar axioms of model-theoretically based epistemic logics by means of the method of counter-derivations see Więckowski (2021b): Remarks 7.4-5. For an analogous assessment of axioms of counterfactual logics see Więckowski (2026): Remark 5.5.
Example 8.2
Some elementary theorems and non-theorems of DM-systems. Figures 3 and 4 display the results of the application of the method of counter-derivations (Definition 6.4) to conditional embeddings of the most elementary kind. Violations of I-rules for stereo implications are listed in Figures 2.
We pick F1, F8 from Figure 3, and C3, C6 from Figure 4:
-
F1.
Since a knows that A, a believes that A.
(15) -
F8.
Since a doesn’t know that A, a might not believe that A.
(16) -
C3.
If a believed that A, a would know that A.
(17) -
C6.
If a didn’t believe that A, a might not know that A.
(18)
The conclusions of the DM-proofs of the theorems in F1 and C6 can both be premisses to applications of \(\textsf {B}_{\underline{a}*}\)I and \(\textsf {K}_{\underline{a}*}\)I.
Remark 8.1
1. By Definition 3.7, an agent may consider an L0-formula A an established theorem (or logical fact), in case a canonical proof of A has been constructed in the agent’s \(\textsf {DR}\)-system. This condition, in effect, precludes an agent’s automatic knowledge of all potential \(\textsf {DR}\)-theorems. In an analogous way, logical omniscience can be avoided also for the agents of \(\textsf {DM}\)-systems.
2. By Definition 7.1(2), the meaning of a DM-theorem A is given by the set of DM-proofs of A. (Due to Corollary 6.1, all such proofs are canonical.) As a consequence, any two theorems A and B will differ in meaning, as their respective sets of canonical proofs will be distinct due to the tree structure of their elements. In this way (perhaps, thinking of these sets as propositions), our semantics can be regarded as being hyperintensionally sensitive.
8.2 Kasperl, Seppel, and Hotzenplotz
We shall now consider a couple of constructions which combine counterfactuals and belief/knowledge which are not natural candidates for theoremhood. The examples of conditional embeddings and doxastic prefixings (cf. Introduction) given below are inspired by Otfried Preußler’s stories about the robber Hotzenplotz. We begin with the two examples informally presented in Section 2.
Example 8.3
On (2.1). Recall:
-
(2.1)
If I (Dimpfelmoser) knew that Hotzenplotz observes Grandmother, I would believe that he is going to rob her.
Let: d (‘Dimpfelmoser’), h (‘Hotzenplotz’), g (‘Grandmother’), O (‘observe’), R (‘rob’). Drawing on the context, we may symbolize (2.1) as \(\textsf {K}_{\underline{d}*}(Ohg) \supset _{c, f} \textsf {B}_{\underline{d}*}(Rhg)\) in L1. Using a DM-system we may model the meaning of (2.1) by means of (normal) canonical derivations for Dimpfelmoser’s own belief system. Here is one such derivation:
If one of the premisses of the \(as_{*}\)I-application were to depend on a counterfactual assumption, the conclusion would take the shape of a ‘might’-counterfactual, \(\textsf {K}_{\underline{d}*}(Ohg) \supset _{c, c} \textsf {B}_{\underline{d}*}(Rhg)\), rather than that of a ‘would’-counterfactual. Note that our DM-systems are defined in such a way that the above conclusion can serve as a premiss to an application of \(\textsf {K}_{\underline{d}*}\)I. This would be precluded, if the conclusion had \(\supset _{c, c}\) as its main operator. The reason is that the systems do not allow for knowledge that rests on counterfactual assumptions. For this reason also an application of \(\textsf {K}_{\underline{d}*}\)I in place of the above application of \(\textsf {B}_{\underline{d}*}\)I would be illegitimate.
Example 8.4
On (2.2). Now, recall:
-
(2.2)
Since I (Seppel) know that Dimpfelmoser is afraid of Hotzenplotz, I might believe that Kasperl will seek Hotzenplotz.
We add: s (‘Seppel’), k (‘Kasperl’), A (‘afraid of’), S (‘seek’). Symbolization of (2.2) in L1: \(\textsf {K}_{\underline{s}*}(Adh) \supset _{f, c} \textsf {B}_{\underline{s}*}(Skh)\). A canonical derivation for (2.2):
If the counterfactual assumption of Sdh were not present in the above derivation, the conclusion would take the shape of an ‘is’-factual, \(\textsf {K}_{\underline{s}*}(Adh) \supset _{f, f} \textsf {B}_{\underline{s}*}(Skh)\). If this were the case, it would be legitimate to apply \(\textsf {K}_{\underline{s}*}\)I to the conclusion, as it would not depend on an undischarged formula assumption.
Example 8.5
Counterfactually mistaking someone else for oneself. To deceive Hotzenplotz, Kasperl and Seppel switch hats. Looking at Kasperl, Seppel says to him:
-
(8.1)
If I didn’t know that I’m looking at you, I’d think (believe) that I’m looking at me.
Let L (‘look at’) and let the other non-logical constants be as before. Again, drawing on the context, we may symbolize (8.1) as \(\lnot _{*} \textsf {K}_{\underline{s}*}(Lsk) \supset _{c, f} \textsf {B}_{\underline{s}*}(Lss)\) in L1. Using a DM-system we may model the meaning of (8.1)—which contains doxastic attitudes de se (cf. Więckowski (2021b))—by means of (normal) canonical derivations for Seppel’s own belief system. Here is one such derivation:
Another canonical derivation for (8.1) is:
Recall that we adopt a contrary-to-fact conception of counterfactuals on which the antecedent is assumed not to be settled. On that conception, the factual status of the relevant background knowledge (here: \(\textsf {K}_{\underline{s}*}(Lsk)\)) may contribute to licensing the counterfactual assumption of its negation (here: \(\lnot _{*} \textsf {K}_{\underline{s}*}(Lsk)\)).Footnote 1
Note that derivations (21) and (22) make crucial use of the intuitionistic absurdity rule. Thus, they are not available in minimal DM-systems. Note, moreover, that due to the side condition imposed on \(\textsf {K}_{\underline{a}*}\)I (cf. Definition 4.10(7)), knowledge introduction can be applied to the conclusion of the former derivation, but not to that of the latter. The intuition here is that knowledge is taken to be unconditional (cf. Remarks 3.5 and 7.1) in the sense that it can be only either directly rooted in proof (the premiss of \(\textsf {K}_{\underline{a}*}\)I is derived as a theorem), or directly rooted in the meaning of the non-logical constants (the premiss of \(\textsf {K}_{\underline{a}*}\)I depends exclusively on term assumption leaves).
Example 8.6
Counterfactually mistaking oneself for someone else. Looking at himself in the mirror, Seppel says to Kasperl:
-
(8.2)
If I didn’t know that I’m looking at me, I’d think that I’m looking at you.
We use the symbolization \(\lnot _{*} \textsf {K}_{\underline{s}*}(Lss) \supset _{c, f} \textsf {B}_{\underline{s}*}(Lsk)\) and modify the derivations from the previous example accordingly.
The following examples are analogous.
Example 8.7
Counterfactually mistaking someone for someone else. Noting that Seppel and Kasperl tried to deceive him, Hotzenplotz says to them:
-
(8.3)
If I didn’t know that I’m looking at Seppel, I’d think that I’m looking at Kasperl. \(\lnot _{*} \textsf {K}_{\underline{h}*}(Lhs) \supset _{c, f} \textsf {B}_{\underline{h}*}(Lhk)\)
This time, the canonical derivations are derivations for Hotzenplotz’s belief system.
Example 8.8
Counterfactually mistaking oneself for oneself. Looking at himself in the mirror, Hotzenplotz says to himself:
-
(8.4)
If I didn’t know that I’m looking at me, I’d think that I’m looking at me. \(\lnot _{*} \textsf {K}_{\underline{h}*}(Lhh) \supset _{c, f} \textsf {B}_{\underline{h}*}(Lhh)\)
We proceed as before. Note that the converse
-
(8.5)
If I didn’t think that I’m looking at me, I’d know that I’m looking at me. \(\lnot _{*} \textsf {B}_{\underline{h}*}(Lhh) \supset _{c, f} \textsf {K}_{\underline{h}*}(Lhh)\)
cannot be derived legitimately:
Knowledge cannot be based on a counterfactual assumption. Note that, here, belief amounts to knowledge, as the derivation of the premiss of \(\textsf {B}_{\underline{h}*}\)I would justify the introduction of knowledge. If that premiss were assumed, the minor premiss of \(\supset _{*, *}\)E would express mere belief which is a special case of conditional belief (cf. Więckowski (2021b)).
Example 8.9
In the scenario of Example 8.5, Seppel may also have uttered a sentence weaker than (8.1):
-
(8.6)
If I didn’t know that I’m looking at you, I might think that I’m looking at me. \(\lnot _{*} \textsf {K}_{\underline{s}*}(Lsk) \supset _{c, c} \textsf {B}_{\underline{s}*}(Lss)\)
A canonical derivation for (8.6):
This derivation construes Seppel as being in a somewhat hazy epistemic state, as Seppel both counterfactually assumes that he does not know that he is looking at Kasperl and also counterfactually assumes that he knows that he is looking at Kasperl. Thus, here, it is neither settled for Seppel that he knows that he is looking at Kasperl, nor that he does not know that he is looking at Kasperl.
An alternative symbolization of (8.6) is \(\lnot _{*} \textsf {K}_{\underline{s}*}(Lsk) \supset _{c, c/i} \textsf {B}_{\underline{s}*}(Lss)\). Here is a canonical derivation for it:
The alternative symbolization of (8.6) is weaker than that of (8.1), since the latter implies the former, but not vice versa. By contrast, (8.1) does not imply the first symbolization of (8.6), nor does the converse implication hold (cf. Więckowski (2026)).
Example 8.10
Believing vs. knowing a counterfactual. Hotzenplotz sells Kasperl to Petrosilius Zwackelmann, a wizard who needs someone who peels his potatoes.
-
(8.7)
Zwackelmann believes that if Kasperl were to try to escape, he would fail.
Let: z (‘Zwackelmann’), k (‘Kasperl’), T (‘try to escape’), F (‘fail’). Symbolization of (8.7): \(\textsf {B}_{\underline{z}*}(Tk \supset _{c, f} Fk)\). A canonical derivation for (8.7):
Note that the last rule applied can be also knowledge introduction. Next, consider:
-
(8.8)
Zwackelmann believes that if Kasperl were to try to escape, he might fail. \(\textsf {B}_{\underline{z}*}(Tk \supset _{c, c} Fk)\)
A canonical derivation for (8.8):
Here, the last rule applied cannot be knowledge introduction.
Example 8.11
Doubting a counterfactual.
-
(8.9)
Zwackelmann doubts that if Kasperl were to try to escape, he would succeed. \(\lnot _{*}\textsf {B}_{\underline{z}*}(Tk \supset _{c, f} Sk)\)
An illegitimate canonical derivation for (8.9):
Here is a legitimate one:
Note that \(-Sk\) is negatively contained in the term assumptions of the non-logical constants S and k that figure in the conclusion. (8.9) is eligible for neg-raising (see Horn and Wansing (2025) for an overview of negation). So ‘a doubts that p’, that is, ‘a does not believe that p’ can be turned into ‘a believes that not-p’.
-
(8.10)
Zwackelmann believes that it is not the case that if Kasperl were to try to escape, he would succeed. \(\textsf {B}_{\underline{z}*}\lnot _{*}(Tk \supset _{c, f} Sk)\)
An illegitimate canonical derivation:
A legitimate canonical derivation:
Obviously, the last rule applied here cannot be replaced by knowledge introduction.
Example 8.12
Ignorance of counterfactuals. Alois Dimpfelmoser seeks a fortuneteller, widow Schlotterbeck, and spies on Hotzenplotz by means of her crystal ball.
-
(8.11)
Dimpfelmoser doesn’t know that if the crystal ball were shaken, it would turn dark.
Let: d (‘Dimpfelmoser’), b (‘the crystal ball’), S (‘is shaken’), D (‘turns dark’). Symbolization of (8.11): \(\lnot _{*}\textsf {K}_{\underline{d}*}(Sb \supset _{c, f} Db)\). A canonical derivation for (8.11):
(A more adequate analysis of (8.11) would use the qualified iota-operator proposed in Więckowski (2024b) to deal with the definite description ‘the cristal ball’.)
Example 8.13
Widow Schlotterbeck’s insight. In order to find Hotzenplotz, Dimpfelmoser lends widow Schlotterbeck’s dog Wasti who has a good nose. Remarkably, since Schlotterbeck’s wizardry mishap, Wasti’s appearance is that of a crocodile.
Let: p (‘Portiunkula Schlotterbeck’), w (‘Wasti’), C (‘is a crocodile’), A (‘is afraid of’). Starting from the assumptions of ‘if I did not know that Wasti isn’t a crocodile, I’d be afraid of him’ (\(\lnot _{*}\textsf {K}_{\underline{p}*}-Cw \supset _{c, f} Apw\)), ‘it is not the case that if I did not know that Wasti isn’t a crocodile, I might not be afraid of him’ (\(\lnot _{*}\textsf {K}_{\underline{p}*}-Cw \supset _{c, c} -Apw\)), and from the counterfactual assumption ‘I don’t know that Wasti isn’t a crocodile’ (\(\lnot _{*}\textsf {K}_{\underline{p}*}-Cw\), abbreviation: X), Schlotterbeck reasons as follows:
This is a canonical proof and its conclusion an instance of a theorem. We may take this proof to represent, how widow Schlotterbeck arrives at solid knowledge. (This knowledge can be sharpened by replacing the first occurrence of \(\supset _{*, *}\) by \(\supset _{c, i}\), and the second one by \(\supset _{i, c}\); cf. Więckowski (2026): Remark 6.4.) She can make this knowledge explicit by applying \(\textsf {K}_{\underline{p}*}\)I to it.
9 A digression on coming to believe after learning
As mentioned in the Introduction, CDL aims at modeling revisable belief. It does so using an operator for conditional belief that crucially appeals to the notion of learning which is beyond the resources of the systems studied above. To represent the content of that operator’s reading “after learning that P, a comes to believe that Q” as an inferential process in a DM-system, we might consider extending these systems with the rules for the addition [subtraction] of atomic information to [from] term assumptions proposed in Więckowski (2016). In a slightly modified form, these rules take the following shape, where \(\tau \in \mathcal {C}\cup \mathcal {P}\) and \(A \in Atm(\tau )\) (cf. Definitions 3.2 and 3.4):
Example 9.1
Kasperl discovers a sobbing toad in the dungeon of Zwackelmann’s castle. The toad reveals to Kasperl that it is in fact Amaryllis, a fairy whom Zwackelmann turned into a toad.
We may represent the process behind “after learning that Amaryllis is a fairy (Fa), Kasperl comes to believe that Amaryllis fails to be a toad (\(-Ta\))” as a subatomic derivation. To this end, we let Kasperl’s term assumptions at \(t_{0}\) be \(T\{Ta\}^{{{\varvec{k}}}}\), \(a\{Ta\}^{{{\varvec{k}}}}\), \(F\{ \}^{{{\varvec{k}}}}\), and we mark the changes to his subatomic base by \(t_{1}\) to \(t_{4}\).
This derivation represents Kasperl’s change of beliefs from Ta (introduced before \(t_{1}\)) via learning that Fa (introduced between \(t_{3}\) and \(t_{4}\)) to \(-Ta\) (introduced after \(t_{4}\)), and making the belief that \(-Ta\) explicit in the last step.
Hoping that a proper elaboration of the extension of DM-system by \(adt_{*}\) and \(sbt_{*}\) might prove useful, we end this digression with only two immediate observations. A removal of the \(as_{*}\)-detours would also remove some of the transparency of the revision process. And, by Definition 4.11, the set of theorems of a DM-system would remain unaffected by that extension.
10 Concluding remarks
In the logic literature, counterfactuals, belief, and knowledge are typically studied from a model-theoretic perspective on which considerations on possible worlds and relations between them have methodological primacy. In contrast to this kind of approach, we have studied these notions from a structural proof-theoretic perspective on which rule-based reasoning from counterfactual assumptions is methodologically primary for their semantics and logic. We took an intuitionistic stance. Our focus was on the inferential interaction between (counter)factuals and belief/knowledge. We have studied this interaction by means of systems of doxastic modal subatomic natural deduction for which we have established preservation, normalization, the subexpression/subformula property, and internal completeness. Drawing on these results, we have defined a subatomic proof-theoretic semantics for elementary constructions which combine (counter)factuals with belief/knowledge.
It could be interesting to consider modifications of doxastic modal systems. For example, one could consider systems which restrict or relax the constraints imposed on belief and knowledge in the systems studied above. One could also consider extensions with, for instance, the modal rules for conjunction and disjunction studied in Więckowski (2026). Specifically, an incorporation of rules for mode-sensitive conjunction and disjunction should not be too involved, as no side conditions are imposed on them. (The preservation tables displayed above together with those presented in Więckowski (2026) can be useful here.) Finally, to mention a last possible modification, the integration of the rules illustrated in the previous section might contribute to the development of a proof-theoretic perspective on modeling revisable belief.
Data Availability
The author does not analyse or generate any datasets.
Notes
I am grateful to the two anonymous reviewers for JoLLI for making me emphasize this point.
References
Arló-Costa, H., & Bicchieri, C. (2007). Knowing and supposing in games of perfect information. Studia Logica, 86(3), 353–373. https://doi.org/10.1007/s11225-007-9065-6
Baltag, A., & Smets, S. (2006). Conditional doxastic models: a qualitative approach to dynamic belief revision. Electronic Notes in Theoretical Computer Science, 165(2), 5–21. https://doi.org/10.1016/j.entcs.2006.05.034
Baltag, A., & Smets, S. (2008). A qualitative theory of dynamic interactive belief revision. In G. Bonanno, W. van der Hoek, & M. Wooldridge (Eds.), Logic and the Foundations of Game and Decision Theory (LOFT 7), Texts in Logic and Games 3 (pp. 13–60). Amsterdam University Press.
Francez, N. (2015). Proof-Theoretic Semantics. London: College Publications.
Gentzen, G. (1934/35). Untersuchungen über das logische Schließen I, II, Mathematische Zeitschrift 39: 176-210, 405-431. https://doi.org/10.1007/BF01201353
Girlando, M., Negri, S., Olivetti, N., & Risch, V. (2018). Conditional beliefs: from neighbourhood semantics to sequent calculus. The Review of Symbolic Logic, 11(4), 736–779. https://doi.org/10.1017/S1755020318000023
Halpern, J. Y. (1999). Hypothetical knowledge and counterfactual reasoning. International Journal of Game Theory, 28(3), 315–330. https://doi.org/10.1007/s001820050113
Horn, L. R., & Wansing, H. (2025). Negation. In Zalta, E. N. and Nodelman, U., eds., The Stanford Encyclopedia of Philosophy (Spring 2025 Edition), Metaphysics Research Lab, Stanford University. https://plato.stanford.edu/archives/spr2025/entries/negation/
Lewis, D. (2001). Counterfactuals, Blackwell Publishers. (First published in 1973.)
Negri, S., & von Plato, J. (2001). Structural Proof Theory. Cambridge: Cambridge University Press. https://doi.org/10.1017/CBO9780511527340
Nute, D. & Cross, C. B. (2001). Conditional logic. In Gabbay, D. M. and Guenthner F., eds., Handbook of Philosophical Logic, 2nd edition, vol. 4, pp. 1-98. Kluwer Academic Publishers. https://doi.org/10.1007/978-94-017-0456-4_1
Prawitz, D. (1965). Natural Deduction. A Proof-Theoretical Study. Stockholm: Almqvist and Wiksell; reprinted Mineola/NY: Dover Publications, 2006.
Samet, D. (1996). Hypothetical knowledge and games with perfect information. Games and Economic Behavior, 17(2), 230–251. https://doi.org/10.1006/game.1996.0104
Schroeder-Heister, P. (2024). Proof-theoretic semantics. In Zalta, E. N. and Nodelman, U., eds., The Stanford Encyclopedia of Philosophy (Summer 2024 Edition), Metaphysics Research Lab, Stanford University. https://plato.stanford.edu/archives/sum2024/entries/proof-theoretic-semantics/
Stalnaker, R. C. (1968). A theory of conditionals. In N. Rescher (Ed.), Studies in Logical Theory (pp. 98–112). Oxford: Basil Blackwell.
Stalnaker, R. (1996). Knowledge, belief, and counterfactual reasoning in games. Economics and Philosophy, 12(2), 133–163. https://doi.org/10.1017/S0266267100004132
Troelstra, A. S., & Schwichtenberg, H. (2000). Basic Proof Theory (2nd ed.). Cambridge: Cambridge University Press. https://doi.org/10.1017/CBO9781139168717
van Dalen, D. (2002). Intuitionistic logic. In D. Gabbay & F. Guenthner (Eds.), Handbook of Philosophical Logic (2nd ed., Vol. 5, pp. 1–114). Dordrecht: Kluwer Academic Publishers.
van Dalen, D. (2004). Logic and Structure (4th ed.). Berlin: Springer-Verlag.
Więckowski, B. (2016). Refinements of subatomic natural deduction. Journal of Logic and Computation, 26(5), 1567–1616. https://doi.org/10.1093/logcom/exu046
Więckowski, B. (2021). Subatomic negation. Journal of Logic, Language and Information, 30(1), 207–262. https://doi.org/10.1007/s10849-020-09325-4
Więckowski, B. (2021b). Intuitionistic multi-agent subatomic natural deduction for belief and knowledge, Journal of Logic and Computation 31(3): 704-770. Special issue on External and Internal Calculi for Non-Classical Logics edited by A. Ciabattoni, D. Galmiche, N. Olivetti, and R. Ramanayake. https://doi.org/10.1093/logcom/exab013
Więckowski, B. (2023). Negative predication and distinctness. Logica Universalis, 17(1), 103–138. https://doi.org/10.1007/s11787-022-00321-9
Więckowski, B. (2024a). Counterfactual assumptions and counterfactual implications. In Piecha, T. and Wehmeier, K. F., eds., Peter Schroeder-Heister on Proof-Theoretic Semantics, Outstanding Contributions to Logic, Vol. 29, pp. 399-423. Cham, Switzerland: Springer. https://doi.org/10.1007/978-3-031-50981-0_15
Więckowski, B. (2024b). Incomplete descriptions and qualified definiteness. In Indrzejczak, A. and Zawidzki, M., eds., Non-Classical Logics. Theory and Applications (NCL’24), EPTCS 415, pp. 109–120. https://doi.org/10.4204/EPTCS.415.12
Więckowski, B. (2026). On the proof-theoretic structure of counterfactual inference. The Bulletin of Symbolic Logic,32(1), 136–196. https://doi.org/10.1017/bsl.2025.20
Acknowledgements
Parts of this work were presented at the Twelfth Scandinavian Logic Symposium (SLSS 2024) at Reykjavík University (June 2024), at the Logic and Epistemology Colloquium at Ruhr University Bochum (November 2024), at the Center for the Advancement of Logic, its Philosophy, History and Applications (C-ALPHA) of the University of California, Irvine (January 2025), and at the Logic and Interactive Rationality Seminar (LIRa) at the Institute for Logic, Language and Computation of the University of Amsterdam (March 2025). I would like to thank the audiences at these events for their very helpful feedback. I would also like to thank Marianna Girlando, Nils Kürbis, Grigory Olkhovikov, Aybüke Özgün, Heinrich Wansing, and Kai Wehmeier for very helpful discussion of issues relating to this material during my visits. Finally, I thank the two anonymous reviewers from JoLLI for their valuable comments and criticisms which helped to improve the paper.
Funding
Open Access funding enabled and organized by Projekt DEAL. This research was supported by the Deutsche Forschungsgemeinschaft (grant number WI 3456/5-1).
Author information
Authors and Affiliations
Corresponding author
Ethics declarations
Competing interests
The author has no competing interests to declare.
Additional information
Publisher's Note
Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.
Rights and permissions
Open Access This article is licensed under a Creative Commons Attribution 4.0 International License, which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons licence, and indicate if changes were made. The images or other third party material in this article are included in the article's Creative Commons licence, unless indicated otherwise in a credit line to the material. If material is not included in the article's Creative Commons licence and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder. To view a copy of this licence, visit http://creativecommons.org/licenses/by/4.0/
About this article
Cite this article
Więckowski, B. Proof-Theoretic Considerations on the Structure of Reasoning with Counterfactuals and Knowledge. J of Log Lang and Inf (2026). https://doi.org/10.1007/s10849-026-09483-x
Received:
Accepted:
Published:
Version of record:
DOI: https://doi.org/10.1007/s10849-026-09483-x