Theories.Semantics.Focus.Comparability #

@cite{umbach-2004} @cite{erteschik-shir-1973} @cite{abeille-et-al-2020}

Theory predicates over the substance taxonomies in Features/:

@cite{umbach-2004} alternative-set well-formedness (similarity + dissimilarity).
@cite{erteschik-shir-1973} / @cite{abeille-et-al-2020} extraction-IS clash constraint, parameterized over the two Krifka axes the paper conflates: filler focus marking (Features.InformationStructure.FocusMark) and domain givenness (Features.BinaryGivenness).

The extractionISClash signature is (filler : FocusMark, domain : BinaryGivenness) → Prop, making the two-axis structure of the FBC explicit. (ExclusionVariety and PolaritySwitchContext were collapsed into Core.Discourse.Coherence.CoherenceRelation in the 0.230.488 cleanup.)

Alternative-Set Well-Formedness (@cite{umbach-2004} §2.2) #

@cite{umbach-2004} identifies two constraints that jointly determine when elements can serve as alternatives (in focus, coordination, or discourse):

Semantic independence: neither alternative entails the other (dissimilarity). Explains why #John had a drink and Mary had a martini is odd — "drink" subsumes "martini".
Common integrator: a concept subsuming all alternatives (similarity). Explains why alternatives must be of a comparable type.

Together these define comparability = similarity + dissimilarity, which is the prerequisite for any type of contrast.

source

def Semantics.Focus.Comparability.semanticallyIndependent {W : Type} (a b : Set W) :

Prop

Two propositions are semantically independent iff neither entails the other. @cite{umbach-2004} §2.2: required for alternatives in focus, coordination, and discourse relations. Violation explains the oddness of #John had a drink and Mary had a martini.

Equations

Semantics.Focus.Comparability.semanticallyIndependent a b = (¬a ⊆ b ∧ ¬b ⊆ a)

Instances For

source

def Semantics.Focus.Comparability.commonIntegrator {W : Type} (alts : List (Set W)) (integ : Set W) :

Prop

A common integrator subsumes all alternatives. @cite{umbach-2004} §2.2, following @cite{lang-1984}: coordinated elements and focus alternatives must share a common superordinate concept. For example, in "beer and martini", "drink" is the common integrator.

Equations

Semantics.Focus.Comparability.commonIntegrator alts integ = ∀ a ∈ alts, a ⊆ integ

Instances For

source

def Semantics.Focus.Comparability.wellFormedAlts {W : Type} (alts : List (Set W)) (integ : Set W) :

Prop

A well-formed alternative set satisfies both constraints. @cite{umbach-2004} §2.2: alternatives must be comparable, i.e., similar (common integrator) and dissimilar (pairwise independent).

Equations

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

Instances For

Extraction and Information-Structural Clash #

@cite{erteschik-shir-1973} @cite{abeille-et-al-2020}

Wh-extraction foregrounds ([FoC]) the moved element. Extracting from a backgrounded ([G]) domain creates an information-structural clash: the element is supposed to address the QUD (as [FoC]) but belongs to a dimension the QUD ignores (as [G]).

This is the constraint underlying both @cite{erteschik-shir-1973}'s Dominance Condition on Extraction and @cite{abeille-et-al-2020}'s Focus Background Constraint (FBC): "a focused element should not be part of a backgrounded constituent."

source

def Semantics.Focus.Comparability.extractionISClash (filler : Features.InformationStructure.FocusMark) (domain : Features.BinaryGivenness) :

Prop

Information-structural extraction clash (@cite{erteschik-shir-1973}, @cite{abeille-et-al-2020}): a focused filler extracted from a given/backgrounded domain creates an incompatibility between the filler's discourse function (addressing the QUD) and the domain's discourse status (QUD-invisible).

The two parameters are independent Krifka axes — filler focus marking (FocusMark, the binary focus axis) and domain givenness (BinaryGivenness, the Prince hearer-status axis).

Use sites:

MoS islands: extractionISClash .focused domainGivenness (filler always focused; only the domain varies)
Subject islands: extractionISClash (fillerFocus c) (subjectGivenness c) (filler focus and domain givenness both vary by construction)
General FBC: same shape, varying both arguments.

Equations