[Bon22] — Anatomy of an Attitude

Embedded clauses come in two sorts. A Cont-CP denotes a predicate of individuals with propositional content, CONT(x) = p ([Kra06], [Mou15]), and projects a ContP whose head is overt in Buryat (gɘ 'say') and Korean (-ta) and null in English and Russian; a Sit-CP denotes a predicate of situations exemplifying p ([Kra89]) and lacks that layer. Content nouns take truth predicates and reject occurrence predicates, situation nouns the reverse, and a Sit-CP is referentially transparent where a Cont-CP is opaque. Content is fixed by equality rather than subset or overlap, which makes CONT a function and rules out clausal conjunction under one content individual ([BB21]).

With verbs, a clause composes either through the verb's situation argument by Predicate Modification or through a DP argument by Functional Application, and the thesis's mapping claim is that bare clauses take only the first path and nominalized clauses only the second: a bare CP is a predicate of situations, a nominalized CP an individual, and every Θ-head (Causer, Theme, About) wants an individual. [Ang26] later attacks this mapping with Greek oti-clauses.

The ch. 2 diagnostics and the Buryat clause shapes are checked here against the thesis's own examples (Bondarenko2022.Examples); the per-language Cont/Comp head assignments are stated over the Buryat and Korean fragment inventories.

Nominal sorts

inductive Bondarenko2022.NominalSort : Type

The two sorts of clause-taking noun (§2.2), content nouns (idea, claim, rumor) and situation nouns (situation, event, case).

• content : NominalSort
• situation : NominalSort

@[instance_reducible]

instance Bondarenko2022.instDecidableEqNominalSort : DecidableEq NominalSort

Equations

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

@[instance_reducible]

instance Bondarenko2022.instFintypeNominalSort : Fintype NominalSort

Equations

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

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

Equations

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

@[instance_reducible]

instance Bondarenko2022.instReprNominalSort : Repr NominalSort

Equations

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

def Bondarenko2022.NominalSort.truthEvaluable : NominalSort → Prop

Combines with 'true' / 'false' / 'mistaken'.

Equations

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

def Bondarenko2022.NominalSort.occurrenceCompatible : NominalSort → Prop

Combines with 'occur' / 'happen' / 'notice'.

Equations

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

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

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

inductive Bondarenko2022.Diagnostic : Type

The predicate a co-occurrence example tests the noun against.

• truth : Diagnostic
• occurrence : Diagnostic

@[instance_reducible]

instance Bondarenko2022.instDecidableEqDiagnostic : DecidableEq Diagnostic

Equations

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

def Bondarenko2022.instReprDiagnostic.repr : Diagnostic → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Bondarenko2022.instReprDiagnostic : Repr Diagnostic

Equations

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

def Bondarenko2022.parseSort : String → Option NominalSort

Equations

• Bondarenko2022.parseSort "content" = some Bondarenko2022.NominalSort.content
• Bondarenko2022.parseSort "situation" = some Bondarenko2022.NominalSort.situation
• Bondarenko2022.parseSort x✝ = none

def Bondarenko2022.parseDiagnostic : String → Option Diagnostic

Equations

• Bondarenko2022.parseDiagnostic "truth-predicates" = some Bondarenko2022.Diagnostic.truth
• Bondarenko2022.parseDiagnostic "occurrence-predicates" = some Bondarenko2022.Diagnostic.occurrence
• Bondarenko2022.parseDiagnostic "situation-only-predicate-notice" = some Bondarenko2022.Diagnostic.occurrence
• Bondarenko2022.parseDiagnostic x✝ = none

structure Bondarenko2022.CooccurrenceDatum : Type

A noun of a given sort under a diagnostic predicate, with its judgment.

• sort : NominalSort
• diagnostic : Diagnostic
• acceptable : Bool

def Bondarenko2022.instDecidableEqCooccurrenceDatum.decEq (x✝ x✝¹ : CooccurrenceDatum) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Bondarenko2022.instDecidableEqCooccurrenceDatum : DecidableEq CooccurrenceDatum

Equations

• Bondarenko2022.instDecidableEqCooccurrenceDatum = Bondarenko2022.instDecidableEqCooccurrenceDatum.decEq

def Bondarenko2022.instReprCooccurrenceDatum.repr : CooccurrenceDatum → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Bondarenko2022.instReprCooccurrenceDatum : Repr CooccurrenceDatum

Equations

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

def Bondarenko2022.cooccurrenceDatum (e : Datum) : Option CooccurrenceDatum

Equations

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

def Bondarenko2022.cooccurrenceData : List CooccurrenceDatum

The ch. 2 co-occurrence examples.

Equations

• Bondarenko2022.cooccurrenceData = List.filterMap Bondarenko2022.cooccurrenceDatum Bondarenko2022.Examples.all

def Bondarenko2022.Diagnostic.accepts : Diagnostic → NominalSort → Prop

Which predicate the datum's sort should accept.

Equations

• Bondarenko2022.Diagnostic.truth.accepts x✝ = x✝.truthEvaluable
• Bondarenko2022.Diagnostic.occurrence.accepts x✝ = x✝.occurrenceCompatible

@[instance_reducible]

instance Bondarenko2022.instDecidableAccepts (d : Diagnostic) (s : NominalSort) : Decidable (d.accepts s)

Equations

• Bondarenko2022.instDecidableAccepts Bondarenko2022.Diagnostic.truth x✝ = Bondarenko2022.instDecidableAccepts._aux_1 x✝
• Bondarenko2022.instDecidableAccepts Bondarenko2022.Diagnostic.occurrence x✝ = Bondarenko2022.instDecidableAccepts._aux_3 x✝

theorem Bondarenko2022.sort_predicts_cooccurrence (d : CooccurrenceDatum) : d ∈ cooccurrenceData → (d.acceptable = true ↔ d.diagnostic.accepts d.sort)

The sort asymmetries reproduce every co-occurrence judgment.

Equality, subset and existential content

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

Existential content CONT(x) ∩ p ≠ ∅ is the overlap semantics that the thesis rejects in favour of equality (comp). Subset semantics is ContentIndividual.entails.

Equations

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

theorem Bondarenko2022.existentialContent_of_comp {W : Type u_1} {xc : ContentIndividual W} {p : W → Prop} (hne : ∃ (w : W), xc.cont w) (h : Anchor.comp p xc) : ExistentialContent xc p

theorem Bondarenko2022.eq_of_comp_of_comp {W : Type u_1} {xc : ContentIndividual W} {p q : W → Prop} (hp : Anchor.comp p xc) (hq : Anchor.comp q xc) : p = q

Equality makes CONT a function, so one individual cannot carry two contents — no clausal conjunction under a content individual.

theorem Bondarenko2022.entails_not_functional : ¬∀ (xc : ContentIndividual Bool) (p q : Bool → Prop), xc.entails p → xc.entails q → p = q

Subset semantics does not make CONT a function, since a content entails every superset of itself.

Transparency

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

A clause is referentially transparent at s when predicates agreeing at s are interchangeable in it.

Equations

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

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

A Sit-CP is evaluated at the situation itself, hence transparent.

theorem Bondarenko2022.comp_not_transparentAt : ¬∀ (xc : ContentIndividual Bool) (w : Bool), ReferentiallyTransparentAt (fun (p : Bool → Prop) (x : Bool) => Anchor.comp p xc) w

A Cont-CP is opaque, since content identity is not settled at one world.

structure Bondarenko2022.SubstitutionDatum : Type

A substitution triple's conclusion, with the sort of the embedded clause and whether the thesis judges the inference valid.

• sort : NominalSort
• valid : Bool

def Bondarenko2022.instDecidableEqSubstitutionDatum.decEq (x✝ x✝¹ : SubstitutionDatum) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Bondarenko2022.instDecidableEqSubstitutionDatum : DecidableEq SubstitutionDatum

Equations

• Bondarenko2022.instDecidableEqSubstitutionDatum = Bondarenko2022.instDecidableEqSubstitutionDatum.decEq

@[instance_reducible]

instance Bondarenko2022.instReprSubstitutionDatum : Repr SubstitutionDatum

Equations

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

def Bondarenko2022.instReprSubstitutionDatum.repr : SubstitutionDatum → ℕ → Std.Format

Equations

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

def Bondarenko2022.parseValidity : String → Option Bool

Equations

• Bondarenko2022.parseValidity "valid" = some true
• Bondarenko2022.parseValidity "invalid" = some false
• Bondarenko2022.parseValidity x✝ = none

def Bondarenko2022.substitutionDatum (e : Datum) : Option SubstitutionDatum

Equations

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

def Bondarenko2022.substitutionData : List SubstitutionDatum

The substitution-test conclusions of §2.2.3.

Equations

• Bondarenko2022.substitutionData = List.filterMap Bondarenko2022.substitutionDatum Bondarenko2022.Examples.all

theorem Bondarenko2022.substitution_valid_iff_situation (d : SubstitutionDatum) : d ∈ substitutionData → (d.valid = true ↔ d.sort = NominalSort.situation)

Substitution goes through exactly under situation nouns.

Clauses as arguments

inductive Bondarenko2022.SemType : Type

The two semantic types of an embedded clause (§4.2).

• individual : SemType
• predicate : SemType

@[instance_reducible]

instance Bondarenko2022.instDecidableEqSemType : DecidableEq SemType

Equations

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

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

Bare CPs are predicates of situations and nominalized CPs are individuals.

• predicateOfIndividuals : ClauseType
• predicateOfSituations : ClauseType

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

@[instance_reducible]

instance Bondarenko2022.instReprClauseType : Repr ClauseType

Equations

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

def Bondarenko2022.ClauseType.semanticType : ClauseType → SemType

Equations

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

inductive Bondarenko2022.ThetaHead : Type

The Θ-heads of §4.4, each demanding an individual.

• causer : ThetaHead
• theme : ThetaHead
• aboutAttitude : ThetaHead

@[instance_reducible]

instance Bondarenko2022.instDecidableEqThetaHead : DecidableEq ThetaHead

Equations

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

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

Equations

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

@[instance_reducible]

instance Bondarenko2022.instReprThetaHead : Repr ThetaHead

Equations

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

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

A clause saturates a Θ-head when its type is the individual type.

Equations

• Bondarenko2022.saturatesTheta ct x✝ = (ct.semanticType = Bondarenko2022.SemType.individual)

@[instance_reducible]

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

Equations

• Bondarenko2022.instDecidableSaturatesTheta ct θ = Bondarenko2022.instDecidableSaturatesTheta._aux_1 ct θ

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.

def Bondarenko2022.composesViaPM : ClauseType → Prop

Bare CPs compose with the verb's situation argument by Predicate Modification (§4.5), and nominalized CPs do not.

Equations

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

@[instance_reducible]

instance Bondarenko2022.instDecidablePredClauseTypeComposesViaPM : DecidablePred composesViaPM

Equations

• Bondarenko2022.instDecidablePredClauseTypeComposesViaPM Bondarenko2022.ClauseType.predicateOfIndividuals = isFalse Bondarenko2022.instDecidablePredClauseTypeComposesViaPM._proof_1
• Bondarenko2022.instDecidablePredClauseTypeComposesViaPM Bondarenko2022.ClauseType.predicateOfSituations = isTrue trivial

inductive Bondarenko2022.CompositionPath : Type

Table 1.1's two composition paths.

• viaSituation : CompositionPath
• viaDPArgument : CompositionPath

@[instance_reducible]

instance Bondarenko2022.instDecidableEqCompositionPath : DecidableEq CompositionPath

Equations

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

@[instance_reducible]

instance Bondarenko2022.instReprCompositionPath : Repr CompositionPath

Equations

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

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

Equations

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

inductive Bondarenko2022.ClauseStructurePath : Type

The four (clause shape, composition path) combinations.

• bareModifier : ClauseStructurePath
• bareArgument : ClauseStructurePath
• nominalizedModifier : ClauseStructurePath
• nominalizedArgument : ClauseStructurePath

@[instance_reducible]

instance Bondarenko2022.instDecidableEqClauseStructurePath : DecidableEq ClauseStructurePath

Equations

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

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

Equations

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

@[instance_reducible]

instance Bondarenko2022.instReprClauseStructurePath : Repr ClauseStructurePath

Equations

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

def Bondarenko2022.transparentSSMapping : ClauseStructurePath → Prop

The transparent syntax–semantics mapping (§1.1.2, ch. 4) is read off the types, making a cell available when its clause type composes on its path.

Equations

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

theorem Bondarenko2022.not_transparentSSMapping_bareArgument : ¬transparentSSMapping ClauseStructurePath.bareArgument

Bare clauses are never arguments — the cell [Ang26] contests.

theorem Bondarenko2022.not_transparentSSMapping_nominalizedModifier : ¬transparentSSMapping ClauseStructurePath.nominalizedModifier

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

The Comp head

def Bondarenko2022.compHead {S : Type u_2} [Preorder S] (p : Set S) (x s : S) : Prop

The Comp head (§2.3 ex. 151) holds of x at s when x is part of the evaluation situation and exactly verifies p.

Equations

• Bondarenko2022.compHead p x s = (x ≤ s ∧ x ∈ p)

theorem Bondarenko2022.mem_upperClosure_of_compHead {S : Type u_2} [Preorder S] {p : Set S} {x s : S} (h : compHead p x s) : s ∈ upperClosure p

Exact exemplification by a part is inexact verification, membership in the upper closure of the exact verifiers.

Cont exponence

structure Bondarenko2022.ContAnalysis : Type

A Cont-exponence analysis of a clause-typing inventory (ch. 4) names the morpheme, if any, that overtly expones Cont.

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

structure Bondarenko2022.ContCompAnalysisextends Bondarenko2022.ContAnalysis : Type

A Cont analysis with the licenser-conditioned Comp allomorphy.

• inventory : List Complementizer
• contExponent : Option Complementizer
• contExponent_mem (c : Complementizer) : c ∈ self.contExponent → c ∈ self.inventory
• compAllomorph : Complementizer.Licenser → Complementizer
• compAllomorph_mem (l : Complementizer.Licenser) : self.compAllomorph l ∈ self.inventory
• licenser_compAllomorph (l : Complementizer.Licenser) : (self.compAllomorph l).licenser = some l
• cover (c : Complementizer) : c ∈ self.inventory → c ∈ self.contExponent ∨ ∃ (l : Complementizer.Licenser), self.compAllomorph l = c

def Bondarenko2022.buryatAnalysis : ContCompAnalysis

In Buryat (§4.3.1 ex. 33) gɘ expones Cont, participial -Aːša is the Comp allomorph next to nouns, and converbial -žA is the one next to verbs.

Equations

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

def Bondarenko2022.koreanAnalysis : ContCompAnalysis

In Korean (§4.3.2 ex. 46) -ta expones Cont, and adnominal -nun and adverbal -ko are the Comp allomorphs.

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 ↔ ∀ m ∈ c.morphs, m.kind = Morphology.Morph.Kind.root)

In Buryat the Cont exponent is exactly the bare say-root. This is no law of ContAnalysis, since Korean's -ta is itself a suffix.

def Bondarenko2022.parseShape : String → Option (List Complementizer)

The clause-typers of a Buryat clause shape (§4.3.1 ex. 30–32).

Equations

• Bondarenko2022.parseShape "bare gɘ-žɘ clause" = some [Buryat.ge, Buryat.zha]
• Bondarenko2022.parseShape "nominalized participial clause" = some [Buryat.aasha]
• Bondarenko2022.parseShape "nominalized gɘ-participial clause" = some [Buryat.ge, Buryat.aasha]
• Bondarenko2022.parseShape x✝ = none

def Bondarenko2022.parseClauseSort : String → Option NominalSort

Equations

• Bondarenko2022.parseClauseSort "Cont-CP" = some Bondarenko2022.NominalSort.content
• Bondarenko2022.parseClauseSort "Sit-CP" = some Bondarenko2022.NominalSort.situation
• Bondarenko2022.parseClauseSort x✝ = none

structure Bondarenko2022.ShapeDatum : Type

A Buryat embedded clause, with its typers and the sort it denotes.

• typers : List Complementizer
• sort : NominalSort

@[instance_reducible]

instance Bondarenko2022.instDecidableEqShapeDatum : DecidableEq ShapeDatum

Equations

• Bondarenko2022.instDecidableEqShapeDatum = Bondarenko2022.instDecidableEqShapeDatum.decEq

def Bondarenko2022.instDecidableEqShapeDatum.decEq (x✝ x✝¹ : ShapeDatum) : Decidable (x✝ = x✝¹)

Equations

• Bondarenko2022.instDecidableEqShapeDatum.decEq { typers := a, sort := a_1 } { typers := b, sort := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

def Bondarenko2022.instReprShapeDatum.repr : ShapeDatum → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Bondarenko2022.instReprShapeDatum : Repr ShapeDatum

Equations

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

def Bondarenko2022.shapeDatum (e : Datum) : Option ShapeDatum

Equations

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

def Bondarenko2022.shapeData : List ShapeDatum

The Buryat clause shapes of §4.3.1.

Equations

• Bondarenko2022.shapeData = List.filterMap Bondarenko2022.shapeDatum Bondarenko2022.Examples.all

theorem Bondarenko2022.content_iff_contExponent_mem (d : ShapeDatum) : d ∈ shapeData → ∀ c ∈ buryatAnalysis.contExponent, d.sort = NominalSort.content ↔ c ∈ d.typers

A clause denotes content exactly when the Cont exponent is among its typers — the thesis's argument that gɘ expones Cont.

theorem Bondarenko2022.hanaxa_typers : (ArgumentFrame.finiteClause.Takes Buryat.zha ∧ ¬ArgumentFrame.finiteClause.Takes Buryat.aasha) ∧ (Buryat.nominalizedFrame.Takes Buryat.aasha ∧ ¬Buryat.nominalizedFrame.Takes Buryat.zha) ∧ Buryat.hanaxa.typers Buryat.complementizers = [Buryat.aasha, Buryat.zha]

hanaxa's two frames (§4.4.3) each take exactly one typer — converbial -žA on the bare frame, participial -Aːša on the nominalized one — and the say-root takes neither.

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

hanaxa is nonveridical on the bare frame, where it means 'think', and veridical on the nominalized one, where it means 'remember'.