Japanese Particles

@cite{dayal-2025} @cite{kubota-2026} @cite{sauerland-yatsushiro-2017}

Part 1: Interrogative Particles

Q-morphemes and related particles in Japanese, following @cite{dayal-2025}.

Japanese has a three-way distinction in interrogative particles that maps directly onto the three layers of the left periphery:

1. ka/no: Clause-typing particle (CP) — obligatory in subordinated interrogatives
2. koto: Appears in declaratives (contrast with ka in interrogatives)
3. kke: Meta question particle (MQP, SAP) — only in matrix and quotation

Part 2: Outlook Markers

Adverbs and focus particles that express subjective evaluation and manage discourse stances, following @cite{kubota-2026}.

inductive Fragments.Japanese.Particles.Layer : Type

Layer of the left periphery that a particle occupies.

• cp : Layer
• perspP : Layer
• sap : Layer

instance Fragments.Japanese.Particles.instDecidableEqLayer : DecidableEq Layer

Equations

• Fragments.Japanese.Particles.instDecidableEqLayer x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Fragments.Japanese.Particles.instReprLayer.repr : Layer → ℕ → Std.Format

Equations

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

instance Fragments.Japanese.Particles.instReprLayer : Repr Layer

Equations

• Fragments.Japanese.Particles.instReprLayer = { reprPrec := Fragments.Japanese.Particles.instReprLayer.repr }

def Fragments.Japanese.Particles.instBEqLayer.beq : Layer → Layer → Bool

Equations

• Fragments.Japanese.Particles.instBEqLayer.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Fragments.Japanese.Particles.instBEqLayer : BEq Layer

Equations

• Fragments.Japanese.Particles.instBEqLayer = { beq := Fragments.Japanese.Particles.instBEqLayer.beq }

structure Fragments.Japanese.Particles.ParticleEntry : Type

A Japanese particle entry.

• form : String
• romaji : String
• layer : Layer
• inSubordinated : Bool

  Does this particle appear in subordinated interrogatives?

• inQuasiSub : Bool

  Does this particle appear in quasi-subordinated interrogatives?

• inMatrix : Bool

  Does this particle appear in matrix questions?

instance Fragments.Japanese.Particles.instReprParticleEntry : Repr ParticleEntry

Equations

• Fragments.Japanese.Particles.instReprParticleEntry = { reprPrec := Fragments.Japanese.Particles.instReprParticleEntry.repr }

def Fragments.Japanese.Particles.instReprParticleEntry.repr : ParticleEntry → ℕ → Std.Format

Equations

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

def Fragments.Japanese.Particles.instBEqParticleEntry.beq : ParticleEntry → ParticleEntry → Bool

Equations

• One or more equations did not get rendered due to their size.
• Fragments.Japanese.Particles.instBEqParticleEntry.beq x✝¹ x✝ = false

instance Fragments.Japanese.Particles.instBEqParticleEntry : BEq ParticleEntry

Equations

• Fragments.Japanese.Particles.instBEqParticleEntry = { beq := Fragments.Japanese.Particles.instBEqParticleEntry.beq }

def Fragments.Japanese.Particles.ka : ParticleEntry

ka — clause-typing Q-morpheme. Obligatory in subordinated interrogatives, optional in matrix (can be dropped). Marks CP as +WH.

Equations

• Fragments.Japanese.Particles.ka = { form := "か", romaji := "ka", layer := Fragments.Japanese.Particles.Layer.cp, inSubordinated := true, inQuasiSub := true, inMatrix := true }

def Fragments.Japanese.Particles.no_ : ParticleEntry

no — clause-typing particle for questions (informal).

Equations

• Fragments.Japanese.Particles.no_ = { form := "の", romaji := "no", layer := Fragments.Japanese.Particles.Layer.cp, inSubordinated := true, inQuasiSub := true, inMatrix := true }

def Fragments.Japanese.Particles.koto : ParticleEntry

koto — complementizer for declarative clauses. Contrast with ka: having ka in the embedded clause suffices for interrogative interpretation, while koto marks a declarative (@cite{dayal-2025}: (15)).

Equations

• Fragments.Japanese.Particles.koto = { form := "こと", romaji := "koto", layer := Fragments.Japanese.Particles.Layer.cp, inSubordinated := true, inQuasiSub := false, inMatrix := false }

def Fragments.Japanese.Particles.kke : ParticleEntry

kke — meta question particle (MQP). Only in matrix questions and quotations. Has a "remind-me" presupposition: speaker has forgotten Ans(Q) and believes the addressee knows it.

Equations

• Fragments.Japanese.Particles.kke = { form := "っけ", romaji := "kke", layer := Fragments.Japanese.Particles.Layer.sap, inSubordinated := false, inQuasiSub := false, inMatrix := true }

def Fragments.Japanese.Particles.daroo : ParticleEntry

daroo (だろう) — conjectural/epistemic copula at PerspP layer. With declarative complement: "x thinks p" (⟦daroo⟧({p})(x) = INQ_x ⊆ {p}↓). With interrogative complement: "x wonders Q" (⟦daroo⟧(Q)(x) = INQ_x ⊆ Q). The dual reading arises from the absence of an ignorance component, unlike wonder (@cite{roelofsen-uegaki-2020}, @cite{uegaki-roelofsen-2018}). Appears in matrix and quasi-subordinated contexts but not in subordinated interrogatives (which use ka).

Equations

• Fragments.Japanese.Particles.daroo = { form := "だろう", romaji := "daroo", layer := Fragments.Japanese.Particles.Layer.perspP, inSubordinated := false, inQuasiSub := true, inMatrix := true }

def Fragments.Japanese.Particles.allParticles : List ParticleEntry

Equations

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

Part 2: Outlook Markers

Japanese adverbs and focus particles that function as "outlook markers" — discourse markers with dual-layered secondary meaning (presuppositional + expressive-like). They require a salient counterstance in the discourse and express the speaker's evaluative stance toward that counterstance.

Classification (: (1)–(2))

Adverbs:

• (1a) dōse 'anyway', shosen 'anyway', yahari 'after all', kekkyoku 'after all'
• (1b) masani 'precisely', mushiro 'rather', mashite 'let alone', semete 'at least'
• (1c) yoppodo 'rather', kaette 'rather'

Focus particles:

• (2) nanka 'anything like', kurai 'at least', koso 'precisely'

inductive Fragments.Japanese.OutlookMarkers.OutlookCat : Type

Syntactic category of an outlook marker.

• adverb : OutlookCat

  Adverbial (modifies VP or sentence)

• focusParticle : OutlookCat

  Focus particle (attaches to NP or phrase)

instance Fragments.Japanese.OutlookMarkers.instDecidableEqOutlookCat : DecidableEq OutlookCat

Equations

• Fragments.Japanese.OutlookMarkers.instDecidableEqOutlookCat x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Fragments.Japanese.OutlookMarkers.instReprOutlookCat.repr : OutlookCat → ℕ → Std.Format

Equations

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

instance Fragments.Japanese.OutlookMarkers.instReprOutlookCat : Repr OutlookCat

Equations

• Fragments.Japanese.OutlookMarkers.instReprOutlookCat = { reprPrec := Fragments.Japanese.OutlookMarkers.instReprOutlookCat.repr }

instance Fragments.Japanese.OutlookMarkers.instBEqOutlookCat : BEq OutlookCat

Equations

• Fragments.Japanese.OutlookMarkers.instBEqOutlookCat = { beq := Fragments.Japanese.OutlookMarkers.instBEqOutlookCat.beq }

def Fragments.Japanese.OutlookMarkers.instBEqOutlookCat.beq : OutlookCat → OutlookCat → Bool

Equations

• Fragments.Japanese.OutlookMarkers.instBEqOutlookCat.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

structure Fragments.Japanese.OutlookMarkers.OutlookEntry : Type

An outlook marker lexical entry.

Encodes the form, stance type, syntactic category, and modal selectional restrictions following.

• form : String
• romaji : String
• gloss : String
• cat : OutlookCat
• stance : Semantics.Lexical.Expressives.OutlookMarker.StanceType
• modalCompat : Semantics.Lexical.Expressives.OutlookMarker.ModalCompatibility

  Modal selectional restrictions (which modal flavors the marker is compatible with).

• requiresCounterstance : Bool

  Does this marker require a salient counterstance in the discourse? True for all outlook markers by definition (: (37)–(38)).

instance Fragments.Japanese.OutlookMarkers.instReprOutlookEntry : Repr OutlookEntry

Equations

• Fragments.Japanese.OutlookMarkers.instReprOutlookEntry = { reprPrec := Fragments.Japanese.OutlookMarkers.instReprOutlookEntry.repr }

def Fragments.Japanese.OutlookMarkers.instReprOutlookEntry.repr : OutlookEntry → ℕ → Std.Format

Equations

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

def Fragments.Japanese.OutlookMarkers.instBEqOutlookEntry.beq : OutlookEntry → OutlookEntry → Bool

Equations

• One or more equations did not get rendered due to their size.
• Fragments.Japanese.OutlookMarkers.instBEqOutlookEntry.beq x✝¹ x✝ = false

instance Fragments.Japanese.OutlookMarkers.instBEqOutlookEntry : BEq OutlookEntry

Equations

• Fragments.Japanese.OutlookMarkers.instBEqOutlookEntry = { beq := Fragments.Japanese.OutlookMarkers.instBEqOutlookEntry.beq }

theorem Fragments.Japanese.OutlookMarkers.allRequireCounterstance (e : OutlookEntry) (h : e.requiresCounterstance = true) : e.requiresCounterstance = true

All outlook markers require a counterstance. This is definitional.

Adverbs (: (1))

def Fragments.Japanese.OutlookMarkers.dōse : OutlookEntry

dōse 'anyway' — signals pessimistic/defeatist outlook. ): "I can't win a gold medal anyway."

Equations

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

def Fragments.Japanese.OutlookMarkers.shosen : OutlookEntry

shosen 'anyway/after all' — pessimistic outlook, similar to dōse.

Equations

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

def Fragments.Japanese.OutlookMarkers.yahari : OutlookEntry

yahari 'after all/as expected' — confirms expected outcome. Incompatible with igai-ni 'unexpectedly' (: (11)).

Equations

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

def Fragments.Japanese.OutlookMarkers.kekkyoku : OutlookEntry

kekkyoku 'after all/in the end' — confirms expected outcome.

Equations

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

def Fragments.Japanese.OutlookMarkers.masani : OutlookEntry

masani 'precisely/exactly' — emphatic confirmation. ): "It is precisely you who should go."

Equations

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

def Fragments.Japanese.OutlookMarkers.mushiro : OutlookEntry

mushiro 'rather' — contrary to expected evaluation. ): "Frankly admitting your mistake actually leaves a better impression." Incompatible with igai-ni 'unexpectedly' (: (11)).

Equations

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

def Fragments.Japanese.OutlookMarkers.kaette : OutlookEntry

kaette 'rather/on the contrary' — contrary to expectation. ).

Equations

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

def Fragments.Japanese.OutlookMarkers.yoppodo : OutlookEntry

yoppodo 'much more/rather' — strong contrary evaluation. ): "Frankly admitting your mistake leaves a far better impression."

Equations

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

def Fragments.Japanese.OutlookMarkers.semete : OutlookEntry

semete 'at least' — minimum standard, settling for less. , (46)): compatible with desiderative -tai and deontic -beki but NOT with epistemic hazu or ability -eru.

Equations

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

def Fragments.Japanese.OutlookMarkers.mashite : OutlookEntry

mashite 'let alone' — a fortiori minimum standard.

Equations

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

Focus Particles (: (2))

def Fragments.Japanese.OutlookMarkers.nanka : OutlookEntry

nanka 'anything like' — negative evaluation focus particle. , (9), (37)–(42)): the prototypical outlook marker. Requires a salient counterstance; allows perspective shift under embedding.

Equations

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

def Fragments.Japanese.OutlookMarkers.kurai : OutlookEntry

kurai 'at least' — minimum standard focus particle. ): "Why don't you have something light, like some tea?"

Equations

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

def Fragments.Japanese.OutlookMarkers.koso : OutlookEntry

koso 'precisely' — emphatic confirmation focus particle. ): "It is you who should go."

Equations

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

def Fragments.Japanese.OutlookMarkers.allOutlookMarkers : List OutlookEntry

All outlook marker entries.

Equations

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

theorem Fragments.Japanese.OutlookMarkers.all_require_counterstance : (allOutlookMarkers.all fun (x : OutlookEntry) => x.requiresCounterstance) = true

All outlook markers have requiresCounterstance = true.

theorem Fragments.Japanese.OutlookMarkers.semete_unique_modal_restriction : List.map (fun (x : OutlookEntry) => x.romaji) (List.filter (fun (e : OutlookEntry) => !e.modalCompat.epistemic) allOutlookMarkers) = ["semete"]

semete is the only marker with restricted modal compatibility (rejects epistemic).

Per-Entry Verification Theorems

Each entry has a theorem verifying its stance classification, ensuring that changing a field in any entry breaks exactly one theorem.

theorem Fragments.Japanese.OutlookMarkers.dōse_is_negative : dōse.stance = Semantics.Lexical.Expressives.OutlookMarker.StanceType.negative

theorem Fragments.Japanese.OutlookMarkers.shosen_is_negative : shosen.stance = Semantics.Lexical.Expressives.OutlookMarker.StanceType.negative

theorem Fragments.Japanese.OutlookMarkers.yahari_is_emphasis : yahari.stance = Semantics.Lexical.Expressives.OutlookMarker.StanceType.emphasis

theorem Fragments.Japanese.OutlookMarkers.kekkyoku_is_emphasis : kekkyoku.stance = Semantics.Lexical.Expressives.OutlookMarker.StanceType.emphasis

theorem Fragments.Japanese.OutlookMarkers.masani_is_emphasis : masani.stance = Semantics.Lexical.Expressives.OutlookMarker.StanceType.emphasis

theorem Fragments.Japanese.OutlookMarkers.mushiro_is_contrary : mushiro.stance = Semantics.Lexical.Expressives.OutlookMarker.StanceType.contrary

theorem Fragments.Japanese.OutlookMarkers.kaette_is_contrary : kaette.stance = Semantics.Lexical.Expressives.OutlookMarker.StanceType.contrary

theorem Fragments.Japanese.OutlookMarkers.yoppodo_is_contrary : yoppodo.stance = Semantics.Lexical.Expressives.OutlookMarker.StanceType.contrary

theorem Fragments.Japanese.OutlookMarkers.semete_is_minimum : semete.stance = Semantics.Lexical.Expressives.OutlookMarker.StanceType.minimum

theorem Fragments.Japanese.OutlookMarkers.mashite_is_minimum : mashite.stance = Semantics.Lexical.Expressives.OutlookMarker.StanceType.minimum

theorem Fragments.Japanese.OutlookMarkers.nanka_is_negative : nanka.stance = Semantics.Lexical.Expressives.OutlookMarker.StanceType.negative

theorem Fragments.Japanese.OutlookMarkers.kurai_is_minimum : kurai.stance = Semantics.Lexical.Expressives.OutlookMarker.StanceType.minimum

theorem Fragments.Japanese.OutlookMarkers.koso_is_emphasis : koso.stance = Semantics.Lexical.Expressives.OutlookMarker.StanceType.emphasis