Small Clause Predication

@cite{dendikken-1995} @cite{baker-1988}

@cite{dendikken-1995}'s central thesis: all subject-predicate relationships are incarnated as small clauses [SC Subject Predicate]. The predicate head's category determines the construction type:

Pred category	Construction	Example
P	Verb-particle / dative	"lift Hsu up", "give the books to Mary"
A	Resultative	"hammer the metal flat"
V	Causative	"make the child laugh"
N	Copular / ECM	"consider John a fool"

The SC analysis unifies these constructions structurally: they share the tree shape V [SC Subj Pred] = node(leaf, node(leaf, leaf)), with differences reduced to the category of the predicate head.

Cross-linguistic extension

Bantu applicative morphemes (-il-, -el-) and Japanese causative -(s)ase are analyzed as affixal particles: grammaticalized instances of P-to-V incorporation. Low applicatives introduce the same structural configuration as particles — SC predication between a goal and a theme, mediated by a P head.

inductive Minimalist.SCPredCategory : Type

Category of the predicate head in a small clause.

@cite{dendikken-1995}: X ∈ {A, N, P, V} — the four LEXICAL categories. The SC family is parameterized by which lexical category serves as the predicate head.

• P : SCPredCategory
• A : SCPredCategory
• V : SCPredCategory
• N : SCPredCategory

@[implicit_reducible]

instance Minimalist.instDecidableEqSCPredCategory : DecidableEq SCPredCategory

Equations

• Minimalist.instDecidableEqSCPredCategory x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Minimalist.instReprSCPredCategory : Repr SCPredCategory

Equations

• Minimalist.instReprSCPredCategory = { reprPrec := Minimalist.instReprSCPredCategory.repr }

def Minimalist.instReprSCPredCategory.repr : SCPredCategory → ℕ → Std.Format

Equations

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

def Minimalist.SCPredCategory.toCat : SCPredCategory → Cat

Map SC predicate categories to syntactic categories.

Equations

• Minimalist.SCPredCategory.P.toCat = Minimalist.Cat.P
• Minimalist.SCPredCategory.A.toCat = Minimalist.Cat.A
• Minimalist.SCPredCategory.V.toCat = Minimalist.Cat.V
• Minimalist.SCPredCategory.N.toCat = Minimalist.Cat.N

@[simp]

theorem Minimalist.SCPredCategory.toCat_P : P.toCat = Cat.P

@[simp]

theorem Minimalist.SCPredCategory.toCat_A : A.toCat = Cat.A

@[simp]

theorem Minimalist.SCPredCategory.toCat_V : V.toCat = Cat.V

@[simp]

theorem Minimalist.SCPredCategory.toCat_N : N.toCat = Cat.N

structure Minimalist.SmallClause : Type

A small clause: subject-predicate pair where the predicate is categorially typed (@cite{dendikken-1995}:27, ex. 44).

[SC subject predicate]

The predCat field determines which member of the SC family this instance belongs to.

• subject : SyntacticObject

  The subject of predication (typically a DP)

• predicate : SyntacticObject

  The predicate head

• predCat : SCPredCategory

  Category of the predicate (determines construction type)

@[implicit_reducible]

instance Minimalist.instReprSmallClause : Repr SmallClause

Equations

• Minimalist.instReprSmallClause = { reprPrec := Minimalist.instReprSmallClause.repr }

def Minimalist.instReprSmallClause.repr : SmallClause → ℕ → Std.Format

Equations

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

def Minimalist.SmallClause.toSO (sc : SmallClause) : SyntacticObject

Build the syntactic object for a small clause: [SC Subj Pred].

Equations

• sc.toSO = Minimalist.merge sc.subject sc.predicate

def Minimalist.SmallClause.embedUnderV (v : SyntacticObject) (sc : SmallClause) : SyntacticObject

Embed a small clause under a verb: V [SC Subj Pred].

Equations

• Minimalist.SmallClause.embedUnderV v sc = Minimalist.merge v sc.toSO

def Minimalist.SCPredCategory.constructionName : SCPredCategory → String

The construction type name for each SC predicate category.

Equations

• Minimalist.SCPredCategory.P.constructionName = "verb-particle / dative"
• Minimalist.SCPredCategory.A.constructionName = "resultative"
• Minimalist.SCPredCategory.V.constructionName = "causative"
• Minimalist.SCPredCategory.N.constructionName = "copular/ECM"

Companion predicate

The bundled structure SmallClause is the Submonoid-style API object: it carries data + the predicate-category discriminator. The companion predicate IsSmallClause : SyntacticObject → Prop lets us ask "is this raw SO an SC?" without constructing a SmallClause. Mathlib analogue: Submonoid (structure) + IsSubmonoid (predicate).

Use this companion to characterize SC encodings written as raw merge-built SyntacticObjects (the prevailing style in study files like HaddicanEtAl2026, Phenomena/ArgumentStructure/Studies/Dendikken1995) without forcing them through the SmallClause constructor.

@[reducible, inline]

noncomputable abbrev Minimalist.SyntacticObject.headCat (so : SyntacticObject) : Cat

Head category of a syntactic object: the leftmost terminal's outer category. By the Minimalist projection convention used in our encodings, the head precedes its complement, so the LEFT child of any non-leaf projects.

Phase 1.0: noncomputable via outerCat (which is itself Quot.out-based after the FreeCommMagma migration). The simp lemmas headCat_leaf / headCat_node no longer hold by rfl and have been removed; consumers should use SyntacticObject.outerCat directly.

Equations

• so.headCat = Minimalist.HeadFunction.leftSpine.outerCat so

def Minimalist.IsSmallClausePredicate (so : SyntacticObject) : Prop

A syntactic object qualifies as a small-clause predicate iff its head category is one of @cite{dendikken-1995}'s four SC-licensed lexical categories (P/A/V/N).

Equations

• Minimalist.IsSmallClausePredicate so = (so.headCat = Minimalist.Cat.P ∨ so.headCat = Minimalist.Cat.A ∨ so.headCat = Minimalist.Cat.V ∨ so.headCat = Minimalist.Cat.N)

@[implicit_reducible]

noncomputable instance Minimalist.instDecidablePredSyntacticObjectIsSmallClausePredicate : DecidablePred IsSmallClausePredicate

Equations

• Minimalist.instDecidablePredSyntacticObjectIsSmallClausePredicate so = id inferInstance

noncomputable def Minimalist.SyntacticObject.rightDaughter? (so : SyntacticObject) : Option SyntacticObject

The "right daughter" of an SO under planar Quot.out. Phase 1.0 placeholder — Phase 2 will replace with an HeadFunction-aware selection of the predicate-side daughter.

Retained as a noncomputable accessor for downstream code that actively wants the planar choice. The IsSmallClause predicate no longer routes through this — see below for the swap-respecting Multiset reformulation.

Equations

• so.rightDaughter? = match Quot.out so with | FreeMagma.of a => none | a.mul r => some (FreeCommMagma.mk r)

def Minimalist.IsSmallClause (so : SyntacticObject) : Prop

A syntactic object IS a small clause when it is a binary node (subject + predicate) some immediate daughter of which satisfies IsSmallClausePredicate. Den Dikken's SC structure (book p. 132 ex. 52a) has the form [SC Spec XP] with Spec one daughter and the projecting predicate XP the other; under MCB nonplanar Merge we don't structurally distinguish "left" from "right", so the swap-invariant formulation asks "one of the immediate daughters is the predicate".

This existential matches the consumer pattern: the test discharges when either the SC's predicate is structurally findable, regardless of which Quot.out representative was chosen. Computable via immediatelyContains (which is decidable and Multiset-based).

Equations

• Minimalist.IsSmallClause so = ∃ (pred : Minimalist.SyntacticObject), Minimalist.immediatelyContains so pred ∧ Minimalist.IsSmallClausePredicate pred

@[implicit_reducible]

noncomputable instance Minimalist.instDecidablePredSyntacticObjectIsSmallClause : DecidablePred IsSmallClause

Equations

• Minimalist.instDecidablePredSyntacticObjectIsSmallClause so = id inferInstance

theorem Minimalist.isSmallClause_merge (l r : SyntacticObject) : IsSmallClause (merge l r) ↔ IsSmallClausePredicate l ∨ IsSmallClausePredicate r

merge-form rewrite for IsSmallClause. Symmetric — by the swap- invariant existential, the predicate can be either the left or the right child.

theorem Minimalist.SmallClause.toSO_isSmallClause (sc : SmallClause) (h : sc.predicate.headCat = sc.predCat.toCat) : IsSmallClause sc.toSO

Round-trip: any SmallClause whose stored predCat agrees with its predicate's actual head category yields a SyntacticObject satisfying IsSmallClause. The hypothesis is the well-formedness invariant the free-form SmallClause constructor doesn't enforce by type — for the standard PVC/Resultative/etc. constructors that use mkLeafPhon matching predCat.toCat, the hypothesis discharges by rfl.

def Minimalist.ApplType.IsAffixalParticle (a : ApplType) : Prop

Whether an applicative head is analyzable as an affixal particle.

Low applicatives introduce a transfer/possession relation between goal and theme — structurally, a P head relating two DPs via SC predication. This is the same configuration as particles.

High applicatives relate the applied argument to the event, not to the theme — they are NOT affixal particles.

Equations

• a.IsAffixalParticle = (a = Minimalist.ApplType.lowRecipient ∨ a = Minimalist.ApplType.lowSource)

@[implicit_reducible]

instance Minimalist.instDecidablePredApplTypeIsAffixalParticle : DecidablePred ApplType.IsAffixalParticle

Equations

• Minimalist.instDecidablePredApplTypeIsAffixalParticle x✝ = Minimalist.instDecidablePredApplTypeIsAffixalParticle._aux_1 x✝

def Minimalist.ApplType.toSCPredCategory : ApplType → Option SCPredCategory

Map low applicatives to SC predicate category P. Low Appl mediates the same structural relation as a particle: [SC Goal [XP Theme]] where the applicative head is the P.

Equations

• Minimalist.ApplType.lowRecipient.toSCPredCategory = some Minimalist.SCPredCategory.P
• Minimalist.ApplType.lowSource.toSCPredCategory = some Minimalist.SCPredCategory.P
• Minimalist.ApplType.high.toSCPredCategory = none

theorem Minimalist.low_recipient_appl_is_particle : ApplType.lowRecipient.IsAffixalParticle

Low recipient applicatives are affixal particles.

theorem Minimalist.low_source_appl_is_particle : ApplType.lowSource.IsAffixalParticle

Low source applicatives are affixal particles.

theorem Minimalist.high_appl_not_particle : ¬ApplType.high.IsAffixalParticle

High applicatives are NOT affixal particles.

theorem Minimalist.low_recipient_appl_is_P : ApplType.lowRecipient.toSCPredCategory = some SCPredCategory.P

Low recipient applicatives map to SC predicate category P.

theorem Minimalist.low_source_appl_is_P : ApplType.lowSource.toSCPredCategory = some SCPredCategory.P

Low source applicatives map to SC predicate category P.

theorem Minimalist.high_appl_no_SC : ApplType.high.toSCPredCategory = none

High applicatives have no SC predication analog.