Epistemic Contradictions — Empirical Data

@cite{holliday-mandelkern-2024}

Theory-neutral observations about epistemic contradictions. These are the empirical facts that any semantic theory of epistemic modals must account for.

Three kinds of contradiction

1. Moore sentences: "It's raining but I don't know that it's raining." Pragmatically odd but embeddable (under "suppose", in conditionals, etc.).
2. Wittgenstein sentences: "It's raining and it might not be raining." Semantically contradictory — infelicitous even under embedding.
3. Classical contradictions: "It's raining and it's not raining." Logically contradictory — always infelicitous.

The key datum: Wittgenstein sentences pattern with classical contradictions (not with Moore sentences) under embedding, suggesting they are semantic contradictions, not merely pragmatic ones.

inductive Phenomena.Modality.EpistemicContradictions.SentenceType : Type

A sentence type: how epistemic modality interacts with assertion.

• moore : SentenceType
• wittgenstein : SentenceType
• classical : SentenceType

instance Phenomena.Modality.EpistemicContradictions.instDecidableEqSentenceType : DecidableEq SentenceType

Equations

• Phenomena.Modality.EpistemicContradictions.instDecidableEqSentenceType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Modality.EpistemicContradictions.instBEqSentenceType.beq : SentenceType → SentenceType → Bool

Equations

• Phenomena.Modality.EpistemicContradictions.instBEqSentenceType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Modality.EpistemicContradictions.instBEqSentenceType : BEq SentenceType

Equations

• Phenomena.Modality.EpistemicContradictions.instBEqSentenceType = { beq := Phenomena.Modality.EpistemicContradictions.instBEqSentenceType.beq }

instance Phenomena.Modality.EpistemicContradictions.instReprSentenceType : Repr SentenceType

Equations

• Phenomena.Modality.EpistemicContradictions.instReprSentenceType = { reprPrec := Phenomena.Modality.EpistemicContradictions.instReprSentenceType.repr }

def Phenomena.Modality.EpistemicContradictions.instReprSentenceType.repr : SentenceType → Nat → Std.Format

Equations

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

inductive Phenomena.Modality.EpistemicContradictions.EmbeddingEnv : Type

Embedding environments that distinguish Moore from Wittgenstein.

• suppose : EmbeddingEnv
• conditional : EmbeddingEnv
• epistemic : EmbeddingEnv
• disjunction : EmbeddingEnv
• attitude : EmbeddingEnv

instance Phenomena.Modality.EpistemicContradictions.instDecidableEqEmbeddingEnv : DecidableEq EmbeddingEnv

Equations

• Phenomena.Modality.EpistemicContradictions.instDecidableEqEmbeddingEnv x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Modality.EpistemicContradictions.instBEqEmbeddingEnv.beq : EmbeddingEnv → EmbeddingEnv → Bool

Equations

• Phenomena.Modality.EpistemicContradictions.instBEqEmbeddingEnv.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Modality.EpistemicContradictions.instBEqEmbeddingEnv : BEq EmbeddingEnv

Equations

• Phenomena.Modality.EpistemicContradictions.instBEqEmbeddingEnv = { beq := Phenomena.Modality.EpistemicContradictions.instBEqEmbeddingEnv.beq }

instance Phenomena.Modality.EpistemicContradictions.instReprEmbeddingEnv : Repr EmbeddingEnv

Equations

• Phenomena.Modality.EpistemicContradictions.instReprEmbeddingEnv = { reprPrec := Phenomena.Modality.EpistemicContradictions.instReprEmbeddingEnv.repr }

def Phenomena.Modality.EpistemicContradictions.instReprEmbeddingEnv.repr : EmbeddingEnv → Nat → Std.Format

Equations

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

def Phenomena.Modality.EpistemicContradictions.felicitousUnderEmbedding : SentenceType → Bool

Moore sentences become felicitous under embedding; Wittgenstein and classical contradictions remain infelicitous. This is the core diagnostic separating pragmatic from semantic contradiction.

Equations

• Phenomena.Modality.EpistemicContradictions.felicitousUnderEmbedding Phenomena.Modality.EpistemicContradictions.SentenceType.moore = true
• Phenomena.Modality.EpistemicContradictions.felicitousUnderEmbedding Phenomena.Modality.EpistemicContradictions.SentenceType.wittgenstein = false
• Phenomena.Modality.EpistemicContradictions.felicitousUnderEmbedding Phenomena.Modality.EpistemicContradictions.SentenceType.classical = false

structure Phenomena.Modality.EpistemicContradictions.DistribIntuition : Type

Distributivity failure intuition: the LHS is felicitous but the classically equivalent RHS is not.

• lhs : String
• rhs : String
• lhsFelicitous : Bool
• rhsFelicitous : Bool

def Phenomena.Modality.EpistemicContradictions.distribFailure : DistribIntuition

"Sue might be the winner and she might not be, and either she is or she isn't" is fine; distributing yields two Wittgenstein sentences joined by "or", which is not.

Equations

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

structure Phenomena.Modality.EpistemicContradictions.DisjSyllIntuition : Type

Disjunctive syllogism failure intuition.

• premise1 : String
• premise2 : String
• conclusion : String
• valid : Bool

def Phenomena.Modality.EpistemicContradictions.disjSyllFailure : DisjSyllIntuition

The argument "either the dog is inside or it must be outside; it's not the case that it must be outside; therefore the dog is inside" is intuitively invalid for epistemic modals.

Equations

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