Bondarenko 2022: Anatomy of an Attitude

[Bon22]

Embedded CPs receive two denotations, tracking a left-peripheral syntactic distinction (§1.1.1, ex. 1): a Cont-CP denotes a predicate on content individuals via CONT ([Kra06]; [Mou09]; [Mou15]; [Ell20a]) and projects a ContP; a Sit-CP denotes a predicate on minimal exemplifying situations ([Kra89]) and lacks one. ContP is overt in Korean (-ta) and Buryat (gɘ 'say'), null in English and Russian.

Formalized here: equality semantics for displacement (eq. 7) against subset (eq. 10) and existential (eq. 15), whence the impossibility of true CP conjunction ([BB21]); Sit-CP transparency vs Cont-CP opacity (§1.1.1.1 ex. 5-6); and the transparent syntax-semantics mapping thesis (§1.1.2, ch. 4) — bare CPs compose only as modifiers, nominalized CPs only as arguments — later attacked by [Ang26] (comparison in Studies/Angelopoulos2026.lean, per the chronology rule).

Main declarations

• ExistentialContent — the rejected existential semantics (eq. 15)
• cont_function_blocks_conjunction — equality forces CONT-functionality
• ReferentiallyTransparentAt, compC_not_transparentAt — the weak transparency contrast
• saturatesTheta, bareCP_satisfies_no_theta — the ch. 4 type-mismatch mechanism behind the Causer/Theme/About bans
• transparentSSMapping, transparentSSMapping_iff_typed — the mapping table and its type-theoretic derivation
• NominalSort.truthEvaluable, NominalSort.occurrenceCompatible — the ch. 2 co-occurrence asymmetries
• ContAnalysis, buryatAnalysis, koreanAnalysis — per-language ContP exponence, tied by law to the fragment inventories
• compHead — the Comp head denotation (§2.3 ex. 151)

Implementation notes

Bare §/ex./eq. locators refer to the dissertation and were verified against its text. Sections track different chapters: nominal sorts through the BE2026 bridge follow the ch. 1 summary, the type-theoretic sections ch. 4 (§§4.2-4.5), the co-occurrence and head-denotation sections ch. 2 (§2.2.3, §2.3). The ch. 1 summary repeats later material: Table 1.1 = Table 4.1, and ch. 1 ex. 1 = §4.2 ex. 1-2.

Out of scope: ch. 3 clausal coordination (only the conjunction-impossibility theorem lands here), ch. 5 polarity subjunctives (Russian NPI data, L-analyticity), and the morphological exposition of ContP, which lives in Fragments/Buryat/Complementizers.lean and Fragments/Korean/Complementizers.lean.

Typed paradigm sentences (§2.2.3 ex. 105–112, 120–122; §4.3.1 ex. 30–32) live in Bondarenko2022.Examples, generated from Data/Examples/Bondarenko2022.json.

Nominal sorts

inductive Bondarenko2022.NominalSort : Type

The dissertation's typology of nouns combining with embedded CPs (§2.2). Studies-local: the substrate (ContentIndividual, SituationIndividual) lives in Semantics/Attitudes/ClauseDenotation/.

• content : NominalSort

  Content nouns (§2.2): idea, rumor, hypothesis, claim, fact, lie.

• situation : NominalSort

  Situation nouns (§2.2): situation, event, case, circumstance, state of affairs.

@[implicit_reducible]

instance Bondarenko2022.instDecidableEqNominalSort : DecidableEq NominalSort

Equations

• Bondarenko2022.instDecidableEqNominalSort x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Bondarenko2022.instReprNominalSort : Repr NominalSort

Equations

• Bondarenko2022.instReprNominalSort = { reprPrec := Bondarenko2022.instReprNominalSort.repr }

def Bondarenko2022.instReprNominalSort.repr : NominalSort → ℕ → Std.Format

Equations

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

Equality vs. subset vs. existential semantics

§1.1.1.2. The substrate exposes equality as compC and subset as ContentIndividual.entails; only the existential candidate is new here.

def Bondarenko2022.ExistentialContent {W : Type u_1} (xc : Semantics.Attitudes.ContentIndividual W) (p : W → Prop) : Prop

Existential semantics for a Cont-CP (eq. 15): CONT(x) ∩ p ≠ ∅. Rejected by the thesis in favor of equality (compC, eq. 7); subset is eq. 10.

Equations

• Bondarenko2022.ExistentialContent xc p = ∃ (w : W), xc.cont w ∧ p w

theorem Bondarenko2022.equality_implies_subset {W : Type u_1} (xc : Semantics.Attitudes.ContentIndividual W) (p : W → Prop) : Semantics.Attitudes.ClauseDenotation.Content.compC p xc → xc.entails p

Equality is stronger than subset (§1.1.1.2); re-export of ContentIndividual.eq_implies_entails.

theorem Bondarenko2022.equality_implies_existential {W : Type u_1} (xc : Semantics.Attitudes.ContentIndividual W) (p : W → Prop) (hne : ∃ (w : W), xc.cont w) : Semantics.Attitudes.ClauseDenotation.Content.compC p xc → ExistentialContent xc p

Equality implies existential for nonempty content; the empty-content witness in ContentIndividual shows the proviso is real.

CP conjunction impossibility

Equality semantics makes CONT a function, so true CP conjunction is impossible ([BB21], §1.1.1.2).

theorem Bondarenko2022.cont_function_blocks_conjunction {W : Type u_1} (xc : Semantics.Attitudes.ContentIndividual W) (p1 p2 : W → Prop) : Semantics.Attitudes.ClauseDenotation.Content.compC p1 xc → Semantics.Attitudes.ClauseDenotation.Content.compC p2 xc → p1 = p2

Equality forces functionality: two contents assigned to the same individual coincide.

theorem Bondarenko2022.subset_does_not_force_functionality : ¬∀ (xc : Semantics.Attitudes.ContentIndividual Bool) (p1 p2 : Bool → Prop), xc.entails p1 → xc.entails p2 → p1 = p2

Subset does not force functionality: a non-vacuous content individual entails every superset of its content. Witness over Bool.

Sit-CP transparency vs. Cont-CP opacity

The substitution test (§2.2.3 ex. 120-122; summarized at ch. 1 ex. 5-6): coextensional DPs substitute salva veritate under a Sit-NP but not under a Cont-NP — Cont-CPs are a referentially opaque domain ([Bar81], [Hig83]). Everywhere-coextensional transparency is funext-trivial; the substantive notion is transparency at the evaluation world.

def Bondarenko2022.ReferentiallyTransparentAt {S : Type u_1} (clause : (S → Prop) → S → Prop) (s : S) : Prop

Weak transparency at s: substituting predicates that agree at s preserves clause truth.

Equations

• Bondarenko2022.ReferentiallyTransparentAt clause s = ∀ (p q : S → Prop), (p s ↔ q s) → (clause p s ↔ clause q s)

theorem Bondarenko2022.sit_cp_transparentAt {S : Type u_1} (s : S) : ReferentiallyTransparentAt (fun (p : S → Prop) (s' : S) => p s') s

A Sit-CP evaluates at the actual situation, hence is weak-transparent.

theorem Bondarenko2022.compC_not_transparentAt : ¬∀ (xc : Semantics.Attitudes.ContentIndividual Bool) (w : Bool), ReferentiallyTransparentAt (fun (p : Bool → Prop) (x : Bool) => Semantics.Attitudes.ClauseDenotation.Content.compC p xc) w

compC is not weak-transparent (witness over Bool). This is the propositional-operator shadow of the §2.2.3 ex. 120 DP-level de dicto claim, whose binding-theoretic encoding ([Ell20a]'s CONT-as-content-restrictor) is not yet substrate.

The transparent syntax-semantics mapping thesis

§1.1.2: bare CPs must compose as modifiers (PM via the situation argument), nominalized CPs as arguments (FA via the DP argument). [Ang26] §7.3 attacks this thesis.

inductive Bondarenko2022.ClauseStructurePath : Type

The four logically possible (clause shape, composition path) combinations.

• bareModifier : ClauseStructurePath

  Bare CP composing via Predicate Modification (modifier path).

• bareArgument : ClauseStructurePath

  Bare CP composing via Functional Application (argument path).

• nominalizedModifier : ClauseStructurePath

  Nominalized CP composing via Predicate Modification.

• nominalizedArgument : ClauseStructurePath

  Nominalized CP composing via Functional Application.

@[implicit_reducible]

instance Bondarenko2022.instDecidableEqClauseStructurePath : DecidableEq ClauseStructurePath

Equations

• Bondarenko2022.instDecidableEqClauseStructurePath x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Bondarenko2022.instReprClauseStructurePath : Repr ClauseStructurePath

Equations

• Bondarenko2022.instReprClauseStructurePath = { reprPrec := Bondarenko2022.instReprClauseStructurePath.repr }

def Bondarenko2022.instReprClauseStructurePath.repr : ClauseStructurePath → ℕ → Std.Format

Equations

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

def Bondarenko2022.transparentSSMapping : ClauseStructurePath → Prop

The mapping thesis as a four-cell table (§1.1.2, ch. 4): the off-diagonal cells are impossible. Paper-fidelity bookkeeping — transparentSSMapping_iff_typed derives the cells from the type-theoretic apparatus; [Ang26] attacks the bareArgument cell with Greek oti/pu.

Equations

• Bondarenko2022.transparentSSMapping Bondarenko2022.ClauseStructurePath.bareModifier = True
• Bondarenko2022.transparentSSMapping Bondarenko2022.ClauseStructurePath.bareArgument = False
• Bondarenko2022.transparentSSMapping Bondarenko2022.ClauseStructurePath.nominalizedModifier = False
• Bondarenko2022.transparentSSMapping Bondarenko2022.ClauseStructurePath.nominalizedArgument = True

theorem Bondarenko2022.bare_argument_predicted_impossible : ¬transparentSSMapping ClauseStructurePath.bareArgument

The (bare, argument) cell is empty — the cell [Ang26] attacks (see Angelopoulos2026).

theorem Bondarenko2022.nominalized_modifier_predicted_impossible : ¬transparentSSMapping ClauseStructurePath.nominalizedModifier

The (nominalized, modifier) cell is empty.

theorem Bondarenko2022.diagonal_attested : transparentSSMapping ClauseStructurePath.bareModifier ∧ transparentSSMapping ClauseStructurePath.nominalizedArgument

The diagonal cells are available.

Composition paths (Table 1.1)

inductive Bondarenko2022.CompositionPath : Type

Table 1.1's two composition paths: PM with the verb's situation argument, or FA into a DP argument slot.

• viaSituation : CompositionPath
• viaDPArgument : CompositionPath

@[implicit_reducible]

instance Bondarenko2022.instDecidableEqCompositionPath : DecidableEq CompositionPath

Equations

• Bondarenko2022.instDecidableEqCompositionPath x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Bondarenko2022.instReprCompositionPath.repr : CompositionPath → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Bondarenko2022.instReprCompositionPath : Repr CompositionPath

Equations

• Bondarenko2022.instReprCompositionPath = { reprPrec := Bondarenko2022.instReprCompositionPath.repr }

def Bondarenko2022.attestedCombination : NominalSort → CompositionPath → Prop

Table 1.1 (attitude and speech verbs; occurrence verbs are exempt, §4.3.3): the (Sit-CP, viaSituation) cell is unattested — intersective combination yields always-trivially-false sentences.

Equations

• Bondarenko2022.attestedCombination Bondarenko2022.NominalSort.content x✝ = True
• Bondarenko2022.attestedCombination Bondarenko2022.NominalSort.situation Bondarenko2022.CompositionPath.viaDPArgument = True
• Bondarenko2022.attestedCombination Bondarenko2022.NominalSort.situation Bondarenko2022.CompositionPath.viaSituation = False

theorem Bondarenko2022.sit_cp_via_situation_blocked : ¬attestedCombination NominalSort.situation CompositionPath.viaSituation

The (Sit-CP, viaSituation) cell is empty by semantic triviality (§1.1.2).

Bridge to BondarenkoElliott2026

theorem Bondarenko2022.be2026_inherits_equality_substrate {W : Type u_1} (xc : Semantics.Attitudes.ContentIndividual W) (p : W → Prop) : Semantics.Attitudes.ClauseDenotation.Content.compC p xc ↔ xc.cont = p

Bondarenko & Elliott 2026's MSI/MSO/TECM apparatus presupposes the equality semantics CONT(x) = ⟦S⟧ defended here; the cross-file bridge awaits a stable BE2026 lemma (this file does not import BE2026).

Type-theoretic apparatus (§4.2)

The §4.4 bans are type-theoretic, not structural: bare CPs are ⟨e,t⟩, nominalized CPs ⟨e⟩, Θ-heads require ⟨e⟩; N/D presence is the exponence of the type-shift, not its cause. In Bare Phrase Structure the X-bar argument/modifier distinction is gone, so the "modifier" claim is semantic.

inductive Bondarenko2022.SemType : Type

The two semantic types the derivation uses: saturated ⟨e⟩ vs unsaturated ⟨e,t⟩.

• individual : SemType
• predicate : SemType

@[implicit_reducible]

instance Bondarenko2022.instDecidableEqSemType : DecidableEq SemType

Equations

• Bondarenko2022.instDecidableEqSemType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Bondarenko2022.instReprSemType : Repr SemType

Equations

• Bondarenko2022.instReprSemType = { reprPrec := Bondarenko2022.instReprSemType.repr }

def Bondarenko2022.instReprSemType.repr : SemType → ℕ → Std.Format

Equations

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

inductive Bondarenko2022.ClauseType : Type

The bare-vs-nominalized cut (§4.2), named by semantic content per Bare Phrase Structure.

• predicateOfIndividuals : ClauseType

  Nominalized CP: type ⟨e⟩. Buryat participial nominalization, with or without the say-root gɘ (§4.3.1 ex. 31–32); Korean -nun + kes clause.

• predicateOfSituations : ClauseType

  Bare CP: type ⟨e,t⟩, predicate over (minimal) situations. Buryat gɘžɘ-clause; Korean -ko-clause; Russian bare čto-clause.

@[implicit_reducible]

instance Bondarenko2022.instDecidableEqClauseType : DecidableEq ClauseType

Equations

• Bondarenko2022.instDecidableEqClauseType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Bondarenko2022.instReprClauseType.repr : ClauseType → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Bondarenko2022.instReprClauseType : Repr ClauseType

Equations

• Bondarenko2022.instReprClauseType = { reprPrec := Bondarenko2022.instReprClauseType.repr }

def Bondarenko2022.ClauseType.semanticType : ClauseType → SemType

Nominalized → individual, bare → predicate.

Equations

• Bondarenko2022.ClauseType.predicateOfIndividuals.semanticType = Bondarenko2022.SemType.individual
• Bondarenko2022.ClauseType.predicateOfSituations.semanticType = Bondarenko2022.SemType.predicate

inductive Bondarenko2022.ThetaHead : Type

The Θ-heads of §4.4, all sharing one selectional restriction: an individual argument. Per-Θ presupposition flavor is deferred.

• causer : ThetaHead

  Θ_Causer. §4.4.1.

• theme : ThetaHead

  Θ_Theme (internal-argument introducer). §4.4.2.

• aboutAttitude : ThetaHead

  Θ_About: introduces the res-argument the attitude is about ([Qui56]; [CvS82]); carries a pre-existence presupposition not formalised here. §4.4.3.

@[implicit_reducible]

instance Bondarenko2022.instDecidableEqThetaHead : DecidableEq ThetaHead

Equations

• Bondarenko2022.instDecidableEqThetaHead x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Bondarenko2022.instReprThetaHead : Repr ThetaHead

Equations

• Bondarenko2022.instReprThetaHead = { reprPrec := Bondarenko2022.instReprThetaHead.repr }

def Bondarenko2022.instReprThetaHead.repr : ThetaHead → ℕ → Std.Format

Equations

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

def Bondarenko2022.ThetaHead.requiredType : ThetaHead → SemType

Every Θ-head requires an individual argument.

Equations

• x✝.requiredType = Bondarenko2022.SemType.individual

def Bondarenko2022.saturatesTheta (ct : ClauseType) (θ : ThetaHead) : Prop

A clause type saturates a Θ-head iff its semantic type matches the head's required type (§4.2).

Equations

• Bondarenko2022.saturatesTheta ct θ = (ct.semanticType = θ.requiredType)

@[implicit_reducible]

instance Bondarenko2022.instDecidableSaturatesTheta (ct : ClauseType) (θ : ThetaHead) : Decidable (saturatesTheta ct θ)

Equations

• Bondarenko2022.instDecidableSaturatesTheta ct θ = id inferInstance

Causer, Theme, About (§4.4)

The three bans are one type-mismatch mechanism, not three stipulations.

theorem Bondarenko2022.bareCP_not_Causer : ¬saturatesTheta ClauseType.predicateOfSituations ThetaHead.causer

§4.4.1: bare CPs cannot be Causers.

theorem Bondarenko2022.bareCP_not_Theme : ¬saturatesTheta ClauseType.predicateOfSituations ThetaHead.theme

§4.4.2: bare CPs cannot be Theme-arguments; cf. the explain-class data ([Pie00], [HS13], [Ell16], [RU21]).

theorem Bondarenko2022.bareCP_not_About : ¬saturatesTheta ClauseType.predicateOfSituations ThetaHead.aboutAttitude

§4.4.3: bare CPs cannot be About-arguments.

theorem Bondarenko2022.bareCP_satisfies_no_theta (θ : ThetaHead) : ¬saturatesTheta ClauseType.predicateOfSituations θ

Bare CPs satisfy no Θ-head (§4.4).

theorem Bondarenko2022.nominalizedCP_satisfies_every_theta (θ : ThetaHead) : saturatesTheta ClauseType.predicateOfIndividuals θ

Nominalized CPs satisfy every Θ-head.

The modifier path (§4.5)

Bare CPs compose with the verb's situation argument by Predicate Modification; composesViaPM is the qualitative projection of the Modifier.intersective substrate (Semantics/Modification/Basic.lean), whose Frame-typed instantiation is queued.

def Bondarenko2022.composesViaPM : ClauseType → Prop

PM-compatibility with a verbal situation argument: bare CPs qualify, nominalized CPs do not.

Equations

• Bondarenko2022.composesViaPM Bondarenko2022.ClauseType.predicateOfIndividuals = False
• Bondarenko2022.composesViaPM Bondarenko2022.ClauseType.predicateOfSituations = True

@[implicit_reducible]

instance Bondarenko2022.instDecidableComposesViaPM (ct : ClauseType) : Decidable (composesViaPM ct)

Equations

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

theorem Bondarenko2022.bareCP_composes_via_PM : composesViaPM ClauseType.predicateOfSituations

§4.5: bare CPs are verbal modifiers.

theorem Bondarenko2022.nominalizedCP_not_PM_modifier : ¬composesViaPM ClauseType.predicateOfIndividuals

Nominalized CPs compose via FA, not PM (§4.5).

Deriving the mapping table

def Bondarenko2022.transparentSSMappingDerived : ClauseStructurePath → Prop

The table's cell values, derived from the type-theoretic predicates.

Equations

• One or more equations did not get rendered due to their size.
• Bondarenko2022.transparentSSMappingDerived Bondarenko2022.ClauseStructurePath.bareModifier = Bondarenko2022.composesViaPM Bondarenko2022.ClauseType.predicateOfSituations
• Bondarenko2022.transparentSSMappingDerived Bondarenko2022.ClauseStructurePath.nominalizedModifier = Bondarenko2022.composesViaPM Bondarenko2022.ClauseType.predicateOfIndividuals

theorem Bondarenko2022.transparentSSMapping_iff_typed (path : ClauseStructurePath) : transparentSSMapping path ↔ transparentSSMappingDerived path

The §1.1.2 table agrees cell-by-cell with the type-theoretic derivation: the four-cell pattern is derived, not stipulated.

Cross-linguistic ContP exponence

Per-language Cont-exponence analyses (ch. 4), tied by law to the fragment inventories. Buryat carries the licenser-conditioned Comp allomorphy (§4.3.1 ex. 33); Korean's parallel rule (§4.3.2 ex. 46) is not yet law-checked, so its witness stays at ContAnalysis. [Cac25]'s Tigrinya extension lives in Studies/Cacchioli2025.lean per the chronology rule.

structure Bondarenko2022.ContAnalysis : Type

A Cont-exponence analysis of one language's clause-typing inventory (ch. 4): the morpheme, if any, overtly exponing Cont (none = null exponence: English, Russian). A structure, not a class — rival frameworks construct rival witnesses.

• inventory : List Complementizer

  The fragment inventory analyzed.

• contExponent : Option Complementizer

  The overt Cont exponent, if any.

• contExponent_mem (c : Complementizer) : c ∈ self.contExponent → c ∈ self.inventory

  The exponent is drawn from the inventory.

structure Bondarenko2022.ContCompAnalysisextends Bondarenko2022.ContAnalysis : Type

A full Cont/Comp head assignment: ContAnalysis plus the licenser-conditioned Comp allomorphy and its laws.

• inventory : List Complementizer
• contExponent : Option Complementizer
• contExponent_mem (c : Complementizer) : c ∈ self.contExponent → c ∈ self.inventory
• compAllomorph : Complementizer.Licenser → Complementizer

  Comp allomorph selected by the licensing category.

• compAllomorph_mem (l : Complementizer.Licenser) : self.compAllomorph l ∈ self.inventory
• licenser_compAllomorph (l : Complementizer.Licenser) : (self.compAllomorph l).licenser = some l

  The selected allomorph reproduces the fragment's distribution datum.

• cover (c : Complementizer) : c ∈ self.inventory → c ∈ self.contExponent ∨ ∃ (l : Complementizer.Licenser), self.compAllomorph l = c

  Head assignment is exhaustive over the inventory.

def Bondarenko2022.buryatAnalysis : ContCompAnalysis

Buryat (§4.3.1 ex. 33): gɘ expones Cont; the suffixes are Comp allomorphs — participial -Aːša next to nominal projections, converbial -žA next to verbs.

Equations

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

def Bondarenko2022.koreanAnalysis : ContCompAnalysis

Korean (§4.3.2 ex. 46; cf. [BAM18]): -ta expones Cont; adnominal -nun and adverbal -ko are the Comp allomorphs, parallel to Buryat ex. 33.

Equations

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

theorem Bondarenko2022.mem_buryatContExponent_iff (c : Complementizer) : c ∈ Buryat.complementizers → (c ∈ buryatAnalysis.contExponent ↔ c.verbForm = none)

In Buryat the Cont exponent is exactly the non-suffixal say-root — a Buryat-specific alignment, not a ContAnalysis law (Korean's -ta is itself a suffix).

theorem Bondarenko2022.hanaxa_frames_realized : Buryat.hanaxa.realizes Buryat.zha ∧ Buryat.hanaxa.realizes Buryat.aasha ∧ ¬Buryat.hanaxa.realizes Buryat.ge

Each of hanaxa's two frames (§4.4.3) is realized by exactly one clause-typer — bare by converbial -žA, nominalized by participial -Aːša — and the say-root gɘ realizes neither.

theorem Bondarenko2022.hanaxa_frame_conditioned_attitude : Buryat.hanaxa.attitudeOn Frame.finiteClause = some (Features.Attitude.doxastic Features.Veridicality.nonVeridical) ∧ Buryat.hanaxa.attitudeOn Buryat.nominalizedFrame = some (Features.Attitude.doxastic Features.Veridicality.veridical)

hanaxa think~remember (§4.4.3): the attitude flips with the frame — nonveridical/opaque on the bare CP, veridical on the nominalized frame. Previously unstateable: attitude was per-lexeme.

Noun-predicate co-occurrence (§2.2.3)

Cont-NPs combine with truth-evaluable predicates, Sit-NPs do not (ex. 105-107); Sit-NPs combine with occurrence predicates, Cont-NPs do not (ex. 108-112). Both asymmetries project the NominalSort distinction: contents are truth-evaluated, situations occur.

def Bondarenko2022.NominalSort.truthEvaluable : NominalSort → Prop

Combines with 'true' / 'false' / 'mistaken' (ex. 105-107).

Equations

• Bondarenko2022.NominalSort.content.truthEvaluable = True
• Bondarenko2022.NominalSort.situation.truthEvaluable = False

@[implicit_reducible]

instance Bondarenko2022.instDecidablePredNominalSortTruthEvaluable : DecidablePred NominalSort.truthEvaluable

Equations

• Bondarenko2022.instDecidablePredNominalSortTruthEvaluable Bondarenko2022.NominalSort.content = isTrue trivial
• Bondarenko2022.instDecidablePredNominalSortTruthEvaluable Bondarenko2022.NominalSort.situation = isFalse Bondarenko2022.instDecidablePredNominalSortTruthEvaluable._proof_1

def Bondarenko2022.NominalSort.occurrenceCompatible : NominalSort → Prop

Combines with 'occur' / 'happen' (Russian proizojti, slučit'sja; Korean ilena) — ex. 108-112. The footnote-28 hedge on alachay is aggregated with the main paradigm.

Equations

• Bondarenko2022.NominalSort.content.occurrenceCompatible = False
• Bondarenko2022.NominalSort.situation.occurrenceCompatible = True

@[implicit_reducible]

instance Bondarenko2022.instDecidablePredNominalSortOccurrenceCompatible : DecidablePred NominalSort.occurrenceCompatible

Equations

• Bondarenko2022.instDecidablePredNominalSortOccurrenceCompatible Bondarenko2022.NominalSort.content = isFalse Bondarenko2022.instDecidablePredNominalSortOccurrenceCompatible._proof_1
• Bondarenko2022.instDecidablePredNominalSortOccurrenceCompatible Bondarenko2022.NominalSort.situation = isTrue trivial

Cont and Comp head denotations (§2.3)

Ex. 150: ⟦Cont⟧ = λp.λx. CONT(x) = p — exactly the substrate compC. Ex. 151: ⟦Comp⟧ = λp.λx. x ⊑ s ∧ x ⊩ p — parthood plus exact exemplification. The dissertation's own abbreviation of ex. 151 drops the anchoring conjunct; its footnote 37 notes the anchoring matters in §5.2.3 (clauses as restrictors of existential quantifiers). compHead keeps it.

theorem Bondarenko2022.cont_head_denotation_is_compC {W : Type u_1} (p : W → Prop) (xc : Semantics.Attitudes.ContentIndividual W) : Semantics.Attitudes.ClauseDenotation.Content.compC p xc ↔ xc.cont = p

Ex. 150 is the existing compC — the ch. 2 proposal introduces no new machinery. The equality shape is further defended in §2.4 (no-stacking, ex. 171; the fact definiteness, ex. 177-178; the complex-claim argument, ex. 183-184), unformalized.

def Bondarenko2022.compHead {S : Type u_1} [Preorder S] (p : S → Prop) (x evalSit : S) : Prop

Ex. 151: x is part of the evaluation situation and exactly verifies p (verifier-membership, vs the part-existential inexactVer of Semantics/Truthmaker/Inexact.lean).

Equations

• Bondarenko2022.compHead p x evalSit = (x ≤ evalSit ∧ p x)

theorem Bondarenko2022.compHead_implies_inexactVerifier {S : Type u_1} [Preorder S] (p : S → Prop) (x evalSit : S) (h : compHead p x evalSit) : ∃ u ≤ evalSit, p u

Exact exemplification implies inexact: a verifier is a part of itself (cf. inexactVer_of_exact).