Sharvit (2003): Embedded Tense and Universal Grammar

Sharvit derives a tense typology from two parameters. Under the Deletion Theory of Ogihara and von Stechow, an SOT language deletes an embedded tense under agreement with a c-commanding attitude tense, leaving a bound zero tense, Heim's relative now; after Schlenker, matrix indexicality decides whether a present under a past must refer to the utterance time. English deletes and has an indexical present, Hebrew does neither, Modern Greek deletes and has a bindable present, and the fourth type is unattested, as the Embeddability Principle (13) predicts: every matrix LF needs a content-matching λ0-abstract embeddable under an attitude verb, and the fourth type has no source of zero tense.

Main results

• embeddabilityPrinciple_iff: a language meets the principle iff it provides a zero tense.
• boundPresent_nonpast, indexicalPresent_no_nonpast, not_doubleAccess_of_short: the readings of a bound and of an indexical present.
• lf7_iff: the LF (7) of the nonpast reading of (1) denotes (10).
• nonpast_rows: the typology predicts the nonpast readings of (1)–(6) and (12).

Implementation notes

• The semantic half of the Embeddability Principle (15) is met by the matrix LF's own λ0-abstract, so EmbeddabilityPrinciple states its syntactic force, that the language can spell out the abstract's free zero tense.
• The classification of the three languages is the paper's and lives in the study; the person-domain extension and free indirect discourse (§3) are not formalized.

References

• [Sha03]
• [Ogi96]
• [vS95]
• [Hei94a]
• [Sch99a]
• [Abu97]

The typology (11)

inductive Sharvit2003.PresentTense : Type

Whether a language's present-tense morpheme is a matrix indexical, obligatorily referring to the utterance time in present-under-past sentences, or may be interpreted as a bound variable.

• matrixIndexical : PresentTense
• bindable : PresentTense

@[instance_reducible]

instance Sharvit2003.instDecidableEqPresentTense : DecidableEq PresentTense

Equations

• Sharvit2003.instDecidableEqPresentTense x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Sharvit2003.instReprPresentTense.repr : PresentTense → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Sharvit2003.instReprPresentTense : Repr PresentTense

Equations

• Sharvit2003.instReprPresentTense = { reprPrec := Sharvit2003.instReprPresentTense.repr }

structure Sharvit2003.Language : Type

A language type of the Deletion Theory (11) is given by whether it has the SOT rule, which deletes a tense under agreement and interprets it as a bound zero tense, and by the indexicality of its present.

• sotRule : Bool

  The language has the SOT rule.

• present : PresentTense

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

Equations

• Sharvit2003.instDecidableEqLanguage.decEq { sotRule := a, present := a_1 } { sotRule := b, present := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance Sharvit2003.instDecidableEqLanguage : DecidableEq Language

Equations

• Sharvit2003.instDecidableEqLanguage = Sharvit2003.instDecidableEqLanguage.decEq

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

Equations

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

@[instance_reducible]

instance Sharvit2003.instReprLanguage : Repr Language

Equations

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

def Sharvit2003.english : Language

English, type 1, has the SOT rule and a matrix-indexical present.

Equations

• Sharvit2003.english = { sotRule := true, present := Sharvit2003.PresentTense.matrixIndexical }

def Sharvit2003.hebrew : Language

Hebrew, type 2, has no SOT rule and a bindable present.

Equations

• Sharvit2003.hebrew = { sotRule := false, present := Sharvit2003.PresentTense.bindable }

def Sharvit2003.greek : Language

Modern Greek, type 3, has the SOT rule and a bindable present.

Equations

• Sharvit2003.greek = { sotRule := true, present := Sharvit2003.PresentTense.bindable }

def Sharvit2003.type4 : Language

The unattested type 4 has no SOT rule and a matrix-indexical present.

Equations

• Sharvit2003.type4 = { sotRule := false, present := Sharvit2003.PresentTense.matrixIndexical }

Zero tense and the Embeddability Principle

inductive Sharvit2003.ZeroTense : Type

The sources of a bound zero tense in a complement clause are a tense deleted under agreement by the SOT rule and a present morpheme interpreted as a bound variable.

• deleted : ZeroTense
• boundPresent : ZeroTense

@[instance_reducible]

instance Sharvit2003.instDecidableEqZeroTense : DecidableEq ZeroTense

Equations

• Sharvit2003.instDecidableEqZeroTense x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Sharvit2003.instReprZeroTense : Repr ZeroTense

Equations

• Sharvit2003.instReprZeroTense = { reprPrec := Sharvit2003.instReprZeroTense.repr }

def Sharvit2003.instReprZeroTense.repr : ZeroTense → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Sharvit2003.instFintypeZeroTense : Fintype ZeroTense

Equations

• Sharvit2003.instFintypeZeroTense = { elems := { val := ↑Sharvit2003.ZeroTense.enumList, nodup := Sharvit2003.ZeroTense.enumList_nodup }, complete := Sharvit2003.instFintypeZeroTense._proof_1 }

def Sharvit2003.Language.Provides (L : Language) : ZeroTense → Prop

A language provides a source of zero tense when it has what the source needs, the SOT rule for deletion and a present morpheme that is not a matrix indexical for a bound present.

Equations

• L.Provides Sharvit2003.ZeroTense.deleted = (L.sotRule = true)
• L.Provides Sharvit2003.ZeroTense.boundPresent = (L.present = Sharvit2003.PresentTense.bindable)

@[instance_reducible]

instance Sharvit2003.instDecidablePredZeroTenseProvides (L : Language) : DecidablePred L.Provides

Equations

• Sharvit2003.instDecidablePredZeroTenseProvides L Sharvit2003.ZeroTense.deleted = Sharvit2003.instDecidablePredZeroTenseProvides._aux_1 L
• Sharvit2003.instDecidablePredZeroTenseProvides L Sharvit2003.ZeroTense.boundPresent = Sharvit2003.instDecidablePredZeroTenseProvides._aux_3 L

def Sharvit2003.EmbeddabilityPrinciple (L : Language) : Prop

The Embeddability Principle (13), as a condition on a language, says that some source of zero tense is available, so that every well-formed matrix LF has a content-matching λ0-abstract that can be embedded under an attitude verb carrying past or present.

Equations

• Sharvit2003.EmbeddabilityPrinciple L = ∃ (z : Sharvit2003.ZeroTense), L.Provides z

@[instance_reducible]

instance Sharvit2003.instDecidableEmbeddabilityPrinciple (L : Language) : Decidable (EmbeddabilityPrinciple L)

Equations

• Sharvit2003.instDecidableEmbeddabilityPrinciple L = { decide := decide (∃ a ∈ Finset.univ, L.Provides a), reflects_decide := ⋯ }

theorem Sharvit2003.embeddabilityPrinciple_iff (L : Language) : EmbeddabilityPrinciple L ↔ L ≠ type4

Exactly type 4 violates the Embeddability Principle.

theorem Sharvit2003.attested_types : english.Provides ZeroTense.deleted ∧ hebrew.Provides ZeroTense.boundPresent ∧ greek.Provides ZeroTense.deleted ∧ greek.Provides ZeroTense.boundPresent

English embeds Mary is pregnant by deleting a tense, Hebrew by binding its present, and Modern Greek either way.

The readings

The nonpast reading of past under past is the simultaneous reading of a deleted tense; the nonpast reading of present under past is the binding of the present morpheme.

inductive Sharvit2003.Embedded : Type

The morpheme embedded under the past attitude verb.

• past : Embedded
• present : Embedded

@[instance_reducible]

instance Sharvit2003.instDecidableEqEmbedded : DecidableEq Embedded

Equations

• Sharvit2003.instDecidableEqEmbedded x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Sharvit2003.instReprEmbedded : Repr Embedded

Equations

• Sharvit2003.instReprEmbedded = { reprPrec := Sharvit2003.instReprEmbedded.repr }

def Sharvit2003.instReprEmbedded.repr : Embedded → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Sharvit2003.instReprEmbedded.repr Sharvit2003.Embedded.past prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sharvit2003.Embedded.past")).group prec✝

@[instance_reducible]

instance Sharvit2003.instFintypeEmbedded : Fintype Embedded

Equations

• Sharvit2003.instFintypeEmbedded = { elems := { val := ↑Sharvit2003.Embedded.enumList, nodup := Sharvit2003.Embedded.enumList_nodup }, complete := Sharvit2003.instFintypeEmbedded._proof_1 }

def Sharvit2003.NonpastAvailable (L : Language) : Embedded → Prop

The nonpast reading is available for an embedded past exactly when the SOT rule licenses the simultaneous reading (Tense.pastUnderPast), and for an embedded present exactly when the present can be bound.

Equations

• Sharvit2003.NonpastAvailable L Sharvit2003.Embedded.past = (Ordering.eq ∈ Tense.pastUnderPast (L.sotRule = true))
• Sharvit2003.NonpastAvailable L Sharvit2003.Embedded.present = L.Provides Sharvit2003.ZeroTense.boundPresent

@[instance_reducible]

instance Sharvit2003.instDecidablePredEmbeddedNonpastAvailable (L : Language) : DecidablePred (NonpastAvailable L)

Equations

• Sharvit2003.instDecidablePredEmbeddedNonpastAvailable L Sharvit2003.Embedded.past = Sharvit2003.instDecidablePredEmbeddedNonpastAvailable._aux_1 L
• Sharvit2003.instDecidablePredEmbeddedNonpastAvailable L Sharvit2003.Embedded.present = Sharvit2003.instDecidablePredEmbeddedNonpastAvailable._aux_3 L

theorem Sharvit2003.nonpastAvailable_past_iff (L : Language) : NonpastAvailable L Embedded.past ↔ L.Provides ZeroTense.deleted

The simultaneous reading of a deleted tense is available exactly in languages with the SOT rule, since the two parameters of the typology are the two sources of zero tense.

theorem Sharvit2003.boundPresent_nonpast {T : Type u_1} {W : Type u_2} [LinearOrder T] (n e : ℕ) (g : Assignment T) (now : T) (w : W) : (Tense.pronoun (Semantics.Denotes.denote Tense.present) n e).presup (Function.update (Function.update g e now) n now) w

A bindable present bound by the attitude verb denotes the attitude's now, the time of its evaluation index, so its present presupposition holds there, which is the nonpast reading of (5) and (12a).

theorem Sharvit2003.indexicalPresent_no_nonpast {T : Type u_1} {W : Type u_2} [LinearOrder T] {n e : ℕ} {g : Assignment T} {w : W} (hSpeech : (Tense.pronoun (Semantics.Denotes.denote Tense.present) n 0).presup g w) (hlt : g e < g 0) : ¬(Tense.pronoun (Semantics.Denotes.denote Tense.present) n e).presup g w

A matrix-indexical present under a past attitude verb refers to the utterance time, the time of the index 0, which the attitude's earlier now cannot match, so its present presupposition fails at the attitude's now and (3) has only the double access reading.

theorem Sharvit2003.not_doubleAccess_of_short {T : Type u_1} [Sub T] [Preorder T] {I : Set T} {b u : T} (h : ∀ x ∈ I, ∀ y ∈ I, y - x < u - b) : ¬{b, u} ⊆ I

The double access reading of (4b) needs the pregnancy interval to contain both the finding out and the utterance time; an interval too short to span the two years between them cannot, hence the oddity.

The nonpast reading of (1) under the Deletion Theory

def Sharvit2003.attitude {T : Type u_1} (compatible : T → Set T) (p : T → Prop) (t : T) : Prop

By the entry (8) for decide and tell, the complement holds at every time compatible with what the holder decides or tells at t.

Equations

• Sharvit2003.attitude compatible p t = ∀ t' ∈ compatible t, p t'

def Sharvit2003.will {T : Type u_1} [LT T] (p : T → Prop) (t : T) : Prop

By the entry (9) for will, the complement holds at some later time, possibility along the relation of the future cell.

Equations

• Sharvit2003.will p t = ModalLogic.Diamond (Tense.toSetRel (Semantics.Denotes.denote Tense.future)) p t

def Sharvit2003.lf7 {T : Type u_1} [LT T] (decides tells : T → Set T) (miss : T → Prop) (g : Assignment T) : Prop

In the LF (7) of the nonpast reading of (1), the matrix past locates the deciding before the utterance time, the time of the index 0, and each complement is a λ0-abstract that rebinds the zero tense read by the deleted past on will, the base-generated zero tense on tell and the deleted past on miss.

Equations

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

theorem Sharvit2003.lf7_iff {T : Type u_1} [LT T] (decides tells : T → Set T) (miss : T → Prop) (g : Assignment T) : lf7 decides tells miss g ↔ ∃ t < g 0, ∀ t' ∈ decides t, ∃ (t'' : T), t' < t'' ∧ ∀ t''' ∈ tells t'', miss t'''

The LF (7) has the interpretation (10), that for every time compatible with what John decides at some time before the utterance time there is a later time at which he tells his mother, and he misses her at every time compatible with that telling.

The paper's examples

structure Sharvit2003.Row : Type

A row of the paper's data records the language, the embedded morpheme, and whether the nonpast reading is available.

• language : Language
• embedded : Embedded
• nonpast : Bool

@[instance_reducible]

instance Sharvit2003.instDecidableEqRow : DecidableEq Row

Equations

• Sharvit2003.instDecidableEqRow = Sharvit2003.instDecidableEqRow.decEq

def Sharvit2003.instDecidableEqRow.decEq (x✝ x✝¹ : Row) : Decidable (x✝ = x✝¹)

Equations

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

def Sharvit2003.instReprRow.repr : Row → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Sharvit2003.instReprRow : Repr Row

Equations

• Sharvit2003.instReprRow = { reprPrec := Sharvit2003.instReprRow.repr }

def Sharvit2003.Row.ofDatum (e : Datum) : Option Row

Read a row off an example's paper features.

Equations

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

def Sharvit2003.rows : List Row

The rows of (1)–(6) and (12).

Equations

• Sharvit2003.rows = List.filterMap Sharvit2003.Row.ofDatum Sharvit2003.Examples.all

theorem Sharvit2003.rows_complete (e : Datum) : e ∈ Examples.all → (Row.ofDatum e).isSome = true

Every example carries the three features.

theorem Sharvit2003.nonpast_rows (r : Row) : r ∈ rows → (r.nonpast = true ↔ NonpastAvailable r.language r.embedded)

The typology (11) predicts the paper's judgments, the nonpast reading being available exactly where the language provides a zero tense for the embedded morpheme.