inductive Phenomena.SubordinateFuture.PortugueseForm : Type

Portuguese verbal forms relevant to SF analysis.

Following standard Portuguese grammar, the forms are:

• Indicative Present: "está" (is)
• Indicative Future: "estará" (will be)
• Subjunctive Present: "esteja" (be.SUBJ)
• Subjunctive Future: "estiver" (be.SF) ← The Subordinate Future

The SF "estiver" is traditionally called "futuro do subjuntivo" (future subjunctive), but Mendes argues it's present tense + subjunctive mood.

• indPresent : PortugueseForm
• indFuture : PortugueseForm
• subjPresent : PortugueseForm
• subjFuture : PortugueseForm

instance Phenomena.SubordinateFuture.instDecidableEqPortugueseForm : DecidableEq PortugueseForm

Equations

• Phenomena.SubordinateFuture.instDecidableEqPortugueseForm x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.SubordinateFuture.instReprPortugueseForm : Repr PortugueseForm

Equations

• Phenomena.SubordinateFuture.instReprPortugueseForm = { reprPrec := Phenomena.SubordinateFuture.instReprPortugueseForm.repr }

def Phenomena.SubordinateFuture.instReprPortugueseForm.repr : PortugueseForm → Nat → Std.Format

Equations

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

def Phenomena.SubordinateFuture.instBEqPortugueseForm.beq : PortugueseForm → PortugueseForm → Bool

Equations

• Phenomena.SubordinateFuture.instBEqPortugueseForm.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.SubordinateFuture.instBEqPortugueseForm : BEq PortugueseForm

Equations

• Phenomena.SubordinateFuture.instBEqPortugueseForm = { beq := Phenomena.SubordinateFuture.instBEqPortugueseForm.beq }

structure Phenomena.SubordinateFuture.SFDecomposition : Type

Morphological decomposition of SF according to Mendes.

The key claim: SF = SUBJ + PRES (not SUBJ + FUT) The future interpretation comes from the subjunctive introducing a situation in the historical alternatives, not from tense.

• mood : String
• tense : String
• futureFromMood : Bool

def Phenomena.SubordinateFuture.mendesSFAnalysis : SFDecomposition

Equations

• Phenomena.SubordinateFuture.mendesSFAnalysis = { }

structure Phenomena.SubordinateFuture.SFExample : Type

An example with its interpretation and key properties.

• exampleNum : String

  Example number from the paper

• portuguese : String

  Portuguese sentence

• gloss : String

  English gloss

• translation : String

  Free translation

• hasFutureRef : Bool

  Does it have future reference?

• isSubordinate : Bool

  Is it in a subordinate context?

• trigger : String

  What triggers the SF?

instance Phenomena.SubordinateFuture.instReprSFExample : Repr SFExample

Equations

• Phenomena.SubordinateFuture.instReprSFExample = { reprPrec := Phenomena.SubordinateFuture.instReprSFExample.repr }

def Phenomena.SubordinateFuture.instReprSFExample.repr : SFExample → Nat → Std.Format

Equations

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

def Phenomena.SubordinateFuture.ex1_basicConditional : SFExample

Example (1): Basic SF in conditional antecedent.

"Se a Maria estiver em casa, ela vai atender o telefone." "If Maria be.SF at home, she will answer the phone."

Key observations:

• SF "estiver" has present morphology
• Interpretation is future-oriented
• Main clause anchored to antecedent time

Equations

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

def Phenomena.SubordinateFuture.ex2_indicativeContrast : SFExample

Example (2): Indicative present in conditional (contrast).

"Se a Maria está em casa, ela vai atender o telefone." "If Maria is.IND at home, she will answer the phone."

Indicative present has present reading, not future. This contrasts with SF which gets future reading.

Equations

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

def Phenomena.SubordinateFuture.ex3_temporalClause : SFExample

Example (3): SF in temporal clause.

"Quando a Maria estiver em casa, ela vai atender." "When Maria be.SF at home, she will answer."

SF also appears with "quando" (when), "depois que" (after), etc.

Equations

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

def Phenomena.SubordinateFuture.ex4_relativeClause : SFExample

Example (4): SF in relative clause.

"O aluno que estiver preparado pode sair." "The student who be.SF prepared can leave."

SF in relative clauses gets future/generic interpretation.

Equations

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

structure Phenomena.SubordinateFuture.ModalDonkeyExample : Type

Modal donkey anaphora data structure.

SF licenses donkey anaphora across clause boundaries in a way that requires a situation dref analysis.

• exampleNum : String
• portuguese : String
• gloss : String
• felicitous : Bool

  Is the anaphora felicitous?

• antecedent : String

  What is the antecedent?

• anaphor : String

  What is the anaphor?

def Phenomena.SubordinateFuture.instReprModalDonkeyExample.repr : ModalDonkeyExample → Nat → Std.Format

Equations

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

instance Phenomena.SubordinateFuture.instReprModalDonkeyExample : Repr ModalDonkeyExample

Equations

• Phenomena.SubordinateFuture.instReprModalDonkeyExample = { reprPrec := Phenomena.SubordinateFuture.instReprModalDonkeyExample.repr }

def Phenomena.SubordinateFuture.ex5_donkeyWithSF : ModalDonkeyExample

Example (5): Donkey anaphora with SF.

"Se um estudante estiver preparado, ele pode sair." "If a student be.SF prepared, he can leave."

The pronoun "ele" (he) is bound by "um estudante" (a student) across the conditional boundary. This is modal donkey anaphora.

Equations

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

def Phenomena.SubordinateFuture.ex6_temporalAnchoring : SFExample

Example (6): Temporal anchoring evidence.

"Se a Maria estiver em casa às 5h, ela vai estar cansada." "If Maria be.SF at home at 5pm, she will be tired."

The tiredness is evaluated at the antecedent time (5pm), not the speech time. This shows temporal anchoring to the situation introduced by SF.

Equations

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

structure Phenomena.SubordinateFuture.CrossLinguisticExample : Type

Cross-linguistic data: Spanish parallel.

Spanish has a similar "futuro de subjuntivo" form, though it's archaic in modern Spanish (preserved in legal language and some dialects).

• language : String
• form : String
• sentence : String
• gloss : String
• isParallelToPortugueseSF : Bool

def Phenomena.SubordinateFuture.instReprCrossLinguisticExample.repr : CrossLinguisticExample → Nat → Std.Format

Equations

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

instance Phenomena.SubordinateFuture.instReprCrossLinguisticExample : Repr CrossLinguisticExample

Equations

• Phenomena.SubordinateFuture.instReprCrossLinguisticExample = { reprPrec := Phenomena.SubordinateFuture.instReprCrossLinguisticExample.repr }

def Phenomena.SubordinateFuture.spanish_sf : CrossLinguisticExample

Equations

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

def Phenomena.SubordinateFuture.italian_congiuntivo : CrossLinguisticExample

Equations

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

structure Phenomena.SubordinateFuture.MendesPrediction : Type

Predictions of Mendes' analysis.

Predictions that follow from treating SF as subjunctive (introducing a situation dref) rather than future indicative.

• prediction : String
• confirmed : Bool
• evidence : String

instance Phenomena.SubordinateFuture.instReprMendesPrediction : Repr MendesPrediction

Equations

• Phenomena.SubordinateFuture.instReprMendesPrediction = { reprPrec := Phenomena.SubordinateFuture.instReprMendesPrediction.repr }

def Phenomena.SubordinateFuture.instReprMendesPrediction.repr : MendesPrediction → Nat → Std.Format

Equations

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

def Phenomena.SubordinateFuture.prediction_futureFromMood : MendesPrediction

Equations

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

def Phenomena.SubordinateFuture.prediction_temporalShift : MendesPrediction

Equations

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

def Phenomena.SubordinateFuture.prediction_donkeyAnaphora : MendesPrediction

Equations

• Phenomena.SubordinateFuture.prediction_donkeyAnaphora = { prediction := "SF licenses modal donkey anaphora", confirmed := true, evidence := "Example 5: cross-clausal binding with SF" }

def Phenomena.SubordinateFuture.prediction_indicativeContrast : MendesPrediction

Equations

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

def Phenomena.SubordinateFuture.sfExamples : List SFExample

All SF examples

Equations

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

def Phenomena.SubordinateFuture.donkeyExamples : List ModalDonkeyExample

All donkey examples

Equations

• Phenomena.SubordinateFuture.donkeyExamples = [Phenomena.SubordinateFuture.ex5_donkeyWithSF]

def Phenomena.SubordinateFuture.crossLinguisticExamples : List CrossLinguisticExample

All cross-linguistic examples

Equations

• Phenomena.SubordinateFuture.crossLinguisticExamples = [Phenomena.SubordinateFuture.spanish_sf, Phenomena.SubordinateFuture.italian_congiuntivo]

def Phenomena.SubordinateFuture.predictions : List MendesPrediction

All predictions

Equations

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