@[reducible, inline]

abbrev NeoGricean.Spector2007.Valuation (Atom : Type u_1) : Type u_1

A valuation assigns truth values to atoms. We represent it as the set of atoms that are TRUE.

Equations

• NeoGricean.Spector2007.Valuation Atom = Finset Atom

@[reducible, inline]

abbrev NeoGricean.Spector2007.Proposition (Atom : Type u_1) : Type u_1

A proposition is a set of valuations (the valuations that make it true).

Equations

• NeoGricean.Spector2007.Proposition Atom = Set (NeoGricean.Spector2007.Valuation Atom)

inductive NeoGricean.Spector2007.Literal (Atom : Type u_2) : Type u_2

A literal is either an atom (positive) or its negation (negative).

• pos {Atom : Type u_2} : Atom → Literal Atom
• neg {Atom : Type u_2} : Atom → Literal Atom

instance NeoGricean.Spector2007.instDecidableEqLiteral {Atom✝ : Type u_2} [DecidableEq Atom✝] : DecidableEq (Literal Atom✝)

Equations

• NeoGricean.Spector2007.instDecidableEqLiteral = NeoGricean.Spector2007.instDecidableEqLiteral.decEq

def NeoGricean.Spector2007.instDecidableEqLiteral.decEq {Atom✝ : Type u_2} [DecidableEq Atom✝] (x✝ x✝¹ : Literal Atom✝) : Decidable (x✝ = x✝¹)

Equations

• NeoGricean.Spector2007.instDecidableEqLiteral.decEq (NeoGricean.Spector2007.Literal.pos a) (NeoGricean.Spector2007.Literal.pos b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• NeoGricean.Spector2007.instDecidableEqLiteral.decEq (NeoGricean.Spector2007.Literal.pos a) (NeoGricean.Spector2007.Literal.neg a_1) = isFalse ⋯
• NeoGricean.Spector2007.instDecidableEqLiteral.decEq (NeoGricean.Spector2007.Literal.neg a) (NeoGricean.Spector2007.Literal.pos a_1) = isFalse ⋯
• NeoGricean.Spector2007.instDecidableEqLiteral.decEq (NeoGricean.Spector2007.Literal.neg a) (NeoGricean.Spector2007.Literal.neg b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

def NeoGricean.Spector2007.instReprLiteral.repr {Atom✝ : Type u_2} [Repr Atom✝] : Literal Atom✝ → ℕ → Std.Format

Equations

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

instance NeoGricean.Spector2007.instReprLiteral {Atom✝ : Type u_2} [Repr Atom✝] : Repr (Literal Atom✝)

Equations

• NeoGricean.Spector2007.instReprLiteral = { reprPrec := NeoGricean.Spector2007.instReprLiteral.repr }

def NeoGricean.Spector2007.Literal.atom {α : Type u_2} : Literal α → α

The atom of a literal.

Equations

• (NeoGricean.Spector2007.Literal.pos a).atom = a
• (NeoGricean.Spector2007.Literal.neg a).atom = a

def NeoGricean.Spector2007.Literal.isPositive {α : Type u_2} : Literal α → Bool

Whether a literal is positive.

Equations

• (NeoGricean.Spector2007.Literal.pos a).isPositive = true
• (NeoGricean.Spector2007.Literal.neg a).isPositive = false

def NeoGricean.Spector2007.Literal.negate {α : Type u_2} : Literal α → Literal α

The negation of a literal.

Equations

• (NeoGricean.Spector2007.Literal.pos a).negate = NeoGricean.Spector2007.Literal.neg a
• (NeoGricean.Spector2007.Literal.neg a).negate = NeoGricean.Spector2007.Literal.pos a

def NeoGricean.Spector2007.Literal.satisfies {α : Type u_2} [DecidableEq α] (L : Literal α) (V : Finset α) : Bool

A valuation satisfies a literal.

Equations

• (NeoGricean.Spector2007.Literal.pos a).satisfies V = decide (a ∈ V)
• (NeoGricean.Spector2007.Literal.neg a).satisfies V = decide (a ∉ V)

def NeoGricean.Spector2007.flipLiteral (Atom : Type u_1) [DecidableEq Atom] (V : Valuation Atom) (L : Literal Atom) : Valuation Atom

V_{-L}: The valuation identical to V except over the atom of L. If L = [p], then V_{-L} has p ∉ V_{-L} iff p ∈ V. If L = [¬p], then V_{-L} has p ∈ V_{-L} iff p ∉ V.

Equations

• NeoGricean.Spector2007.flipLiteral Atom V L = if h : L.atom ∈ V then Finset.erase V L.atom else Finset.cons L.atom V h

def NeoGricean.Spector2007.favors (Atom : Type u_1) [DecidableEq Atom] (P : Proposition Atom) (L : Literal Atom) : Prop

Definition 2 (Favoring): A proposition P favors a literal L if there exists a valuation V such that:

1. V ∈ P (V makes P true)
2. L.satisfies V = true (V makes L true)
3. flipLiteral V L ∉ P (flipping L makes P false)

Equations

• NeoGricean.Spector2007.favors Atom P L = ∃ V ∈ P, L.satisfies V = true ∧ NeoGricean.Spector2007.flipLiteral Atom V L ∉ P

def NeoGricean.Spector2007.isPositive (Atom : Type u_1) [DecidableEq Atom] (P : Proposition Atom) : Prop

Definition 4 (Positive Proposition): A proposition is positive if it favors at least one positive literal and no negative literal.

"A positive proposition is a proposition that favors no negative literal and is distinct from ⊥ and ⊤."

Equations

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

def NeoGricean.Spector2007.isNegative (Atom : Type u_1) [DecidableEq Atom] (P : Proposition Atom) : Prop

A proposition is negative if it favors at least one negative literal and no positive literal.

Equations

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

def NeoGricean.Spector2007.properSubset (Atom : Type u_1) (V' V : Valuation Atom) : Prop

V' is a proper subset of V (as sets of true atoms).

Equations

• NeoGricean.Spector2007.properSubset Atom V' V = (V' ⊂ V)

def NeoGricean.Spector2007.Exhaust (Atom : Type u_1) (P : Proposition Atom) : Proposition Atom

Definition 6 (Exhaustification): The set of minimal valuations in P.

Exhaust(P) = {V ∈ P | ¬∃V' ∈ P, V' ⊂ V}

Equations

• NeoGricean.Spector2007.Exhaust Atom P = {V : NeoGricean.Spector2007.Valuation Atom | V ∈ P ∧ ∀ V' ∈ P, ¬V' ⊂ V}

def NeoGricean.Spector2007.Pos (Atom : Type u_1) (P : Proposition Atom) : Proposition Atom

Definition 5 (Positive Extension): The upward closure of P.

Pos(P) = {V | ∃V' ∈ P, V' ⊆ V}

"For any non-negative proposition P, there is a unique positive proposition Q such that P entails Q and Q entails all other positive propositions that P entails."

Equations

• NeoGricean.Spector2007.Pos Atom P = {V : NeoGricean.Spector2007.Valuation Atom | ∃ V' ∈ P, V' ⊆ V}

theorem NeoGricean.Spector2007.Exhaust_subset (Atom : Type u_1) (P : Proposition Atom) : Exhaust Atom P ⊆ P

theorem NeoGricean.Spector2007.exists_minimal (Atom : Type u_1) (P : Set (Valuation Atom)) (s : Valuation Atom) (hs : s ∈ P) : ∃ t ∈ P, t ⊆ s ∧ ∀ u ∈ P, ¬u ⊂ t

Helper lemma: Every element of P has a minimal element below it in P. Uses strong induction on Finset cardinality.

theorem NeoGricean.Spector2007.positive_upward_closed (Atom : Type u_1) [DecidableEq Atom] (P : Proposition Atom) (hpos : isPositive Atom P) (W : Valuation Atom) (hWP : W ∈ P) (a : Atom) (ha_not_W : a ∉ W) : Finset.cons a W ha_not_W ∈ P

Helper: If P is positive and W ∈ P and a ∉ W, then W ∪ {a} ∈ P. (Otherwise P would favor [¬a].)

theorem NeoGricean.Spector2007.positive_superset_mem (Atom : Type u_1) [DecidableEq Atom] (P : Proposition Atom) (hpos : isPositive Atom P) (V' V : Valuation Atom) (hV'P : V' ∈ P) (hV'_sub : V' ⊆ V) : V ∈ P

Helper: Positive propositions are upward closed (if V' ⊆ V and V' ∈ P, then V ∈ P). Proved by strong induction on |V \ V'| (the "gap" between V' and V).

theorem NeoGricean.Spector2007.P_subset_Pos (Atom : Type u_1) (P : Proposition Atom) : P ⊆ Pos Atom P

theorem NeoGricean.Spector2007.Pos_of_positive (Atom : Type u_1) [DecidableEq Atom] (P : Proposition Atom) (hpos : isPositive Atom P) : Pos Atom P = P

Fact 1: If P is positive, then Pos(P) = P.

"If P is positive, Pos(P) = P"

theorem NeoGricean.Spector2007.Pos_Exhaust_eq_Pos (Atom : Type u_1) (P : Proposition Atom) : Pos Atom (Exhaust Atom P) = Pos Atom P

Fact 2: Pos(Exhaust(P)) = Pos(P).

"Pos(Exhaust(P)) = P" [when P is positive, this is Pos(P)]

@[reducible, inline]

abbrev NeoGricean.Spector2007.InfoState (Atom : Type u_1) : Type u_1

An information state is itself a proposition (set of valuations the speaker considers possible).

Equations

• NeoGricean.Spector2007.InfoState Atom = NeoGricean.Spector2007.Proposition Atom

def NeoGricean.Spector2007.I (Atom : Type u_1) (P : Proposition Atom) : Set (InfoState Atom)

Definition 3 (Optimal States): I(P) is the set of information states where P is the strongest positive proposition entailed.

I(P) = {i | Pos(i) = P}

An information state i makes P optimal iff P is the strongest positive proposition that i entails.

Equations

• NeoGricean.Spector2007.I Atom P = {i : NeoGricean.Spector2007.InfoState Atom | NeoGricean.Spector2007.Pos Atom i = P}

def NeoGricean.Spector2007.Max (Atom : Type u_1) (P : Proposition Atom) : Set (InfoState Atom)

Definition 4 (Maximal Optimal States): Max(P) is the set of maximal elements of I(P) - the most informed states that still make P optimal.

"Max(S, α, Q) = {i | i ∈ I(S, α, Q) and ∀i' (i' ∈ I(S, α, Q)) → ¬(i'/Q ⊂ i/Q)}"

In our setting: Max(P) = {i ∈ I(P) | ∀i' ∈ I(P), ¬(i' ⊂ i)}

Equations

• NeoGricean.Spector2007.Max Atom P = {i : NeoGricean.Spector2007.InfoState Atom | i ∈ NeoGricean.Spector2007.I Atom P ∧ ∀ i' ∈ NeoGricean.Spector2007.I Atom P, ¬i' ⊂ i}

theorem NeoGricean.Spector2007.Exhaust_mem_I (Atom : Type u_1) [DecidableEq Atom] (P : Proposition Atom) (hpos : isPositive Atom P) : Exhaust Atom P ∈ I Atom P

Exhaust(P) is in I(P) for positive P.

Since Pos(Exhaust(P)) = Pos(P) = P (by Facts 1 and 2), Exhaust(P) is an information state that makes P optimal.

theorem NeoGricean.Spector2007.Exhaust_entails_I (Atom : Type u_1) [DecidableEq Atom] (P : Proposition Atom) (_hpos : isPositive Atom P) (i : InfoState Atom) : i ∈ I Atom P → Exhaust Atom P ⊆ i

Exhaust(P) entails all members of I(P).

"We want to show that Exhaust(P) entails all the other members of I(P)."

theorem NeoGricean.Spector2007.main_theorem (Atom : Type u_1) [DecidableEq Atom] (P : Proposition Atom) (hpos : isPositive Atom P) : Max Atom P = {Exhaust Atom P}

@cite{spector-2007}:

For any positive proposition P, Max(P) = {Exhaust(P)}.

"Theorem: if P is a positive proposition, then Max(P) = {Exhaust(P)}, and therefore P implicates Exhaust(P)."

This derives exhaustive interpretation from Gricean reasoning:

• The speaker uttered P (Quality: they believe P)
• P was optimal among alternatives (Quantity: no better option)
• Assuming maximal informativeness → the speaker's state is Exhaust(P)
• Therefore P implicates Exhaust(P)

def NeoGricean.Spector2007.orProp (Atom : Type u_1) (A B : Atom) : Proposition Atom

Example: The proposition "A or B" (at least one of A, B is true).

Equations

• NeoGricean.Spector2007.orProp Atom A B = {V : NeoGricean.Spector2007.Valuation Atom | A ∈ V ∨ B ∈ V}

def NeoGricean.Spector2007.exclOrProp (Atom : Type u_1) (A B : Atom) : Proposition Atom

Example: The exhaustification of "A or B" is "exactly A or exactly B".

This is the minimal exclusive disjunction (singletons only). The more general "A xor B" (A ∈ V ↔ B ∉ V) includes non-minimal sets like {A, C}.

Equations

• NeoGricean.Spector2007.exclOrProp Atom A B = {V : NeoGricean.Spector2007.Valuation Atom | V = {A} ∨ V = {B}}

theorem NeoGricean.Spector2007.exhaust_or_eq_exclOr (Atom : Type u_1) [DecidableEq Atom] (A B : Atom) (_hne : A ≠ B) : Exhaust Atom (orProp Atom A B) = exclOrProp Atom A B

The exhaustification of "A or B" yields exclusive disjunction (minimal singletons).