Flatness of Question — Anttila Proposition 2.2.16 specialised to inquisitive content

@cite{anttila-2021} @cite{ciardelli-groenendijk-roelofsen-2018} @cite{aloni-2022}

Anttila 2021 Proposition 2.2.16 (specialised from Proposition 2.2.2): a team-semantic predicate is flat iff it is downward-closed, union-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 flat (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).

What the file proves

For any Question W, with teamSupport lifting (s : Finset W) ↦ ↑s ∈ P.props:

• teamSupport_downwardClosed and teamSupport_emptyTeam are immediate re-statements of P.downward_closed and P.contains_empty.
• isDeclarative_iff_sUnion_closed characterises declarativity via arbitrary-union closure on Set W (the natural carrier for Question).
• IsBinaryUnionClosed is the binary form, directly comparable to Core.Logic.Team.unionClosed at the Finset carrier; the two coincide via finite induction.
• Capstone: teamSupport_flat_of_isDeclarative derives Anttila's flat predicate for declarative Questions by composing the three closure properties through flat_of_downwardClosed_unionClosed_emptyTeam.

Why this is one fact, not two

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

Carrier note

The substrate's Core.Logic.Team.unionClosed is stated over the Finset W carrier (binary union); Question's natural form is Set W (arbitrary union via ⋃₀). For finite W the two coincide via induction; for infinite W arbitrary union is the principled form because binary union doesn't suffice to recover info P = ⋃₀ P.props. A future carrier-polymorphic substrate would let us state this with a single shared predicate.

def Core.Question.teamSupport {W : Type u_1} (P : Question W) : Unit → Unit → Finset W → Prop

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

The Unit → Unit → shape matches Core.Logic.Team.downwardClosed's Model → Form → signature with both pinned to Unit; Question is its own self-contained "model + formula."

Equations

• P.teamSupport x✝¹ x✝ s = (↑s ∈ P.props)

theorem Core.Question.teamSupport_downwardClosed {W : Type u_1} (P : Question W) : Logic.Team.downwardClosed P.teamSupport ()

Substrate fact: every Question's teamSupport is downward-closed in Core.Logic.Team.downwardClosed's sense. The proof IS just P.downward_closed lifted through Finset.coe_subset.

theorem Core.Question.teamSupport_emptyTeam {W : Type u_1} (P : Question W) : Logic.Team.emptyTeam P.teamSupport ()

Substrate fact: every Question's teamSupport has the empty-team property. The proof IS P.contains_empty (modulo Finset.coe_empty).

theorem Core.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. This is 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 (by its bundled axioms); declarativity is exactly when it also satisfies the third.

theorem Core.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. Specialisation of isDeclarative_iff_sUnion_closed that emphasises the info decomposition.

def Core.Question.IsBinaryUnionClosed {W : Type u_1} (P : Question W) : Prop

A Question's props is binary-union-closed iff for any two resolving states their union is also resolving. This is the binary form, directly comparable to Core.Logic.Team.unionClosed's shape (which is binary at the Finset carrier).

Equations

• P.IsBinaryUnionClosed = ∀ (s t : Set W), s ∈ P.props → t ∈ P.props → s ∪ t ∈ P.props

theorem Core.Question.isDeclarative_imp_binary_union_closed {W : Type u_1} (P : Question W) (hdecl : P.isDeclarative) : P.IsBinaryUnionClosed

Declarative implies binary-union-closed: the union of two states each contained in info P is contained in info P, hence in props by downward closure.

theorem Core.Question.isDeclarative_of_binary_union_closed_of_finite_props {W : Type u_1} (P : Question W) (hfin : P.props.Finite) (huc : P.IsBinaryUnionClosed) : P.isDeclarative

For Questions with finite props, binary-union-closed implies declarative. Proof goes via isDeclarative_iff_sUnion_closed plus Set.Finite.induction_on to lift binary closure to arbitrary union.

theorem Core.Question.teamSupport_unionClosed_of_isDeclarative {W : Type u_1} [DecidableEq W] (P : Question W) (hdecl : P.isDeclarative) : Logic.Team.unionClosed P.teamSupport ()

Declarative Question teamSupport is binary-union-closed in the Core.Logic.Team.unionClosed sense (i.e., over Finset W with s ∪ t).

theorem Core.Question.teamSupport_flat_of_isDeclarative {W : Type u_1} [DecidableEq W] (P : Question W) (hdecl : P.isDeclarative) : Logic.Team.flat P.teamSupport ()

Capstone bridge (Anttila Proposition 2.2.16 instantiated for inquisitive content): a declarative Question is flat in the Core.Logic.Team.flat sense. The substrate's flatness theorem flat_of_downwardClosed_unionClosed_emptyTeam applies because every Question already provides downward closure and the empty-team property by its bundled axioms; declarativity adds the missing union closure.

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

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

Question's downward_closed axiom IS IsLowerSet at the Set W carrier. The mathlib primitive IsLowerSet (s : Set α) [LE α] says b ≤ a → a ∈ s → b ∈ s; for Set W the LE instance is ⊆, so this is exactly Question.downward_closed.

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

Mathlib-aligned binary union closure for declarative Questions: SupClosed P.props (mathlib's binary-⊔ closure on Set α, where ⊔ = ∪). Direct corollary of isDeclarative_imp_binary_union_closed rewrapped in mathlib's predicate.

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

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