Knowledge, belief, normality, and introspection

Abstract

We study two logics of knowledge and belief stemming from the work of Stalnaker (2006), omitting positive introspection for knowledge. The two systems are equivalent with positive introspection, but not without. We show that while the logic of beliefs remains unaffected by omitting introspection for knowledge in one system, it brings significant changes to the other. The resulting logic of belief is non-normal, and its complete axiomatization uses an infinite hierarchy of coherence constraints. We conclude by returning to the philosophical interpretation underlying both models of belief, showing that neither is strong enough to support a probabilistic interpretation, nor an interpretation in terms of certainty or the “mental component” of knowledge.

Appendix—Proof theory for Stalnaker’s system

In this appendix we present a version of Stalnaker’s $\mathsf {S}$ in the setting of Display logic; which we shall call $\mathsf {DS}$. This is interesting because this system is a bimodal logic and proof-theoretic investigations of such logics are still sparse.

Display logic has been designed by Belnap (1982) to provide for a powerful syntactic framework which is also a generalization of Gentzen’s (1935) sequent calculus. Display logic allows for an elegant proof of cut elimination given that several conditions hold. These conditions are usually easy to verify. For this end the system contains not only formulas and sequents (also termed consecutions) but also structures. Due to its richness, however, there also downsides to Display logic, see e.g. Kracht (1996). For connections to other logical frameworks cf. Ciabattoni et al. (2014) and Poggiolesi (2011).

Wansing (1998, 2002) enriched Belnap’s orignial work with an intensional marker $\bullet$, in order to allows for a smooth formalization of normal modal logics within. For our purposes we introduce two bullets, one corresponding to knowledge, $\bullet _K$ and one corresponding to belief, $\bullet _B$.

In what follows we present a concise version of $\mathsf {DS}$. We start with definitions of formulas and structures; throughout we use standard terminology as eg. in Wansing (1998).

Definition 6

(Formulas of$\mathsf {DS}$) $\varphi := p \mid \lnot \varphi \mid \varphi \rightarrow \varphi \mid \varphi \vee \varphi \mid \varphi \wedge \varphi \mid K\varphi \mid B\varphi$

Definition 7

(Structures of$\mathsf {DS}$) $X := \mathrm {I} \mid \varphi \mid *X \mid X \circ Y \mid \bullet _K \mid \bullet _B$

The particular system $\mathsf {DS}$ consists of an axiom, structural and (propositional) logical rules, Display equivalence rules, and eventually rules for the introduction of the modalities K and B.

A presentation of the system $\mathsf {DS}$

The rules for the introduction of K and B are structurally identical. So present them using $\square$ for referring to either K or B and, do not index the intensional marker $\bullet$ with $_K$ or $_B$.

Additionally we need the structural rule $(\mathrm {I}\bullet )$ and the display equivalence rule $(\bullet )$:

The four rules above capture the fact that both modalities K and B are normal operators (in the technical sense). The additional logical content of Stalnaker’s $\mathsf {S}$ is expressed by the following structural rules. Due to the fact that the logical content is expressed by use of structural rules and applications of cut are warranted only for formulas no new cases arise for the general cut elimination procedure.

This completes the presentation of $\mathsf {DS}$. Here are three important derivations that illustrate how the system works.

Fact 2

The right counterparts of the structural rules P, C, and A are derivable.

Fact 3

$\mathsf {DS} \vdash \varphi \Longrightarrow \varphi$ for all $\varphi$.

At the center of any Display logic is the Display theorem which is a main ingredient for establishing the cut elimination theorem. For this end we need two further definitions. It is not difficult to see that from these the Display theorem follows.

Definition 8

(Positive and negative occurrence) An occurrence of a substructure in a given structure is called positive if it is in the scope of an even number of $*$ (otherwise it is coined negative).

Definition 9

(Antecedent and succedent parts) In a sequent $Y \Longrightarrow Z$ an occurrence of X is an antecedent part if it occurs positively in the antecedent or negatively in the succedent. An occurrence that is not an antecedent part is a succedent part.

Theorem 3

(Display theorem) Each antecedent part of X of a sequent S can be displayed as the whole antecedent of a display-equivalent sequent $X \Longrightarrow Y$. Likewise, each consequent part of a sequent can be displayed as the whole succedent of a display-equivalent sequent.

From the Display theorem together with the conditions (listed below) a general cut elimination result follows in a straightforward way. The conditions (C2)–(C8) guarantee cut elimination, whereas (C1) ensures the subformula property.

Definition 10

(Belnap’s conditions (C1)–(C8))

(C1) :

Preservation of formulas Each formula occurring in a premise of a rule instance is a subformula of some formula in the conclusion (except Cut).

(C2) :

Shape-likeness of parameters Congruent parameters are occurrences of the same structure.

(C3) :

Non-proliferation of parameters Each parameter is congruent to at most one constituent in the conclusion; that is, no two constituents in the conclusion are congruent to each other.

(C4) :

Position-likeness of parameters Congruent parameters are either all antecedent or all consequent parts in their respective sequence.

(C5) :

Display of principal constituents If a formula is principal constituent in the conclusion of an inference, then it is either the entire antecedent or the entire consequent of the conclusion.

(C6) :

Closure under substitution of consequent parts Each inference rule is closed under simultaneous substitution of arbitrary structures in consequent parts for congruent parameters.

(C7) :

Closure under substitution of antecedent parts Each inference rule is closed under simultaneous substitution of arbitrary structures in antecedent parts for congruent parameters.

(C8) :

Cut of matching principal constituents If there are inferences Inf$_1$ and Inf$_2$ with respective conclusions (1) $X \Longrightarrow \varphi$ and (2) $\varphi \Longrightarrow Y$, with $\varphi$ principal in both inferences, then either (3) $X \Longrightarrow Y$ is identical to one of (1) or (2), or there is a derivation of (3) from the premises of Inf$_1$ and Inf$_2$ in which (Cut) is only used on proper subformulas of $\varphi$.

The following two theorems are direct consequences of the above definition.

Theorem 4

(Cut elimination for $\mathsf {DS}$) Cut is eliminable for $\mathsf {DS}$.

Let us pause to note that condition (C1) does not play a role in proving the eliminability of cut, i.e. conditions (C2) through (C8) are sufficient to prove the general cut elimination theorem. However, if all eight conditions do hold for a system, then it follows that the system possesses the subformula property meaning that each provable sequent has a proof where every formula occurring in any step of the derivation is a subformula of a formula in the conclusion.

Theorem 5

(Subformula property of $\mathsf {DS}$) The display calculus $\mathsf {DS}$ without (Cut) has the subformula property.

We can in fact prove that if (1) $\mathsf {S} \vdash \varphi$ then $\mathsf {DS} \vdash \mathrm {I} \Longrightarrow \varphi$ and furthermore that (2) if $\mathsf {DS} \vdash X \Longrightarrow Y$, then $\mathsf {D} \vdash \tau (X) \rightarrow \tau (Y)$. Part (2) needs an explicit treatment of the translation function $\tau$, which is tedious but not particularly difficult. We omit it here.

Fact 4

$\mathsf {DS}$ and $\mathsf {S}$ are deductively equivalent.

This fact gives rise to soundness and completeness:

Fact 5

$\mathsf {DS}$ is sound and complete with respect to the semantics of $\mathsf {S}$.