Hintikka (1962): Knowledge and Belief

This file formalizes the model-set semantics of [Hin62] for the operators "a knows that", "it is possible, for all that a knows, that", "a believes that" and "it is compatible with everything a believes that", and the book's applications of it to Moore's sentence "p but I do not believe that p" and to knowing that one knows. A ModelSystem is a set of model sets, partial descriptions of states of affairs closed under the (C) conditions of Chapter 3, with epistemic and doxastic alternativeness relations between them; a set of sentences is Defensible when it can be embedded in a member of a model system, and a sentence VirtuallyImplies another when the implication between them is self-sustaining. Chapter 4's solution to Moore's problem is that the sentence is defensible but its believed form is not, so that the sentence is DoxasticallyIndefensible for its speaker to utter; the reductive arguments of the book are the proofs, one condition per step, and the model systems it exhibits are possible-worlds models carried to model systems by Model.toModelSystem. Chapter 5's equivalence of knowing and knowing that one knows, and the failure of its doxastic counterpart in Section 5.10, close the file.

Implementation notes

• Model systems carry the first of the combinations of conditions listed in Section 3.4, (C.K) with (C.KK*), and the belief conditions (C.b*), (C.B*) and (C.BB*) of Section 3.5; the reflexivity and transitivity of alternativeness that the book shows to be equivalent to these as far as defensibility is concerned are the frame conditions of Model, whose truth sets are model sets.
• Virtual implication is the self-sustenance of the material implication, as in Section 2.6; Section 3.10 is used in the direction from the indefensibility of the antecedent with the negated consequent to the self-sustenance of the implication, the only direction the reductive arguments need, since the failures of virtual implication are witnessed by models.
• Doxastic and epistemic indefensibility are defined for a sentence, the conjunction of the book's finite set of statements.

References

• [Hin62]

inductive Hintikka1962.Formula (V : Type u_1) (A : Type u_2) : Type (max u_1 u_2)

The formulas of Section 1.6: atomic sentences, negation, conjunction, disjunction and the epistemic operators K a ("a knows that"), P a ("it is possible, for all that a knows, that"), B a ("a believes that") and C a ("it is compatible with everything a believes that").

• atom {V : Type u_1} {A : Type u_2} : V → Formula V A
• neg {V : Type u_1} {A : Type u_2} : Formula V A → Formula V A
• and {V : Type u_1} {A : Type u_2} : Formula V A → Formula V A → Formula V A
• or {V : Type u_1} {A : Type u_2} : Formula V A → Formula V A → Formula V A
• K {V : Type u_1} {A : Type u_2} : A → Formula V A → Formula V A
• P {V : Type u_1} {A : Type u_2} : A → Formula V A → Formula V A
• B {V : Type u_1} {A : Type u_2} : A → Formula V A → Formula V A
• C {V : Type u_1} {A : Type u_2} : A → Formula V A → Formula V A

def Hintikka1962.Formula.«term∼_» : Lean.ParserDescr

Negation.

Equations

• Hintikka1962.Formula.«term∼_» = Lean.ParserDescr.node `Hintikka1962.Formula.«term∼_» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "∼") (Lean.ParserDescr.cat `term 66))

def Hintikka1962.Formula.«term_⋏_» : Lean.TrailingParserDescr

Conjunction.

Equations

• One or more equations did not get rendered due to their size.

def Hintikka1962.Formula.«term_⋎_» : Lean.TrailingParserDescr

Disjunction.

Equations

• One or more equations did not get rendered due to their size.

def Hintikka1962.Formula.imp {V : Type u_1} {A : Type u_2} (p q : Formula V A) : Formula V A

Material implication, eliminated in terms of the other connectives.

Equations

• p.imp q = (p.and q.neg).neg

def Hintikka1962.Formula.«term_⟹_» : Lean.TrailingParserDescr

Material implication, eliminated in terms of the other connectives.

Equations

• One or more equations did not get rendered due to their size.

def Hintikka1962.Formula.knowsWhether {V : Type u_1} {A : Type u_2} (a : A) (p : Formula V A) : Formula V A

(2)*: "a knows whether p", K a p ⋎ K a ∼p.

Equations

• Hintikka1962.Formula.knowsWhether a p = (Hintikka1962.Formula.K a p).or (Hintikka1962.Formula.K a p.neg)

def Hintikka1962.Formula.notKnowsWhether {V : Type u_1} {A : Type u_2} (a : A) (p : Formula V A) : Formula V A

(4)*: "a does not know whether p", ∼K a p ⋏ ∼K a ∼p.

Equations

• Hintikka1962.Formula.notKnowsWhether a p = (Hintikka1962.Formula.K a p).neg.and (Hintikka1962.Formula.K a p.neg).neg

Model sets and model systems

structure Hintikka1962.IsModelSet {V : Type u_1} {A : Type u_2} (μ : Set (Formula V A)) : Prop

A model set (Sections 3.1 and 3.2): a set of formulas closed under the (C) conditions that concern a single set, a partial description of a possible state of affairs.

• neg {p : Formula V A} : p ∈ μ → p.neg ∉ μ

  (C.∼)

• and {p q : Formula V A} : p.and q ∈ μ → p ∈ μ ∧ q ∈ μ

  (C.&)

• or {p q : Formula V A} : p.or q ∈ μ → p ∈ μ ∨ q ∈ μ

  (C.v)

• neg_neg {p : Formula V A} : p.neg.neg ∈ μ → p ∈ μ

  (C.∼∼)

• neg_and {p q : Formula V A} : (p.and q).neg ∈ μ → p.neg ∈ μ ∨ q.neg ∈ μ

  (C.∼&)

• neg_or {p q : Formula V A} : (p.or q).neg ∈ μ → p.neg ∈ μ ∧ q.neg ∈ μ

  (C.∼v)

• know {a : A} {p : Formula V A} : Formula.K a p ∈ μ → p ∈ μ

  (C.K): whatever is known is true.

• neg_know {a : A} {p : Formula V A} : (Formula.K a p).neg ∈ μ → Formula.P a p.neg ∈ μ

  (C.∼K)

• neg_poss {a : A} {p : Formula V A} : (Formula.P a p).neg ∈ μ → Formula.K a p.neg ∈ μ

  (C.∼P)

• neg_believe {a : A} {p : Formula V A} : (Formula.B a p).neg ∈ μ → Formula.C a p.neg ∈ μ

  (C.∼B)

• neg_compat {a : A} {p : Formula V A} : (Formula.C a p).neg ∈ μ → Formula.B a p.neg ∈ μ

  (C.∼C)

structure Hintikka1962.ModelSystem (V : Type u_4) (A : Type u_5) : Type (max u_4 u_5)

A model system (Sections 3.2 to 3.6): a set of model sets with, for each agent, an epistemic and a doxastic alternativeness relation, satisfying the starred conditions on knowledge and belief and (C.dox), that doxastic alternatives are epistemic alternatives.

• sets : Set (Set (Formula V A))

  The model sets.

• epi : A → ↑self.sets → ↑self.sets → Prop

  Epistemic alternativeness with respect to an agent.

• dox : A → ↑self.sets → ↑self.sets → Prop

  Doxastic alternativeness with respect to an agent.

• isModelSet (μ : ↑self.sets) : IsModelSet ↑μ
• P_star {a : A} {p : Formula V A} (μ : ↑self.sets) : Formula.P a p ∈ ↑μ → ∃ (ν : ↑self.sets), self.epi a μ ν ∧ p ∈ ↑ν

  (C.P*)

• KK_star {a : A} {p : Formula V A} {μ ν : ↑self.sets} : self.epi a μ ν → Formula.K a p ∈ ↑μ → Formula.K a p ∈ ↑ν

  (C.KK*)

• C_star {a : A} {p : Formula V A} (μ : ↑self.sets) : Formula.C a p ∈ ↑μ → ∃ (ν : ↑self.sets), self.dox a μ ν ∧ p ∈ ↑ν

  (C.C*)

• b_star {a : A} {p : Formula V A} (μ : ↑self.sets) : Formula.B a p ∈ ↑μ → ∃ (ν : ↑self.sets), self.dox a μ ν ∧ p ∈ ↑ν

  (C.b*)

• B_star {a : A} {p : Formula V A} {μ ν : ↑self.sets} : self.dox a μ ν → Formula.B a p ∈ ↑μ → p ∈ ↑ν

  (C.B*)

• BB_star {a : A} {p : Formula V A} {μ ν : ↑self.sets} : self.dox a μ ν → Formula.B a p ∈ ↑μ → Formula.B a p ∈ ↑ν

  (C.BB*)

• dox_le_epi (a : A) : self.dox a ≤ self.epi a

  (C.dox)

theorem Hintikka1962.ModelSystem.K_star {V : Type u_1} {A : Type u_2} {S : ModelSystem V A} {a : A} {p : Formula V A} {μ ν : ↑S.sets} (h : S.epi a μ ν) (hp : Formula.K a p ∈ ↑μ) : p ∈ ↑ν

(C.K*), from (C.KK*) and (C.K) (Section 3.4).

theorem Hintikka1962.ModelSystem.KK_star_dox {V : Type u_1} {A : Type u_2} {S : ModelSystem V A} {a : A} {p : Formula V A} {μ ν : ↑S.sets} (h : S.dox a μ ν) (hp : Formula.K a p ∈ ↑μ) : Formula.K a p ∈ ↑ν

(C.KKdox), from (C.KK) and (C.dox) (Section 3.6).

theorem Hintikka1962.ModelSystem.K_star_dox {V : Type u_1} {A : Type u_2} {S : ModelSystem V A} {a : A} {p : Formula V A} {μ ν : ↑S.sets} (h : S.dox a μ ν) (hp : Formula.K a p ∈ ↑μ) : p ∈ ↑ν

(C.K*dox).

Defensibility

def Hintikka1962.Defensible {V : Type u_1} {A : Type u_2} (Γ : Set (Formula V A)) : Prop

A set of sentences is defensible when it can be embedded in a member of a model system (Section 3.3).

Equations

• Hintikka1962.Defensible Γ = ∃ (S : Hintikka1962.ModelSystem V A) (μ : ↑S.sets), Γ ⊆ ↑μ

def Hintikka1962.Indefensible {V : Type u_1} {A : Type u_2} (Γ : Set (Formula V A)) : Prop

Indefensibility, the book's reinterpretation of inconsistency (Section 2.6).

Equations

• Hintikka1962.Indefensible Γ = ¬Hintikka1962.Defensible Γ

def Hintikka1962.SelfSustaining {V : Type u_1} {A : Type u_2} (p : Formula V A) : Prop

A sentence is self-sustaining when its negation is indefensible (Section 2.6).

Equations

• Hintikka1962.SelfSustaining p = Hintikka1962.Indefensible {p.neg}

def Hintikka1962.VirtuallyImplies {V : Type u_1} {A : Type u_2} (p q : Formula V A) : Prop

p virtually implies q when p ⟹ q is self-sustaining (Section 2.6).

Equations

• Hintikka1962.VirtuallyImplies p q = Hintikka1962.SelfSustaining (p.imp q)

def Hintikka1962.VirtuallyEquivalent {V : Type u_1} {A : Type u_2} (p q : Formula V A) : Prop

Virtual equivalence: virtual implication in both directions.

Equations

• Hintikka1962.VirtuallyEquivalent p q = (Hintikka1962.VirtuallyImplies p q ∧ Hintikka1962.VirtuallyImplies q p)

theorem Hintikka1962.virtuallyImplies_of_indefensible {V : Type u_1} {A : Type u_2} {p q : Formula V A} (h : Indefensible {p, q.neg}) : VirtuallyImplies p q

Section 3.10: an implication is self-sustaining once its antecedent together with the negation of its consequent is indefensible, the form in which every reductive argument below is run.

def Hintikka1962.DoxasticallyIndefensible {V : Type u_1} {A : Type u_2} (a : A) (p : Formula V A) : Prop

A sentence is doxastically indefensible for the person referred to by a to utter when its believed form is indefensible (Section 4.8).

Equations

• Hintikka1962.DoxasticallyIndefensible a p = Hintikka1962.Indefensible {Hintikka1962.Formula.B a p}

def Hintikka1962.DoxasticallyImplies {V : Type u_1} {A : Type u_2} (a : A) (p q : Formula V A) : Prop

Doxastic implication: p implies q doxastically for a when p ⋏ ∼q is doxastically indefensible (Section 4.9).

Equations

• Hintikka1962.DoxasticallyImplies a p q = Hintikka1962.DoxasticallyIndefensible a (p.and q.neg)

def Hintikka1962.EpistemicallyIndefensible {V : Type u_1} {A : Type u_2} (a : A) (p : Formula V A) : Prop

Epistemic indefensibility for the person referred to by a: the known form is indefensible (Section 4.12).

Equations

• Hintikka1962.EpistemicallyIndefensible a p = Hintikka1962.Indefensible {Hintikka1962.Formula.K a p}

def Hintikka1962.EpistemicallyImplies {V : Type u_1} {A : Type u_2} (a : A) (p q : Formula V A) : Prop

Epistemic implication (Section 4.12).

Equations

• Hintikka1962.EpistemicallyImplies a p q = Hintikka1962.EpistemicallyIndefensible a (p.and q.neg)

Possible-worlds models

Section 2.8 glosses the notions in terms of worlds "in which everybody follows the consequences of what he knows as far as they lead him": a model is a set of such worlds with epistemic alternativeness reflexive and transitive, doxastic alternativeness serial and transitive, and doxastic alternatives among the epistemic ones, the frame conditions that the book shows to be equivalent to its conditions (Sections 3.4 to 3.6). The formulas true at a world form a model set, and the truth sets of a model form a model system, so that satisfiability in a model yields defensibility.

structure Hintikka1962.Model (V : Type u_4) (A : Type u_5) (W : Type u_6) : Type (max (max u_4 u_5) u_6)

A possible-worlds model of the epistemic language.

• epi : A → SetRel W W

  Epistemic alternativeness.

• dox : A → SetRel W W

  Doxastic alternativeness.

• val : V → W → Prop

  Valuation of the atomic sentences.

• epi_refl (a : A) : (self.epi a).IsRefl
• epi_trans (a : A) : (self.epi a).IsTrans
• dox_serial (a : A) : ModalLogic.IsSerial (self.dox a)
• dox_trans (a : A) : (self.dox a).IsTrans
• dox_le_epi (a : A) : self.dox a ⊆ self.epi a

def Hintikka1962.Model.Sat {V : Type u_1} {A : Type u_2} {W : Type u_3} (M : Model V A W) : Formula V A → W → Prop

Satisfaction: the epistemic operators are box and diamond over the agent's alternativeness.

Equations

• M.Sat (Hintikka1962.Formula.atom v) x✝ = M.val v x✝
• M.Sat p.neg x✝ = ¬M.Sat p x✝
• M.Sat (p.and q) x✝ = (M.Sat p x✝ ∧ M.Sat q x✝)
• M.Sat (p.or q) x✝ = (M.Sat p x✝ ∨ M.Sat q x✝)
• M.Sat (Hintikka1962.Formula.K a p) x✝ = ModalLogic.Box (M.epi a) (M.Sat p) x✝
• M.Sat (Hintikka1962.Formula.P a p) x✝ = ModalLogic.Diamond (M.epi a) (M.Sat p) x✝
• M.Sat (Hintikka1962.Formula.B a p) x✝ = ModalLogic.Box (M.dox a) (M.Sat p) x✝
• M.Sat (Hintikka1962.Formula.C a p) x✝ = ModalLogic.Diamond (M.dox a) (M.Sat p) x✝

def Hintikka1962.Model.truthSet {V : Type u_1} {A : Type u_2} {W : Type u_3} (M : Model V A W) (w : W) : Set (Formula V A)

The formulas true at a world.

Equations

• M.truthSet w = {p : Hintikka1962.Formula V A | M.Sat p w}

theorem Hintikka1962.Model.isModelSet_truthSet {V : Type u_1} {A : Type u_2} {W : Type u_3} (M : Model V A W) (w : W) : IsModelSet (M.truthSet w)

def Hintikka1962.Model.toModelSystem {V : Type u_1} {A : Type u_2} {W : Type u_3} (M : Model V A W) : ModelSystem V A

The truth sets of a model, with alternativeness inherited from the worlds, form a model system.

Equations

• One or more equations did not get rendered due to their size.

theorem Hintikka1962.Model.defensible_of_subset_truthSet {V : Type u_1} {A : Type u_2} {W : Type u_3} (M : Model V A W) {Γ : Set (Formula V A)} {w : W} (h : Γ ⊆ M.truthSet w) : Defensible Γ

theorem Hintikka1962.Model.defensible_of_sat {V : Type u_1} {A : Type u_2} {W : Type u_3} (M : Model V A W) {p : Formula V A} {w : W} (h : M.Sat p w) : Defensible {p}

theorem Hintikka1962.Model.not_virtuallyImplies_of_sat {V : Type u_1} {A : Type u_2} {W : Type u_3} (M : Model V A W) {p q : Formula V A} {w : W} (h : M.Sat (p.and q.neg) w) : ¬VirtuallyImplies p q

def Hintikka1962.Model.decSat {V : Type u_1} {A : Type u_2} {W : Type u_3} (M : Model V A W) [Fintype W] [(a : A) → (w v : W) → Decidable ((w, v) ∈ M.epi a)] [(a : A) → (w v : W) → Decidable ((w, v) ∈ M.dox a)] [(v : V) → DecidablePred (M.val v)] (p : Formula V A) (w : W) : Decidable (M.Sat p w)

Satisfaction is decidable over finitely many worlds.

Equations

• M.decSat (Hintikka1962.Formula.atom v) x✝ = Hintikka1962.Model.decSat._aux_1 M v x✝
• M.decSat p.neg x✝ = { decide := !decide (M.Sat p x✝), reflects_decide := ⋯ }
• M.decSat (p.and q) x✝ = { decide := decide (M.Sat p x✝) && decide (M.Sat q x✝), reflects_decide := ⋯ }
• M.decSat (p.or q) x✝ = { decide := decide (M.Sat p x✝) || decide (M.Sat q x✝), reflects_decide := ⋯ }
• M.decSat (Hintikka1962.Formula.K a p) x✝ = { decide := decide (∀ a_1 ∈ Finset.univ, (fun (v : W) => (x✝, v) ∈ M.epi a → M.Sat p v) a_1), reflects_decide := ⋯ }
• M.decSat (Hintikka1962.Formula.P a p) x✝ = { decide := decide (∃ a_1 ∈ Finset.univ, (fun (v : W) => (x✝, v) ∈ M.epi a ∧ M.Sat p v) a_1), reflects_decide := ⋯ }
• M.decSat (Hintikka1962.Formula.B a p) x✝ = { decide := decide (∀ a_1 ∈ Finset.univ, (fun (v : W) => (x✝, v) ∈ M.dox a → M.Sat p v) a_1), reflects_decide := ⋯ }
• M.decSat (Hintikka1962.Formula.C a p) x✝ = { decide := decide (∃ a_1 ∈ Finset.univ, (fun (v : W) => (x✝, v) ∈ M.dox a ∧ M.Sat p v) a_1), reflects_decide := ⋯ }

@[instance_reducible]

instance Hintikka1962.Model.instDecidableSat {V : Type u_1} {A : Type u_2} {W : Type u_3} (M : Model V A W) [Fintype W] [(a : A) → (w v : W) → Decidable ((w, v) ∈ M.epi a)] [(a : A) → (w v : W) → Decidable ((w, v) ∈ M.dox a)] [(v : V) → DecidablePred (M.val v)] (p : Formula V A) (w : W) : Decidable (M.Sat p w)

Equations

• M.instDecidableSat p w = M.decSat p w

Chapter 3: consequences and rejected conditions

(C.KB), that whatever is known is believed to be known, follows from (C.dox) (Section 3.6). (C.BK), that whatever is believed is known to be believed, would make "a believes that p" virtually imply "a knows that it is possible, for all a knows, that p", and (C.PK), that whatever is possible is known to be possible, would make (13) self-sustaining; neither is a consequence of the conditions (Sections 3.7 and 3.8).

theorem Hintikka1962.virtuallyImplies_K_B_K {V : Type u_1} {A : Type u_2} (a : A) (p : Formula V A) : VirtuallyImplies (Formula.K a p) (Formula.B a (Formula.K a p))

(C.KB): K a p virtually implies B a (K a p).

@[reducible, inline]

abbrev Hintikka1962.mK : Model Unit (Fin 2) (Fin 3)

A model in which belief and knowledge diverge: from world 0 the doxastic alternative is 1 and the epistemic alternatives are all three worlds, each other world being its own only alternative; the atom holds at 0 and 1.

Equations

• One or more equations did not get rendered due to their size.

theorem Hintikka1962.not_virtuallyImplies_B_K_P : ¬VirtuallyImplies (Formula.B 0 (Formula.atom ())) (Formula.K 0 (Formula.P 0 (Formula.atom ())))

(C.BK) rejected: B a p does not virtually imply K a (P a p).

theorem Hintikka1962.not_virtuallyImplies_B_K_B : ¬VirtuallyImplies (Formula.B 0 (Formula.atom ())) (Formula.K 0 (Formula.B 0 (Formula.atom ())))

Section 3.7: B a p does not virtually imply K a (B a p).

theorem Hintikka1962.not_virtuallyImplies_K_P : ¬VirtuallyImplies (Formula.atom ()) (Formula.K 0 (Formula.P 0 (Formula.atom ())))

(C.PK) rejected: (13), p ⟹ K a (P a p), is not self-sustaining.

Chapter 4: knowing that others know

theorem Hintikka1962.virtuallyImplies_K_K_K {V : Type u_1} {A : Type u_2} (a b : A) (p : Formula V A) : VirtuallyImplies (Formula.K a (Formula.K b p)) (Formula.K a p)

(20): knowledge is transmissible, K a (K b p) virtually implies K a p (Sections 4.1 and 4.2), by (C.∼K), (C.P*), (C.K*) and (C.K).

@[reducible, inline]

abbrev Hintikka1962.mB : Model Unit (Fin 2) (Fin 3)

A model of belief: from world 0 agent 0 considers 1 and 2 doxastically possible, from the other worlds only 1; agent 1 always considers only 0 possible; knowledge is trivial; the atom holds at 0 and 1.

Equations

• One or more equations did not get rendered due to their size.

theorem Hintikka1962.not_virtuallyImplies_B_B_B : ¬VirtuallyImplies (Formula.B 0 (Formula.B 1 (Formula.atom ()))) (Formula.B 0 (Formula.atom ()))

(27): belief is not transmissible, B a (B b p) does not virtually imply B a p (Section 4.3).

theorem Hintikka1962.not_virtuallyImplies_B_K_K : ¬VirtuallyImplies (Formula.B 0 (Formula.K 1 (Formula.atom ()))) (Formula.K 0 (Formula.atom ()))

Section 4.4: "I believe that you know that p" does not virtually imply "I know that p".

Chapter 4: Moore's problem

Moore's sentence (8), "p but I do not believe that p", is defensible, but (30)*, its believed form, is not: what uttering (8) violates is the presumption that the speaker can believe what he says (Sections 4.5 and 4.6). The believed form of the third-person variant (8)(a) is defensible unless the believer is the person spoken about.

def Hintikka1962.mooreModel {V : Type u_1} {A : Type u_2} (a : A) : Model V A Bool

The model of Section 4.6's discussion of (8) and (8)(a): two states of affairs, the atom true in the first; every agent believes only the second, except a, who believes only the first.

Equations

• One or more equations did not get rendered due to their size.

theorem Hintikka1962.defensible_moore {V : Type u_1} {A : Type u_2} (a : A) (v : V) : Defensible {(Formula.atom v).and (Formula.B a (Formula.atom v)).neg}

(8) is defensible: the world true of mooreModel a satisfies p ⋏ ∼B a p.

theorem Hintikka1962.defensible_B_moore_of_ne {V : Type u_1} {A : Type u_2} (a b : A) (hab : b ≠ a) (v : V) : Defensible {Formula.B b ((Formula.atom v).and (Formula.B a (Formula.atom v)).neg)}

(30)(a)*: the believed form of (8)(a) is defensible when the believer b is not the person a spoken about.

theorem Hintikka1962.indefensible_B_moore {V : Type u_1} {A : Type u_2} (a : A) (p : Formula V A) : Indefensible {Formula.B a (p.and (Formula.B a p).neg)}

(30): the believed Moore sentence is indefensible, by the reductive argument (33)–(39): (C.b), (C.BB*), (C.&), (C.∼B), (C.C*), (C.B*), (C.&) and (C.∼).

theorem Hintikka1962.indefensible_moore_and_B_moore {V : Type u_1} {A : Type u_2} (a : A) (p : Formula V A) : Indefensible {(p.and (Formula.B a p).neg).and (Formula.B a (p.and (Formula.B a p).neg))}

Section 4.7: the explanation made independent of (C.BB*), the speaker cannot add "and I believe what I just said": (p ⋏ ∼B a p) ⋏ B a (p ⋏ ∼B a p) is indefensible by (C.&), (C.∼B), (C.C*), (C.B*) and (C.∼) alone.

theorem Hintikka1962.doxasticallyIndefensible_moore {V : Type u_1} {A : Type u_2} (a : A) (p : Formula V A) : DoxasticallyIndefensible a (p.and (Formula.B a p).neg)

Section 4.8: (8) is doxastically indefensible for its speaker to utter.

theorem Hintikka1962.doxasticallyImplies_B {V : Type u_1} {A : Type u_2} (a : A) (p : Formula V A) : DoxasticallyImplies a p (Formula.B a p)

Section 4.9: p implies "I believe that p" doxastically.

Chapter 4: the analogue for knowledge

(9), "p but I do not know whether p", is (4)'s p ⋏ notKnowsWhether a p; its known form (40) and the simpler (41) are indefensible without (C.KK*), so that any sentence implies "I know it" epistemically (Sections 4.11 to 4.13). Knowledge and belief come apart in (44) and (45) (Section 4.14).

theorem Hintikka1962.indefensible_K_moore {V : Type u_1} {A : Type u_2} (a : A) (p : Formula V A) : Indefensible {Formula.K a (p.and (Formula.K a p).neg)}

(41): K a (p ⋏ ∼K a p) is indefensible, by (C.K), (C.&), (C.∼K), (C.P*), (C.K*), (C.&) and (C.∼).

theorem Hintikka1962.indefensible_K_moore_whether {V : Type u_1} {A : Type u_2} (a : A) (p : Formula V A) : Indefensible {Formula.K a (p.and (Formula.notKnowsWhether a p))}

(40)*: the known form of (9) is indefensible in the same way.

theorem Hintikka1962.epistemicallyImplies_K {V : Type u_1} {A : Type u_2} (a : A) (p : Formula V A) : EpistemicallyImplies a p (Formula.K a p)

Section 4.12: any sentence implies "I know that it" epistemically.

theorem Hintikka1962.epistemicallyIndefensible_K_neg_K {V : Type u_1} {A : Type u_2} (a b : A) (p : Formula V A) : EpistemicallyIndefensible b ((Formula.K a p).and (Formula.K b p).neg)

(42)*: "a knows that p but b does not know it" is epistemically indefensible for b to utter (Section 4.13).

theorem Hintikka1962.indefensible_K_neg_B {V : Type u_1} {A : Type u_2} (a : A) (p : Formula V A) : Indefensible {Formula.K a (p.and (Formula.B a p).neg)}

(44): K a (p ⋏ ∼B a p) is indefensible, by (C.dox) (Section 4.14).

theorem Hintikka1962.virtuallyImplies_B_and {V : Type u_1} {A : Type u_2} (a : A) (p : Formula V A) : VirtuallyImplies (Formula.B a (p.and (Formula.K a p).neg)) ((Formula.B a p).and (Formula.K a p).neg)

(46) virtually implies (47): B a (p ⋏ ∼K a p) virtually implies B a p ⋏ ∼K a p.

theorem Hintikka1962.doxasticallyImplies_B_of_and {V : Type u_1} {A : Type u_2} (a : A) (p : Formula V A) : DoxasticallyImplies a ((Formula.B a p).and (Formula.K a p).neg) (Formula.B a (p.and (Formula.K a p).neg))

(47) implies (46) doxastically.

@[reducible, inline]

abbrev Hintikka1962.mKB : Model Unit (Fin 2) (Fin 3)

A model in which every world is epistemically possible from every world while only world 1, where the atom holds, is doxastically possible.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Hintikka1962.mWhether : Model Unit (Fin 2) (Fin 3)

A model in which agent 0 knows whether the atom holds and agent 1 does not.

Equations

• One or more equations did not get rendered due to their size.

theorem Hintikka1962.defensible_K_knowsWhether : Defensible {Formula.K 1 ((Formula.knowsWhether 0 (Formula.atom ())).and (Formula.knowsWhether 1 (Formula.atom ())).neg)}

(43): "he knows whether p although I don't" is epistemically defensible (Section 4.13).

theorem Hintikka1962.defensible_B_neg_K : Defensible {Formula.B 0 ((Formula.atom ()).and (Formula.K 0 (Formula.atom ())).neg)}

(45): B a (p ⋏ ∼K a p) is defensible (Section 4.14).

theorem Hintikka1962.defensible_K_B_neg_K : Defensible {Formula.K 0 ((Formula.B 0 (Formula.atom ())).and (Formula.K 0 (Formula.atom ())).neg)}

(48): the known form of (47), K a (B a p ⋏ ∼K a p), is defensible.

theorem Hintikka1962.defensible_K_B_P : Defensible {Formula.K 0 ((Formula.B 0 (Formula.atom ())).and (Formula.P 0 (Formula.atom ()).neg))}

(51), "I believe that p but I may be mistaken", is epistemically defensible (Section 4.16).

theorem Hintikka1962.defensible_B_B_P : Defensible {Formula.B 0 ((Formula.B 0 (Formula.atom ())).and (Formula.P 0 (Formula.atom ()).neg))}

(51) is doxastically defensible.

theorem Hintikka1962.epistemicallyIndefensible_P {V : Type u_1} {A : Type u_2} (a : A) (p : Formula V A) : EpistemicallyIndefensible a (p.and (Formula.P a p.neg))

(51)(c): p ⋏ P a ∼p is epistemically indefensible (Section 4.16).

theorem Hintikka1962.epistemicallyIndefensible_C {V : Type u_1} {A : Type u_2} (a : A) (p : Formula V A) : EpistemicallyIndefensible a (p.and (Formula.C a p.neg))

(51)(b): p ⋏ C a ∼p is epistemically indefensible.

theorem Hintikka1962.doxasticallyIndefensible_C {V : Type u_1} {A : Type u_2} (a : A) (p : Formula V A) : DoxasticallyIndefensible a (p.and (Formula.C a p.neg))

(51)(b) is doxastically indefensible as well.

theorem Hintikka1962.indefensible_B_C {V : Type u_1} {A : Type u_2} (a : A) (p : Formula V A) : Indefensible {(Formula.B a p).and (Formula.C a p.neg)}

(51)(a): B a p ⋏ C a ∼p is indefensible simpliciter.

Chapter 5: knowing that one knows

theorem Hintikka1962.virtuallyImplies_K_KK {V : Type u_1} {A : Type u_2} (a : A) (p : Formula V A) : VirtuallyImplies (Formula.K a p) (Formula.K a (Formula.K a p))

(65)–(69): K a p virtually implies K a (K a p), by (C.∼K), (C.P*) and (C.KK*) (Section 5.2).

theorem Hintikka1962.virtuallyImplies_KK_K {V : Type u_1} {A : Type u_2} (a : A) (p : Formula V A) : VirtuallyImplies (Formula.K a (Formula.K a p)) (Formula.K a p)

K a (K a p) virtually implies K a p, by (C.K) and (C.∼).

theorem Hintikka1962.virtuallyEquivalent_K_KK {V : Type u_1} {A : Type u_2} (a : A) (p : Formula V A) : VirtuallyEquivalent (Formula.K a p) (Formula.K a (Formula.K a p))

(63) and (64) are virtually equivalent: knowing that one knows only differs in words from knowing (Section 5.4).

theorem Hintikka1962.virtuallyImplies_B_BB {V : Type u_1} {A : Type u_2} (a : A) (p : Formula V A) : VirtuallyImplies (Formula.B a p) (Formula.B a (Formula.B a p))

(72) virtually implies (73): B a p virtually implies B a (B a p), by (C.BB*) (Section 5.10).

theorem Hintikka1962.not_virtuallyImplies_negK_K_negK : ¬VirtuallyImplies (Formula.K 0 (Formula.atom ())).neg (Formula.K 0 (Formula.K 0 (Formula.atom ())).neg)

Section 5.2: one may fail to know one's ignorance, ∼K a p does not virtually imply K a ∼K a p.

theorem Hintikka1962.not_virtuallyImplies_BB_B : ¬VirtuallyImplies (Formula.B 0 (Formula.B 0 (Formula.atom ()))) (Formula.B 0 (Formula.atom ()))

Section 5.10: (73) does not virtually imply (72), B a (B a p) does not virtually imply B a p.