Japanese Particles

[Day25] [Kub26] [SY17]

Part 1: Interrogative Particles

Q-morphemes and related particles in Japanese, as Particle values with embedding-distribution facets. The left-peripheral layer assignments are derived from those facets in BhattDayal2020.

1. ka/no: Clause-typing Q-morphemes — appear in subordinated interrogatives
2. koto: Declarative complementizer (contrast with ka in interrogatives)
3. kke: Meta question particle — only in matrix and quotation
4. daroo: Conjectural/epistemic copula

Part 2: Outlook Markers

Adverbs and focus particles that express subjective evaluation and manage discourse stances, following [Kub26]. The fragment carries the theory-neutral lexical inventory (form + category); [Kub26]'s stance classification and modal selectional restrictions live in Studies/Kubota2026.lean.

def Japanese.Particles.ka : Particle

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

Equations

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

def Japanese.Particles.no_ : Particle

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

Equations

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

def Japanese.Particles.koto : Particle

koto — complementizer for declarative clauses. Contrast with ka: having ka in the embedded clause suffices for interrogative interpretation, while koto marks a declarative ([Day25]: (15)). Subordinated clauses only.

Equations

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

def Japanese.Particles.kke : Particle

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

Equations

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

def Japanese.Particles.daroo : Particle

daroo (だろう) — conjectural/epistemic copula. 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 ([RU20], [UR18]). Appears in matrix and quasi-subordinated contexts but not in subordinated interrogatives (which use ka).

Equations

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

def Japanese.Particles.allParticles : List Particle

Equations

• Japanese.Particles.allParticles = [Japanese.Particles.ka, Japanese.Particles.no_, Japanese.Particles.koto, Japanese.Particles.kke, Japanese.Particles.daroo]

Part 2: Outlook Markers

Theory-neutral lexical inventory of the Japanese adverbs and focus particles that [Kub26] analyses as outlook markers ([Kub26] (1)-(2)). The stance classification, modal restrictions, and dual-layer denotation are paper apparatus and live in Studies/Kubota2026.lean.

inductive Japanese.OutlookMarkers.Category : Type

Gross syntactic category of an outlook marker ([Kub26] (1)-(2)): the standard adverb vs. toritate focus-particle distinction.

• adverb : Category
• focusParticle : Category

@[implicit_reducible]

instance Japanese.OutlookMarkers.instDecidableEqCategory : DecidableEq Category

Equations

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

def Japanese.OutlookMarkers.instReprCategory.repr : Category → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Japanese.OutlookMarkers.instReprCategory : Repr Category

Equations

• Japanese.OutlookMarkers.instReprCategory = { reprPrec := Japanese.OutlookMarkers.instReprCategory.repr }

@[implicit_reducible]

instance Japanese.OutlookMarkers.instInhabitedCategory : Inhabited Category

Equations

• Japanese.OutlookMarkers.instInhabitedCategory = { default := Japanese.OutlookMarkers.instInhabitedCategory.default }

structure Japanese.OutlookMarkers.OutlookMarkerForm : Type

An outlook-marker lexical entry — theory-neutral surface facts only.

• form : String
• romaji : String
• gloss : String
• category : Category

@[implicit_reducible]

instance Japanese.OutlookMarkers.instDecidableEqOutlookMarkerForm : DecidableEq OutlookMarkerForm

Equations

• Japanese.OutlookMarkers.instDecidableEqOutlookMarkerForm = Japanese.OutlookMarkers.instDecidableEqOutlookMarkerForm.decEq

def Japanese.OutlookMarkers.instDecidableEqOutlookMarkerForm.decEq (x✝ x✝¹ : OutlookMarkerForm) : Decidable (x✝ = x✝¹)

Equations

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

def Japanese.OutlookMarkers.instReprOutlookMarkerForm.repr : OutlookMarkerForm → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Japanese.OutlookMarkers.instReprOutlookMarkerForm : Repr OutlookMarkerForm

Equations

• Japanese.OutlookMarkers.instReprOutlookMarkerForm = { reprPrec := Japanese.OutlookMarkers.instReprOutlookMarkerForm.repr }

def Japanese.OutlookMarkers.expressiveKind : Features.Expressive

Outlook markers are all use-conditional items of one expressive class — the consensus metadata Fragments carry; the diagnostic fingerprint lives in Studies/Kubota2026.lean.

Equations

• Japanese.OutlookMarkers.expressiveKind = Features.Expressive.outlookMarker

Adverbs ([Kub26] (1))

def Japanese.OutlookMarkers.dōse : OutlookMarkerForm

Equations

• Japanese.OutlookMarkers.dōse = { form := "どうせ", romaji := "dōse", gloss := "anyway", category := Japanese.OutlookMarkers.Category.adverb }

def Japanese.OutlookMarkers.shosen : OutlookMarkerForm

Equations

• Japanese.OutlookMarkers.shosen = { form := "所詮", romaji := "shosen", gloss := "anyway/after all", category := Japanese.OutlookMarkers.Category.adverb }

def Japanese.OutlookMarkers.yahari : OutlookMarkerForm

Equations

• Japanese.OutlookMarkers.yahari = { form := "やはり", romaji := "yahari", gloss := "after all/as expected", category := Japanese.OutlookMarkers.Category.adverb }

def Japanese.OutlookMarkers.kekkyoku : OutlookMarkerForm

Equations

• Japanese.OutlookMarkers.kekkyoku = { form := "結局", romaji := "kekkyoku", gloss := "after all/in the end", category := Japanese.OutlookMarkers.Category.adverb }

def Japanese.OutlookMarkers.masani : OutlookMarkerForm

Equations

• Japanese.OutlookMarkers.masani = { form := "まさに", romaji := "masani", gloss := "precisely", category := Japanese.OutlookMarkers.Category.adverb }

def Japanese.OutlookMarkers.mushiro : OutlookMarkerForm

Equations

• Japanese.OutlookMarkers.mushiro = { form := "むしろ", romaji := "mushiro", gloss := "rather", category := Japanese.OutlookMarkers.Category.adverb }

def Japanese.OutlookMarkers.kaette : OutlookMarkerForm

Equations

• Japanese.OutlookMarkers.kaette = { form := "かえって", romaji := "kaette", gloss := "rather/on the contrary", category := Japanese.OutlookMarkers.Category.adverb }

def Japanese.OutlookMarkers.yoppodo : OutlookMarkerForm

Equations

• Japanese.OutlookMarkers.yoppodo = { form := "よっぽど", romaji := "yoppodo", gloss := "much more/rather", category := Japanese.OutlookMarkers.Category.adverb }

def Japanese.OutlookMarkers.semete : OutlookMarkerForm

Equations

• Japanese.OutlookMarkers.semete = { form := "せめて", romaji := "semete", gloss := "at least", category := Japanese.OutlookMarkers.Category.adverb }

def Japanese.OutlookMarkers.mashite : OutlookMarkerForm

Equations

• Japanese.OutlookMarkers.mashite = { form := "まして", romaji := "mashite", gloss := "let alone", category := Japanese.OutlookMarkers.Category.adverb }

Focus particles ([Kub26] (2))

def Japanese.OutlookMarkers.nanka : OutlookMarkerForm

Equations

• Japanese.OutlookMarkers.nanka = { form := "なんか", romaji := "nanka", gloss := "anything like", category := Japanese.OutlookMarkers.Category.focusParticle }

def Japanese.OutlookMarkers.kurai : OutlookMarkerForm

Equations

• Japanese.OutlookMarkers.kurai = { form := "くらい", romaji := "kurai", gloss := "at least", category := Japanese.OutlookMarkers.Category.focusParticle }

def Japanese.OutlookMarkers.koso : OutlookMarkerForm

Equations

• Japanese.OutlookMarkers.koso = { form := "こそ", romaji := "koso", gloss := "precisely", category := Japanese.OutlookMarkers.Category.focusParticle }

def Japanese.OutlookMarkers.all : List OutlookMarkerForm

The Japanese outlook-marker lexical inventory ([Kub26] (1)-(2)).

Equations

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