Documentation

Linglib.Studies.Hintikka1962

Hintikka (1962): Doxastic indefensibility of Moore's sentence #

[Hin62]

[Hin62] Ch. 4 analysis of Moore's paradox. The sentence "p but I do not believe that p" is not self-contradictory — there are worlds where p holds while the speaker fails to believe p. But its would-be-believed form B_a (p ∧ ¬ B_a p) is indefensible in any KD4 doxastic model: a 1-line specialisation of Core.Logic.Modal.box_not_moore to the agent-indexed belief accessibility of CommitmentState. The knowledge analogue specialises the same substrate lemma to epistemic accessibility.

source
def Hintikka1962.mooreContent {W : Type u_1} {A : Type u_2} (c : Discourse.Commitment.Frame.CommitmentState W A) (s : A) (p : Set W) :
Set W

The Moore content for speaker s and proposition p: worlds where p holds and s does not believe p.

Equations
Instances For
    source
    def Hintikka1962.DoxasticallyIndefensible {W : Type u_1} {A : Type u_2} (c : Discourse.Commitment.Frame.CommitmentState W A) (a : A) (P : Set W) :
    Prop

    Doxastic indefensibility of a propositional content for an agent in a given commitment state: a does not believe P at any world. Restricted to set-valued contents; Hintikka §4.8's general definition ranges over finite sets of sentences.

    Equations
    Instances For
      source
      theorem Hintikka1962.mooreContent_doxasticallyIndefensible {W : Type u_1} {A : Type u_2} (c : Discourse.Commitment.Frame.CommitmentState W A) (a : A) (p : Set W) :
      DoxasticallyIndefensible c a (mooreContent c a p)

      The Moore-paradox theorem: under KD4 belief, no agent can believe the Moore content at any world.

      source
      def Hintikka1962.mooreWitness :
      Discourse.Commitment.Frame.CommitmentState Bool Unit

      A two-world KD4 frame: every world treats only false as belief- accessible. Used as a witness for true_mem_mooreContent.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem Hintikka1962.true_mem_mooreContent :
        true ∈ mooreContent mooreWitness () {true}

        Satisfiability of the Moore sentence: with p := {true} over mooreWitness, the world true lies in mooreContent. The propositional content p ∧ ¬B_a p is consistent — contrast with p ∧ ¬p, which has no models; only the believed form fails.

        source
        theorem Hintikka1962.knowledge_unknowable {W : Type u_1} {E : Type u_3} (Rs : Core.Logic.Modal.AgentAccessRel W E) (i : E) [Core.Logic.Modal.IsSerial (Rs i)] [IsTrans W (Rs i)] (p : W → Prop) (w : W) :
        ¬Semantics.Modality.EpistemicLogic.knows Rs i (fun (v : W) => p v ∧ ¬Semantics.Modality.EpistemicLogic.knows Rs i p v) w

        Epistemic analogue (Hintikka §4.11): under KD4 knowledge, "p but I don't know whether p" is unknowable. Direct corollary of box_not_moore for knows.

        source
        theorem Hintikka1962.not_committed_mooreContent_of_sincere {W : Type u_1} {A : Type u_2} (c : Discourse.Commitment.Frame.CommitmentState W A) (hsin : Discourse.Commitment.Frame.Sincere c) (s b : A) (p : Set W) (w : W) :
        ¬Discourse.Commitment.Frame.Committed c s b (mooreContent c s p) w

        Performatory corollary (state-theoretic restatement of Hintikka §4.10): under sincerity, no commitment state hosts a self-commitment to the Moore content. Hintikka's performatoriness claim is about the act of asserting; this is the resulting constraint on states a sincere assertion could leave behind.