Documentation

Studies.ArreguiKusumoto1998

Arregui and Kusumoto (1998): Tense in Temporal Adjunct Clauses #

Japanese mae 'before' takes a present clause and ato 'after' a past one, while English and Polish before- and after-clauses take the past. Ogihara's relative-tense account has the adjunct tense order its event against the matrix event, in agreement with the connective, unless the sequence-of-tense rule deletes it. Arregui and Kusumoto object that Polish has no such rule and patterns with English, and that a Japanese toki 'when'-clause takes the past. For them the past tense is Prior's operator and the present a variable. English and Polish adjuncts and Japanese past when-clauses are relative clauses over times, whose past is evaluated at the speech time, and mae and ato select a tensed clause directly, mae being stipulated to bind a variable. The logical forms are interpreted by Heim and Kratzer's type-driven composition, which gives a past under mae and a present under ato no denotation.

Main statements #

Implementation notes #

TODO #

References #

The fragment #

source
inductive ArreguiKusumoto1998.Word :
Type

The words of the fragment are the tenseless verb phrases and the attitude verbs, each numbered, the past tense, the speech time, the preposition at, before, after and the covert adverb of quantification.

Instances For
    source
    def ArreguiKusumoto1998.instDecidableEqWord.decEq (x✝ x✝¹ : Word) :
    Decidable (x✝ = x✝¹)
    Equations
    Instances For
      source
      @[instance_reducible]
      instance ArreguiKusumoto1998.instDecidableEqWord :
      DecidableEq Word
      Equations
      source
      @[reducible, inline]
      abbrev ArreguiKusumoto1998.LF :
      Type

      A logical form is a binary tree of words, traces and binders.

      Equations
      Instances For
        source
        structure ArreguiKusumoto1998.Model (T : Type) [LinearOrder T] :
        Type

        A model gives the times each verb phrase holds at, the times each attitude verb holds at given the times of its complement, and the speech time.

        • vp : ℕ → NonemptyInterval T → Prop

          The times at which the verb phrase of a number holds.

        • attitude : ℕ → (NonemptyInterval T → Prop) → NonemptyInterval T → Prop

          The times at which the attitude verb of a number holds of a property of times.

        • speechTime : NonemptyInterval T

          The speech time.

        Instances For
          source
          def ArreguiKusumoto1998.before {T : Type} [LinearOrder T] (X : NonemptyInterval T → Prop) (t : NonemptyInterval T) :
          Prop

          Before (19) holds of the times that precede every time of its clause.

          Equations
          Instances For
            source
            def ArreguiKusumoto1998.Word.ty :
            Word → Montague.Ty

            The semantic type of a word.

            Equations
            Instances For
              source
              def ArreguiKusumoto1998.Model.denote {T : Type} [LinearOrder T] (M : Model T) (w : Word) :
              Montague.Ty.Domain (NonemptyInterval T) Unit w.ty

              The denotation of a word in a model. The past tense is Prior's operator (13), whose denotation after shares (19), at identifies two times, and the adverb of quantification (34c) holds of a time when each time of its restrictor within it contains a time of its scope.

              Equations
              Instances For
                source
                def ArreguiKusumoto1998.Model.lex {T : Type} [LinearOrder T] (M : Model T) (w : Word) :
                Option (Montague.Denotation (NonemptyInterval T) Unit)

                The lexicon of a model gives each word its type and its denotation.

                Equations
                Instances For
                  source
                  def ArreguiKusumoto1998.Interpretable (lf : LF) :
                  Prop

                  A logical form is interpretable when type-driven composition gives it a type.

                  Equations
                  Instances For
                    source
                    @[instance_reducible]
                    instance ArreguiKusumoto1998.instDecidablePredLFInterpretable :
                    DecidablePred Interpretable
                    Equations
                    source
                    theorem ArreguiKusumoto1998.interpretable_iff {T : Type} [LinearOrder T] (M : Model T) (g : Assignment (NonemptyInterval T)) (lf : LF) :
                    Interpretable lf ↔ (HeimKratzer.Tree.interp M.lex g lf).isSome = true

                    An interpretable logical form is one with a denotation, in any model.

                    source
                    def ArreguiKusumoto1998.Model.Holds {T : Type} [LinearOrder T] (M : Model T) (lf : LF) :
                    Prop

                    A logical form is true in a model when it composes to a true truth value, its free variables denoting the speech time, as an unbound tense variable does (12).

                    Equations
                    Instances For
                      source
                      def ArreguiKusumoto1998.Model.extension {T : Type} [LinearOrder T] (M : Model T) (lf : LF) :
                      NonemptyInterval T → Prop

                      The extension of a logical form in a model is the set of times it composes to, its free variables denoting the speech time.

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

                        Before and after #

                        source
                        theorem ArreguiKusumoto1998.before_iff_not_diamond {T : Type} [LinearOrder T] {X : NonemptyInterval T → Prop} {t : NonemptyInterval T} :
                        before X t ↔ ¬ModalLogic.Diamond (Tense.Perspective.toSetRel (Semantics.Denotes.denote Tense.future)ᶜ) X t

                        A time is before a clause exactly when no time of the clause precedes or overlaps it, which sharpens the paper's gloss of before as the times that are not after a time of the clause.

                        source
                        theorem ArreguiKusumoto1998.before_of_forall_not {T : Type} [LinearOrder T] {X : NonemptyInterval T → Prop} (h : ∀ (t' : NonemptyInterval T), ¬X t') (t : NonemptyInterval T) :
                        before X t

                        Before is not veridical (18a), holding of every time when its clause has none.

                        source
                        theorem ArreguiKusumoto1998.beforeEver_of_before {T : Type} [LinearOrder T] {t : NonemptyInterval T} {A B : Set (NonemptyInterval T)} (ht : t ∈ A) (h : before (fun (x : NonemptyInterval T) => x ∈ B) t) :
                        Tense.beforeEver A B

                        A time of one clause before another clause puts the first before ever the second, the universal before of Anscombe.

                        Tense as operator and as variable #

                        source
                        def ArreguiKusumoto1998.pastOperator :
                        LF

                        The past tense is an operator on properties of times (13).

                        Equations
                        Instances For
                          source
                          def ArreguiKusumoto1998.presentVariable :
                          LF

                          The present tense is a variable over times (12), here of index 0.

                          Equations
                          Instances For
                            source
                            def ArreguiKusumoto1998.clause :
                            LF → LF → LF

                            A root or relative clause of tense τ over a verb phrase. A tense variable saturates the verb phrase (12b), and with an operator the speech time in C saturates the tensed clause (13b).

                            Equations
                            Instances For
                              source
                              theorem ArreguiKusumoto1998.holds_present {T : Type} [LinearOrder T] {M : Model T} {k : ℕ} :
                              M.Holds (clause presentVariable (PhraseStructure.Tree.leaf (Word.vp k))) ↔ M.vp k M.speechTime

                              A present clause is true when its verb phrase holds at the speech time (12).

                              source
                              theorem ArreguiKusumoto1998.holds_past {T : Type} [LinearOrder T] {M : Model T} {k : ℕ} :
                              M.Holds (clause pastOperator (PhraseStructure.Tree.leaf (Word.vp k))) ↔ ∃ (t : NonemptyInterval T), t.Precedes M.speechTime ∧ M.vp k t

                              A past clause is true when its verb phrase holds at a time before the speech time (13).

                              source
                              theorem ArreguiKusumoto1998.not_interpretable_speechTime_present {k : ℕ} :
                              ¬Interpretable ((PhraseStructure.Tree.leaf Word.speechTime).bin (PhraseStructure.Tree.bin presentVariable (PhraseStructure.Tree.leaf (Word.vp k))))

                              The speech time does not combine with a present clause, which is a truth value.

                              Relative-clause adjuncts #

                              source
                              def ArreguiKusumoto1998.atTrace (vp : LF) :
                              LF

                              A verb phrase modified by at and the trace of the relative pronoun, of index 1 (16b).

                              Equations
                              Instances For
                                source
                                def ArreguiKusumoto1998.relative (τ vp : LF) :
                                LF

                                A relative clause over times, in which the relative pronoun binds its trace in a clause of tense τ (16b).

                                Equations
                                Instances For
                                  source
                                  def ArreguiKusumoto1998.matrix (vp adjunct : LF) :
                                  LF

                                  A past matrix clause whose verb phrase a temporal adjunct modifies (17).

                                  Equations
                                  Instances For
                                    source
                                    theorem ArreguiKusumoto1998.extension_relative {T : Type} [LinearOrder T] {M : Model T} {t : NonemptyInterval T} {k : ℕ} :
                                    M.extension (relative pastOperator (atTrace (PhraseStructure.Tree.leaf (Word.vp k)))) t ↔ t.Precedes M.speechTime ∧ M.vp k t

                                    A past relative clause denotes the times before the speech time at which its verb phrase holds, whatever clause it modifies (16b).

                                    source
                                    theorem ArreguiKusumoto1998.holds_after_relative {T : Type} [LinearOrder T] {M : Model T} {k l : ℕ} :
                                    M.Holds (matrix (PhraseStructure.Tree.leaf (Word.vp k)) ((PhraseStructure.Tree.leaf Word.after).bin (relative pastOperator (atTrace (PhraseStructure.Tree.leaf (Word.vp l)))))) ↔ ∃ (t : NonemptyInterval T), t.Precedes M.speechTime ∧ M.vp k t ∧ ∃ (t' : NonemptyInterval T), t'.Precedes M.speechTime ∧ M.vp l t' ∧ t'.Precedes t

                                    In Satoshi left after Junko came (24) both events precede the speech time, and the connective alone orders them.

                                    source
                                    theorem ArreguiKusumoto1998.holds_before_relative {T : Type} [LinearOrder T] {M : Model T} {k l : ℕ} :
                                    M.Holds (matrix (PhraseStructure.Tree.leaf (Word.vp k)) ((PhraseStructure.Tree.leaf Word.before).bin (relative pastOperator (atTrace (PhraseStructure.Tree.leaf (Word.vp l)))))) ↔ ∃ (t : NonemptyInterval T), t.Precedes M.speechTime ∧ M.vp k t ∧ ∀ (t' : NonemptyInterval T), t'.Precedes M.speechTime → M.vp l t' → t.Precedes t'

                                    In Satoshi left before Junko came (25) the leaving precedes every past coming.

                                    source
                                    theorem ArreguiKusumoto1998.holds_when_relative {T : Type} [LinearOrder T] {M : Model T} {k l : ℕ} :
                                    M.Holds (matrix (PhraseStructure.Tree.leaf (Word.vp k)) (relative pastOperator (atTrace (PhraseStructure.Tree.leaf (Word.vp l))))) ↔ ∃ (t : NonemptyInterval T), t.Precedes M.speechTime ∧ M.vp k t ∧ M.vp l t

                                    With a past when-clause, Junko was in her room when Satoshi came (33) reports an episode at one past time.

                                    source
                                    theorem ArreguiKusumoto1998.exists_of_holds_after {T : Type} [LinearOrder T] {M : Model T} {k l : ℕ} (h : M.Holds (matrix (PhraseStructure.Tree.leaf (Word.vp k)) ((PhraseStructure.Tree.leaf Word.after).bin (relative pastOperator (atTrace (PhraseStructure.Tree.leaf (Word.vp l))))))) :
                                    ∃ (t : NonemptyInterval T), M.vp l t

                                    An after-sentence entails that its clause held (18b).

                                    source
                                    theorem ArreguiKusumoto1998.holds_before_of_forall_not {T : Type} [LinearOrder T] {M : Model T} {k l : ℕ} (h : ∀ (t : NonemptyInterval T), ¬M.vp l t) :
                                    M.Holds (matrix (PhraseStructure.Tree.leaf (Word.vp k)) ((PhraseStructure.Tree.leaf Word.before).bin (relative pastOperator (atTrace (PhraseStructure.Tree.leaf (Word.vp l)))))) ↔ M.Holds (clause pastOperator (PhraseStructure.Tree.leaf (Word.vp k)))

                                    A before-sentence whose clause never held says what its matrix says (18a).

                                    source
                                    theorem ArreguiKusumoto1998.not_holds_present_relative {T : Type} [LinearOrder T] {M : Model T} {k l : ℕ} :
                                    ¬M.Holds (matrix (PhraseStructure.Tree.leaf (Word.vp k)) ((PhraseStructure.Tree.leaf Word.after).bin (relative presentVariable (atTrace (PhraseStructure.Tree.leaf (Word.vp l)))))) ∧ ¬M.Holds (matrix (PhraseStructure.Tree.leaf (Word.vp k)) (relative presentVariable (atTrace (PhraseStructure.Tree.leaf (Word.vp l)))))

                                    Left free in a relative clause, the present variable denotes the speech time, which no past time follows or is, so a present after- or when-clause that is a relative clause contradicts a past matrix. The paper gives a present when-clause the other form, on which an adverb binds the variable (34).

                                    source
                                    theorem ArreguiKusumoto1998.holds_before_present_relative {T : Type} [LinearOrder T] {M : Model T} {k l : ℕ} :
                                    M.Holds (matrix (PhraseStructure.Tree.leaf (Word.vp k)) ((PhraseStructure.Tree.leaf Word.before).bin (relative presentVariable (atTrace (PhraseStructure.Tree.leaf (Word.vp l)))))) ↔ M.Holds (clause pastOperator (PhraseStructure.Tree.leaf (Word.vp k)))

                                    A present before-clause adds nothing to a past matrix, every past time preceding the speech time.

                                    Connectives that select a tensed clause #

                                    source
                                    theorem ArreguiKusumoto1998.extension_after_past {T : Type} [LinearOrder T] {M : Model T} {t : NonemptyInterval T} {k : ℕ} [DenselyOrdered T] :
                                    M.extension ((PhraseStructure.Tree.leaf Word.after).bin (PhraseStructure.Tree.bin pastOperator (PhraseStructure.Tree.leaf (Word.vp k)))) t ↔ ∃ (t' : NonemptyInterval T), t'.Precedes t ∧ M.vp k t'

                                    On dense time after absorbs the past operator of the clause it selects. The paper prints the absorbed form at the root of (27) without comment.

                                    source
                                    theorem ArreguiKusumoto1998.not_extension_after_past_int :
                                    ∃ (M : Model ℤ) (t : NonemptyInterval ℤ), (∃ (t' : NonemptyInterval ℤ), t'.Precedes t ∧ M.vp 0 t') ∧ ¬M.extension ((PhraseStructure.Tree.leaf Word.after).bin (PhraseStructure.Tree.bin pastOperator (PhraseStructure.Tree.leaf (Word.vp 0)))) t

                                    On discrete time after does not absorb the past operator, since no time lies between an event and the next moment.

                                    source
                                    theorem ArreguiKusumoto1998.extension_before_present {T : Type} [LinearOrder T] {M : Model T} {k : ℕ} :
                                    M.extension ((PhraseStructure.Tree.leaf Word.before).bin (PhraseStructure.Tree.binder 0 (PhraseStructure.Tree.bin presentVariable (PhraseStructure.Tree.leaf (Word.vp k))))) = before (M.vp k)

                                    Before binds the present variable of the clause it selects (30).

                                    source
                                    theorem ArreguiKusumoto1998.interpretable_selected {k : ℕ} :
                                    Interpretable ((PhraseStructure.Tree.leaf Word.before).bin (PhraseStructure.Tree.binder 0 (PhraseStructure.Tree.bin presentVariable (PhraseStructure.Tree.leaf (Word.vp k))))) ∧ ¬Interpretable ((PhraseStructure.Tree.leaf Word.before).bin (PhraseStructure.Tree.binder 0 (PhraseStructure.Tree.bin pastOperator (PhraseStructure.Tree.leaf (Word.vp k))))) ∧ Interpretable ((PhraseStructure.Tree.leaf Word.after).bin (PhraseStructure.Tree.bin pastOperator (PhraseStructure.Tree.leaf (Word.vp k)))) ∧ ¬Interpretable ((PhraseStructure.Tree.leaf Word.after).bin (PhraseStructure.Tree.bin presentVariable (PhraseStructure.Tree.leaf (Word.vp k))))

                                    Of the four tensed clauses a connective can select, the present composes under before, which the paper stipulates to bear a binder index, and the past under after, which bears none. A past is a set of times with no variable to bind, the paper's reason for (5a), and a present is a truth value, which accounts for (6b), a case the paper leaves implicit.

                                    source
                                    theorem ArreguiKusumoto1998.holds_after_selected {T : Type} [LinearOrder T] {M : Model T} {k l : ℕ} [DenselyOrdered T] :
                                    M.Holds (matrix (PhraseStructure.Tree.leaf (Word.vp k)) ((PhraseStructure.Tree.leaf Word.after).bin (PhraseStructure.Tree.bin pastOperator (PhraseStructure.Tree.leaf (Word.vp l))))) ↔ ∃ (t : NonemptyInterval T), t.Precedes M.speechTime ∧ M.vp k t ∧ ∃ (t' : NonemptyInterval T), t'.Precedes t ∧ M.vp l t'

                                    In Japanese, Satoshi left after Junko came (28) says that the coming precedes the leaving, the paper's truth conditions, which hold of the logical form on dense time.

                                    source
                                    theorem ArreguiKusumoto1998.holds_before_selected {T : Type} [LinearOrder T] {M : Model T} {k l : ℕ} :
                                    M.Holds (matrix (PhraseStructure.Tree.leaf (Word.vp k)) ((PhraseStructure.Tree.leaf Word.before).bin (PhraseStructure.Tree.binder 0 (PhraseStructure.Tree.bin presentVariable (PhraseStructure.Tree.leaf (Word.vp l)))))) ↔ ∃ (t : NonemptyInterval T), t.Precedes M.speechTime ∧ M.vp k t ∧ ∀ (t' : NonemptyInterval T), M.vp l t' → t.Precedes t'

                                    In Japanese, Satoshi left before Junko came (29) says that the leaving precedes every coming.

                                    source
                                    theorem ArreguiKusumoto1998.holds_after_relative_iff_selected {T : Type} [LinearOrder T] {M : Model T} {k l : ℕ} [DenselyOrdered T] :
                                    M.Holds (matrix (PhraseStructure.Tree.leaf (Word.vp k)) ((PhraseStructure.Tree.leaf Word.after).bin (relative pastOperator (atTrace (PhraseStructure.Tree.leaf (Word.vp l)))))) ↔ M.Holds (matrix (PhraseStructure.Tree.leaf (Word.vp k)) ((PhraseStructure.Tree.leaf Word.after).bin (PhraseStructure.Tree.bin pastOperator (PhraseStructure.Tree.leaf (Word.vp l)))))

                                    On dense time an after-sentence has the same truth conditions whether its clause is a relative clause (24) or is selected directly (28).

                                    The ambiguity of an adjunct that embeds a clause #

                                    source
                                    def ArreguiKusumoto1998.amherst :
                                    Model ℤ

                                    In the paper's scenario for I encountered Satoshi when you said he had left (14), you said at three that Satoshi left at ten. Times are hours of the day, and the speech time, which the paper leaves open, is put at eight in the evening.

                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For
                                      source
                                      theorem ArreguiKusumoto1998.extension_upstairs_downstairs :
                                      have upstairs := relative pastOperator (atTrace ((PhraseStructure.Tree.leaf (Word.attitude 0)).bin (PhraseStructure.Tree.bin pastOperator (PhraseStructure.Tree.leaf (Word.vp 0))))); have downstairs := relative pastOperator ((PhraseStructure.Tree.leaf (Word.attitude 0)).bin (PhraseStructure.Tree.bin pastOperator (atTrace (PhraseStructure.Tree.leaf (Word.vp 0))))); (amherst.extension upstairs (NonemptyInterval.pure 15) ∧ ¬amherst.extension upstairs (NonemptyInterval.pure 10)) ∧ amherst.extension downstairs (NonemptyInterval.pure 10) ∧ ¬amherst.extension downstairs (NonemptyInterval.pure 15)

                                      With the relative pronoun extracted from the higher clause (15a) the adjunct holds of the time of the saying and not of the time of the leaving, and extracted from the lower clause (15b) of the time of the leaving and not of the time of the saying.

                                      source
                                      theorem ArreguiKusumoto1998.mem_freeIndices_selected {k l : ℕ} :
                                      1 ∈ ((PhraseStructure.Tree.leaf Word.after).bin (PhraseStructure.Tree.bin pastOperator ((PhraseStructure.Tree.leaf (Word.attitude k)).bin (PhraseStructure.Tree.bin pastOperator (atTrace (PhraseStructure.Tree.leaf (Word.vp l))))))).freeIndices

                                      In a clause that a connective selects, the trace of a relative pronoun is free.

                                      The present of a when-clause #

                                      source
                                      def ArreguiKusumoto1998.quantificational (τ vp : LF) :
                                      LF

                                      The covert adverb of quantification with its restrictor, a clause of tense τ over whose tense variable the adverb abstracts (34c).

                                      Equations
                                      Instances For
                                        source
                                        theorem ArreguiKusumoto1998.holds_whenever {T : Type} [LinearOrder T] {M : Model T} {k l : ℕ} :
                                        M.Holds (matrix (PhraseStructure.Tree.leaf (Word.vp k)) (quantificational presentVariable (PhraseStructure.Tree.leaf (Word.vp l)))) ↔ ∃ (t : NonemptyInterval T), t.Precedes M.speechTime ∧ ∀ t' ≤ t, M.vp l t' → ∃ t'' ≤ t', M.vp k t''

                                        In Junko was in her room whenever Satoshi came (34) a covert adverb of quantification, which the when-clause restricts, binds the present variable of the clause.

                                        source
                                        theorem ArreguiKusumoto1998.holds_whenever_of_forall_not {T : Type} [LinearOrder T] {M : Model T} {t : NonemptyInterval T} {k l : ℕ} (ht : t.Precedes M.speechTime) (h : ∀ t' ≤ t, ¬M.vp l t') :
                                        M.Holds (matrix (PhraseStructure.Tree.leaf (Word.vp k)) (quantificational presentVariable (PhraseStructure.Tree.leaf (Word.vp l))))

                                        The truth conditions (34b) hold as soon as some past time contains no time of the when-clause, the past tense quantifying over the domain of the adverb. The paper does not remark on this.

                                        Languages #

                                        source
                                        structure ArreguiKusumoto1998.Language :
                                        Type

                                        The tense parameters of a language.

                                        • sot : Bool

                                          The language has the sequence-of-tense rule.

                                        • present : Finset Ordering

                                          The positions the present admits against its evaluation time.

                                        • selectsTP : Bool

                                          Before and after select a tensed clause, where they otherwise take a relative clause over times.

                                        Instances For
                                          source
                                          def ArreguiKusumoto1998.english :
                                          Language

                                          English has the sequence-of-tense rule, and its adjuncts are relative clauses.

                                          Equations
                                          Instances For
                                            source
                                            def ArreguiKusumoto1998.polish :
                                            Language

                                            Polish has no sequence-of-tense rule, and its adjuncts are relative clauses.

                                            Equations
                                            Instances For
                                              source
                                              def ArreguiKusumoto1998.japanese :
                                              Language

                                              Japanese has no sequence-of-tense rule, a present with a future interpretation (fn. 1), and before and after that select a tensed clause.

                                              Equations
                                              Instances For
                                                source
                                                def ArreguiKusumoto1998.Language.cell (L : Language) :
                                                Tense → Finset Ordering

                                                The positions a tense of a language admits against its evaluation time.

                                                Equations
                                                Instances For
                                                  source
                                                  def ArreguiKusumoto1998.Language.adjunct (L : Language) :
                                                  Tense.Connective.Relation → LF → LF → Option LF

                                                  The adjunct of a temporal relation over a verb phrase in the tense τ. A when-clause in a tense variable restricts the adverb of quantification that binds the variable, the form the paper gives the Japanese present (34c), and is otherwise a relative clause over times (16). The clause of before and after is a relative clause (23) unless they select a tensed clause (27), over whose tense variable before, bearing a binder index, abstracts (30).

                                                  Equations
                                                  Instances For
                                                    source
                                                    def ArreguiKusumoto1998.head? :
                                                    Tense → Option LF

                                                    The tense heads the paper analyses, the past an operator and the present a variable. The Polish future has none.

                                                    Equations
                                                    Instances For
                                                      source
                                                      theorem ArreguiKusumoto1998.interpretable_mae_ato :
                                                      (∃ lf ∈ japanese.adjunct Japanese.TemporalConnectives.mae.relation presentVariable (PhraseStructure.Tree.leaf (Word.vp 0)), Interpretable lf) ∧ (∃ lf ∈ japanese.adjunct Japanese.TemporalConnectives.mae.relation pastOperator (PhraseStructure.Tree.leaf (Word.vp 0)), ¬Interpretable lf) ∧ (∃ lf ∈ japanese.adjunct Japanese.TemporalConnectives.ato.relation pastOperator (PhraseStructure.Tree.leaf (Word.vp 0)), Interpretable lf) ∧ ∃ lf ∈ japanese.adjunct Japanese.TemporalConnectives.ato.relation presentVariable (PhraseStructure.Tree.leaf (Word.vp 0)), ¬Interpretable lf

                                                      mae takes the present and not the past, and ato the past and not the present, (5) and (6).

                                                      The relative-tense account #

                                                      source
                                                      def ArreguiKusumoto1998.adjunctCell? :
                                                      Tense.Connective.Relation → Option (Finset Ordering)

                                                      The positions a temporal relation admits for the adjunct event against the matrix event.

                                                      Equations
                                                      Instances For
                                                        source
                                                        def ArreguiKusumoto1998.Language.RelativeTense (L : Language) (c : Finset Ordering) (τ : Tense) :
                                                        Prop

                                                        On the relative-tense account a tense in an adjunct under a past locates the adjunct event against the matrix event, in a position the connective, of cell c, must admit, unless it is a past that the sequence-of-tense rule deletes.

                                                        Equations
                                                        Instances For
                                                          source
                                                          @[instance_reducible]
                                                          instance ArreguiKusumoto1998.instDecidableRelativeTense (L : Language) (c : Finset Ordering) (τ : Tense) :
                                                          Decidable (L.RelativeTense c τ)
                                                          Equations
                                                          source
                                                          theorem ArreguiKusumoto1998.relativeTense_iff_interpretable (rel : Tense.Connective.Relation) :
                                                          rel ∈ [Tense.Connective.Relation.before, Tense.Connective.Relation.after] → ∀ τ ∈ [Tense.past, Tense.present], ∃ c ∈ adjunctCell? rel, ∃ h ∈ head? τ, ∃ lf ∈ japanese.adjunct rel h (PhraseStructure.Tree.leaf (Word.vp 0)), japanese.RelativeTense c τ ↔ Interpretable lf

                                                          On mae and ato the two accounts agree.

                                                          The examples #

                                                          source
                                                          def ArreguiKusumoto1998.languages :
                                                          List (String × Language)

                                                          The languages of the example rows.

                                                          Equations
                                                          Instances For
                                                            source
                                                            def ArreguiKusumoto1998.relations :
                                                            List (String × Tense.Connective.Relation)

                                                            The temporal relations of the adjuncts of the example rows.

                                                            Equations
                                                            Instances For
                                                              source
                                                              def ArreguiKusumoto1998.tenses :
                                                              List (String × Tense)

                                                              The tenses of the example rows.

                                                              Equations
                                                              Instances For
                                                                source
                                                                def ArreguiKusumoto1998.positions :
                                                                List (String × Ordering)

                                                                The readings of a complement tense, by the position of its event against the matrix event.

                                                                Equations
                                                                Instances For
                                                                  source
                                                                  theorem ArreguiKusumoto1998.complement_readings (r : Datum) :
                                                                  r ∈ Examples.all → r.feature? "clause" = some "complement" → ∃ L ∈ List.lookup r.language languages, ∃ τ ∈ r.parse? "embeddedTense" tenses, ∀ p ∈ positions, (List.lookup p.1 r.readings = some Judgment.acceptable → p.2 ∈ if τ = Tense.past then Tense.pastUnderPast (L.sot = true) else L.cell τ) ∧ (τ = Tense.past → p.2 ∈ Tense.pastUnderPast (L.sot = true) → List.lookup p.1 r.readings = some Judgment.acceptable)

                                                                  A past complement under a past has exactly the readings the sequence-of-tense rule of the language gives it, and the reading the paper reports for a present or future complement is one its tense admits, (1) to (4) and (10).

                                                                  source
                                                                  theorem ArreguiKusumoto1998.judgment_iff_interpretable (r : Datum) :
                                                                  r ∈ Examples.all → ∀ rel ∈ r.parse? "clause" relations, ∀ τ ∈ r.parse? "embeddedTense" tenses, ∀ h ∈ head? τ, ∃ L ∈ List.lookup r.language languages, ∃ lf ∈ L.adjunct rel h (PhraseStructure.Tree.leaf (Word.vp 0)), (r.judgment = Judgment.acceptable ↔ Interpretable lf) ↔ ¬(τ = Tense.present ∧ rel ≠ Tense.Connective.Relation.when_ ∧ ¬L.selectsTP = true)

                                                                  An adjunct in the past or the present is acceptable exactly where its logical form composes, except for the present in a before- or after-clause that is a relative clause, the Polish (11b) and fn. 3 (i-b), which composes and which the paper stars without deriving. A relative clause composes in either tense, so the stars derived are those of mae with the past (5a) and ato with the present (6b), and the Polish future (11c) has no logical form.

                                                                  source
                                                                  theorem ArreguiKusumoto1998.judgment_iff_relativeTense (r : Datum) :
                                                                  r ∈ Examples.all → ∀ rel ∈ r.parse? "clause" relations, ∃ τ ∈ r.parse? "embeddedTense" tenses, ∃ L ∈ List.lookup r.language languages, ∃ c ∈ adjunctCell? rel, (r.judgment = Judgment.acceptable ↔ L.RelativeTense c τ) ↔ ¬(¬L.sot = true ∧ (τ = Tense.past ∧ (rel = Tense.Connective.Relation.when_ ∨ rel = Tense.Connective.Relation.before ∧ ¬L.selectsTP = true) ∨ τ = Tense.future))

                                                                  The relative-tense account gives the judgment on an adjunct except, in a language without the sequence-of-tense rule, for the past of a when-clause, the Japanese (8) and (32), and of a before-clause that is a relative clause, the Polish (11a) and (22b), which it rules out, and for the future, the Polish (11c), which it lets in. It lets in the present of a Japanese when-clause (9) without accounting for its habitual reading.

                                                                  source
                                                                  theorem ArreguiKusumoto1998.not_exists_sot_polish :
                                                                  ¬∃ (sot : Bool), (List.lookup "simultaneous" Examples.ex_10b.readings = some Judgment.acceptable ↔ Ordering.eq ∈ Tense.pastUnderPast (sot = true)) ∧ (Examples.ex_11a.judgment = Judgment.acceptable ↔ (have __src := polish; { sot := sot, present := __src.present, selectsTP := __src.selectsTP }).RelativeTense (Semantics.Denotes.denote Tense.future) Tense.past)

                                                                  No setting of the sequence-of-tense rule gives the relative-tense account both the past complement of Polish, which has only the shifted reading (10b), and its past before-clause (11a).

                                                                  source
                                                                  theorem ArreguiKusumoto1998.downstairs_iff (r : Datum) :
                                                                  r ∈ Examples.all → r.feature? "embeddedClauses" = some "2" → ∃ rel ∈ r.parse? "clause" relations, ∃ L ∈ List.lookup r.language languages, List.lookup "downstairs" r.readings = some Judgment.acceptable ↔ rel = Tense.Connective.Relation.when_ ∨ ¬L.selectsTP = true

                                                                  An adjunct that embeds a clause has the downstairs reading exactly where it is a relative clause, whose pronoun may be extracted from either clause, (14), (20), (22) and (32), a selected clause having no pronoun to bind a trace in it (26).

                                                                  source
                                                                  theorem ArreguiKusumoto1998.habitual_iff (r : Datum) :
                                                                  r ∈ Examples.all → r.language = "nucl1643" → r.feature? "clause" ∈ [some "when", some "relative"] → ∃ τ ∈ r.parse? "embeddedTense" tenses, ∃ h ∈ head? τ, List.lookup "habitual" r.readings = some Judgment.acceptable ↔ Interpretable (quantificational h (PhraseStructure.Tree.leaf (Word.vp 0)))

                                                                  A Japanese when-clause has the habitual reading exactly where its tense composes as the variable that the adverb of quantification binds, (8) and (9), and so do the relative clauses of (35) and (36), where the paper observes the contrast.