Flatness of Question — Anttila 2.2.16 specialised to inquisitive content

[Ant21] [CGR18] [Alo22]

Anttila Proposition 2.2.16 (specialised from Proposition 2.2.2): a team-semantic predicate is flat iff it is downward-closed, sup-closed, and contains the empty team. This file specialises that fact to Question W — the bundled inquisitive-semantics propositional content type — and discovers an exact correspondence:

inquisitive isDeclarative ↔ team-semantic flatness (under teamSupport)

since Question's structural axioms contains_empty and downward_closed already provide two of the three Anttila properties; declarativity is exactly what supplies the third (union closure).

Main declarations

• isLowerSet_props — Question.downward_closed IS IsLowerSet P.props.
• bot_mem_props — Question.contains_empty IS ⊥ ∈ P.props.
• isDeclarative_iff_sUnion_closed — declarativity ↔ closure under arbitrary unions on P.props.
• supClosed_props_of_isDeclarative — declarative Questions have mathlib-SupClosed (binary) P.props.
• teamSupport — natural carrier-bridge from Set W (Question's native carrier) to Finset W (team-semantic substrate's carrier).
• isFlat_teamSupport_of_isDeclarative — the capstone: declarative Questions are flat in Core.Logic.Team.IsFlat's sense.

Why this is one fact, not two

Inquisitive semantics (Ciardelli-Groenendijk-Roelofsen) and team-semantic modal logic (Aloni / Anttila) developed independently. "Flatness" (Anttila 2.2.16) and "declarativity" (CGR 2018) were named in different literatures for the same structural property. This file makes that identification explicit through the carrier-bridge.

Carrier note

Question's natural carrier is Set W (arbitrary unions via ⋃₀); the team-semantic substrate's carrier is Finset W (binary unions). For finite W the two coincide; for infinite W arbitrary union is the principled form because binary union doesn't suffice to recover info P = ⋃₀ P.props. Mathlib's IsLowerSet and SupClosed are already polymorphic in their carrier; IsFlat is Finset α-specific by design. The teamSupport bridge is how a Set W-carried Question instantiates the Finset W-carried IsFlat.

Question's bundled axioms ARE IsLowerSet + ⊥ ∈ · on Set W

theorem Question.isLowerSet_props {W : Type u_1} (P : Question W) : IsLowerSet P.props

Question.downward_closed IS IsLowerSet at the Set W carrier. For Set W the LE instance is ⊆, so this matches mathlib's IsLowerSet (s : Set α) [LE α].

theorem Question.bot_mem_props {W : Type u_1} (P : Question W) : ⊥ ∈ P.props

Question.contains_empty IS ⊥ ∈ P.props. For Set W, ⊥ = ∅.

Declarativity ↔ arbitrary union closure

theorem Question.isDeclarative_iff_sUnion_closed {W : Type u_1} (P : Question W) : P.isDeclarative ↔ ∀ S ⊆ P.props, ⋃₀ S ∈ P.props

A Question W is declarative iff its props is closed under arbitrary unions. The bridge between two traditions:

• Anttila/Aloni: the third Anttila Definition 2.2.1 property is union closure; combined with downward closure and empty-team it characterises flat contents (Anttila Proposition 2.2.2).
• Ciardelli-Groenendijk-Roelofsen: a content is declarative iff info P ∈ P.props, i.e., the union of its resolving states is itself a resolving state.

The two predicates are the same. Every Question automatically satisfies the first two Anttila properties; declarativity is exactly when it also satisfies the third.

theorem Question.isDeclarative_iff_info_in_props {W : Type u_1} (P : Question W) : P.isDeclarative ↔ P.info ∈ P.props

Restated using info: a Question is declarative iff every union of resolving states is itself a resolving state.

theorem Question.supClosed_props_of_isDeclarative {W : Type u_1} (P : Question W) (hdecl : P.isDeclarative) : SupClosed P.props

Declarativity gives mathlib's SupClosed (binary closure under ⊔ = ∪) on P.props. Direct corollary of arbitrary-union closure via isDeclarative_iff_sUnion_closed applied to the binary case.

Bridge to Finset W carrier and the flatness capstone

def Question.teamSupport {W : Type u_1} (P : Question W) (s : Finset W) : Prop

The natural team-semantic predicate of a Question: a Finset W team is "supported" iff its underlying Set W is in P.props. Carrier-bridge between Question's Set W and the team-semantic substrate's Finset W.

Equations

• P.teamSupport s = (↑s ∈ P.props)

theorem Question.isLowerSet_teamSupport {W : Type u_1} [DecidableEq W] (P : Question W) : IsLowerSet {s : Finset W | P.teamSupport s}

theorem Question.teamSupport_empty {W : Type u_1} (P : Question W) : P.teamSupport ∅

theorem Question.supClosed_teamSupport_of_isDeclarative {W : Type u_1} [DecidableEq W] (P : Question W) (hdecl : P.isDeclarative) : SupClosed {s : Finset W | P.teamSupport s}

theorem Question.isFlat_teamSupport_of_isDeclarative {W : Type u_1} [DecidableEq W] (P : Question W) (hdecl : P.isDeclarative) : Core.Logic.Team.IsFlat {s : Finset W | P.teamSupport s}

Capstone bridge (Anttila Proposition 2.2.16 instantiated for inquisitive content): a declarative Question is flat in the Core.Logic.Team.IsFlat sense at the teamSupport carrier-bridge.

The substrate-unity claim made concrete: the inquisitive isDeclarative predicate and the team-semantic IsFlat predicate are the same property under the natural carrier-bridge. Two communities, one fact.