Angelopoulos 2026: On clausal complementation, once more

[Ang26]

Greek oti- and pu-clauses present three puzzles (§1): near- complementary distribution after verbs (oti with saying/belief, pu with emotive factives, ex. 1); freedom as internal arguments and derived subjects but a ban from external-argument position (§2.2); and a novel stativity restriction on complement pu-clauses (§2.3).

The analysis reverses selection (§3.1): oti and pu bear an uninterpretable [n]-feature checked by a light noun merged in their specifier (partly adopting Arsenijević 2009; the paper is neutral on the categorial status of oti and pu, fn. 3). The noun must incorporate into a lexical verbal head — possible from complement position, impossible from Spec,vP (nearest head T) or under P — which derives the argument asymmetry and the P-ban (§3.1 ex. 27–32). The oti ~ pu distribution follows from the content/situation dichotomy (§3.2, adopting [Bon22]); the stativity restriction from aspectual-head selection (§4.1: vState selects both otiP and puP, vEvent only otiP). §7.1 extends the adjunct-selection account to Uyghur dep (= de 'say' + converb -ip, per Major 2024) — the structural parallel of Buryat gɘ-žɘ.

§7.3 departs from [Bon22]'s transparent syntax–semantics mapping: bare oti-clauses are merged in COMPLEMENT position (the §2 argumenthood diagnostics: clitic doubling, passivization, derived subjects) while composing via Predicate Modification (the explanans reading, [Ell20a]) — the same syntactic position yields either composition mode.

Main declarations

• bearsN — the §3.1 [n]-feature datum over the fragment entries
• NounHost, ClausePosition, licensedIn — the incorporation mechanism and the derived argument-position asymmetry
• selectsClause, pu_requires_stative — the §4.1 stativity locus
• clauseSort — oti = content, pu = situation, consuming Bondarenko2022.NominalSort (§3.2 ex. 33–34)
• bareOtiAttested, transparency_conflates_axes — the §7.3 counterclaim against Bondarenko2022.transparentSSMapping

Typed paradigm sentences (ex. 1, 31–34) live in Angelopoulos2026.Examples, generated from Data/Examples/Angelopoulos2026.json.

Reversed selection: the [n]-feature (§3.1)

def Angelopoulos2026.bearsN (c : Complementizer) : Prop

oti and pu bear an uninterpretable [n]-feature checked by a light noun merged in their specifier (§3.1); na does not (its licensing is mood-driven). Paper-specific datum projected over the fragment entries; the paper is neutral on the category of oti and pu (fn. 3).

Equations

• Angelopoulos2026.bearsN c = (c = Greek.StandardModern.Complementizers.oti ∨ c = Greek.StandardModern.Complementizers.pu)

@[implicit_reducible]

instance Angelopoulos2026.instDecidablePredComplementizerBearsN : DecidablePred bearsN

Equations

• Angelopoulos2026.instDecidablePredComplementizerBearsN c = id inferInstance

Incorporation licensing and the argument asymmetry (§3.1)

inductive Angelopoulos2026.NounHost : Type

Heads adjacent to a clause's light noun. Only a lexical verbal head licenses noun incorporation ([HK93]); functional T and P do not (§3.1 ex. 29–32).

• vLex : NounHost
• t : NounHost
• p : NounHost

@[implicit_reducible]

instance Angelopoulos2026.instDecidableEqNounHost : DecidableEq NounHost

Equations

• Angelopoulos2026.instDecidableEqNounHost x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Angelopoulos2026.instFintypeNounHost : Fintype NounHost

Equations

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

def Angelopoulos2026.instReprNounHost.repr : NounHost → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Angelopoulos2026.instReprNounHost : Repr NounHost

Equations

• Angelopoulos2026.instReprNounHost = { reprPrec := Angelopoulos2026.instReprNounHost.repr }

def Angelopoulos2026.NounHost.licenses : NounHost → Prop

Whether a host licenses light-noun incorporation.

Equations

• Angelopoulos2026.NounHost.vLex.licenses = True
• Angelopoulos2026.NounHost.t.licenses = False
• Angelopoulos2026.NounHost.p.licenses = False

inductive Angelopoulos2026.ClausePosition : Type

Positions a bare oti/pu-clause can occupy, each with the nearest potential incorporation host: internal arguments sit under an aspectual v; incorporation precedes movement for derived subjects; the nearest head above Spec,vP is T; P cannot host (§3.1 ex. 27–32).

• internalArgument : ClausePosition
• derivedSubject : ClausePosition
• externalArgument : ClausePosition
• pComplement : ClausePosition

@[implicit_reducible]

instance Angelopoulos2026.instDecidableEqClausePosition : DecidableEq ClausePosition

Equations

• Angelopoulos2026.instDecidableEqClausePosition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Angelopoulos2026.instFintypeClausePosition : Fintype ClausePosition

Equations

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

@[implicit_reducible]

instance Angelopoulos2026.instReprClausePosition : Repr ClausePosition

Equations

• Angelopoulos2026.instReprClausePosition = { reprPrec := Angelopoulos2026.instReprClausePosition.repr }

def Angelopoulos2026.instReprClausePosition.repr : ClausePosition → ℕ → Std.Format

Equations

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

def Angelopoulos2026.ClausePosition.nearestHost : ClausePosition → NounHost

The nearest potential incorporation host from each position.

Equations

• Angelopoulos2026.ClausePosition.internalArgument.nearestHost = Angelopoulos2026.NounHost.vLex
• Angelopoulos2026.ClausePosition.derivedSubject.nearestHost = Angelopoulos2026.NounHost.vLex
• Angelopoulos2026.ClausePosition.externalArgument.nearestHost = Angelopoulos2026.NounHost.t
• Angelopoulos2026.ClausePosition.pComplement.nearestHost = Angelopoulos2026.NounHost.p

def Angelopoulos2026.licensedIn (pos : ClausePosition) : Prop

A bare oti/pu-clause is licensed in a position iff the nearest host licenses light-noun incorporation — the paper's derivation of the distribution, not a stipulated table.

Equations

• Angelopoulos2026.licensedIn pos = pos.nearestHost.licenses

theorem Angelopoulos2026.internal_and_derived_subject_licensed : licensedIn ClausePosition.internalArgument ∧ licensedIn ClausePosition.derivedSubject

Internal arguments and derived subjects are licensed (§2.1–2.2).

theorem Angelopoulos2026.external_argument_banned : ¬licensedIn ClausePosition.externalArgument

The external-argument ban (§2.2): T cannot host incorporation.

theorem Angelopoulos2026.p_complement_banned : ¬licensedIn ClausePosition.pComplement

Bare clauses are excluded after P (ex. 31c, 32c).

The stativity locus (§4.1)

inductive Angelopoulos2026.AspectualHead : Type

Aspectual heads introducing internal arguments (§4.1, following Borer and Merchant as cited there).

• vState : AspectualHead
• vEvent : AspectualHead

@[implicit_reducible]

instance Angelopoulos2026.instDecidableEqAspectualHead : DecidableEq AspectualHead

Equations

• Angelopoulos2026.instDecidableEqAspectualHead x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Angelopoulos2026.instFintypeAspectualHead : Fintype AspectualHead

Equations

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

@[implicit_reducible]

instance Angelopoulos2026.instReprAspectualHead : Repr AspectualHead

Equations

• Angelopoulos2026.instReprAspectualHead = { reprPrec := Angelopoulos2026.instReprAspectualHead.repr }

def Angelopoulos2026.instReprAspectualHead.repr : AspectualHead → ℕ → Std.Format

Equations

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

def Angelopoulos2026.selectsClause : AspectualHead → Complementizer → Prop

§4.1: vState selects both otiP and puP as its complement; vEvent selects only otiP.

Equations

• Angelopoulos2026.selectsClause Angelopoulos2026.AspectualHead.vState x✝ = (x✝ = Greek.StandardModern.Complementizers.oti ∨ x✝ = Greek.StandardModern.Complementizers.pu)
• Angelopoulos2026.selectsClause Angelopoulos2026.AspectualHead.vEvent x✝ = (x✝ = Greek.StandardModern.Complementizers.oti)

theorem Angelopoulos2026.pu_requires_stative (h : AspectualHead) (hp : selectsClause h Greek.StandardModern.Complementizers.pu) : h = AspectualHead.vState

The stativity restriction (§2.3), derived: a pu-complement forces the stative aspectual head.

theorem Angelopoulos2026.pu_only_verbs_stative (v : Verb) : v ∈ [Greek.StandardModern.Complementizers.metaniono, Greek.StandardModern.Complementizers.areso, Greek.StandardModern.Complementizers.xerome] → v.vendlerClass = some Features.VendlerClass.state

The verb-level reflex over the fragment sample: the pu-only matrix verbs (ex. 1b, 13–14, 20) are all stative.

Content vs situation (§3.2)

def Angelopoulos2026.clauseSort (c : Complementizer) : Option Bondarenko2022.NominalSort

The sort of clause each complementizer introduces — oti content, pu situation — which must match the incorporating noun's sort (§3.2). The sorts and their diagnostics ('true'/'mistaken' vs 'happen', ex. 33–34) are [Bon22]'s (Bondarenko2022.NominalSort, §2.2.3); na is outside the dichotomy.

Equations

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

theorem Angelopoulos2026.clauseSort_matches_diagnostics : clauseSort Greek.StandardModern.Complementizers.oti = some Bondarenko2022.NominalSort.content ∧ Bondarenko2022.NominalSort.content.truthEvaluable ∧ clauseSort Greek.StandardModern.Complementizers.pu = some Bondarenko2022.NominalSort.situation ∧ Bondarenko2022.NominalSort.situation.occurrenceCompatible

The assigned sorts pass the §3.2 diagnostics: oti's sort is truth-evaluable, pu's occurrence-compatible (ex. 33–34, matching [Bon22] §2.2.3).

Against the transparent syntax–semantics mapping (§7.3)

inductive Angelopoulos2026.SynPosition : Type

Syntactic position of an embedded clause — one of the two axes [Bon22]'s ClauseStructurePath conflates.

• complement : SynPosition
• adjunct : SynPosition

@[implicit_reducible]

instance Angelopoulos2026.instDecidableEqSynPosition : DecidableEq SynPosition

Equations

• Angelopoulos2026.instDecidableEqSynPosition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Angelopoulos2026.instReprSynPosition.repr : SynPosition → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Angelopoulos2026.instReprSynPosition : Repr SynPosition

Equations

• Angelopoulos2026.instReprSynPosition = { reprPrec := Angelopoulos2026.instReprSynPosition.repr }

inductive Angelopoulos2026.CompMode : Type

Composition mode — the other axis.

• pm : CompMode
• fa : CompMode

@[implicit_reducible]

instance Angelopoulos2026.instDecidableEqCompMode : DecidableEq CompMode

Equations

• Angelopoulos2026.instDecidableEqCompMode x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Angelopoulos2026.instReprCompMode : Repr CompMode

Equations

• Angelopoulos2026.instReprCompMode = { reprPrec := Angelopoulos2026.instReprCompMode.repr }

def Angelopoulos2026.instReprCompMode.repr : CompMode → ℕ → Std.Format

Equations

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

def Angelopoulos2026.bareOtiAttested : SynPosition → CompMode → Prop

The paper's claim for bare oti-clauses (§2 diagnostics + §7.3): complement position composing via PM is attested (the explanans reading); FA requires the nominalizing D (§7.3 ex. 57), so bare clauses never compose via FA from either position.

Equations

• Angelopoulos2026.bareOtiAttested Angelopoulos2026.SynPosition.complement Angelopoulos2026.CompMode.pm = True
• Angelopoulos2026.bareOtiAttested Angelopoulos2026.SynPosition.complement Angelopoulos2026.CompMode.fa = False
• Angelopoulos2026.bareOtiAttested Angelopoulos2026.SynPosition.adjunct Angelopoulos2026.CompMode.pm = True
• Angelopoulos2026.bareOtiAttested Angelopoulos2026.SynPosition.adjunct Angelopoulos2026.CompMode.fa = False

def Angelopoulos2026.transparentBare : SynPosition → CompMode → Prop

[Bon22]'s transparent mapping restated on the split axes: a bare clause composing via PM must be a syntactic adjunct (the composition path is reflected in syntax).

Equations

• Angelopoulos2026.transparentBare Angelopoulos2026.SynPosition.adjunct Angelopoulos2026.CompMode.pm = True
• Angelopoulos2026.transparentBare x✝¹ x✝ = False

theorem Angelopoulos2026.diverges_from_transparent_mapping : bareOtiAttested SynPosition.complement CompMode.pm ∧ ¬transparentBare SynPosition.complement CompMode.pm

The §7.3 divergence: bare oti-clauses occupy complement position while composing via PM — attested here, excluded by the transparent mapping. Conditional on the paper's premises: the clauses are BARE (no covert nominal shell — the analysis rejects Arsenijević's DP layer and Faure's case-less-DP treatment, §3.1) and are internal ARGUMENTS (clitic doubling, passivization, derived subjects, §2.1–2.2). [Bon22] can deny either premise.

theorem Angelopoulos2026.transparency_conflates_axes : ¬Bondarenko2022.transparentSSMapping Bondarenko2022.ClauseStructurePath.bareArgument ∧ bareOtiAttested SynPosition.complement CompMode.pm

Against Bondarenko2022.transparentSSMapping directly: Bondarenko predicts the (bare, argument) cell empty (Bondarenko2022.bare_argument_predicted_impossible), identifying argument position with the FA path; Greek realizes syntactic argumenthood for bare clauses WITHOUT FA — the identification of the two axes is what fails.