Kubota (2026): Outlook Management

This file formalizes Kubota's account of the Japanese outlook markers, adverbs and focus particles such as dōse 'anyway', nanka 'anything like', semete 'at least', mushiro 'rather', and koso 'precisely', whose secondary meaning is two-layered: a presupposition that the prior discourse has made a counterstance salient, and an expressive-like stance that situates the prejacent relative to that counterstance. Outlook carries the three components, with the stance layer indexed by an outlook in the sense of Coppock. Its presuppositional and expressive projections are its trivalent and TwoDim images, so that denial reaches the prejacent alone ((40)–(41)), and the shifted readings under attitude verbs ((42)) are exactly the non-rigidity of the stance layer (isRigid_iff), which a pure expressive in the sense of Potts lacks (ofTwoDim_isRigid).

The chapter's judgment data are the rows of Data/Examples/Kubota2026.json, and its generalizations are stated over them. An outlook-marked utterance is felicitous iff the prior move raises a counterstance, an evaluative assertion or a polar question about the prejacent's issue rather than a general wh-question (counterstance_requirement, (37)–(39)). The contrary marker mushiro and the confirmatory yahari are licensed by opposite expectations and neither stance can be cancelled (mushiro_yahari_expectation, (11)–(12)). Nanka combines with every modal flavor but is pejorative only under priority modality (nanka_pejorative_iff_priority, (45)), while semete combines only with priority modals (semete_selects_priority, (46)), priority modality being the deontic and bouletic flavors of Portner.

Implementation notes

The chapter is descriptive and defers its formal analysis to Kubota and Ido, where both layers derive from a counterstance-marker discourse function over a Farkas and Bruce Table; Outlook records the chapter-level picture with the two layers as fields. Perspective shift is modelled as outlook-relativity of the stance layer, following the chapter's remark that outlook markers fail Potts's independence and nondisplaceability and instead behave like locally accommodated presuppositions (Heim). Judgments the chapter marks ?? are recorded as questionable. The substrate's circumstantial flavor stands in for the chapter's ability modals.

TODO

• Deriving the two layers from a Table update, as Kubota and Ido do, is not attempted.

References

• [Kub26]
• [KI25]
• [Cop18]
• [Pot07b]
• [Hei92]
• [Por09]
• [FB10]

The two-layered meaning (§3)

structure Kubota2026.Outlook (W : Type u_1) (O : Type u_2) : Type (max u_1 u_2)

The meaning of an outlook-marked clause, made up of the at-issue prejacent, the presupposed salient counterstance, and a stance layer evaluated relative to an outlook.

• prejacent : W → Prop

  The at-issue content.

• counterstance : W → Prop

  The presupposition that a counterstance is salient ((37)–(39)).

• evaluation : O → W → Prop

  The evaluative stance, relative to an outlook.

noncomputable def Kubota2026.Outlook.toTrivalent {W : Type u_1} {O : Type u_2} (m : Outlook W O) : W → SignType

The presuppositional projection presupposes the counterstance and asserts the prejacent.

Equations

• m.toTrivalent = {w : W | m.counterstance w}.indicator fun (w : W) => SignType.ofProp (m.prejacent w)

def Kubota2026.Outlook.toTwoDim {W : Type u_1} {O : Type u_2} (m : Outlook W O) (o : O) : ConventionalImplicature.TwoDim W (W → Prop)

The expressive projection at an outlook pairs the prejacent with the stance as its use-conditional dimension.

Equations

• m.toTwoDim o = { atIssue := m.prejacent, notAtIssue := m.evaluation o }

@[simp]

theorem Kubota2026.Outlook.toTwoDim_notAtIssue {W : Type u_1} {O : Type u_2} (m : Outlook W O) (o : O) (a✝ : W) : (m.toTwoDim o).notAtIssue a✝ = m.evaluation o a✝

@[simp]

theorem Kubota2026.Outlook.toTwoDim_atIssue {W : Type u_1} {O : Type u_2} (m : Outlook W O) (o : O) (a✝ : W) : (m.toTwoDim o).atIssue a✝ = m.prejacent a✝

theorem Kubota2026.Outlook.support_neg_toTrivalent {W : Type u_1} {O : Type u_2} (m : Outlook W O) : Function.support (-m.toTrivalent) = {w : W | m.counterstance w}

Negation, and so denial, leaves the counterstance presupposition in place ((40)–(41)).

theorem Kubota2026.Outlook.toTwoDim_neg_notAtIssue {W : Type u_1} {O : Type u_2} (m : Outlook W O) (o : O) : (m.toTwoDim o).neg.notAtIssue = m.evaluation o

Negation leaves the stance layer in place at every outlook ((40)–(41)).

def Kubota2026.Outlook.IsRigid {W : Type u_1} {O : Type u_2} (m : Outlook W O) : Prop

A meaning is rigid when its stance layer does not depend on the outlook.

Equations

• m.IsRigid = Reference.IsRigid m.evaluation

theorem Kubota2026.Outlook.isRigid_iff {W : Type u_1} {O : Type u_2} (m : Outlook W O) : m.IsRigid ↔ ∀ (o o' : O), m.toTwoDim o = m.toTwoDim o'

The expressive projection varies with the outlook iff the stance layer does, so perspective shift is non-rigidity ((42)).

def Kubota2026.Outlook.ofTwoDim {W : Type u_1} {O : Type u_2} (t : ConventionalImplicature.TwoDim W (W → Prop)) : Outlook W O

The outlook-marked meaning of a pure expressive, whose conventional implicature is the same at every outlook and which presupposes nothing.

Equations

• Kubota2026.Outlook.ofTwoDim t = { prejacent := t.atIssue, counterstance := fun (x : W) => True, evaluation := fun (x : O) => t.notAtIssue }

theorem Kubota2026.Outlook.ofTwoDim_isRigid {W : Type u_1} {O : Type u_2} (t : ConventionalImplicature.TwoDim W (W → Prop)) : (ofTwoDim t).IsRigid

Pure expressives are rigid, so they do not shift under embedding ([Pot07b]'s nondisplaceability).

The counterstance requirement ((37)–(39))

def Kubota2026.RaisesCounterstance (t : Clause.SentenceType) : Prop

A prior move raises a counterstance when it puts the prejacent's issue at issue, as an evaluative assertion about its topic, (37), or a polar question about it, (39) Q1, does and a general wh-question that leaves the issue unraised, (38) and (39) Q2, does not.

Equations

• Kubota2026.RaisesCounterstance t = (t = Clause.SentenceType.declarative ∨ t = Clause.SentenceType.polar)

@[instance_reducible]

instance Kubota2026.instDecidablePredSentenceTypeRaisesCounterstance : DecidablePred RaisesCounterstance

Equations

• Kubota2026.instDecidablePredSentenceTypeRaisesCounterstance x✝ = { decide := decide (x✝ = Clause.SentenceType.declarative) || decide (x✝ = Clause.SentenceType.polar), reflects_decide := ⋯ }

def Kubota2026.priorMove? (row : Datum) : Option Clause.SentenceType

The sentence type of the row's prior move.

Equations

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

def Kubota2026.PredictsFelicitous (row : Datum) : Prop

A row is predicted felicitous iff its prior move raises a counterstance.

Equations

• Kubota2026.PredictsFelicitous row = match Kubota2026.priorMove? row with | some t => Kubota2026.RaisesCounterstance t | none => False

@[instance_reducible]

instance Kubota2026.instDecidablePredictsFelicitous (row : Datum) : Decidable (PredictsFelicitous row)

Equations

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

theorem Kubota2026.counterstance_requirement (row : Datum) : row ∈ Examples.all → row.feature? "phenomenon" = some "counterstance" → (row.judgment = Judgment.acceptable ↔ PredictsFelicitous row)

An outlook-marked utterance is felicitous iff the prior move raises a counterstance.

Non-cancelability ((10)–(12))

theorem Kubota2026.mushiro_yahari_expectation (row : Datum) : row ∈ Examples.all → row.feature? "phenomenon" = some "noncancelability" → row.feature? "contextExpectation" ≠ none → (row.feature? "marker" = some "mushiro" ↔ row.feature? "contextExpectation" = some "unexpected")

Under a context marked as unexpected the contrary marker mushiro is licensed and the confirmatory yahari is not, and conversely under a context marked as expected, so the stance is conventional and cannot be cancelled.

Modal interactions ((45)–(46))

def Kubota2026.IsPriority : Modality.ModalFlavor → Prop

Priority modality after [Por09] comprises the deontic and bouletic flavors, as against epistemic and ability modality.

Equations

• Kubota2026.IsPriority Modality.ModalFlavor.deontic = True
• Kubota2026.IsPriority Modality.ModalFlavor.bouletic = True
• Kubota2026.IsPriority Modality.ModalFlavor.epistemic = False
• Kubota2026.IsPriority Modality.ModalFlavor.circumstantial = False

@[instance_reducible]

instance Kubota2026.instDecidablePredModalFlavorIsPriority : DecidablePred IsPriority

Equations

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

def Kubota2026.flavor? (row : Datum) : Option Modality.ModalFlavor

The row's modal flavor.

Equations

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

def Kubota2026.PriorityRow (row : Datum) : Prop

The row's modal is a priority modal.

Equations

• Kubota2026.PriorityRow row = match Kubota2026.flavor? row with | some f => Kubota2026.IsPriority f | none => False

@[instance_reducible]

instance Kubota2026.instDecidablePriorityRow (row : Datum) : Decidable (PriorityRow row)

Equations

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

theorem Kubota2026.nanka_unrestricted (row : Datum) : row ∈ Examples.all → row.feature? "marker" = some "nanka" → row.feature? "phenomenon" = some "modalInteraction" → row.judgment = Judgment.acceptable

Nanka combines with modals of every flavor ((45)).

theorem Kubota2026.nanka_pejorative_iff_priority (row : Datum) : row ∈ Examples.all → row.feature? "marker" = some "nanka" → row.feature? "phenomenon" = some "modalInteraction" → (row.feature? "evaluation" = some "pejorative" ↔ PriorityRow row)

The negative implication of nanka is pejorative under priority modals and comparatively neutral under epistemic and ability modals ((45)).

theorem Kubota2026.semete_selects_priority (row : Datum) : row ∈ Examples.all → row.feature? "marker" = some "semete" → row.feature? "phenomenon" = some "modalInteraction" → (row.judgment = Judgment.acceptable ↔ PriorityRow row)

Semete combines with priority modals and not with epistemic or ability modals ((46)).