Arka (2013): the typology and syntax of TAM in Indonesian

[arka-2013] argues that Indonesian TAM is morphosemantic and contextual, not grammatical: there is no obligatory morphosyntactic TAM opposition, yet the language shows a genuine finiteness contrast, diagnosed by the distribution of the TAM auxiliaries (sudah/telah, mau, sedang, akan) occupying I(NFL).

Formalized over Time.ReichenbachFrame and the [Sne96] marker inventory (Fragments/Indonesian/TAM.lean):

1. Grammaticalization contrast (§2): sudah/telah expresses bare E < R; the English present perfect additionally pins R to speech time. Hence [klein-1992]'s present perfect puzzle (Kiparsky2002.present_perfect_puzzle) does not arise: Dia sudah pergi kemarin is satisfiable (E < R < S). Following [kibort-2009], the underlying semantics is shared and only the grammaticalized E,R,S configuration differs.
2. Finiteness (§3): auxiliaries sit in I; truncated/controlled complements are bare VPs; equational/nominal predications project no I — jointly predicting the auxiliary-acceptability paradigm.
3. Cross-source bridge: Arka's auxiliary class matches the [Sne96] temporal markers except mau, which Sneddon sets apart as a full verb — a genuine classification divergence between the sources.

Not formalized (documented for follow-up): the default-past temporal axis of =nya nominalization and its cancellability by nanti (Arka's kapan-question evidence), the voice–TAM affinities, and evidential katanya.

Reichenbachian semantics of the TAM auxiliaries

def Arka2013.frameSemantics {T : Type u_1} [LinearOrder T] : Indonesian.TemporalMeaning → Option (Time.ReichenbachFrame T → Prop)

The frame relation [arka-2013] assigns to each auxiliary meaning: sudah/telah E < R with R free, sedang E = R, akan future R with E at R (point form of his S < E-R). none for marker meanings the paper does not analyze.

Equations

• Arka2013.frameSemantics Indonesian.TemporalMeaning.occurred = some fun (x : Time.ReichenbachFrame T) => x.isPerfect
• Arka2013.frameSemantics Indonesian.TemporalMeaning.inProgress = some fun (x : Time.ReichenbachFrame T) => x.isPerfective
• Arka2013.frameSemantics Indonesian.TemporalMeaning.future = some fun (f : Time.ReichenbachFrame T) => f.isFuture ∧ f.isPerfective
• Arka2013.frameSemantics x✝ = none

def Arka2013.englishPresentPerfect {T : Type u_1} [LinearOrder T] (f : Time.ReichenbachFrame T) : Prop

The English present perfect grammaticalizes E < R together with R pinned to the deictic centre ([arka-2013] §2, after [klein-1992] and [kibort-2009]).

Equations

• Arka2013.englishPresentPerfect f = (f.isPerfect ∧ f.isPresent)

@[implicit_reducible]

instance Arka2013.instDecidableEnglishPresentPerfect {T : Type u_1} [LinearOrder T] (f : Time.ReichenbachFrame T) : Decidable (englishPresentPerfect f)

Equations

• Arka2013.instDecidableEnglishPresentPerfect f = id inferInstance

theorem Arka2013.telah_sudah_same_semantics {T : Type u_1} [LinearOrder T] : frameSemantics Indonesian.telah.meaning = frameSemantics Indonesian.sudah.meaning

telah expresses the same frame relation as sudah — the fragment's register-only contrast (Indonesian.telah_sudah_same_meaning_distinct_register) transported through [arka-2013]'s semantic assignment.

theorem Arka2013.sudah_allows_past_reference : ∃ (f : Time.ReichenbachFrame ℤ), f.isPerfect ∧ f.isPast ∧ f.isSimpleCase

Dia sudah pergi kemarin: sudah tolerates a past reference time — witness frame E < R < P = S. "Sudah/telah is also compatible with a specific past reference such as kemarin."

theorem Arka2013.sudah_allows_present_reference : ∃ (f : Time.ReichenbachFrame ℤ), f.isPerfect ∧ f.isPresent ∧ f.isSimpleCase

Dia sudah pergi (sekarang): the English-present-perfect-like reading E < R = S is also available — R is genuinely free.

theorem Arka2013.klein_puzzle_dissolved : (∀ (f : Time.ReichenbachFrame ℤ), englishPresentPerfect f → f.isPast → False) ∧ ∃ (f : Time.ReichenbachFrame ℤ), f.isPerfect ∧ f.isPast

[klein-1992]'s puzzle and its Indonesian dissolution: with a past-time adverbial (R < P), the English present perfect is contradictory (Kiparsky2002.present_perfect_puzzle), while sudah under the same constraint is satisfiable. Languages grammaticalize different E,R,S configurations of one underlying semantics ([kibort-2009]).

theorem Arka2013.english_pp_strictly_stronger {T : Type u_1} [LinearOrder T] : (∀ (f : Time.ReichenbachFrame T), englishPresentPerfect f → f.isPerfect) ∧ ∃ (f : Time.ReichenbachFrame ℤ), f.isPerfect ∧ ¬englishPresentPerfect f

The English present perfect strictly strengthens sudah: every English present-perfect frame is a sudah frame, but not conversely.

Finiteness: auxiliaries in I, truncated complements as bare VPs

inductive Arka2013.Projection : Type

Clause projections in [arka-2013]'s LFG analysis: finite clauses project IP whose I hosts the TAM auxiliaries; truncated/controlled complements are bare VPs; equational/nominal predications project no verbal structure.

• ip : Projection
• vp : Projection
• nominal : Projection

@[implicit_reducible]

instance Arka2013.instDecidableEqProjection : DecidableEq Projection

Equations

• Arka2013.instDecidableEqProjection x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Arka2013.instReprProjection.repr : Projection → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Arka2013.instReprProjection.repr Arka2013.Projection.ip prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Arka2013.Projection.ip")).group prec✝
• Arka2013.instReprProjection.repr Arka2013.Projection.vp prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Arka2013.Projection.vp")).group prec✝

@[implicit_reducible]

instance Arka2013.instReprProjection : Repr Projection

Equations

• Arka2013.instReprProjection = { reprPrec := Arka2013.instReprProjection.repr }

def Arka2013.Projection.hasInfl (p : Projection) : Prop

The I(NFL) position exists only in IP.

Equations

• p.hasInfl = (p = Arka2013.Projection.ip)

@[implicit_reducible]

instance Arka2013.instDecidablePredProjectionHasInfl : DecidablePred Projection.hasInfl

Equations

• Arka2013.instDecidablePredProjectionHasInfl p = Arka2013.instDecidablePredProjectionHasInfl._aux_1 p

structure Arka2013.ClauseType : Type

A clause type from [arka-2013]'s finiteness paradigm: the construction, the projection his analysis assigns, and the observed acceptability of a TAM auxiliary inside it.

• construction : String
• projection : Projection
• auxAcceptable : Bool

  Observed: a TAM auxiliary is acceptable inside the clause.

@[implicit_reducible]

instance Arka2013.instDecidableEqClauseType : DecidableEq ClauseType

Equations

• Arka2013.instDecidableEqClauseType = Arka2013.instDecidableEqClauseType.decEq

def Arka2013.instDecidableEqClauseType.decEq (x✝ x✝¹ : ClauseType) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Arka2013.instReprClauseType : Repr ClauseType

Equations

• Arka2013.instReprClauseType = { reprPrec := Arka2013.instReprClauseType.repr }

def Arka2013.instReprClauseType.repr : ClauseType → ℕ → Std.Format

Equations

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

def Arka2013.rootClause : ClauseType

Root clause: Dia akan/sudah/sedang makan.

Equations

• Arka2013.rootClause = { construction := "root clause", projection := Arka2013.Projection.ip, auxAcceptable := true }

def Arka2013.bahwaComplement : ClauseType

Finite bahwa 'that' complement: Saya tahu bahwa mereka akan datang.

Equations

• Arka2013.bahwaComplement = { construction := "bahwa complement", projection := Arka2013.Projection.ip, auxAcceptable := true }

def Arka2013.agarPurposive : ClauseType

Finite agar 'so that' purposive: Saya belajar agar (bisa) menembak.

Equations

• Arka2013.agarPurposive = { construction := "agar purposive", projection := Arka2013.Projection.ip, auxAcceptable := true }

def Arka2013.inginComplement : ClauseType

Truncated complement of ingin 'want': Mereka ingin [(ˣakan) datang].

Equations

• Arka2013.inginComplement = { construction := "ingin complement", projection := Arka2013.Projection.vp, auxAcceptable := false }

def Arka2013.menyuruhComplement : ClauseType

Controlled complement of menyuruh 'order': Saya menyuruh dia [(ˣakan/sudah/sedang) makan].

Equations

• Arka2013.menyuruhComplement = { construction := "menyuruh complement", projection := Arka2013.Projection.vp, auxAcceptable := false }

def Arka2013.resultativeComplement : ClauseType

Resultative complement: Orang itu mendorong saya [(ˣakan/sedang/sudah) jatuh].

Equations

• Arka2013.resultativeComplement = { construction := "resultative complement", projection := Arka2013.Projection.vp, auxAcceptable := false }

def Arka2013.sambilAdjunct : ClauseType

sambil 'while' adjunct: Dia datang [(sambil) (ˣsedang) menangis].

Equations

• Arka2013.sambilAdjunct = { construction := "sambil adjunct", projection := Arka2013.Projection.vp, auxAcceptable := false }

def Arka2013.belajarComplement : ClauseType

Complement of belajar 'learn': Saya belajar [(ˣbisa) menembak].

Equations

• Arka2013.belajarComplement = { construction := "belajar complement", projection := Arka2013.Projection.vp, auxAcceptable := false }

def Arka2013.nominalPredication : ClauseType

Equational/nominal predication: (ˣakan) tanyanya, (ˣsedang) tampaknya — "a nominal predicate cannot take an auxiliary".

Equations

• Arka2013.nominalPredication = { construction := "nominal predication", projection := Arka2013.Projection.nominal, auxAcceptable := false }

def Arka2013.paradigm : List ClauseType

[arka-2013]'s finiteness paradigm.

Equations

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

theorem Arka2013.aux_distribution_diagnoses_finiteness (c : ClauseType) : c ∈ paradigm → (c.projection.hasInfl ↔ c.auxAcceptable = true)

The I-position account predicts the paradigm exactly: an auxiliary is acceptable iff the clause projects I. Auxiliary distribution thereby diagnoses finiteness in a language with no inflectional TAM — Arka's central claim.

Arka's auxiliary class vs the Sneddon inventory

def Arka2013.auxiliaryForms : List String

[arka-2013]'s TAM auxiliaries: "sudah/telah, mau, sedang, and akan".

Equations

• Arka2013.auxiliaryForms = ["sudah", "telah", "mau", "sedang", "akan"]

theorem Arka2013.auxiliaries_vs_sneddon_markers : List.filter (fun (s : String) => (List.map (fun (x : Indonesian.TemporalMarker) => x.form) Indonesian.temporalMarkers).contains s) auxiliaryForms = ["sudah", "telah", "sedang", "akan"] ∧ ¬(List.map (fun (x : Indonesian.TemporalMarker) => x.form) Indonesian.temporalMarkers).contains "mau" = true

Every Arka auxiliary except mau is a [Sne96] temporal marker, and mau is not one: Sneddon sets volitional mau/ingin apart as full verbs where Arka classifies mau as an I-position auxiliary — a genuine classification divergence between the sources.

theorem Arka2013.glosses_match_fragment : Indonesian.akan.meaning = Indonesian.TemporalMeaning.future ∧ Indonesian.sedang.meaning = Indonesian.TemporalMeaning.inProgress ∧ Indonesian.sudah.meaning = Indonesian.TemporalMeaning.occurred ∧ Indonesian.telah.meaning = Indonesian.TemporalMeaning.occurred

[arka-2013]'s glosses (akan 'FUT', sedang 'PROG', sudah/telah 'PERF') agree with the [Sne96]-derived meanings in the fragment.