Team-semantic properties of formulas (Anttila 2021 §2.2) — re-exports

@cite{anttila-2021}

This file is now a re-export shim. The substrate moved to Core/Logic/Team/Closure.lean, which states the four canonical Anttila Definition 2.2.1 properties as facts about TeamPred α := Finset α → Prop using mathlib's IsLowerSet and SupClosed:

Anttila property	TeamPred predicate
Downward closure	TeamPred.IsDownward
Union closure	TeamPred.IsSupClosed
Empty team property	TeamPred.HasEmpty
Flatness	TeamPred.IsFlat

The central technical theorem (Anttila Proposition 2.2.2) is Core.Logic.Team.TeamPred.isFlat_iff — flatness ↔ all three closure properties.

Migration from the old parametric API

Pre-0.230.653 this file held parametric definitions downwardClosed (support : Model → Form → Finset W → Prop) (φ : Form) that decorated a per-(M, φ) team-predicate with the Form/Model wrapping. The decoration was unused — every theorem reduced to a fact about the team-predicate support M φ : Finset W → Prop. Consumers now invoke (support M φ).IsDownward etc. directly.

The audit-flagged "decorative parameters" objection (mathlib-reviewer + linglib-integration-auditor, May 2026) is closed by this re-export.

Deprecated aliases

For backward compatibility during the transition, deprecated aliases preserve the parametric shape: downwardClosed support φ ≡ ∀ M, (support M φ).IsDownward (etc.). Consumers should prefer the TeamPred form.

def Core.Logic.Team.downwardClosed {W : Type u_1} {Form : Type u_2} {Model : Type u_3} (support : Model → Form → Finset W → Prop) (φ : Form) : Prop

Deprecated: use (support M φ).IsDownward (per TeamPred) directly. Kept as a wrapper around the universal-over-models form.

Equations

• Core.Logic.Team.downwardClosed support φ = ∀ (M : Model), Core.Logic.Team.TeamPred.IsDownward (support M φ)

def Core.Logic.Team.unionClosed {W : Type u_1} [DecidableEq W] {Form : Type u_2} {Model : Type u_3} (support : Model → Form → Finset W → Prop) (φ : Form) : Prop

Deprecated: use (support M φ).IsSupClosed directly.

Equations

• Core.Logic.Team.unionClosed support φ = ∀ (M : Model), Core.Logic.Team.TeamPred.IsSupClosed (support M φ)

def Core.Logic.Team.emptyTeam {W : Type u_1} {Form : Type u_2} {Model : Type u_3} (support : Model → Form → Finset W → Prop) (φ : Form) : Prop

Deprecated: use (support M φ).HasEmpty directly.

Equations

• Core.Logic.Team.emptyTeam support φ = ∀ (M : Model), Core.Logic.Team.TeamPred.HasEmpty (support M φ)

def Core.Logic.Team.flat {W : Type u_1} {Form : Type u_2} {Model : Type u_3} (support : Model → Form → Finset W → Prop) (φ : Form) : Prop

Deprecated: use (support M φ).IsFlat directly.

Equations

• Core.Logic.Team.flat support φ = ∀ (M : Model), Core.Logic.Team.TeamPred.IsFlat (support M φ)

theorem Core.Logic.Team.flat_iff_downwardClosed_unionClosed_emptyTeam {W : Type u_1} [DecidableEq W] {Form : Type u_2} {Model : Type u_3} (support : Model → Form → Finset W → Prop) (φ : Form) : flat support φ ↔ downwardClosed support φ ∧ unionClosed support φ ∧ emptyTeam support φ

Anttila Proposition 2.2.2 in parametric form: a formula is flat iff it is downward-closed, sup-closed, and has the empty team property. Delegates per-M to TeamPred.isFlat_iff.

Prefer Core.Logic.Team.TeamPred.isFlat_iff for new code (no Form/Model wrapping).

theorem Core.Logic.Team.flat_of_downwardClosed_unionClosed_emptyTeam {W : Type u_1} [DecidableEq W] {Form : Type u_2} {Model : Type u_3} {support : Model → Form → Finset W → Prop} {φ : Form} (hd : downwardClosed support φ) (hu : unionClosed support φ) (he : emptyTeam support φ) : flat support φ

Constructive form: combine the three to get flatness.

theorem Core.Logic.Team.downwardClosed_of_flat {W : Type u_1} [DecidableEq W] {Form : Type u_2} {Model : Type u_3} {support : Model → Form → Finset W → Prop} {φ : Form} (h : flat support φ) : downwardClosed support φ

Forward extraction.

theorem Core.Logic.Team.unionClosed_of_flat {W : Type u_1} [DecidableEq W] {Form : Type u_2} {Model : Type u_3} {support : Model → Form → Finset W → Prop} {φ : Form} (h : flat support φ) : unionClosed support φ

theorem Core.Logic.Team.emptyTeam_of_flat {W : Type u_1} [DecidableEq W] {Form : Type u_2} {Model : Type u_3} {support : Model → Form → Finset W → Prop} {φ : Form} (h : flat support φ) : emptyTeam support φ