[Sha14]: On the universal principles of tense embedding

[Sha14] [OS12] [Sha03] [BC03] [Par73]

[Sha14] ("On the universal principles of tense embedding: The lesson from before", J. Semantics 31(2):263-313) makes the pronominal/quantificational tense distinction (after [Par73] vs Prior 1967) the engine for cross-linguistic variation in before-clauses (English/Polish vs Japanese) and attitude reports. The IPF mechanism it rests on is the [BC03] before semantics (Studies/BeaverCondoravdi2003.lean); the pronominal/quantificational apparatus ((30)) is defined below.

Main definitions

• Shiftability — three-valued present shiftability ((71), p. 289): a fully shiftable present (Japanese), a semi-shiftable one (Polish), or a non-shiftable one (English).
• LanguageTenseProfile — a language's three tense parameters ((98), p. 300): the SOT rule, the present's shiftability, and the past tense's lexical type (Option LexicalType, no-mixing structural; none = tenseless / out of scope).
• The derived predicates (wellFormedPastUnderPastBefore, …) are grounded in the substrate, not re-stipulated: well-formedness routes through triggersIPFInBefore, SOT-deletion through Decomposition.sotDeletionApplicable.
• eq99a/eq99b/eq99c — Sharvit's three universal predictions ((99), p. 301).

Scope

In the typology: English (type 6), Polish (type 10), Japanese (type 11) of (98). Excluded: Modern Greek and Spanish A/B (§6.2, (105), pp. 303-304), which need a mood parameter and — for Spanish B — a mixed past/present lexical type this profile cannot represent (Sharvit frames them as illustrative, p. 305); and tenseless languages (pastLexicalType = none), outside the no-tenseless assumption (§6.1, p. 299).

The two lexical types of tense ((30))

inductive Sharvit2014.LexicalType : Type

[Sha14]'s two semantic types of tense ((30), p. 274): pronominal (after [Par73]; an element of D_i) and quantificational (a Priorean operator over time-predicates).

• pronominal : LexicalType

  Pronominal: an element of D_i, two-indexed past_{j,k}.

• quantificational : LexicalType

  Quantificational: an operator over time-predicates.

@[instance_reducible]

instance Sharvit2014.instDecidableEqLexicalType : DecidableEq LexicalType

Equations

• Sharvit2014.instDecidableEqLexicalType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Sharvit2014.instReprLexicalType.repr : LexicalType → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Sharvit2014.instReprLexicalType : Repr LexicalType

Equations

• Sharvit2014.instReprLexicalType = { reprPrec := Sharvit2014.instReprLexicalType.repr }

def Sharvit2014.quantificationalPast {Time : Type u_1} [LT Time] (K : Set Time) (p : Time → Prop) (t : Time) : Prop

[Sha14] (30b): quantificational past as the generalized quantifier some (Quantification.some_sem) over the contextual restrictor K, with scope "precedes t and satisfies p". Definitionally ∃ t' ∈ K, t' < t ∧ p t'.

Equations

• Sharvit2014.quantificationalPast K p t = Quantification.some_sem (fun (x : Time) => x ∈ K) fun (t' : Time) => t' < t ∧ p t'

theorem Sharvit2014.evalPast_iff_quantificationalPast {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (p : Semantics.Aspect.PointPred W Time) (tc : Time) (w : W) : Tense.TenseAspectComposition.evalPast p tc w ↔ quantificationalPast Set.univ (fun (t : Time) => p { world := w, time := t }) tc

The pipeline's existential past is the quantificational past with trivial restrictor: evalPast = quantificationalPast over Set.univ. Together with pronominalLookup_eq_some_iff_tensePronoun below, this places both of Sharvit's tense lexical types over operators the rest of the codebase already uses.

theorem Sharvit2014.ipf_quantificationalPast {Time : Type u_1} [LinearOrder Time] {C K : Set Time} (hK : K ⊆ C) (hC_dense : ∀ (a b : Time), a ∈ C → b ∈ C → a < b → ∃ c ∈ C, a < c ∧ c < b) (q : Time → Prop) : ¬BeaverCondoravdi2003.hasEarliest C (quantificationalPast K q)

IPF ([Sha14] (27), p. 272): when the body of before^{B&C} is the quantificational past [[PAST]]^{K,g}(q), and the restrictor C is order-dense (interval-like) with K ⊆ C, the EARLIEST presupposition (BeaverCondoravdi2003.hasEarliest) fails: a witness t_q < t_min with q t_q lifts via density to a strictly smaller body-witness. The technical core of the thesis that only languages with pronominal tenses license past-under-past in before-clauses.

def Sharvit2014.triggersIPFInBefore : LexicalType → Bool

The Bool-valued IPF dispatch on tense lexical type: quantificational tenses trigger IPF in before-clauses; pronominal tenses do not.

Equations

• Sharvit2014.triggersIPFInBefore Sharvit2014.LexicalType.quantificational = true
• Sharvit2014.triggersIPFInBefore Sharvit2014.LexicalType.pronominal = false

@[simp]

theorem Sharvit2014.pastUnderBefore_wellFormed_iff (τ : LexicalType) : triggersIPFInBefore τ = false ↔ τ = LexicalType.pronominal

((27), p. 272): a language's past tense is well-formed under before^{B&C} iff its tense lexical type does not trigger IPF — i.e., iff it is pronominal.

The pronominal past ((30a))

The pronominal-past lookup and its grounding in the codebase's canonical tense pronoun: pronominalLookup is the presupposition-gated referent of a past-constraint TensePronoun, so [Sha14]'s (30a) and [Par73]'s tense-pronoun carrier coincide (pronominalLookup_eq_some_iff_tensePronoun).

def Sharvit2014.pronominalLookup {Time : Type u_1} [LT Time] [DecidableLT Time] (g : ℕ → Time) (j k : ℕ) : Option Time

[Sha14] (30a): pronominal-past lookup [[past_{j,k}]]^g. Indices j (evaluation), k (referential); defined iff g k < g j, then g k. Uses Option (not Part/PFun) as the domain is decidable.

Equations

• Sharvit2014.pronominalLookup g j k = if g k < g j then some (g k) else none

@[simp]

theorem Sharvit2014.pronominalLookup_eq_some_iff {Time : Type u_1} [LT Time] [DecidableLT Time] (g : ℕ → Time) (j k : ℕ) (t : Time) : pronominalLookup g j k = some t ↔ g k < g j ∧ g k = t

The pronominal past denotes the referential index when defined.

@[simp]

theorem Sharvit2014.pronominalLookup_eq_none_iff {Time : Type u_1} [LT Time] [DecidableLT Time] (g : ℕ → Time) (j k : ℕ) : pronominalLookup g j k = none ↔ ¬g k < g j

The pronominal past is undefined exactly when the constraint fails.

theorem Sharvit2014.pronominalLookup_eq_some_iff_tensePronoun {Time : Type u_1} [LinearOrder Time] (g : Tense.TemporalAssignment Time) (j k : ℕ) (t : Time) (mode : Intensional.ReferentialMode) : pronominalLookup g j k = some t ↔ { varIndex := k, constraint := Tense.past, mode := mode, evalTimeIndex := j }.fullPresupposition g ∧ { varIndex := k, constraint := Tense.past, mode := mode, evalTimeIndex := j }.resolve g = t

(30a) coincides with the codebase's [Par73] carrier: the lookup is defined with value t iff the past-constraint TensePronoun with referential index k and evaluation index j satisfies its presupposition and resolves to t — for any binding mode.

The parameter space ((98))

inductive Sharvit2014.Shiftability : Type

The present tense's shiftability, three-valued per [Sha14] (71)/(78), pp. 288-291: Japanese is fully shiftable, Polish semi-shiftable (bindable, but not by the same binder as its referential index), English non-shiftable (forced free). The distinction is load-bearing: only a fully shiftable present yields a well-formed present-under-past before-clause, so Polish patterns with English there despite being bindable in attitudes.

• nonShiftable : Shiftability

  Forced free; cannot be bound (English).

• semiShiftable : Shiftability

  Bindable, but not by the binder of its referential index (Polish).

• fullyShiftable : Shiftability

  Freely bindable (Japanese).

@[instance_reducible]

instance Sharvit2014.instDecidableEqShiftability : DecidableEq Shiftability

Equations

• Sharvit2014.instDecidableEqShiftability x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Sharvit2014.instReprShiftability : Repr Shiftability

Equations

• Sharvit2014.instReprShiftability = { reprPrec := Sharvit2014.instReprShiftability.repr }

def Sharvit2014.instReprShiftability.repr : Shiftability → ℕ → Std.Format

Equations

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

structure Sharvit2014.LanguageTenseProfile : Type

A language's tense profile per [Sha14] (98), p. 300: the SOT rule, the present's shiftability, and the past tense's lexical type. The no-mixing assumption (§6.1, p. 300) is enforced structurally by Option LexicalType (one past type, or none for tenseless).

• hasSOT : Bool

  The SOT rule: deletion of an agreeing embedded tense.

• presentShiftability : Shiftability

  The present tense's shiftability ((71), p. 289).

• pastLexicalType : Option LexicalType

  The past tense's lexical type, or none for tenseless languages (outside [Sha14]'s framework).

def Sharvit2014.instDecidableEqLanguageTenseProfile.decEq (x✝ x✝¹ : LanguageTenseProfile) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Sharvit2014.instDecidableEqLanguageTenseProfile : DecidableEq LanguageTenseProfile

Equations

• Sharvit2014.instDecidableEqLanguageTenseProfile = Sharvit2014.instDecidableEqLanguageTenseProfile.decEq

def Sharvit2014.instReprLanguageTenseProfile.repr : LanguageTenseProfile → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Sharvit2014.instReprLanguageTenseProfile : Repr LanguageTenseProfile

Equations

• Sharvit2014.instReprLanguageTenseProfile = { reprPrec := Sharvit2014.instReprLanguageTenseProfile.repr }

def Sharvit2014.LanguageTenseProfile.hasTenses (L : LanguageTenseProfile) : Bool

The language has tenses ([Sha14]'s no-tenseless precondition, §6.1, p. 299).

Equations

• L.hasTenses = L.pastLexicalType.isSome

def Sharvit2014.LanguageTenseProfile.isPronominal (L : LanguageTenseProfile) : Bool

The past tense is pronominal (after [Par73]).

Equations

• L.isPronominal = (L.pastLexicalType == some Sharvit2014.LexicalType.pronominal)

def Sharvit2014.LanguageTenseProfile.isQuantificational (L : LanguageTenseProfile) : Bool

The past tense is quantificational (after Prior 1967).

Equations

• L.isQuantificational = (L.pastLexicalType == some Sharvit2014.LexicalType.quantificational)

def Sharvit2014.LanguageTenseProfile.hasShiftablePresent (L : LanguageTenseProfile) : Bool

The present can be bound at all (semi- or fully shiftable) — enough to host a "now"-thought in attitudes.

Equations

• L.hasShiftablePresent = (L.presentShiftability != Sharvit2014.Shiftability.nonShiftable)

def Sharvit2014.LanguageTenseProfile.hasFullyShiftablePresent (L : LanguageTenseProfile) : Bool

The present is fully shiftable (Japanese), the condition for a well-formed present-under-past before-clause ((78), p. 291).

Equations

• L.hasFullyShiftablePresent = (L.presentShiftability == Sharvit2014.Shiftability.fullyShiftable)

Derived empirical predicates

These are not independent stipulations: the before-well-formedness predicate routes through the IPF dispatch triggersIPFInBefore, and the SOT-derived predicates through Kratzer's deletion condition Decomposition.sotDeletionApplicable.

def Sharvit2014.LanguageTenseProfile.sotAppliesPastUnderPast (L : LanguageTenseProfile) : Bool

SOT-deletion of an agreeing past-under-past applies when the language has the SOT rule, routed through Decomposition.sotDeletionApplicable (Kratzer's morphological-identity condition, here .past/.past).

Equations

• L.sotAppliesPastUnderPast = (L.hasSOT && Tense.Decomposition.sotDeletionApplicable Tense.past Tense.past)

def Sharvit2014.LanguageTenseProfile.wellFormedPastUnderPastBefore (L : LanguageTenseProfile) : Bool

PAST-under-PAST in before is well-formed iff the past does not trigger IPF — the technical core ipf_quantificationalPast. The body calls the IPF dispatch triggersIPFInBefore; wellFormedPastUnderPastBefore_iff_pronominal records the resulting equivalence to isPronominal (= pastUnderBefore_wellFormed_iff).

Equations

• L.wellFormedPastUnderPastBefore = match L.pastLexicalType with | some τ => !Sharvit2014.triggersIPFInBefore τ | none => false

def Sharvit2014.LanguageTenseProfile.wellFormedPresentUnderPastBefore (L : LanguageTenseProfile) : Bool

PRES-under-PAST in before is well-formed iff the present is fully shiftable (the Stump effect, p. 278): English (non-shiftable) and Polish (semi-shiftable) are both ruled out; only Japanese is well-formed ((78), p. 291).

Equations

• L.wellFormedPresentUnderPastBefore = L.hasFullyShiftablePresent

def Sharvit2014.LanguageTenseProfile.simultaneousAttitudeReading (L : LanguageTenseProfile) : Bool

"Simultaneous" past-under-past reading in attitude reports ((59b), p. 284): the past is pronominal and SOT-deletion applies. This is the SOT-derived reading; Japanese's distinct (present-tense) simultaneous reading ((47), p. 280) is a different mechanism, not this.

Equations

• L.simultaneousAttitudeReading = (L.isPronominal && L.sotAppliesPastUnderPast)

def Sharvit2014.LanguageTenseProfile.pShiftabilityBare (L : LanguageTenseProfile) : Bool

Bare before-clause p-shiftability ((51), p. 281): the embedded past can refer to a future time. Requires a quantificational past (Japanese); absent in English/Polish.

Equations

• L.pShiftabilityBare = L.isQuantificational

def Sharvit2014.LanguageTenseProfile.pShiftabilityEmbedded (L : LanguageTenseProfile) : Bool

Embedded before-clause p-shiftability ((66)-(68), p. 287): under a matrix attitude verb, even pronominal-past languages acquire p-shiftability via SOT-deletion of the matrix past. (Hedged in the paper — "for many speakers".)

Equations

• L.pShiftabilityEmbedded = (L.isQuantificational || L.isPronominal && L.sotAppliesPastUnderPast)

def Sharvit2014.LanguageTenseProfile.respectsEmbeddability (L : LanguageTenseProfile) : Bool

[Sha14]'s Embeddability Principle (Sharvit 2003, restated p. 299): every language has at least one mechanism for embedding a "now"-thought (SOT, a shiftable present, or a quantificational past).

Equations

• L.respectsEmbeddability = (L.hasSOT || L.hasShiftablePresent || L.isQuantificational)

theorem Sharvit2014.LanguageTenseProfile.isQuantificational_eq_false_of_isPronominal (L : LanguageTenseProfile) : L.isPronominal = true → L.isQuantificational = false

A pronominal past is not quantificational — the Option LexicalType no-mixing constraint.

theorem Sharvit2014.LanguageTenseProfile.wellFormedPastUnderPastBefore_iff_pronominal (L : LanguageTenseProfile) : L.wellFormedPastUnderPastBefore = true ↔ L.isPronominal = true

Well-formedness of past-under-past in before coincides with a pronominal past — imported from the IPF result (pastUnderBefore_wellFormed_iff), not re-stipulated.

Attested language types ((98), p. 300)

def Sharvit2014.english : LanguageTenseProfile

English (type 6 in (98)): SOT, non-shiftable present, pronominal past.

Equations

• Sharvit2014.english = { hasSOT := true, presentShiftability := Sharvit2014.Shiftability.nonShiftable, pastLexicalType := some Sharvit2014.LexicalType.pronominal }

def Sharvit2014.polish : LanguageTenseProfile

Polish (type 10 in (98)): no SOT, semi-shiftable present, pronominal past. The "semi-shiftable" hedge (§4.2) distinguishes Polish from Japanese: Polish's present is bindable in attitudes but not fully shiftable, so present-under-past in before is still ill-formed (it patterns with English, not Japanese). Grønn & von Stechow argue against the parameter, attributing the Polish pattern to Aktionsart; the encoding here follows Sharvit.

Equations

• Sharvit2014.polish = { hasSOT := false, presentShiftability := Sharvit2014.Shiftability.semiShiftable, pastLexicalType := some Sharvit2014.LexicalType.pronominal }

def Sharvit2014.japanese : LanguageTenseProfile

Japanese (type 11 in (98)): no SOT, fully-shiftable present, quantificational past. The quantificational classification follows [Ogi96], the canonical and dominant view; it is contested by relative-tense alternatives (Kusumoto 1999, Sudo 2012).

Equations

• Sharvit2014.japanese = { hasSOT := false, presentShiftability := Sharvit2014.Shiftability.fullyShiftable, pastLexicalType := some Sharvit2014.LexicalType.quantificational }

def Sharvit2014.attestedTypes : List LanguageTenseProfile

The attested language types in Sharvit's table ((98)).

Equations

• Sharvit2014.attestedTypes = [Sharvit2014.english, Sharvit2014.polish, Sharvit2014.japanese]

Structural constraints (§6.1)

theorem Sharvit2014.all_attested_have_tenses (L : LanguageTenseProfile) : L ∈ attestedTypes → L.hasTenses = true

Every attested language has tenses (the no-tenseless assumption holds within scope).

theorem Sharvit2014.all_attested_respect_embeddability (L : LanguageTenseProfile) : L ∈ attestedTypes → L.respectsEmbeddability = true

Every attested language respects [Sha14]'s Embeddability Principle.

Cross-linguistic predictions ((99), p. 301)

Stated and proved over all profiles, not the three attested rows: each prediction follows structurally from the parameter definitions and the substrate grounding.

theorem Sharvit2014.eq99a_pres_under_past_before_implies_shiftable (L : LanguageTenseProfile) : L.wellFormedPresentUnderPastBefore = true → L.hasShiftablePresent = true

[Sha14] (99a): a well-formed present-under-past in before implies a shiftable present. Non-trivial under the three-valued Shiftability: well-formedness needs full shiftability, which strictly implies the weaker "shiftable at all" (Polish witnesses the gap).

theorem Sharvit2014.eq99b_before_and_embedded_pshift_imply_simultaneous (L : LanguageTenseProfile) : L.wellFormedPastUnderPastBefore = true → L.pShiftabilityEmbedded = true → L.simultaneousAttitudeReading = true

[Sha14] (99b): well-formed PAST-under-PAST in before + embedded p-shiftability ⇒ a simultaneous reading of past-under-past in attitudes. Given a pronominal past (from well-formedness), the isQuantificational disjunct of pShiftabilityEmbedded vanishes, so the embedded p-shiftability is the SOT-deletion that licenses the simultaneous reading.

theorem Sharvit2014.eq99c_before_and_no_simultaneous_imply_no_bare_pshift (L : LanguageTenseProfile) : L.wellFormedPastUnderPastBefore = true → L.simultaneousAttitudeReading = false → L.pShiftabilityBare = false

[Sha14] (99c): well-formed PAST-under-PAST in before + no simultaneous reading ⇒ No-p-shiftability of bare past-under-past before. Under this encoding the consequent already follows from well-formedness (a pronominal past is not quantificational, so the bare clause lacks p-shiftability); the no-simultaneous antecedent (_hNoSim) is Sharvit's, kept for fidelity to (99c) but not load-bearing here.

Substrate connection: IPF and quantificational past

The wellFormedPastUnderPastBefore predicate is grounded in the [BC03] IPF result formalized via BeaverCondoravdi2003.hasEarliest; the two theorems below consume that grounding via wellFormedPastUnderPastBefore_iff_pronominal.

theorem Sharvit2014.quant_past_languages_fail_before (L : LanguageTenseProfile) : L.isQuantificational = true → L.wellFormedPastUnderPastBefore = false

Quantificational-past languages (Japanese) fail wellFormedPastUnderPastBefore, matching the IPF prediction (ipf_quantificationalPast).

theorem Sharvit2014.pronominal_past_languages_pass_before (L : LanguageTenseProfile) : L.isPronominal = true → L.wellFormedPastUnderPastBefore = true

Pronominal-past languages (English, Polish) satisfy wellFormedPastUnderPastBefore, in keeping with pastUnderBefore_wellFormed_iff.

Per-language payload

The central typological contrast — and a regression guard on the three-valued shiftability: a binary shiftablePresent would wrongly make Polish's present-under-past in before well-formed.

Cross-paper bridge to [Kra98a]

The Sharvit ↔ [Kle16] comparison (same simultaneous-reading prediction, different mechanisms) lives in the later paper's study file, Studies/Klecha2016.lean §F1.

theorem Sharvit2014.english_predicts_simultaneous : english.simultaneousAttitudeReading = true

[Sha14]'s prediction for English: SOT + pronominal past yields the simultaneous reading of past-under-past in attitudes.

theorem Sharvit2014.english_sot_realizes_kratzer_deletion : english.sotAppliesPastUnderPast = true

Bridge to [Kra98a]: English's SOT rule realizes Kratzer's deletion of an agreeing past-under-past — english.hasSOT and Kratzer's morphological-identity condition (Decomposition.sotDeletionApplicable .past .past) jointly license the "null" embedded past.