Sharvit (2014): On the universal principles of tense embedding: The lesson from before

Sharvit derives the tenses a language allows in before-clauses from the kind of tense it has. Before presupposes, with Beaver and Condoravdi, an earliest time of its clause within the contextually relevant interval, later than the start of that interval. A tense that quantifies existentially over times makes the presupposition fail on dense time: the times after some event have no earliest member, and where the event precedes the interval, the interval itself qualifies. A pronominal tense, after Partee, has no quantifier and leaves an earliest time, which its own presupposition places before the speech time. A tense with no meaning of its own, deleted by the sequence-of-tense rule or null, leaves the earliest time unconstrained. A present whose evaluation time stays the speech time makes the order of the two events follow from the tenses alone, the effect noted by Stump. With the sequence-of-tense rule and the shiftability of the present as parameters, the kind of tense gives the pattern of English, Japanese and Polish, a table of permissible languages, and three predictions.

Main statements

• IsEarliest.eq_fst_of_diamond: on dense time the earliest moment of an existentially quantified tense within an interval is the start of the interval, whatever the tense.
• Reading.fails_iff, Reading.stumpEffect_iff: of the readings of a tensed clause under before, the existential ones fail and the pronominal present has the Stump effect.
• judgment_iff, simultaneous_iff: the parameters of English, Japanese and Polish give the paper's judgments on before-clauses and attitude reports.
• pShiftable_present_of_wellFormed, simultaneous_past_of_pShiftable, noPShiftability_past_of_not_simultaneous: the three predictions.

Implementation notes

• A time is a closed interval of a dense linear order of moments, mathlib's NonemptyInterval, and precedence and overlap are those of Semantics/Tense/Perspective.lean.
• Before is the extensional one of the main text, and the contextual restrictor of the quantificational past is left out, as in the paper's own derivations.
• The Stump effect is the entailment the paper identifies, that the matrix event ends before the embedded one does, and not a pragmatic principle that rules the sentence out.
• The simultaneous readings of attitude reports are those of Studies/Sharvit2003.lean, and the examples are the rows of Data.Examples.Sharvit2014.

TODO

• Modern Greek and the two Spanish varieties need a mood parameter and a language whose past and present differ in kind, which the parameters here cannot express.
• The intensional before of the appendix, the relative-clause analysis and Geis ambiguities, and the behaviour of the present in relative clauses are not formalized.

References

• [Sha14]
• [Sha03]
• [BC03]
• [Par73]
• [Pri67]
• [Stu85]
• [OS12]

The earliest time and before

def Sharvit2014.IsEarliest {M : Type u_1} [LinearOrder M] (C : NonemptyInterval M) (P : Set (NonemptyInterval M)) (m : M) : Prop

IsEarliest C P m says that m is the leftmost moment of the intervals of P within C, the EARLIEST of (23).

Equations

• Sharvit2014.IsEarliest C P m = IsLeast (Tense.timeTrace (P ∩ Set.Iic C)) m

theorem Sharvit2014.IsEarliest.fst_le {M : Type u_1} [LinearOrder M] {C : NonemptyInterval M} {P : Set (NonemptyInterval M)} {m : M} (h : IsEarliest C P m) : C.toProd.1 ≤ m

theorem Sharvit2014.IsEarliest.le_of_mem {M : Type u_1} [LinearOrder M] {C t : NonemptyInterval M} {P : Set (NonemptyInterval M)} {m : M} (h : IsEarliest C P m) (ht : t ∈ P) (htC : t ≤ C) {a : M} (ha : a ∈ t) : m ≤ a

theorem Sharvit2014.IsEarliest.eq_fst_of_mem {M : Type u_1} [LinearOrder M] {C : NonemptyInterval M} {P : Set (NonemptyInterval M)} {m : M} (h : IsEarliest C P m) (hC : C ∈ P) : m = C.toProd.1

Where the interval C itself is among the times of the clause, the earliest moment is the start of C.

theorem Sharvit2014.isEarliest_fst_of_subset_singleton {M : Type u_1} [LinearOrder M] {C d : NonemptyInterval M} {P : Set (NonemptyInterval M)} (hd : d ∈ P) (hP : P ⊆ {d}) (hdC : d ≤ C) : IsEarliest C P d.toProd.1

A clause with one time d, within C, has the start of d as its earliest moment.

def Sharvit2014.BeforeDefined {M : Type u_1} [LinearOrder M] (C : NonemptyInterval M) (P : Set (NonemptyInterval M)) : Prop

Before (24) presupposes that its clause has an earliest moment within the contextually relevant interval C, later than the start of C.

Equations

• Sharvit2014.BeforeDefined C P = ∃ (m : M), Sharvit2014.IsEarliest C P m ∧ C.toProd.1 < m

theorem Sharvit2014.IsEarliest.eq_fst_of_diamond {M : Type u_1} [LinearOrder M] {C : NonemptyInterval M} {q : Set (NonemptyInterval M)} {m : M} [DenselyOrdered M] {c : Finset Ordering} (h : IsEarliest C {t : NonemptyInterval M | ModalLogic.Diamond (Tense.Perspective.toSetRel c) (fun (x : NonemptyInterval M) => x ∈ q) t} m) : m = C.toProd.1

On dense time, the earliest moment of a clause with an existentially quantified tense is the start of the contextually relevant interval, whatever the cell of the tense. A clause time that follows a time of the predicate can be started later, one that overlaps it can be widened to the whole interval, and one that precedes it can be started at the start of the interval.

theorem Sharvit2014.not_beforeDefined_diamond {M : Type u_1} [LinearOrder M] {C : NonemptyInterval M} {q : Set (NonemptyInterval M)} [DenselyOrdered M] {c : Finset Ordering} : ¬BeforeDefined C {t : NonemptyInterval M | ModalLogic.Diamond (Tense.Perspective.toSetRel c) (fun (x : NonemptyInterval M) => x ∈ q) t}

On dense time a clause with an existentially quantified tense never satisfies the presupposition of before, the inherent presupposition failure of (27).

Tensed clauses under before

def Sharvit2014.cell : Sharvit2003.Embedded → Finset Ordering

The cell of an embedded tense.

Equations

• Sharvit2014.cell Sharvit2003.Embedded.past = Semantics.Denotes.denote Tense.past
• Sharvit2014.cell Sharvit2003.Embedded.present = Semantics.Denotes.denote Tense.present

inductive Sharvit2014.Reading : Type

The readings of a tensed clause that is the complement of before.

• pronominal (τ : Sharvit2003.Embedded) : Reading

  A pronominal tense whose referential index before binds and whose evaluation index is free, hence the speech time, as in (35) and (37).

• existential (τ : Sharvit2003.Embedded) : Reading

  A quantificational tense (34), or a pronominal one whose evaluation index before binds and whose referential index is existentially closed (42).

• null : Reading

  A tense with no meaning of its own, whether deleted by the sequence-of-tense rule (56), a null present (36), or a present with both indices bound by before (44).

@[instance_reducible]

instance Sharvit2014.instDecidableEqReading : DecidableEq Reading

Equations

• Sharvit2014.instDecidableEqReading = Sharvit2014.instDecidableEqReading.decEq

def Sharvit2014.instDecidableEqReading.decEq (x✝ x✝¹ : Reading) : Decidable (x✝ = x✝¹)

Equations

• Sharvit2014.instDecidableEqReading.decEq (Sharvit2014.Reading.pronominal a) (Sharvit2014.Reading.pronominal b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Sharvit2014.instDecidableEqReading.decEq (Sharvit2014.Reading.pronominal τ) (Sharvit2014.Reading.existential τ_1) = isFalse ⋯
• Sharvit2014.instDecidableEqReading.decEq (Sharvit2014.Reading.pronominal τ) Sharvit2014.Reading.null = isFalse ⋯
• Sharvit2014.instDecidableEqReading.decEq (Sharvit2014.Reading.existential τ) (Sharvit2014.Reading.pronominal τ_1) = isFalse ⋯
• Sharvit2014.instDecidableEqReading.decEq (Sharvit2014.Reading.existential a) (Sharvit2014.Reading.existential b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Sharvit2014.instDecidableEqReading.decEq (Sharvit2014.Reading.existential τ) Sharvit2014.Reading.null = isFalse ⋯
• Sharvit2014.instDecidableEqReading.decEq Sharvit2014.Reading.null (Sharvit2014.Reading.pronominal τ) = isFalse ⋯
• Sharvit2014.instDecidableEqReading.decEq Sharvit2014.Reading.null (Sharvit2014.Reading.existential τ) = isFalse ⋯
• Sharvit2014.instDecidableEqReading.decEq Sharvit2014.Reading.null Sharvit2014.Reading.null = isTrue ⋯

@[instance_reducible]

instance Sharvit2014.instFintypeReading : Fintype Reading

Equations

• Sharvit2014.instFintypeReading = Fintype.ofEquiv (Sharvit2003.Embedded ⊕ Sharvit2003.Embedded ⊕ Unit) Sharvit2014.Reading.proxyTypeEquiv

def Sharvit2014.Reading.denote {M : Type u_1} [LinearOrder M] (SP : NonemptyInterval M) (q : Set (NonemptyInterval M)) : Reading → Set (NonemptyInterval M)

The times a clause holds at on a reading, with q the times of its predicate and SP the speech time.

Equations

• One or more equations did not get rendered due to their size.
• Sharvit2014.Reading.denote SP q (Sharvit2014.Reading.pronominal a) = {t : NonemptyInterval M | Tense.Perspective.Presup (Sharvit2014.cell a) SP t ∧ t ∈ q}
• Sharvit2014.Reading.denote SP q Sharvit2014.Reading.null = q

def Sharvit2014.clause {M : Type u_1} [LinearOrder M] (τ : Sharvit2003.Embedded) (j k : ℕ) (q : Set (NonemptyInterval M)) : Assignment (NonemptyInterval M) → Prop

A clause whose verb takes the pronominal tense τ with evaluation index j and referential index k, as in (30a), says that the time of k stands to the time of j as the tense requires and that the predicate holds at it.

Equations

• Sharvit2014.clause τ j k q g = (Tense.Perspective.Presup (Sharvit2014.cell τ) (g j) (g k) ∧ g k ∈ q)

theorem Sharvit2014.lambdaAbsG_clause {M : Type u_1} [LinearOrder M] {q : Set (NonemptyInterval M)} {τ : Sharvit2003.Embedded} {j k : ℕ} {g : Assignment (NonemptyInterval M)} (hjk : j ≠ k) : {t : NonemptyInterval M | HeimKratzer.lambdaAbsG k (clause τ j k q) g t} = Reading.denote (g j) q (Reading.pronominal τ)

Abstraction over the referential index gives the pronominal reading at the time of the evaluation index.

theorem Sharvit2014.lambdaAbsG_exists_clause {M : Type u_1} [LinearOrder M] {SP : NonemptyInterval M} {q : Set (NonemptyInterval M)} {τ : Sharvit2003.Embedded} {j k : ℕ} {g : Assignment (NonemptyInterval M)} (hjk : j ≠ k) : {t : NonemptyInterval M | HeimKratzer.lambdaAbsG j (fun (g : Assignment (NonemptyInterval M)) => ∃ (t' : NonemptyInterval M), HeimKratzer.lambdaAbsG k (clause τ j k q) g t') g t} = Reading.denote SP q (Reading.existential τ)

Existential closure of the referential index under abstraction over the evaluation index gives the existential reading.

theorem Sharvit2014.lambdaAbsG_clause_self {M : Type u_1} [LinearOrder M] {SP : NonemptyInterval M} {q : Set (NonemptyInterval M)} {k : ℕ} {g : Assignment (NonemptyInterval M)} : {t : NonemptyInterval M | HeimKratzer.lambdaAbsG k (clause Sharvit2003.Embedded.present k k q) g t} = Reading.denote SP q Reading.null

A present with both indices bound by one binder has no meaning of its own.

def Sharvit2014.Reading.Fails (r : Reading) : Prop

A reading fails when on dense time its clause never satisfies the presupposition of before, the paper's inherent presupposition failure.

Equations

• r.Fails = ∀ (M : Type) [inst : LinearOrder M] [DenselyOrdered M] (C SP : NonemptyInterval M) (q : Set (NonemptyInterval M)), ¬Sharvit2014.BeforeDefined C (Sharvit2014.Reading.denote SP q r)

def Sharvit2014.Reading.StumpEffect (r : Reading) : Prop

A reading has the Stump effect when every past time ends before each time of the clause does, so that the order of the two events follows from the tenses alone.

Equations

• r.StumpEffect = ∀ (M : Type) [inst : LinearOrder M] (SP t d : NonemptyInterval M) (q : Set (NonemptyInterval M)), t.Precedes SP → d ∈ Sharvit2014.Reading.denote SP q r → t.toProd.2 < d.toProd.2

def Sharvit2014.Reading.NoPShiftability (r : Reading) : Prop

A reading has no p-shiftability when the earliest time of the clause precedes the speech time.

Equations

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

theorem Sharvit2014.Reading.fails_iff {r : Reading} : r.Fails ↔ ∃ (τ : Sharvit2003.Embedded), r = existential τ

The existential readings are the ones that fail.

theorem Sharvit2014.Reading.stumpEffect_iff {r : Reading} : r.StumpEffect ↔ r = pronominal Sharvit2003.Embedded.present

The pronominal present is the reading with the Stump effect.

theorem Sharvit2014.Reading.noPShiftability_pronominal_past : (pronominal Sharvit2003.Embedded.past).NoPShiftability

The pronominal past has no p-shiftability, its earliest time preceding the speech time (35).

theorem Sharvit2014.Reading.not_noPShiftability_null : ¬null.NoPShiftability

A tense with no meaning of its own is p-shiftable, in that the earliest time of its clause may follow the speech time (36).

def Sharvit2014.Reading.Felicitous (r : Reading) : Prop

A reading is felicitous when it neither fails nor has the Stump effect.

Equations

• r.Felicitous = (¬r.Fails ∧ ¬r.StumpEffect)

theorem Sharvit2014.Reading.felicitous_iff {r : Reading} : r.Felicitous ↔ r = pronominal Sharvit2003.Embedded.past ∨ r = null

The felicitous readings are the pronominal past and the tense with no meaning.

Languages

inductive Sharvit2014.Shiftability : Type

The shiftability of a present tense (71) says whether its evaluation index must be free, may be bound though not by the binder of its referential index, or may be bound freely.

• non : Shiftability
• semi : Shiftability
• full : Shiftability

@[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.instFintypeShiftability : Fintype Shiftability

Equations

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

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

Equations

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

@[instance_reducible]

instance Sharvit2014.instReprShiftability : Repr Shiftability

Equations

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

structure Sharvit2014.Language : Type

A language's tense parameters say whether it has the sequence-of-tense rule, how shiftable its present is, and whether it has pronominal and quantificational tenses.

• sot : Bool

  The language has the sequence-of-tense rule.

• present : Shiftability

  The shiftability of the present.

• pronominal : Bool

  The language has pronominal tenses.

• quantificational : Bool

  The language has quantificational tenses.

@[instance_reducible]

instance Sharvit2014.instDecidableEqLanguage : DecidableEq Language

Equations

• Sharvit2014.instDecidableEqLanguage = Sharvit2014.instDecidableEqLanguage.decEq

def Sharvit2014.instDecidableEqLanguage.decEq (x✝ x✝¹ : Language) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Sharvit2014.instFintypeLanguage : Fintype Language

Equations

• Sharvit2014.instFintypeLanguage = Fintype.ofEquiv ((_ : Bool) × (_ : Sharvit2014.Shiftability) × (_ : Bool) × Bool) Sharvit2014.Language.proxyTypeEquiv

@[instance_reducible]

instance Sharvit2014.instReprLanguage : Repr Language

Equations

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

def Sharvit2014.instReprLanguage.repr : Language → ℕ → Std.Format

Equations

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

def Sharvit2014.Language.HasExistential (L : Language) : Sharvit2003.Embedded → Prop

A language gives a tense in a before-clause its existential reading when the tense is a quantificational past (34), a pronominal past, whose evaluation index may always be bound (42b), or a pronominal present whose evaluation index may be bound (69b).

Equations

• L.HasExistential Sharvit2003.Embedded.past = (L.pronominal = true ∨ L.quantificational = true)
• L.HasExistential Sharvit2003.Embedded.present = (L.pronominal = true ∧ L.present ≠ Sharvit2014.Shiftability.non)

def Sharvit2014.Language.HasNull (L : Language) : Sharvit2003.Embedded → Prop

A language gives a tense in a before-clause no meaning of its own when the tense is a past that a quantificational matrix past raises above and deletes (56), since a pronominal matrix past does not raise (60), or a fully shiftable present, null if quantificational (36) and with both indices bound by before if pronominal (44).

Equations

• L.HasNull Sharvit2003.Embedded.past = (L.quantificational = true ∧ L.sot = true)
• L.HasNull Sharvit2003.Embedded.present = ((L.pronominal = true ∨ L.quantificational = true) ∧ L.present = Sharvit2014.Shiftability.full)

@[instance_reducible]

instance Sharvit2014.Language.instDecidablePredEmbeddedHasNull (L : Language) : DecidablePred L.HasNull

Equations

• One or more equations did not get rendered due to their size.
• L.instDecidablePredEmbeddedHasNull Sharvit2003.Embedded.past = { decide := decide (L.quantificational = true) && decide (L.sot = true), reflects_decide := ⋯ }

def Sharvit2014.Language.Available (L : Language) (τ : Sharvit2003.Embedded) : Reading → Prop

The readings a language's grammar gives the tense τ of a before-clause under a past.

Equations

• L.Available τ (Sharvit2014.Reading.pronominal a) = (a = τ ∧ L.pronominal = true)
• L.Available τ (Sharvit2014.Reading.existential a) = (a = τ ∧ L.HasExistential τ)
• L.Available τ Sharvit2014.Reading.null = L.HasNull τ

def Sharvit2014.Language.WellFormed (L : Language) (τ : Sharvit2003.Embedded) : Prop

The tense τ is well-formed in a before-clause under a past when it has a felicitous reading there.

Equations

• L.WellFormed τ = ∃ (r : Sharvit2014.Reading), L.Available τ r ∧ r.Felicitous

def Sharvit2014.Language.PShiftable (L : Language) (τ : Sharvit2003.Embedded) : Prop

A before-clause in the tense τ is p-shiftable when a felicitous reading lets its time follow the speech time.

Equations

• L.PShiftable τ = ∃ (r : Sharvit2014.Reading), L.Available τ r ∧ r.Felicitous ∧ ¬r.NoPShiftability

def Sharvit2014.Language.NoPShiftability (L : Language) (τ : Sharvit2003.Embedded) : Prop

A before-clause in the tense τ has no p-shiftability when it is well-formed and its time precedes the speech time on every felicitous reading.

Equations

• L.NoPShiftability τ = (L.WellFormed τ ∧ ∀ (r : Sharvit2014.Reading), L.Available τ r → r.Felicitous → r.NoPShiftability)

theorem Sharvit2014.Language.wellFormed_iff {L : Language} {τ : Sharvit2003.Embedded} : L.WellFormed τ ↔ τ = Sharvit2003.Embedded.past ∧ L.pronominal = true ∨ L.HasNull τ

theorem Sharvit2014.Language.pShiftable_iff {L : Language} {τ : Sharvit2003.Embedded} : L.PShiftable τ ↔ L.HasNull τ

@[instance_reducible]

instance Sharvit2014.Language.instDecidableWellFormed {L : Language} {τ : Sharvit2003.Embedded} : Decidable (L.WellFormed τ)

Equations

• Sharvit2014.Language.instDecidableWellFormed = decidable_of_iff (τ = Sharvit2003.Embedded.past ∧ L.pronominal = true ∨ L.HasNull τ) ⋯

@[instance_reducible]

instance Sharvit2014.Language.instDecidablePShiftable {L : Language} {τ : Sharvit2003.Embedded} : Decidable (L.PShiftable τ)

Equations

• Sharvit2014.Language.instDecidablePShiftable = decidable_of_iff (L.HasNull τ) ⋯

theorem Sharvit2014.Language.noPShiftability_iff {L : Language} {τ : Sharvit2003.Embedded} : L.NoPShiftability τ ↔ L.WellFormed τ ∧ ¬L.PShiftable τ

A well-formed clause has no p-shiftability exactly when it is not p-shiftable.

def Sharvit2014.Language.toSharvit2003 (L : Language) : Sharvit2003.Language

The language as a type of Sharvit's earlier typology, which has the sequence-of-tense rule and whether the present may be bound.

Equations

• L.toSharvit2003 = { sotRule := L.sot, present := if L.present = Sharvit2014.Shiftability.non then Sharvit2003.PresentTense.matrixIndexical else Sharvit2003.PresentTense.bindable }

def Sharvit2014.Language.Simultaneous (L : Language) (τ : Sharvit2003.Embedded) : Prop

The tense τ under a past attitude verb has a simultaneous reading, a past where the sequence-of-tense rule deletes it and a present where its evaluation index may be bound.

Equations

• L.Simultaneous τ = Sharvit2003.NonpastAvailable L.toSharvit2003 τ

@[instance_reducible]

instance Sharvit2014.Language.instDecidableSimultaneous (L : Language) (τ : Sharvit2003.Embedded) : Decidable (L.Simultaneous τ)

Equations

• L.instDecidableSimultaneous τ = Sharvit2014.Language.instDecidableSimultaneous._aux_1 L τ

theorem Sharvit2014.Language.simultaneous_past_iff {L : Language} : L.Simultaneous Sharvit2003.Embedded.past ↔ L.sot = true

English, Japanese and Polish

def Sharvit2014.english : Language

English has the sequence-of-tense rule, a present that cannot be bound, and pronominal tenses.

Equations

• Sharvit2014.english = { sot := true, present := Sharvit2014.Shiftability.non, pronominal := true, quantificational := false }

def Sharvit2014.japanese : Language

Japanese has no sequence-of-tense rule, a fully shiftable present, and quantificational tenses.

Equations

• Sharvit2014.japanese = { sot := false, present := Sharvit2014.Shiftability.full, pronominal := false, quantificational := true }

def Sharvit2014.polish : Language

Polish has no sequence-of-tense rule, a semi-shiftable present, and pronominal tenses.

Equations

• Sharvit2014.polish = { sot := false, present := Sharvit2014.Shiftability.semi, pronominal := true, quantificational := false }

theorem Sharvit2014.toSharvit2003_eq : english.toSharvit2003 = Sharvit2003.english ∧ japanese.toSharvit2003 = Sharvit2003.hebrew ∧ polish.toSharvit2003 = Sharvit2003.hebrew

In attitude reports English is the first type of the earlier typology, and Japanese and Polish the second, with Hebrew.

theorem Sharvit2014.japanese_past_fails {r : Reading} (h : japanese.Available Sharvit2003.Embedded.past r) : r.Fails

A Japanese past in a before-clause has only a reading that fails (34).

theorem Sharvit2014.english_present_stumpEffect {r : Reading} (h : english.Available Sharvit2003.Embedded.present r) : r.StumpEffect

An English present in a before-clause has only the reading with the Stump effect (37).

theorem Sharvit2014.polish_present_fails_or_stumpEffect {r : Reading} (h : polish.Available Sharvit2003.Embedded.present r) : r.Fails ∨ r.StumpEffect

A Polish present in a before-clause has the reading with the Stump effect and, with its evaluation index bound, a reading that fails (69b).

def Sharvit2014.languages : List (String × Language)

The languages of the example rows.

Equations

• Sharvit2014.languages = [("stan1293", Sharvit2014.english), ("nucl1643", Sharvit2014.japanese), ("poli1260", Sharvit2014.polish)]

def Sharvit2014.tenses : List (String × Sharvit2003.Embedded)

The embedded tenses of the example rows.

Equations

• Sharvit2014.tenses = [("past", Sharvit2003.Embedded.past), ("present", Sharvit2003.Embedded.present)]

theorem Sharvit2014.judgment_iff (e : Datum) : e ∈ Examples.all → e.language ≠ "mode1248" → e.feature? "construction" = some "before" → e.feature? "clauseTime" ≠ some "after speech" → ∃ L ∈ List.lookup e.language languages, ∃ τ ∈ e.parse? "embedded" tenses, e.judgment = Judgment.acceptable ↔ L.WellFormed τ

A tense in a before-clause under a past is acceptable exactly where the language's parameters make it well-formed.

theorem Sharvit2014.clauseTime_iff (e : Datum) : e ∈ Examples.all → e.feature? "clauseTime" = some "after speech" → ∃ L ∈ List.lookup e.language languages, ∃ τ ∈ e.parse? "embedded" tenses, e.judgment = Judgment.acceptable ↔ L.PShiftable τ

A before-clause whose time follows the speech time is acceptable exactly where the language's parameters make the clause p-shiftable.

theorem Sharvit2014.simultaneous_iff (e : Datum) : e ∈ Examples.all → e.language ≠ "mode1248" → e.feature? "construction" = some "attitude" → ∃ L ∈ List.lookup e.language languages, ∃ τ ∈ e.parse? "embedded" tenses, List.lookup "simultaneous" e.readings = some Judgment.acceptable ↔ L.Simultaneous τ

A tense under a past attitude verb has a simultaneous reading exactly where the language's parameters give it one.

Permissible languages

def Sharvit2014.Language.Permissible (L : Language) : Prop

A language is permissible when it has tenses of exactly one kind and meets the Embeddability Principle for attitude reports, having the sequence-of-tense rule or a present that may be bound.

Equations

• L.Permissible = ((L.pronominal = true ∨ L.quantificational = true) ∧ ¬(L.pronominal = true ∧ L.quantificational = true) ∧ Sharvit2003.EmbeddabilityPrinciple L.toSharvit2003)

@[instance_reducible]

instance Sharvit2014.Language.instDecidablePermissible (L : Language) : Decidable L.Permissible

Equations

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

def Sharvit2014.Language.row (L : Language) : ℕ

The number of a language's type in the table of language types (98), which lists the sixteen settings of the sequence-of-tense rule, a shiftable present, pronominal tenses and quantificational tenses.

Equations

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

theorem Sharvit2014.Language.permissible_iff (L : Language) : L.Permissible ↔ L.row ∈ {2, 3, 6, 7, 10, 11}

The permissible types are six of the sixteen.

theorem Sharvit2014.Language.permissible_without_economy_iff (L : Language) : (L.pronominal = true ∨ L.quantificational = true) ∧ Sharvit2003.EmbeddabilityPrinciple L.toSharvit2003 ↔ L.row ∈ {1, 2, 3, 5, 6, 7, 9, 10, 11}

A language that may have tenses of both kinds is of one of nine types.

theorem Sharvit2014.Language.wellFormed_past_or_present_iff {L : Language} : L.WellFormed Sharvit2003.Embedded.past ∨ L.WellFormed Sharvit2003.Embedded.present ↔ L.pronominal = true ∨ L.quantificational = true ∧ (L.sot = true ∨ L.present = Shiftability.full)

By the Embeddability Principle for before, some tense is well-formed in a before-clause under a past, which holds unless the language has only quantificational tenses, no sequence-of-tense rule and no fully shiftable present.

theorem Sharvit2014.row_eq : english.row = 6 ∧ polish.row = 10 ∧ japanese.row = 11

English, Polish and Japanese are of the sixth, tenth and eleventh type.

theorem Sharvit2014.semiShiftable_quantificational : (have __src := japanese; { sot := __src.sot, present := Shiftability.semi, pronominal := __src.pronominal, quantificational := __src.quantificational }).Permissible ∧ ¬(have __src := japanese; { sot := __src.sot, present := Shiftability.semi, pronominal := __src.pronominal, quantificational := __src.quantificational }).WellFormed Sharvit2003.Embedded.past ∧ ¬(have __src := japanese; { sot := __src.sot, present := Shiftability.semi, pronominal := __src.pronominal, quantificational := __src.quantificational }).WellFormed Sharvit2003.Embedded.present

A language like Japanese but with a semi-shiftable present is of a permissible type and has no well-formed tense in a before-clause under a past, so a quantificational present is fully shiftable.

Predictions

theorem Sharvit2014.pShiftable_present_of_wellFormed {L : Language} (h : L.WellFormed Sharvit2003.Embedded.present) : L.PShiftable Sharvit2003.Embedded.present

A language with a well-formed present in before-clauses under a past has p-shiftability there (99a), since the present is then fully shiftable.

theorem Sharvit2014.simultaneous_past_of_pShiftable {L : Language} (h : L.PShiftable Sharvit2003.Embedded.past) : L.Simultaneous Sharvit2003.Embedded.past

A language with p-shiftability in past before-clauses under a past has simultaneous readings of a past under a past attitude verb (99b), since the embedded past is then deleted by the sequence-of-tense rule.

theorem Sharvit2014.noPShiftability_past_of_not_simultaneous {L : Language} (hw : L.WellFormed Sharvit2003.Embedded.past) (hs : ¬L.Simultaneous Sharvit2003.Embedded.past) : L.NoPShiftability Sharvit2003.Embedded.past

A language with a well-formed past in before-clauses under a past and no simultaneous reading of a past under a past attitude verb has no p-shiftability there (99c), since the past of the before-clause is then pronominal.

theorem Sharvit2014.wellFormed_past_of_simultaneous {L : Language} (ht : L.pronominal = true ∨ L.quantificational = true) (h : L.Simultaneous Sharvit2003.Embedded.past) : L.WellFormed Sharvit2003.Embedded.past

A language with tenses and a simultaneous reading of a past under a past attitude verb has a well-formed past in before-clauses under a past, since a past that the sequence-of-tense rule can delete is either pronominal or deleted there too (102).

theorem Sharvit2014.not_exists_modernGreek : ¬∃ (L : Language), (L.pronominal = true ∨ L.quantificational = true) ∧ (List.lookup "simultaneous" Examples.ex_104.readings = some Judgment.acceptable ↔ L.Simultaneous Sharvit2003.Embedded.past) ∧ (Examples.ex_103.judgment = Judgment.acceptable ↔ L.WellFormed Sharvit2003.Embedded.past)

Modern Greek has the simultaneous reading (104) and no past in before-clauses (103), so no setting of the parameters gives its judgments.