Small Clause Predication

[dD95] [Bak88]

[dD95]'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.

[dD95]: 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 ([dD95]: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.

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

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

Equations

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

noncomputable 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.SO.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, Studies/Dendikken1995) without forcing them through the SmallClause constructor.

@[reducible, inline]

abbrev Minimalist.SO.headCat (so : SyntacticObject) : Option Cat

Head category of a syntactic object: the outer category of the projecting (selection-driven) head ([Adg03] eq. 137 / [MCB25] Lemma 1.13.7 — "the item that projects becomes head"). none at exocentric/symmetric nodes outside the endocentric domain Dom(h).

Computable, section-free alias of outerCatC for the SC-domain reading. Supersedes the former Quot.out-based leftSpine.outerCat (arbitrary leftmost leaf): the value now tracks the genuine selector, not the representative choice.

Equations

• Minimalist.SO.headCat so = Minimalist.SO.outerCatC so

Binary-node leaf/node counts

SO.merge / SO.node are noncomputable (the Nonplanar carrier round-trips through Quotient.out), so decide/rfl can't read back the shape of a merge-built tree. These two lemmas give the structural facts study files need — a binary node has the summed leaf count of its children and exactly one more internal node — by quotient induction, mirroring Nonplanar.numNodes_node.

theorem Minimalist.SO.leafCount_node (l r : SyntacticObject) : (node l r).leafCount = leafCount l + leafCount r

Leaf count of a binary Merge node is the sum of its children's.

@[simp]

theorem Minimalist.SO.leafCount_merge (l r : SyntacticObject) : (merge l r).leafCount = leafCount l + leafCount r

Leaf count of a Merge is the sum of its children's (SO.merge = SO.node).

def Minimalist.IsSmallClausePredicate (so : SyntacticObject) : Prop

A syntactic object qualifies as a small-clause predicate iff its head category is one of [dD95]'s four SC-licensed lexical categories (P/A/V/N).

Equations

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

@[implicit_reducible]

instance Minimalist.instDecidablePredSyntacticObjectIsSmallClausePredicate : DecidablePred IsSmallClausePredicate

Equations

• Minimalist.instDecidablePredSyntacticObjectIsSmallClausePredicate so = id inferInstance

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.SO), Minimalist.SO.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 (SO.merge l r) ↔ IsSmallClausePredicate l ∨ IsSmallClausePredicate r

SO.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 : SO.headCat sc.predicate = some 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.