Liu and Yip (2026): Again, finiteness, and split aspect in Chinese languages

This file formalizes the size-based account of finiteness and of exceptional scope in Liu and Yip's paper. Verb complements in Mandarin and Cantonese come in three sizes, a finite CP, a nonfinite TP and a nonfinite vP, and the two aspect projections of the split aspect approach sit at fixed heights, the outer one at the level of T above vP and the inner one at the level of v, so every complement contains inner aspect and only a TP or larger contains outer aspect (Contains). An again-element or aspectual suffix associates with one of the two projections, by movement for Mandarin preverbal you and by agreement for the suffixes, and takes exceptional scope across a complement, skipping the matrix predicate or lowering onto it, exactly when the complement has no projection of its kind to intervene, so that it associates with the matrix one (ExceptionalScope). The paper's tables follow from that one definition: outer-associated elements, Mandarin you, Cantonese -faan and the outer aspectual suffixes, take exceptional scope across a vP and across nothing larger (exceptionalScope_outer_iff); inner-associated elements, Mandarin zai, Cantonese zoi and repetitive -gwo, the continuous -zyu and the phase complements, never do (not_exceptionalScope_inner), which is the argument that vP is the minimal size of a nonfinite clause; and transparency is downward closed along the size hierarchy (ExceptionalScope.anti), the implicational complementation hierarchy of Wurmbrand and Lohninger. Mandarin you alone carries the unvalued dynamic feature of Lin and Liu and must be licensed by an outer aspect head bearing [+D], which the paper's selectional table for xiang 'want', rang 'let' and xiangxin 'believe' turns into the embeddability of you (Pred.embedsYou) and into the blocking of aspect lowering by an embedded you (not_exceptionalScope_of_licensesDynamic).

Main definitions

• AspProjection, AspProjection.level — the outer and inner aspect projections of the split aspect approach and their heights in the functional sequence.
• Contains, ExceptionalScope — a complement size contains an aspect projection, and an element associated with it takes exceptional scope across it.
• Again, Again.projection, Again.NeedsDynamic — the six again-elements, the projection each associates with, and the dynamic feature of you.
• aspectProjection, phaseComplementProjection — the association of the Cantonese aspect suffixes and phase complements.
• Pred.selects, Complement.LicensesDynamic, CPred.size — the complements the Mandarin and Cantonese predicates select.

Main results

• exceptionalScope_outer_iff, not_exceptionalScope_inner, ExceptionalScope.anti — the scope pattern by size and projection, and the implicational hierarchy.
• generalization_I, generalization_II, correlation_I, correlation_II — the Mandarin generalizations as consequences.
• cantonese_lowering, aspect_lowering, no_phaseComplement_lowering — the Cantonese pattern for the again-elements, the aspect suffixes and the phase complements.
• embedsYou, not_exceptionalScope_of_licensesDynamic — the licensing of you and its blocking of aspect lowering.

Implementation notes

The two projections are the binary split of [Tra10b], [MD08], [Tsa08] and [Syb17]; their heights are those of the functional sequence in Syntax/Minimalist/Category/FunctionalSequence, outer aspect at the level of T and inner aspect at the level of v, so containment is a comparison of levels. Chomsky's defective intervention is not a relation between heads: an embedded projection blocks association whatever its features, which is the paper's claim. The semicomplementizer and Exfoliation, the restitutive reading, the Italian parallel and the crosstype ambiguity of dasuan 'plan' are not represented.

References

• [LY26]
• [WL23]
• [LL09]
• [Cho00]
• [Tra10b]
• [MD08]
• [Tsa08]
• [Syb17]

Clause sizes and the projections they contain

inductive LiuYip2026.AspProjection : Type

The two aspect projections of the split aspect approach: the outer one above vP, which hosts viewpoint aspect, and the inner one in the v shell, which hosts Aktionsart.

• outer : AspProjection
• inner : AspProjection

@[instance_reducible]

instance LiuYip2026.instDecidableEqAspProjection : DecidableEq AspProjection

Equations

• LiuYip2026.instDecidableEqAspProjection x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance LiuYip2026.instReprAspProjection : Repr AspProjection

Equations

• LiuYip2026.instReprAspProjection = { reprPrec := LiuYip2026.instReprAspProjection.repr }

def LiuYip2026.instReprAspProjection.repr : AspProjection → ℕ → Std.Format

Equations

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

def LiuYip2026.AspProjection.level : AspProjection → ℕ

The height of a projection in the functional sequence, the level of T for the outer one and of v for the inner one.

Equations

• LiuYip2026.AspProjection.outer.level = Minimalist.Cat.T.fValue
• LiuYip2026.AspProjection.inner.level = Minimalist.Cat.v.fValue

def LiuYip2026.typeI : Minimalist.ComplementSize

Type I, the finite CP.

Equations

• LiuYip2026.typeI = Minimalist.ComplementSize.cP

def LiuYip2026.typeII : Minimalist.ComplementSize

Type II, the nonfinite TP without aspect restructuring.

Equations

• LiuYip2026.typeII = Minimalist.ComplementSize.tP

def LiuYip2026.typeIII : Minimalist.ComplementSize

Type III, the nonfinite vP with aspect restructuring.

Equations

• LiuYip2026.typeIII = Minimalist.ComplementSize.vP

def LiuYip2026.Contains (s : Minimalist.ComplementSize) (f : AspProjection) : Prop

A complement of size s contains the aspect projection f when it reaches the projection's height, the level of T for the outer one and the level of v for the inner one.

Equations

• LiuYip2026.Contains s f = (f.level ≤ s.fLevel)

@[instance_reducible]

instance LiuYip2026.instDecidableContains (s : Minimalist.ComplementSize) (f : AspProjection) : Decidable (Contains s f)

Equations

• LiuYip2026.instDecidableContains s f = { decide := f.level.ble s.fLevel, reflects_decide := ⋯ }

theorem LiuYip2026.contains_inner {s : Minimalist.ComplementSize} (h : Minimalist.ComplementSize.vP ≤ s) : Contains s AspProjection.inner

Every complement from vP up contains inner aspect.

theorem LiuYip2026.contains_outer_iff (s : Minimalist.ComplementSize) : Contains s AspProjection.outer ↔ Minimalist.ComplementSize.tP ≤ s

A complement contains outer aspect exactly when it is at least a TP.

def LiuYip2026.ExceptionalScope (f : AspProjection) (s : Minimalist.ComplementSize) : Prop

An element associated with the projection f takes exceptional scope across a complement of size s, skipping the matrix predicate or lowering onto it, when the complement has no projection of that kind to intervene, so that the element associates with the matrix one.

Equations

• LiuYip2026.ExceptionalScope f s = ¬LiuYip2026.Contains s f

@[instance_reducible]

instance LiuYip2026.instDecidableExceptionalScope (f : AspProjection) (s : Minimalist.ComplementSize) : Decidable (ExceptionalScope f s)

Equations

• LiuYip2026.instDecidableExceptionalScope f s = { decide := !decide (LiuYip2026.Contains s f), reflects_decide := ⋯ }

theorem LiuYip2026.ExceptionalScope.anti {f : AspProjection} {s s' : Minimalist.ComplementSize} (h : s ≤ s') (hs : ExceptionalScope f s') : ExceptionalScope f s

Transparency is downward closed along the size hierarchy, the implicational complementation hierarchy, so what crosses a larger complement crosses a smaller one.

theorem LiuYip2026.exceptionalScope_outer_iff (s : Minimalist.ComplementSize) : ExceptionalScope AspProjection.outer s ↔ s < Minimalist.ComplementSize.tP

Outer-associated elements take exceptional scope across a complement smaller than a TP, the vP, and across nothing larger.

theorem LiuYip2026.not_exceptionalScope_inner {s : Minimalist.ComplementSize} (h : Minimalist.ComplementSize.vP ≤ s) : ¬ExceptionalScope AspProjection.inner s

Inner-associated elements never take exceptional scope: every complement contains inner aspect, so vP is the minimal size of a nonfinite clause.

theorem LiuYip2026.generalization_II : ExceptionalScope AspProjection.outer typeIII ∧ ¬ExceptionalScope AspProjection.outer typeII ∧ ¬ExceptionalScope AspProjection.outer typeI

Generalization II says that exceptional scope crosses a nonfinite vP, not a nonfinite TP nor a finite CP.

The again-elements and their projections

inductive LiuYip2026.Again : Type

The again-type elements of the two languages: Mandarin preverbal you and zai, Cantonese preverbal jau and zoi and postverbal -faan and repetitive -gwo.

• you : Again
• zai : Again
• jau : Again
• zoi : Again
• faan : Again
• gwo : Again

@[instance_reducible]

instance LiuYip2026.instDecidableEqAgain : DecidableEq Again

Equations

• LiuYip2026.instDecidableEqAgain x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def LiuYip2026.instReprAgain.repr : Again → ℕ → Std.Format

Equations

• LiuYip2026.instReprAgain.repr LiuYip2026.Again.you prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LiuYip2026.Again.you")).group prec✝
• LiuYip2026.instReprAgain.repr LiuYip2026.Again.zai prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LiuYip2026.Again.zai")).group prec✝
• LiuYip2026.instReprAgain.repr LiuYip2026.Again.jau prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LiuYip2026.Again.jau")).group prec✝
• LiuYip2026.instReprAgain.repr LiuYip2026.Again.zoi prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LiuYip2026.Again.zoi")).group prec✝
• LiuYip2026.instReprAgain.repr LiuYip2026.Again.faan prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LiuYip2026.Again.faan")).group prec✝
• LiuYip2026.instReprAgain.repr LiuYip2026.Again.gwo prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LiuYip2026.Again.gwo")).group prec✝

@[instance_reducible]

instance LiuYip2026.instReprAgain : Repr Again

Equations

• LiuYip2026.instReprAgain = { reprPrec := LiuYip2026.instReprAgain.repr }

def LiuYip2026.Again.item : Again → Presupposition.TriggerItem

The lexical entry of an element in its language's fragment.

Equations

• LiuYip2026.Again.you.item = Mandarin.Adverbs.you
• LiuYip2026.Again.zai.item = Mandarin.Adverbs.zai
• LiuYip2026.Again.jau.item = Cantonese.Particles.jau
• LiuYip2026.Again.zoi.item = Cantonese.Particles.zoi
• LiuYip2026.Again.faan.item = Cantonese.Particles.faan
• LiuYip2026.Again.gwo.item = Cantonese.Particles.gwo

theorem LiuYip2026.Again.item_triggerClass (a : Again) : a.item.triggerClass = Presupposition.TriggerClass.iterative

Every again-element is an iterative trigger in its fragment.

def LiuYip2026.Again.projection : Again → Option AspProjection

The projection each element associates with. You associates by movement and -faan by agreement with the outer one, and zai, zoi and repetitive -gwo with the inner one; preverbal jau is base-generated where it is pronounced and associates with neither.

Equations

• LiuYip2026.Again.you.projection = some LiuYip2026.AspProjection.outer
• LiuYip2026.Again.faan.projection = some LiuYip2026.AspProjection.outer
• LiuYip2026.Again.zai.projection = some LiuYip2026.AspProjection.inner
• LiuYip2026.Again.zoi.projection = some LiuYip2026.AspProjection.inner
• LiuYip2026.Again.gwo.projection = some LiuYip2026.AspProjection.inner
• LiuYip2026.Again.jau.projection = none

def LiuYip2026.Again.NeedsDynamic (a : Again) : Prop

The element carries the unvalued dynamic feature [u+D] that an outer aspect head bearing [+D] must check, which you alone does.

Equations

• a.NeedsDynamic = (a = LiuYip2026.Again.you)

@[instance_reducible]

instance LiuYip2026.instDecidablePredAgainNeedsDynamic : DecidablePred Again.NeedsDynamic

Equations

• LiuYip2026.instDecidablePredAgainNeedsDynamic a = LiuYip2026.instDecidablePredAgainNeedsDynamic._aux_1 a

def LiuYip2026.Again.Skips (a : Again) : Prop

The element takes exceptional scope across some complement.

Equations

• a.Skips = ∃ f ∈ a.projection, ∃ s ∈ [LiuYip2026.typeI, LiuYip2026.typeII, LiuYip2026.typeIII], LiuYip2026.ExceptionalScope f s

@[instance_reducible]

instance LiuYip2026.instDecidablePredAgainSkips : DecidablePred Again.Skips

Equations

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

theorem LiuYip2026.skips_iff (a : Again) : a.Skips ↔ a.projection = some AspProjection.outer

An element takes exceptional scope somewhere exactly when it associates with the outer projection.

theorem LiuYip2026.generalization_I : Again.you.Skips ∧ ¬Again.zai.Skips

Generalization I says that exceptional scope is found with you but not with zai.

theorem LiuYip2026.cantonese_lowering : Again.faan.Skips ∧ ¬Again.gwo.Skips ∧ ¬Again.jau.Skips ∧ ¬Again.zoi.Skips

In Cantonese -faan lowers, repetitive -gwo does not, and neither preverbal adverb has exceptional scope.

theorem LiuYip2026.correlation_I (a : Again) : a ∈ [Again.you, Again.zai] → (a.Skips ↔ a.NeedsDynamic)

Correlation I says that a Mandarin again-element has exceptional scope iff it cannot surface in an embedded nonfinite clause without a dynamic aspect, that is, iff it carries [u+D].

theorem LiuYip2026.correlation_II (a : Again) : a.Skips ↔ ∃ f ∈ a.projection, Minimalist.Cat.Asp.fValue ≤ f.level

Correlation II says that an again-element has exceptional scope iff its projection is at least as high as the aspectual heads, the level of Asp in the functional sequence.

Aspect suffixes and phase complements

def LiuYip2026.aspectProjection (m : Aspect.Marker) : AspProjection

The Cantonese aspect suffixes associate with a projection, the perfective -zo, the progressive -gan and the experiential -gwo with the outer one and the continuous -zyu with the inner one.

Equations

• LiuYip2026.aspectProjection m = if m = Cantonese.Aspect.zyu then LiuYip2026.AspProjection.inner else LiuYip2026.AspProjection.outer

def LiuYip2026.phaseComplementProjection : Cantonese.ResultativeComplements.PhaseComplement → AspProjection

Every phase complement associates with the inner projection.

Equations

• LiuYip2026.phaseComplementProjection x✝ = LiuYip2026.AspProjection.inner

theorem LiuYip2026.aspect_lowering (m : Aspect.Marker) : m ∈ Cantonese.Aspect.markers → (ExceptionalScope (aspectProjection m) typeIII ↔ m ≠ Cantonese.Aspect.zyu)

Under aspect lowering an outer aspect suffix embedded in a vP is interpreted on the matrix predicate, and the continuous -zyu alone is not.

theorem LiuYip2026.no_phaseComplement_lowering (pc : Cantonese.ResultativeComplements.PhaseComplement) {s : Minimalist.ComplementSize} (h : Minimalist.ComplementSize.vP ≤ s) : ¬ExceptionalScope (phaseComplementProjection pc) s

No phase complement lowers across any complement.

Selection and the licensing of you

inductive LiuYip2026.Complement : Type

A complement as a predicate selects it is a vP, a TP whose outer aspect head has the given dynamicity, or a CP.

• vP : Complement
• tP (d : Aspect.Dynamicity) : Complement
• cP : Complement

def LiuYip2026.instDecidableEqComplement.decEq (x✝ x✝¹ : Complement) : Decidable (x✝ = x✝¹)

Equations

• LiuYip2026.instDecidableEqComplement.decEq LiuYip2026.Complement.vP LiuYip2026.Complement.vP = isTrue ⋯
• LiuYip2026.instDecidableEqComplement.decEq LiuYip2026.Complement.vP (LiuYip2026.Complement.tP d) = isFalse ⋯
• LiuYip2026.instDecidableEqComplement.decEq LiuYip2026.Complement.vP LiuYip2026.Complement.cP = isFalse LiuYip2026.instDecidableEqComplement.decEq._proof_4
• LiuYip2026.instDecidableEqComplement.decEq (LiuYip2026.Complement.tP d) LiuYip2026.Complement.vP = isFalse ⋯
• LiuYip2026.instDecidableEqComplement.decEq (LiuYip2026.Complement.tP a) (LiuYip2026.Complement.tP b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• LiuYip2026.instDecidableEqComplement.decEq (LiuYip2026.Complement.tP d) LiuYip2026.Complement.cP = isFalse ⋯
• LiuYip2026.instDecidableEqComplement.decEq LiuYip2026.Complement.cP LiuYip2026.Complement.vP = isFalse LiuYip2026.instDecidableEqComplement.decEq._proof_8
• LiuYip2026.instDecidableEqComplement.decEq LiuYip2026.Complement.cP (LiuYip2026.Complement.tP d) = isFalse ⋯
• LiuYip2026.instDecidableEqComplement.decEq LiuYip2026.Complement.cP LiuYip2026.Complement.cP = isTrue ⋯

@[instance_reducible]

instance LiuYip2026.instDecidableEqComplement : DecidableEq Complement

Equations

• LiuYip2026.instDecidableEqComplement = LiuYip2026.instDecidableEqComplement.decEq

def LiuYip2026.instReprComplement.repr : Complement → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• LiuYip2026.instReprComplement.repr LiuYip2026.Complement.vP prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LiuYip2026.Complement.vP")).group prec✝
• LiuYip2026.instReprComplement.repr LiuYip2026.Complement.cP prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LiuYip2026.Complement.cP")).group prec✝

@[instance_reducible]

instance LiuYip2026.instReprComplement : Repr Complement

Equations

• LiuYip2026.instReprComplement = { reprPrec := LiuYip2026.instReprComplement.repr }

def LiuYip2026.Complement.size : Complement → Minimalist.ComplementSize

The size of a complement.

Equations

• LiuYip2026.Complement.vP.size = Minimalist.ComplementSize.vP
• (LiuYip2026.Complement.tP d).size = Minimalist.ComplementSize.tP
• LiuYip2026.Complement.cP.size = Minimalist.ComplementSize.cP

def LiuYip2026.Complement.LicensesDynamic (c : Complement) : Prop

A complement licenses a [u+D] element when it has an outer aspect head bearing [+D], as a dynamic TP does, and a CP, whose outer aspect head may be dynamic.

Equations

• c.LicensesDynamic = (c = LiuYip2026.Complement.tP Aspect.Dynamicity.dynamic ∨ c = LiuYip2026.Complement.cP)

@[instance_reducible]

instance LiuYip2026.instDecidablePredComplementLicensesDynamic : DecidablePred Complement.LicensesDynamic

Equations

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

theorem LiuYip2026.not_exceptionalScope_of_licensesDynamic {c : Complement} (h : c.LicensesDynamic) : ¬ExceptionalScope AspProjection.outer c.size

A complement that licenses you contains outer aspect, so nothing outer-associated takes exceptional scope across it: an embedded you blocks aspect lowering.

inductive LiuYip2026.Pred : Type

The three Mandarin predicates of the selectional table.

• xiang : Pred
• rang : Pred
• xiangxin : Pred

@[instance_reducible]

instance LiuYip2026.instDecidableEqPred : DecidableEq Pred

Equations

• LiuYip2026.instDecidableEqPred x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance LiuYip2026.instReprPred : Repr Pred

Equations

• LiuYip2026.instReprPred = { reprPrec := LiuYip2026.instReprPred.repr }

def LiuYip2026.instReprPred.repr : Pred → ℕ → Std.Format

Equations

• LiuYip2026.instReprPred.repr LiuYip2026.Pred.xiang prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LiuYip2026.Pred.xiang")).group prec✝
• LiuYip2026.instReprPred.repr LiuYip2026.Pred.rang prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LiuYip2026.Pred.rang")).group prec✝
• LiuYip2026.instReprPred.repr LiuYip2026.Pred.xiangxin prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LiuYip2026.Pred.xiangxin")).group prec✝

def LiuYip2026.Pred.entry : Pred → Mandarin.Verb

The lexical entry of a predicate.

Equations

• LiuYip2026.Pred.xiang.entry = Mandarin.xiang
• LiuYip2026.Pred.rang.entry = Mandarin.rang
• LiuYip2026.Pred.xiangxin.entry = Mandarin.xiangxin

def LiuYip2026.Pred.selects : Pred → List Complement

The complements each predicate selects. Xiang 'want' selects a vP or a stative TP, rang 'let' a vP or a TP of either dynamicity, and xiangxin 'believe' a CP.

Equations

• LiuYip2026.Pred.xiang.selects = [LiuYip2026.Complement.vP, LiuYip2026.Complement.tP Aspect.Dynamicity.stative]
• LiuYip2026.Pred.rang.selects = [LiuYip2026.Complement.vP, LiuYip2026.Complement.tP Aspect.Dynamicity.stative, LiuYip2026.Complement.tP Aspect.Dynamicity.dynamic]
• LiuYip2026.Pred.xiangxin.selects = [LiuYip2026.Complement.cP]

def LiuYip2026.Pred.EmbedsYou (p : Pred) : Prop

You can surface in a complement of the predicate iff the predicate selects a complement licensing [u+D].

Equations

• p.EmbedsYou = ∃ c ∈ p.selects, c.LicensesDynamic

@[instance_reducible]

instance LiuYip2026.instDecidablePredPredEmbedsYou : DecidablePred Pred.EmbedsYou

Equations

• LiuYip2026.instDecidablePredPredEmbedsYou x✝ = LiuYip2026.instDecidablePredPredEmbedsYou._aux_1 x✝

def LiuYip2026.Pred.SkipsYou (p : Pred) : Prop

You skips the predicate iff the predicate selects a vP.

Equations

• p.SkipsYou = ∃ c ∈ p.selects, LiuYip2026.ExceptionalScope LiuYip2026.AspProjection.outer c.size

@[instance_reducible]

instance LiuYip2026.instDecidablePredPredSkipsYou : DecidablePred Pred.SkipsYou

Equations

• LiuYip2026.instDecidablePredPredSkipsYou x✝ = LiuYip2026.instDecidablePredPredSkipsYou._aux_1 x✝

theorem LiuYip2026.embedsYou : (¬Pred.xiang.EmbedsYou ∧ Pred.xiang.SkipsYou) ∧ (Pred.rang.EmbedsYou ∧ Pred.rang.SkipsYou) ∧ Pred.xiangxin.EmbedsYou ∧ ¬Pred.xiangxin.SkipsYou

In the selectional table want embeds no you but is skipped, let does both, and believe embeds you and is not skipped.

inductive LiuYip2026.CPred : Type

The Cantonese predicates and the size of the complement each selects. The nonfinite clause-taking soeng 'want', hyun 'urge', bik 'force', giu 'ask' and daasyun 'intend' select a vP, and the finite clause-taking seon 'believe', gong 'say' and geidak 'remember' a CP.

• soeng : CPred
• hyun : CPred
• bik : CPred
• giu : CPred
• daasyun : CPred
• seon : CPred
• gong : CPred
• geidak : CPred

@[instance_reducible]

instance LiuYip2026.instDecidableEqCPred : DecidableEq CPred

Equations

• LiuYip2026.instDecidableEqCPred x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def LiuYip2026.instReprCPred.repr : CPred → ℕ → Std.Format

Equations

• LiuYip2026.instReprCPred.repr LiuYip2026.CPred.soeng prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LiuYip2026.CPred.soeng")).group prec✝
• LiuYip2026.instReprCPred.repr LiuYip2026.CPred.hyun prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LiuYip2026.CPred.hyun")).group prec✝
• LiuYip2026.instReprCPred.repr LiuYip2026.CPred.bik prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LiuYip2026.CPred.bik")).group prec✝
• LiuYip2026.instReprCPred.repr LiuYip2026.CPred.giu prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LiuYip2026.CPred.giu")).group prec✝
• LiuYip2026.instReprCPred.repr LiuYip2026.CPred.daasyun prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LiuYip2026.CPred.daasyun")).group prec✝
• LiuYip2026.instReprCPred.repr LiuYip2026.CPred.seon prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LiuYip2026.CPred.seon")).group prec✝
• LiuYip2026.instReprCPred.repr LiuYip2026.CPred.gong prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LiuYip2026.CPred.gong")).group prec✝
• LiuYip2026.instReprCPred.repr LiuYip2026.CPred.geidak prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LiuYip2026.CPred.geidak")).group prec✝

@[instance_reducible]

instance LiuYip2026.instReprCPred : Repr CPred

Equations

• LiuYip2026.instReprCPred = { reprPrec := LiuYip2026.instReprCPred.repr }

def LiuYip2026.CPred.entry : CPred → Cantonese.Verbs.Verb

The lexical entry of a predicate.

Equations

• LiuYip2026.CPred.soeng.entry = Cantonese.Verbs.soeng
• LiuYip2026.CPred.hyun.entry = Cantonese.Verbs.hyun
• LiuYip2026.CPred.bik.entry = Cantonese.Verbs.bik
• LiuYip2026.CPred.giu.entry = Cantonese.Verbs.giu
• LiuYip2026.CPred.daasyun.entry = Cantonese.Verbs.daasyun
• LiuYip2026.CPred.seon.entry = Cantonese.Verbs.seon
• LiuYip2026.CPred.gong.entry = Cantonese.Verbs.gong
• LiuYip2026.CPred.geidak.entry = Cantonese.Verbs.geidak

def LiuYip2026.CPred.size : CPred → Minimalist.ComplementSize

The size of the complement each predicate selects.

Equations

• LiuYip2026.CPred.soeng.size = Minimalist.ComplementSize.vP
• LiuYip2026.CPred.hyun.size = Minimalist.ComplementSize.vP
• LiuYip2026.CPred.bik.size = Minimalist.ComplementSize.vP
• LiuYip2026.CPred.giu.size = Minimalist.ComplementSize.vP
• LiuYip2026.CPred.daasyun.size = Minimalist.ComplementSize.vP
• LiuYip2026.CPred.seon.size = Minimalist.ComplementSize.cP
• LiuYip2026.CPred.gong.size = Minimalist.ComplementSize.cP
• LiuYip2026.CPred.geidak.size = Minimalist.ComplementSize.cP

theorem LiuYip2026.CPred.size_eq_cP_iff (p : CPred) : p.size = Minimalist.ComplementSize.cP ↔ ∃ fr ∈ p.entry.valency.frames.head?, fr.HasFinite

The sizes agree with the fragment's frames, in that a predicate selects a CP iff its basic frame is a finite clause.

theorem LiuYip2026.Pred.selects_cP_iff (p : Pred) : Complement.cP ∈ p.selects ↔ ∃ fr ∈ p.entry.valency.frames.head?, fr.HasFinite

Among the Mandarin predicates xiangxin alone selects a CP.

theorem LiuYip2026.faan_lowering : ExceptionalScope AspProjection.outer CPred.soeng.size ∧ ¬ExceptionalScope AspProjection.outer CPred.seon.size

-Faan lowers across the complement of soeng 'want' and not across that of seon 'believe'.

The implicational complementation hierarchy

inductive LiuYip2026.ComplementClass : Type

The semantic complement classes of the hierarchy, event, situation and proposition, and the minimal size each maps to.

• event : ComplementClass
• situation : ComplementClass
• proposition : ComplementClass

@[instance_reducible]

instance LiuYip2026.instDecidableEqComplementClass : DecidableEq ComplementClass

Equations

• LiuYip2026.instDecidableEqComplementClass x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance LiuYip2026.instReprComplementClass : Repr ComplementClass

Equations

• LiuYip2026.instReprComplementClass = { reprPrec := LiuYip2026.instReprComplementClass.repr }

def LiuYip2026.instReprComplementClass.repr : ComplementClass → ℕ → Std.Format

Equations

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

def LiuYip2026.ComplementClass.size : ComplementClass → Minimalist.ComplementSize

The minimal sizes of the three classes are vP, TP and CP.

Equations

• LiuYip2026.ComplementClass.event.size = Minimalist.ComplementSize.vP
• LiuYip2026.ComplementClass.situation.size = Minimalist.ComplementSize.tP
• LiuYip2026.ComplementClass.proposition.size = Minimalist.ComplementSize.cP

theorem LiuYip2026.ComplementClass.exceptionalScope_of_le {f : AspProjection} {c c' : ComplementClass} (h : c.size ≤ c'.size) (hs : ExceptionalScope f c'.size) : ExceptionalScope f c.size

A dependency transparent for a class is transparent for every more integrated class.