Documentation

Linglib.Studies.Angelopoulos2026

Angelopoulos 2026: On clausal complementation, once more #

[Ang26] derives the distribution of Greek oti- and pu-clauses — near-complementary after verbs (ex. 1), free as internal arguments and derived subjects yet banned as external arguments (§2.2), stativity-restricted as pu-complements (§2.3) — from reversed selection: oti and pu bear an uninterpretable [n]-feature checked by a light noun in their specifier (partly adopting [Ars09]) that must incorporate into a lexical verbal head, licit only from complement position (§3.1). The oti ~ pu split follows from the content/situation dichotomy (§3.2, adopting [Bon22]) with pu's factivity derived from situation-anchoring, the stativity restriction from aspectual-head selection (§4.1), and §7.3 turns the §2 argumenthood diagnostics against Bondarenko's transparent syntax–semantics mapping: bare oti-clauses sit in complement position while composing via Predicate Modification (the explanans reading, [Ell20a]). Typed paradigm sentences (ex. 1, 31–34) live in Angelopoulos2026.Examples.

Reversed selection: the light noun (§3.1) #

def Angelopoulos2026.nProbe :

Minimalist.GramFeature

The uninterpretable [n]-feature oti and pu bear, checked by merging a light noun in their specifier (§3.1: selection as feature checking).

Equations

Angelopoulos2026.nProbe = Minimalist.GramFeature.unvalued (Minimalist.FeatureVal.catN true)

Instances For

def Angelopoulos2026.nGoal :

Minimalist.GramFeature

The light noun's [n]-feature, interpretable and valued on a nominal.

Equations

Angelopoulos2026.nGoal = Minimalist.GramFeature.valued (Minimalist.FeatureVal.catN true)

Instances For

def Angelopoulos2026.nProbes (c : Complementizer) :

List Minimalist.GramFeature

The §3.1 lexical assignment: oti and pu carry the [n]-feature, an and na none.

Equations

Angelopoulos2026.nProbes c = if c = Greek.StandardModern.Complementizers.oti ∨ c = Greek.StandardModern.Complementizers.pu then [Angelopoulos2026.nProbe] else []

Instances For

def Angelopoulos2026.selectsLightNoun (c : Complementizer) :

oti and pu select a light noun in their specifier: their feature bundle carries the [n]-feature (§3.1).

Equations

Angelopoulos2026.selectsLightNoun c = (Angelopoulos2026.nProbe ∈ Angelopoulos2026.nProbes c)

Instances For

@[instance_reducible]

instance Angelopoulos2026.instDecidablePredComplementizerSelectsLightNoun :

DecidablePred selectsLightNoun

Equations

Angelopoulos2026.instDecidablePredComplementizerSelectsLightNoun x✝ = Angelopoulos2026.instDecidablePredComplementizerSelectsLightNoun._aux_1 x✝

theorem Angelopoulos2026.lightNoun_checks_nProbe :

Minimalist.featuresMatch nProbe nGoal = true ∧ nGoal.isValued = true ∧ nProbe.isUnvalued = true

The merged noun's valued [n] checks the complementizer's under specifier–head matching.

The attested selection classes (§1–§2.3) #

def Angelopoulos2026.otiOnlyVerbs :

List Verb

Matrix verbs attested with oti only: saying, belief, knowledge (ex. 1a, 3–4, 21).

Equations

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

Instances For

def Angelopoulos2026.puOnlyVerbs :

List Verb

Matrix verbs attested with pu only: the emotive factives (ex. 1b, 13–14, 20).

Equations

Angelopoulos2026.puOnlyVerbs = [Greek.StandardModern.Complementizers.metaniono, Greek.StandardModern.Complementizers.areso, Greek.StandardModern.Complementizers.xerome]

Instances For

def Angelopoulos2026.dualVerbs :

List (Verb × Verb)

Verbs attested with both, as (eventive oti-sense, stative pu-sense) pairs (ex. 19, 22–23).

Equations

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

Instances For

theorem Angelopoulos2026.frames_underdetermine_distribution (v : Verb) :

v ∈ otiOnlyVerbs ++ puOnlyVerbs → v.takes Greek.StandardModern.Complementizers.oti ∧ v.takes Greek.StandardModern.Complementizers.pu ∧ ¬v.takes Greek.StandardModern.Complementizers.na

Every sample verb's frames admit both oti and pu and already exclude na: coding and force underdetermine the split (§1).

theorem Angelopoulos2026.factivity_anti_aligned :

Greek.StandardModern.Complementizers.oti.factive = none ∧ Greek.StandardModern.Complementizers.pu.factive = some true ∧ List.filter (fun (x : Verb) => x.factivePresup) otiOnlyVerbs = [Greek.StandardModern.Complementizers.ksero, Greek.StandardModern.Complementizers.katalaveno, Greek.StandardModern.Complementizers.sinidhitopio] ∧ List.filter (fun (x : Verb) => x.factivePresup) puOnlyVerbs = []

Verb-level and C-level factivity are anti-aligned: the oti-selectors that presuppose their complement are exactly the knowledge verbs, no pu-only emotive factive presupposes, and only pu is lexically factive.

Incorporation licensing and the argument asymmetry (§3.1) #

inductive Angelopoulos2026.NounHost :

Heads adjacent to a clause's light noun: a lexical verbal head, T, or P (§3.1).

vLex : NounHost
t : NounHost
p : NounHost

Instances For

@[instance_reducible]

instance Angelopoulos2026.instDecidableEqNounHost :

DecidableEq NounHost

Equations

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

def Angelopoulos2026.instReprNounHost.repr :

NounHost → ℕ → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance Angelopoulos2026.instReprNounHost :

Equations

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

def Angelopoulos2026.NounHost.licenses :

NounHost → Prop

Only the lexical verbal head licenses light-noun incorporation ([HK93]); functional T and P do not.

Equations

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

Instances For

@[instance_reducible]

instance Angelopoulos2026.instDecidablePredNounHostLicenses :

DecidablePred NounHost.licenses

Equations

inductive Angelopoulos2026.ClausePosition :

Positions a bare oti/pu-clause can occupy (§3.1 ex. 27–32).

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

Instances For

@[instance_reducible]

instance Angelopoulos2026.instDecidableEqClausePosition :

DecidableEq ClausePosition

Equations

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

def Angelopoulos2026.instReprClausePosition.repr :

ClausePosition → ℕ → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance Angelopoulos2026.instReprClausePosition :

Repr ClausePosition

Equations

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

def Angelopoulos2026.ClausePosition.nearestHost :

ClausePosition → NounHost

The nearest potential incorporation host from each position.

Equations

Instances For

def Angelopoulos2026.licensedIn (pos : ClausePosition) :

A bare oti/pu-clause is licensed in a position iff its nearest host licenses light-noun incorporation (§3.1).

Equations

Angelopoulos2026.licensedIn pos = pos.nearestHost.licenses

Instances For

@[instance_reducible]

instance Angelopoulos2026.instDecidablePredClausePositionLicensedIn :

DecidablePred licensedIn

Equations

Angelopoulos2026.instDecidablePredClausePositionLicensedIn pos = Angelopoulos2026.instDecidablePredClausePositionLicensedIn._aux_1 pos

theorem Angelopoulos2026.internal_and_derived_subject_licensed :

licensedIn ClausePosition.internalArgument ∧ licensedIn ClausePosition.derivedSubject

Bare clauses are licensed as internal arguments and derived subjects (§2.1–2.2).

theorem Angelopoulos2026.external_argument_banned :

¬licensedIn ClausePosition.externalArgument

Bare clauses are banned from external-argument position: T cannot host incorporation (§2.2).

theorem Angelopoulos2026.p_complement_banned :

¬licensedIn ClausePosition.pComplement

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

theorem Angelopoulos2026.licensing_matches_judgments (p : ClausePosition × Data.Examples.LinguisticExample) :

p ∈ [(ClausePosition.internalArgument, Examples.ex_31b), (ClausePosition.internalArgument, Examples.ex_32b), (ClausePosition.pComplement, Examples.ex_31c), (ClausePosition.pComplement, Examples.ex_32c)] → (licensedIn p.1 ↔ p.2.judgment ≠ Features.Judgment.ungrammatical)

The licensing predictions match the ex. 31–32 judgments: acceptable as internal arguments, ungrammatical after P.

The stativity locus (§4.1) #

inductive Angelopoulos2026.AspectualHead :

Aspectual heads introducing internal arguments (§4.1).

vState : AspectualHead
vEvent : AspectualHead

Instances For

@[instance_reducible]

instance Angelopoulos2026.instDecidableEqAspectualHead :

DecidableEq AspectualHead

Equations

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

@[instance_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.

Instances For

def Angelopoulos2026.AspectualHead.ofVendler (vc : Features.VendlerClass) :

The aspectual head determined by a verb's Vendler class: vState for stative classes, vEvent for dynamic ones (§4.1).

Equations

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

Instances For

def Angelopoulos2026.selectsClause :

AspectualHead → Complementizer → Prop

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

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)

Instances For

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

h = AspectualHead.vState

A pu-complement forces the stative aspectual head (§2.3).

theorem Angelopoulos2026.pu_complement_verb_stative (vc : Features.VendlerClass) (hp : selectsClause (AspectualHead.ofVendler vc) Greek.StandardModern.Complementizers.pu) :

vc = Features.VendlerClass.state

A verb whose aspectual head licenses a pu-complement is Vendler-stative (§2.3).

theorem Angelopoulos2026.pu_only_verbs_stative (v : Verb) :

v ∈ puOnlyVerbs → Option.map AspectualHead.ofVendler v.vendlerClass = some AspectualHead.vState

Every pu-only matrix verb's aspectual head is vState.

theorem Angelopoulos2026.dual_verbs_stative_with_pu (p : Verb × Verb) :

p ∈ dualVerbs → Option.map AspectualHead.ofVendler p.2.vendlerClass = some AspectualHead.vState ∧ Option.map AspectualHead.ofVendler p.1.vendlerClass = some AspectualHead.vEvent

Each dual verb's pu-sense takes vState and its oti-sense vEvent (ex. 19, 22–23).

Content vs situation (§3.2) #

def Angelopoulos2026.clauseSort (c : Complementizer) :

Option Bondarenko2022.NominalSort

The sort of clause each complementizer introduces — oti content, pu situation, na neither — which must match the incorporating noun's sort (§3.2).

Equations

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

Instances For

def Angelopoulos2026.mergeableInSpec (n : Bondarenko2022.NominalSort) (c : Complementizer) :

A light noun of sort n can merge in the complementizer's specifier iff its sort is the clause's sort (§3.2).

Equations

Angelopoulos2026.mergeableInSpec n c = (Angelopoulos2026.clauseSort c = some n)

Instances For

@[instance_reducible]

instance Angelopoulos2026.instDecidableMergeableInSpec (n : Bondarenko2022.NominalSort) (c : Complementizer) :

Decidable (mergeableInSpec n c)

Equations

Angelopoulos2026.instDecidableMergeableInSpec n c = Angelopoulos2026.instDecidableMergeableInSpec._aux_1 n c

theorem Angelopoulos2026.spec_noun_sorted :

mergeableInSpec Bondarenko2022.NominalSort.content Greek.StandardModern.Complementizers.oti ∧ ¬mergeableInSpec Bondarenko2022.NominalSort.situation Greek.StandardModern.Complementizers.oti ∧ mergeableInSpec Bondarenko2022.NominalSort.situation Greek.StandardModern.Complementizers.pu ∧ ¬mergeableInSpec Bondarenko2022.NominalSort.content Greek.StandardModern.Complementizers.pu

Only the content noun merges in Spec,otiP and only the situation noun in Spec,puP (§3.2).

def Angelopoulos2026.nounSort (v : Verb) :

Option Bondarenko2022.NominalSort

The sort of the light noun a verb verbalizes under incorporation: stative senses, stative preferential attitudes, and occurrence verbs relate to situations; saying, belief, and knowledge to content (§3.2).

Equations

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

Instances For

def Angelopoulos2026.verbalizes (v : Verb) (n : Bondarenko2022.NominalSort) :

A verb verbalizes the light noun of sort n (§3.1–§3.2).

Equations

Angelopoulos2026.verbalizes v n = (Angelopoulos2026.nounSort v = some n)

Instances For

@[instance_reducible]

instance Angelopoulos2026.instDecidableVerbalizes (v : Verb) (n : Bondarenko2022.NominalSort) :

Decidable (verbalizes v n)

Equations

Angelopoulos2026.instDecidableVerbalizes v n = Angelopoulos2026.instDecidableVerbalizes._aux_1 v n

theorem Angelopoulos2026.distribution_via_light_noun :

(∀ v ∈ otiOnlyVerbs, ∃ (n : Bondarenko2022.NominalSort), verbalizes v n ∧ mergeableInSpec n Greek.StandardModern.Complementizers.oti) ∧ (∀ v ∈ puOnlyVerbs, ∃ (n : Bondarenko2022.NominalSort), verbalizes v n ∧ mergeableInSpec n Greek.StandardModern.Complementizers.pu) ∧ ∀ p ∈ dualVerbs, (∃ (n : Bondarenko2022.NominalSort), verbalizes p.1 n ∧ mergeableInSpec n Greek.StandardModern.Complementizers.oti) ∧ ∃ (n : Bondarenko2022.NominalSort), verbalizes p.2 n ∧ mergeableInSpec n Greek.StandardModern.Complementizers.pu

The near-complementary distribution through the light noun: each attested pairing has a noun the verb verbalizes that merges in the complementizer's specifier (§3.2).

simvéni 'happen' rejects oti by sort mismatch and pu by eventivity, leaving its subjunctive na-frame (fn. 14).

theorem Angelopoulos2026.situation_clause_factive (c : Complementizer) :

c ∈ Greek.StandardModern.Complementizers.complementizers → clauseSort c = some Bondarenko2022.NominalSort.situation → c.factive = some true

The situation-sorted complementizer is the lexically factive one (§3.2).

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 sorts pass the §3.2 diagnostics: oti's is truth-evaluable ('true'/'mistaken'), pu's occurrence-compatible ('happen') (ex. 33–34).

theorem Angelopoulos2026.selectsLightNoun_iff_sorted (c : Complementizer) :

c ∈ Greek.StandardModern.Complementizers.complementizers → (selectsLightNoun c ↔ (clauseSort c).isSome = true)

The light-noun selectors are exactly the sort-bearing complementizers: the noun must match its clause's sort (§3.1–§3.2).

theorem Angelopoulos2026.oti_pu_lexically_distinct :

clauseSort Greek.StandardModern.Complementizers.oti ≠ clauseSort Greek.StandardModern.Complementizers.pu ∧ Roussou2010.profile Greek.StandardModern.Complementizers.oti ≠ Roussou2010.profile Greek.StandardModern.Complementizers.pu

oti and pu are lexically distinct on this account (content vs situation) and on [Rou10]'s (indefinite vs definite), against fn. 17's allomorphy alternative.

Factivity from situation semantics (§3.2) #

def Angelopoulos2026.Anchored {S : Type u_1} {X : Type u_2} (verb : SituationVerb S X) :

A situation verb is anchored when it relates agents only to situation individuals realized at the evaluation situation.

Equations

Angelopoulos2026.Anchored verb = ∀ (a : X) (xs : SituationIndividual S) (s : S), verb a xs s → xs.sit s

Instances For

theorem Angelopoulos2026.pu_report_factive {S : Type u_1} {X : Type u_2} {verb : SituationVerb S X} (h : Anchored verb) (a : X) (q : S → Prop) (s : S) :

Anchor.existsClosure verb a q s → q s

An anchored verb's pu-report entails its complement — the factive presupposition of pu-clauses derived from situation semantics (§3.2).

theorem Angelopoulos2026.content_report_not_factive :

¬∀ (verb : ContentVerb Bool Unit) (a : Unit) (p : Bool → Prop) (w : Bool), Anchor.existsClosure verb a p w → p w

Content reports carry no such entailment.

theorem Angelopoulos2026.ex_1b_reading :

Anchor.existsClosure Angelopoulos2026.toyRegret✝ () (fun (x : Bool) => x = true) true

ex. 1b's pu-report composed through existsClosure.

Against the transparent syntax–semantics mapping (§7.3) #

inductive Angelopoulos2026.SynPosition :

Syntactic position of an embedded clause: complement or adjunct (§7.3).

complement : SynPosition
adjunct : SynPosition

Instances For

@[instance_reducible]

instance Angelopoulos2026.instDecidableEqSynPosition :

DecidableEq SynPosition

Equations

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

@[instance_reducible]

instance Angelopoulos2026.instReprSynPosition :

Repr SynPosition

Equations

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

def Angelopoulos2026.instReprSynPosition.repr :

SynPosition → ℕ → Std.Format

Equations

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

Instances For

def Angelopoulos2026.bareOtiAttested :

SynPosition → Bondarenko2022.CompositionPath → Prop

The (position, composition-path) pairs attested for bare oti-clauses: Predicate Modification from either position, Functional Application from neither (§2, §7.3).

Equations

Instances For

theorem Angelopoulos2026.bare_never_via_dp (p : SynPosition) :

¬bareOtiAttested p Bondarenko2022.CompositionPath.viaDPArgument

Bare clauses never compose via FA from either position: FA requires the nominalizing D (§7.3 ex. 57).

theorem Angelopoulos2026.transparency_conflates_axes :

¬Bondarenko2022.transparentSSMapping Bondarenko2022.ClauseStructurePath.bareArgument ∧ bareOtiAttested SynPosition.complement Bondarenko2022.CompositionPath.viaSituation

Greek bare oti-clauses fill the cell [Bon22]'s transparent mapping predicts empty: syntactic argumenthood without Functional Application (§7.3).