@cite{ogihara-1996}: Tense, Attitudes, and Scope

@cite{ogihara-1989} @cite{ogihara-1996}

Ogihara's theory: embedded past is ambiguous between a genuine past reading and a zero-tense reading. Zero tense is a bound variable that receives the matrix event time, producing the simultaneous reading.

Core Mechanisms

1. Ambiguous past: past morphology has two semantic values:
   • Genuine past: temporal precedence (R < eval time)
   • Zero tense: bound variable with no independent temporal content
2. Zero tense = bound variable: receives binder time via lambda abstraction
3. SOT = zero tense: the simultaneous reading is the zero-tense reading

Key Distinction from Kratzer

• Ogihara: past IS semantically ambiguous (genuinePast vs zeroTense)
• Kratzer: past is NEVER ambiguous; simultaneous comes from deletion

Both make identical predictions for SOT phenomena, but they disagree about the source: ambiguity (Ogihara) vs deletion (Kratzer).

inductive Semantics.Tense.Ogihara.OgiharaPastReading : Type

Ogihara's two readings of past morphology in embedded contexts.

• genuinePast : OgiharaPastReading

  Genuine past: temporal precedence (R < eval time)

• zeroTense : OgiharaPastReading

  Zero tense: bound variable, no independent temporal content

instance Semantics.Tense.Ogihara.instDecidableEqOgiharaPastReading : DecidableEq OgiharaPastReading

Equations

• Semantics.Tense.Ogihara.instDecidableEqOgiharaPastReading x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Semantics.Tense.Ogihara.instReprOgiharaPastReading.repr : OgiharaPastReading → ℕ → Std.Format

Equations

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

instance Semantics.Tense.Ogihara.instReprOgiharaPastReading : Repr OgiharaPastReading

Equations

• Semantics.Tense.Ogihara.instReprOgiharaPastReading = { reprPrec := Semantics.Tense.Ogihara.instReprOgiharaPastReading.repr }

def Semantics.Tense.Ogihara.instBEqOgiharaPastReading.beq : OgiharaPastReading → OgiharaPastReading → Bool

Equations

• Semantics.Tense.Ogihara.instBEqOgiharaPastReading.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Semantics.Tense.Ogihara.instBEqOgiharaPastReading : BEq OgiharaPastReading

Equations

• Semantics.Tense.Ogihara.instBEqOgiharaPastReading = { beq := Semantics.Tense.Ogihara.instBEqOgiharaPastReading.beq }

def Semantics.Tense.Ogihara.pastUnderPastReadings : List OgiharaPastReading

Both readings are available for past-under-past in SOT languages.

Equations

• Semantics.Tense.Ogihara.pastUnderPastReadings = [Semantics.Tense.Ogihara.OgiharaPastReading.genuinePast, Semantics.Tense.Ogihara.OgiharaPastReading.zeroTense]

def Semantics.Tense.Ogihara.zeroTenseSemantics {Time : Type u_1} (g : Core.Tense.TemporalAssignment Time) (n : ℕ) (matrixEventTime : Time) : Time

Zero tense semantics: the tense variable is bound by the attitude verb and receives the matrix event time. This produces R' = E_matrix (the simultaneous reading).

This is exactly zeroTense_receives_binder_time from Core.Tense, applied to the attitude embedding context.

Equations

• Semantics.Tense.Ogihara.zeroTenseSemantics g n matrixEventTime = Core.Tense.interpTense n (Core.Tense.updateTemporal g n matrixEventTime)

theorem Semantics.Tense.Ogihara.zeroTenseSemantics_eq {Time : Type u_1} (g : Core.Tense.TemporalAssignment Time) (n : ℕ) (matrixEventTime : Time) : zeroTenseSemantics g n matrixEventTime = matrixEventTime

Zero tense semantics gives the matrix event time.

theorem Semantics.Tense.Ogihara.ogihara_derives_simultaneous {Time : Type u_1} (matrixFrame : Core.Reichenbach.ReichenbachFrame Time) (g : Core.Tense.TemporalAssignment Time) (n : ℕ) : have embeddedR := zeroTenseSemantics g n matrixFrame.eventTime; (embeddedFrame matrixFrame embeddedR embeddedR).isPresent

Ogihara derives the simultaneous reading via the zero tense reading of past: the bound variable receives E_matrix.

theorem Semantics.Tense.Ogihara.ogihara_zero_is_bound_var {Time : Type u_1} (g : Core.Tense.TemporalAssignment Time) (n : ℕ) (binderTime : Time) : zeroTenseSemantics g n binderTime = binderTime

Ogihara's zero tense IS the bound-variable mechanism from Core.Tense.

theorem Semantics.Tense.Ogihara.ogihara_derives_shifted {Time : Type u_1} [LinearOrder Time] (matrixFrame : Core.Reichenbach.ReichenbachFrame Time) (embeddedR embeddedE : Time) (_hReading : OgiharaPastReading.genuinePast = OgiharaPastReading.genuinePast) (hPast : embeddedR < matrixFrame.eventTime) : (embeddedFrame matrixFrame embeddedR embeddedE).isPast

Ogihara derives the shifted reading via the genuine-past reading: the past tense contributes temporal precedence.

def Semantics.Tense.Ogihara.Ogihara : TenseTheory

@cite{ogihara-1996} theory identity card.

Equations

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

theorem Semantics.Tense.Ogihara.ogihara_ambiguity_vs_deletion : OgiharaPastReading.genuinePast ≠ OgiharaPastReading.zeroTense ∧ Ogihara.hasZeroTense = true

Ogihara's key claim: past IS ambiguous between genuine past and zero tense. This is a categorical structural difference from Kratzer. In Ogihara, the simultaneous reading = the zero-tense READING of past (semantic ambiguity); in Kratzer, it = deletion of past (morphological operation, no ambiguity).