[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 (Semantics/Tense/TemporalConnectives/Before.lean); the pronominal/quantificational substrate is Semantics/Tense/LexicalType.lean.

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 Before.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 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).

@[implicit_reducible]

instance Sharvit2014.instDecidableEqShiftability : DecidableEq Shiftability

Equations

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

@[implicit_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 Tense.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.

@[implicit_reducible]

instance Sharvit2014.instDecidableEqLanguageTenseProfile : DecidableEq LanguageTenseProfile

Equations

• Sharvit2014.instDecidableEqLanguageTenseProfile = Sharvit2014.instDecidableEqLanguageTenseProfile.decEq

@[implicit_reducible]

instance Sharvit2014.instReprLanguageTenseProfile : Repr LanguageTenseProfile

Equations

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

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

Equations

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

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 Tense.LexicalType.pronominal)

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

The past tense is quantificational (after Prior 1967).

Equations

• L.isQuantificational = (L.pastLexicalType == some Tense.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 [BC03] IPF dispatch Before.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.SOT.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 Before.ipf_quantificationalPast. The body calls the IPF dispatch Before.triggersIPFInBefore; wellFormedPastUnderPastBefore_iff_pronominal records the resulting equivalence to isPronominal (= Before.pastUnderBefore_wellFormed_iff).

Equations

• L.wellFormedPastUnderPastBefore = match L.pastLexicalType with | some τ => !Tense.TemporalConnectives.Before.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 (Before.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 Tense.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 Tense.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 Tense.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 in TemporalConnectives/Before.lean; 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 (Before.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 Before.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.