Unalternative Semantics

Focus marking without [F]-features ([buring-2015], [assmann-etal-2023]): constructions directly constrain the focal targets they can realize.

• Morphosyntactic ([assmann-etal-2023] §2): a construction focally marks exactly one constituent; No Projection lets it realize any focus within that constituent, and Blocking preempts it wherever a strictly more specific marking would do. Usable packages both; usable_iff_minimal identifies it with minimality among inventory covers.
• Prosodic ([buring-2015]): a branching node's metrical pattern restricts targets pointwise. weakBanned (his Weak Restriction) bans targets that vary the weak daughter over its alternative domain while the strong daughter stays at its ordinary value; strongAllowed (his Strong Restriction) allows only targets varying the accented daughter non-trivially. Both are Set.seq images of AltMeaning.aSet — Hamblin application with one side held at its ordinary value — so the prosodic calculus runs through the same applicative as the Roothian engine (AltMeaning.aSet_seq).

licensedFocusValue is the pipeline connector: the composable targets minus the banned ones. At propositional type its values are PropFocusValues, the focus values [Roo92]'s squiggle consumes — the metrical structure derives the focus value that F-marking stipulates (Antecedent.Admits.of_licensed).

Morphosyntactic focal marking

def Semantics.Focus.Usable {C : Type u_1} [PartialOrder C] (inv : List C) (m f : C) : Prop

A focally marked constituent is usable for focus f ([assmann-etal-2023] §2.2–2.3): it is in the language's inventory, f lies within it (No Projection), and no strictly more specific inventory constituent also covers f (Blocking).

Equations

• Semantics.Focus.Usable inv m f = (m ∈ inv ∧ f ≤ m ∧ ∀ m' ∈ inv, f ≤ m' → m' ≤ m → m' = m)

@[implicit_reducible]

instance Semantics.Focus.instDecidableUsableOfDecidableEqOfDecidableLE {C : Type u_1} [PartialOrder C] {inv : List C} {m f : C} [DecidableEq C] [DecidableLE C] : Decidable (Usable inv m f)

Equations

• Semantics.Focus.instDecidableUsableOfDecidableEqOfDecidableLE = Semantics.Focus.instDecidableUsableOfDecidableEqOfDecidableLE._aux_1

theorem Semantics.Focus.usable_iff_minimal {C : Type u_1} [PartialOrder C] {inv : List C} {m f : C} : Usable inv m f ↔ Minimal (fun (c : C) => c ∈ inv ∧ f ≤ c) m

Usability is minimality among inventory covers of the focus.

Prosodic focal restrictions

def Semantics.Focus.weakBanned {α : Type u_2} {β : Type u_3} (dw : Alternatives.AltMeaning (α → β)) (ds : Alternatives.AltMeaning α) : Set β

Weak Restriction ([buring-2015]): under the default weak–strong pattern, the banned focal targets vary the weak (function) daughter over its alternative domain while the strong daughter stays at its ordinary value.

Equations

• Semantics.Focus.weakBanned dw ds = dw.aSet.seq {ds.oValue}

def Semantics.Focus.strongAllowed {α : Type u_2} {β : Type u_3} (dm : Alternatives.AltMeaning (α → β)) (ds : Alternatives.AltMeaning α) : Set β

Strong Restriction ([buring-2015]): under prosodic reversal, the allowed focal targets vary the accented (function) daughter non-trivially while the deaccented daughter stays at its ordinary value.

Equations

• Semantics.Focus.strongAllowed dm ds = (dm.aSet \ {dm.oValue}).seq {ds.oValue}

theorem Semantics.Focus.strongAllowed_subset_weakBanned {α : Type u_2} {β : Type u_3} (dm : Alternatives.AltMeaning (α → β)) (ds : Alternatives.AltMeaning α) : strongAllowed dm ds ⊆ weakBanned dm ds

Reversal allows only targets that the default bans.

def Semantics.Focus.licensedFocusValue {α : Type u_2} {β : Type u_3} (dw : Alternatives.AltMeaning (α → β)) (ds : Alternatives.AltMeaning α) : Set β

The focal targets a metrical configuration licenses: everything the daughters compose to, minus the banned targets. At β := Set W this is a PropFocusValue W — the focus value the prosody derives.

Equations

• Semantics.Focus.licensedFocusValue dw ds = dw.aSet.seq ds.aSet \ Semantics.Focus.weakBanned dw ds

theorem Semantics.Focus.licensedFocusValue_subset_seq {α : Type u_2} {β : Type u_3} (dw : Alternatives.AltMeaning (α → β)) (ds : Alternatives.AltMeaning α) : licensedFocusValue dw ds ⊆ dw.aSet.seq ds.aSet

theorem Semantics.Focus.disjoint_licensedFocusValue_weakBanned {α : Type u_2} {β : Type u_3} (dw : Alternatives.AltMeaning (α → β)) (ds : Alternatives.AltMeaning α) : Disjoint (licensedFocusValue dw ds) (weakBanned dw ds)

theorem Semantics.Focus.Antecedent.Admits.of_licensed {W : Type u_1} {α : Type u_2} {a : Antecedent W} {dw : Alternatives.AltMeaning (α → Set W)} {ds : Alternatives.AltMeaning α} (h : a.Admits (licensedFocusValue dw ds)) : a.Admits (dw.aSet.seq ds.aSet)

Prosodic restriction only strengthens admission: an antecedent the licensed focus value admits is admitted by the unrestricted Hamblin composition — [Roo92]'s fip against the prosodically derived focus value.