Docs / Studies / Studies.Deal2025a

Current models of Agree

Deal, A. R. (2025). Berkeley Papers in Formal Linguistics, 4(1)

Deal traces the Agree operation from Chomsky's uninterpretable features to the interaction and satisfaction theory, and states the latter as an algorithm, (30) of the appendix, which Minimalist.Probe.Spec.agree implements. The appendix adds dynamic interaction to the main text's algorithm: a goal bearing a feature marked for it resets the probe's interaction condition to that feature and the features it dominates. In the 2024 derivations a feature copied from a goal instead joins a set of features that every later goal must bear. This file runs the grammars of the 2024 PCC typology through (30) and compares the outcomes.

References

Deal 2025a, Current models of Agree
Deal 2024, Interaction, Satisfaction, and the PCC formalized

Declarations

L33–36

L38–41

L43

Under (30) a combination is licit exactly when the direct object does not satisfy the probe and the indirect object bears a feature dominated by every dynamic feature of the direct object, the geometric closure of each containing it.

theorem licit_iff L45–51

(g : Deal2024.Grammar) (s : Clause.Scenario Person) :

Licit g s ↔ (∀ x ∈ g.satisfaction, x ∉ Phi.PersonSegment.spec s.low) ∧ ∃ y ∈ Phi.PersonSegment.spec s.high, ∀ x ∈ Phi.PersonSegment.spec s.low ∩ g.dynamic, x ≤ y

Built from

(30) licenses no more than the 2024 algorithm, since a person bears whatever its segments depend on: the two part only where the direct object's dynamic features have no common dependent.

theorem Licit.deal2024 L53–59

{g : Deal2024.Grammar} {s : Clause.Scenario Person} (h : Licit g s) :

Deal2024.Licit g s

Built from

L61–72

The two algorithms agree on every combination exactly when the grammar has a satisfaction condition or does not mark both [SPKR] and [ADDR] for dynamic interaction ((30)).

theorem forall_licit_iff_iff L74–80

(g : Deal2024.Grammar) :

(∀ (s : Clause.Scenario Person), Licit g s ↔ Deal2024.Licit g s) ↔ ¬(g.satisfaction = none ∧ Phi.PersonSegment.speaker ∈ g.dynamic ∧ Phi.PersonSegment.addressee ∈ g.dynamic)

Built from

With [SPKR] and [ADDR] both dynamic and no satisfaction condition, an inclusive direct object licenses an inclusive indirect object in 2024 but not under (30).

theorem inclusive_divergence L82–87

Deal2024.Licit { satisfaction := none, dynamic := {Phi.PersonSegment.speaker, Phi.PersonSegment.addressee} } { high := Person.firstInclusive, low := Person.firstInclusive } ∧ ¬Licit { satisfaction := none, dynamic := {Phi.PersonSegment.speaker, Phi.PersonSegment.addressee} } { high := Person.firstInclusive, low := Person.firstInclusive }

Built from

On the six cells of table (1) the two algorithms agree for every grammar ((53), (57), (30)).

theorem licit_iff_on_cells L89–93

(g : Deal2024.Grammar) (s : Clause.Scenario Person) :

s ∈ PCC.distinctPairs → (Licit g s ↔ Deal2024.Licit g s)

Built from