Kwon and Lee (2026): Accessibility Markers in Korean

This file formalizes [KL26]'s three experiments on Korean null pronouns, the colloquial overt pronoun kyay, and demonstrative-plus-noun full NPs as markers on [Ari01]'s Accessibility Marking Scale. KoreanRefForm places the three forms on the substrate's scale and inherits its linear order, so the form–function criteria, more accessible forms being more attenuated and less informative, are monotonicity statements (attenuation_strictMono, informativity_antitone). The paper's central finding, from the globally ambiguous contexts of Experiment 3, is that subject-antecedent choice increases strictly with accessibility (subjectBias_strictMono), separating the three forms (three_way_split) while naturalness stays flat (exp3_naturalness_flat). Experiment 1 finds the null pronoun most natural with a sole antecedent and no difference between the overt pronoun and the full NP (exp1_null_most_natural, exp1_overt_fullNP_close); Experiment 2 finds only the null pronoun sensitive to a context biased against its subject preference, in comprehension accuracy and in naturalness alike (exp2_only_null_context_sensitive, exp2_naturalness_only_null_asymmetric), with trials interpreted as intended rated more natural (correct_trials_more_natural).

The comparison the paper draws in its introduction with Italian ([Car02]), Spanish ([CDD21]), Chinese ([ZK22]), and the earlier Korean studies ([Kwe11], [Cho21]) is recorded as CrossLingProfiles: the null pronoun is more subject-biased than the overt one in every study (null_gt_overt_universally), the spread is widest in Italian (italian_widest_spread), the present overt pronoun is object-biased as in [Kwe11] and unlike [Cho21] (overt_object_biased_as_kweon), and in Korean the null-versus-overt step in bias far exceeds the overt-versus-full-NP step (null_nonnull_cliff), the paper's conclusion that the primary accessibility contrast in Korean is between null and non-null forms.

Implementation notes

Percentages are rounded to whole points as the paper reports them, means on the seven-point scale to hundredths. Kyay is placed at the unstressed-pronoun level rather than at a demonstrative one, following the paper's argument that it has become a third-person pronoun, and the full NP at the distal-demonstrative-plus-noun level. Subject-bias values of the comparison studies are complements of the reported object biases where only those are given.

References

• [KL26]
• [Ari01]
• [Car02]
• [CDD21]
• [ZK22]
• [Kwe11]
• [Cho21]

The three referential forms on the accessibility scale

inductive KwonLee2026.KoreanRefForm : Type

The three Korean referring expressions tested.

• nullPro : KoreanRefForm

  The null pronoun.

• overt : KoreanRefForm

  The colloquial gender-neutral third-person pronoun kyay.

• fullNP : KoreanRefForm

  A demonstrative followed by a noun, such as ku chinkwu 'that friend'.

@[instance_reducible]

instance KwonLee2026.instDecidableEqKoreanRefForm : DecidableEq KoreanRefForm

Equations

• KwonLee2026.instDecidableEqKoreanRefForm x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance KwonLee2026.instReprKoreanRefForm : Repr KoreanRefForm

Equations

• KwonLee2026.instReprKoreanRefForm = { reprPrec := KwonLee2026.instReprKoreanRefForm.repr }

def KwonLee2026.instReprKoreanRefForm.repr : KoreanRefForm → ℕ → Std.Format

Equations

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

def KwonLee2026.KoreanRefForm.toAccessibility : KoreanRefForm → Discourse.AccessibilityLevel

The position of each form on the Accessibility Marking Scale.

Equations

• KwonLee2026.KoreanRefForm.nullPro.toAccessibility = Discourse.AccessibilityLevel.zero
• KwonLee2026.KoreanRefForm.overt.toAccessibility = Discourse.AccessibilityLevel.unstressedPron
• KwonLee2026.KoreanRefForm.fullNP.toAccessibility = Discourse.AccessibilityLevel.distalDemNP

def KwonLee2026.KoreanRefForm.rank (f : KoreanRefForm) : ℕ

The accessibility rank of a form.

Equations

• f.rank = f.toAccessibility.rank

@[instance_reducible]

instance KwonLee2026.instLinearOrderKoreanRefForm : LinearOrder KoreanRefForm

The forms ordered by accessibility: fullNP < overt < nullPro.

Equations

• KwonLee2026.instLinearOrderKoreanRefForm = LinearOrder.lift' KwonLee2026.KoreanRefForm.rank ⋯

theorem KwonLee2026.fullNP_lt_overt : KoreanRefForm.fullNP < KoreanRefForm.overt

theorem KwonLee2026.overt_lt_nullPro : KoreanRefForm.overt < KoreanRefForm.nullPro

def KwonLee2026.KoreanRefForm.surface : KoreanRefForm → Option String

The surface form: the overt pronoun is the fragment's gyae; the full NP varies with the item.

Equations

• KwonLee2026.KoreanRefForm.nullPro.surface = none
• KwonLee2026.KoreanRefForm.overt.surface = some Korean.Pronouns.gyae.form
• KwonLee2026.KoreanRefForm.fullNP.surface = some "ku chinkwu"

theorem KwonLee2026.attenuation_strictMono : StrictMono fun (f : KoreanRefForm) => f.toAccessibility.attenuation

More accessible forms are more phonologically attenuated.

theorem KwonLee2026.informativity_antitone : Antitone fun (f : KoreanRefForm) => f.toAccessibility.informativity

More accessible forms are no more informative; the null and the overt pronoun both carry no lexical information.

Experiment 3: antecedent choice under global ambiguity

structure KwonLee2026.AntecedentChoice : Type

Antecedent choice for one form, as percentages of subject and object choices (Figure 3).

• form : KoreanRefForm

  The form.

• subjectPercent : ℕ

  The percentage of subject-antecedent choices.

• objectPercent : ℕ

  The percentage of object-antecedent choices.

@[instance_reducible]

instance KwonLee2026.instReprAntecedentChoice : Repr AntecedentChoice

Equations

• KwonLee2026.instReprAntecedentChoice = { reprPrec := KwonLee2026.instReprAntecedentChoice.repr }

def KwonLee2026.instReprAntecedentChoice.repr : AntecedentChoice → ℕ → Std.Format

Equations

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

def KwonLee2026.exp3_pro : AntecedentChoice

The null pronoun: 70.6% subject choices.

Equations

• KwonLee2026.exp3_pro = { form := KwonLee2026.KoreanRefForm.nullPro, subjectPercent := 71, objectPercent := 29 }

def KwonLee2026.exp3_overt : AntecedentChoice

Kyay: 42.8% subject choices.

Equations

• KwonLee2026.exp3_overt = { form := KwonLee2026.KoreanRefForm.overt, subjectPercent := 43, objectPercent := 57 }

def KwonLee2026.exp3_fullNP : AntecedentChoice

The full NP: 35.3% subject choices.

Equations

• KwonLee2026.exp3_fullNP = { form := KwonLee2026.KoreanRefForm.fullNP, subjectPercent := 35, objectPercent := 65 }

def KwonLee2026.subjectBias : KoreanRefForm → ℕ

Subject-antecedent bias by form.

Equations

• KwonLee2026.subjectBias KwonLee2026.KoreanRefForm.nullPro = KwonLee2026.exp3_pro.subjectPercent
• KwonLee2026.subjectBias KwonLee2026.KoreanRefForm.overt = KwonLee2026.exp3_overt.subjectPercent
• KwonLee2026.subjectBias KwonLee2026.KoreanRefForm.fullNP = KwonLee2026.exp3_fullNP.subjectPercent

def KwonLee2026.objectBias : KoreanRefForm → ℕ

Object-antecedent bias by form.

Equations

• KwonLee2026.objectBias KwonLee2026.KoreanRefForm.nullPro = KwonLee2026.exp3_pro.objectPercent
• KwonLee2026.objectBias KwonLee2026.KoreanRefForm.overt = KwonLee2026.exp3_overt.objectPercent
• KwonLee2026.objectBias KwonLee2026.KoreanRefForm.fullNP = KwonLee2026.exp3_fullNP.objectPercent

theorem KwonLee2026.exp3_partitions (f : KoreanRefForm) : subjectBias f + objectBias f = 100

The forced choice partitions the responses.

theorem KwonLee2026.subjectBias_strictMono : StrictMono subjectBias

Subject-antecedent bias increases strictly with accessibility: the form–function correlation of Accessibility Theory.

theorem KwonLee2026.objectBias_strictAnti : StrictAnti objectBias

Object-antecedent bias decreases strictly with accessibility.

theorem KwonLee2026.three_way_split : Function.Injective subjectBias

The three forms are three distinct markers, not a null-versus-non-null contrast.

def KwonLee2026.exp3_naturalness : KoreanRefForm → ℚ

Mean naturalness on the seven-point scale (Table 5).

Equations

• KwonLee2026.exp3_naturalness KwonLee2026.KoreanRefForm.nullPro = 53 / 10
• KwonLee2026.exp3_naturalness KwonLee2026.KoreanRefForm.overt = 53 / 10
• KwonLee2026.exp3_naturalness KwonLee2026.KoreanRefForm.fullNP = 54 / 10

theorem KwonLee2026.exp3_naturalness_flat (f g : KoreanRefForm) : exp3_naturalness f - exp3_naturalness g ≤ 1 / 10

Under global ambiguity the three forms are equally natural: the accessibility distinction shows in interpretation, not in acceptability.

Experiment 1: a sole antecedent

def KwonLee2026.exp1_naturalness : KoreanRefForm → ℚ

Mean naturalness on the seven-point scale with a single available antecedent (Table 1).

Equations

• KwonLee2026.exp1_naturalness KwonLee2026.KoreanRefForm.nullPro = 641 / 100
• KwonLee2026.exp1_naturalness KwonLee2026.KoreanRefForm.overt = 618 / 100
• KwonLee2026.exp1_naturalness KwonLee2026.KoreanRefForm.fullNP = 623 / 100

theorem KwonLee2026.exp1_null_most_natural : exp1_naturalness KoreanRefForm.overt < exp1_naturalness KoreanRefForm.nullPro ∧ exp1_naturalness KoreanRefForm.fullNP < exp1_naturalness KoreanRefForm.nullPro

The null pronoun is the most natural way to refer to the sole, hence maximally accessible, antecedent.

theorem KwonLee2026.exp1_overt_fullNP_close : exp1_naturalness KoreanRefForm.fullNP - exp1_naturalness KoreanRefForm.overt ≤ 1 / 10

The overt pronoun and the full NP do not differ, against a strict reading of the scale.

Experiment 2: a context biased toward the subject or the object

structure KwonLee2026.Exp2Result : Type

One form's results in Experiment 2: comprehension accuracy (Figure 1, in percent) and mean naturalness (Figure 2) under a subject-biased and under an object-biased context.

• form : KoreanRefForm

  The form.

• subjectAccuracy : ℕ

  Accuracy under a subject-biased context.

• objectAccuracy : ℕ

  Accuracy under an object-biased context.

• subjectNaturalness : ℚ

  Naturalness under a subject-biased context.

• objectNaturalness : ℚ

  Naturalness under an object-biased context.

def KwonLee2026.instReprExp2Result.repr : Exp2Result → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance KwonLee2026.instReprExp2Result : Repr Exp2Result

Equations

• KwonLee2026.instReprExp2Result = { reprPrec := KwonLee2026.instReprExp2Result.repr }

def KwonLee2026.exp2_pro : Exp2Result

The null pronoun: 92.9% against 60.3% accuracy, 4.58 against 3.94 naturalness.

Equations

• KwonLee2026.exp2_pro = { form := KwonLee2026.KoreanRefForm.nullPro, subjectAccuracy := 93, objectAccuracy := 60, subjectNaturalness := 458 / 100, objectNaturalness := 394 / 100 }

def KwonLee2026.exp2_overt : Exp2Result

Kyay: 81.4% against 78.2% accuracy, 4.62 against 4.42 naturalness.

Equations

• KwonLee2026.exp2_overt = { form := KwonLee2026.KoreanRefForm.overt, subjectAccuracy := 81, objectAccuracy := 78, subjectNaturalness := 462 / 100, objectNaturalness := 442 / 100 }

def KwonLee2026.exp2_fullNP : Exp2Result

The full NP: 79.4% against 79.5% accuracy, 4.33 against 4.56 naturalness.

Equations

• KwonLee2026.exp2_fullNP = { form := KwonLee2026.KoreanRefForm.fullNP, subjectAccuracy := 79, objectAccuracy := 80, subjectNaturalness := 433 / 100, objectNaturalness := 456 / 100 }

def KwonLee2026.Exp2Result.accuracyGap (r : Exp2Result) : ℕ

The accuracy gap between the two contexts.

Equations

• r.accuracyGap = max r.subjectAccuracy r.objectAccuracy - min r.subjectAccuracy r.objectAccuracy

def KwonLee2026.Exp2Result.naturalnessGap (r : Exp2Result) : ℚ

The naturalness gap between the two contexts.

Equations

• r.naturalnessGap = max r.subjectNaturalness r.objectNaturalness - min r.subjectNaturalness r.objectNaturalness

theorem KwonLee2026.exp2_only_null_context_sensitive : 30 < exp2_pro.accuracyGap ∧ exp2_overt.accuracyGap ≤ 5 ∧ exp2_fullNP.accuracyGap ≤ 5

Only the null pronoun resists a context biased against its subject preference: its accuracy drops by over thirty points while the other forms move by at most five.

theorem KwonLee2026.exp2_naturalness_only_null_asymmetric : 1 / 2 < exp2_pro.naturalnessGap ∧ exp2_overt.naturalnessGap ≤ 1 / 4 ∧ exp2_fullNP.naturalnessGap ≤ 1 / 4

The naturalness ratings show the same asymmetry: only the null pronoun is rated more than half a point lower under the object-biased context.

def KwonLee2026.correctTrialNaturalness : ℚ

Mean naturalness of trials answered as intended, 4.40, and of the others, 4.05.

Equations

• KwonLee2026.correctTrialNaturalness = 440 / 100

def KwonLee2026.incorrectTrialNaturalness : ℚ

Equations

• KwonLee2026.incorrectTrialNaturalness = 405 / 100

theorem KwonLee2026.correct_trials_more_natural : incorrectTrialNaturalness < correctTrialNaturalness

Trials interpreted as intended are rated more natural: the form–function match is felt.

The cross-linguistic comparison

structure KwonLee2026.CrossLingProfile : Type

A study's subject-antecedent bias for the null and the overt pronoun under global ambiguity, in percent.

• study : String

  The language and study.

• nullSubject : ℕ

  Subject choices for the null pronoun.

• overtSubject : ℕ

  Subject choices for the overt pronoun.

@[instance_reducible]

instance KwonLee2026.instReprCrossLingProfile : Repr CrossLingProfile

Equations

• KwonLee2026.instReprCrossLingProfile = { reprPrec := KwonLee2026.instReprCrossLingProfile.repr }

def KwonLee2026.instReprCrossLingProfile.repr : CrossLingProfile → ℕ → Std.Format

Equations

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

def KwonLee2026.italian : CrossLingProfile

Italian ([Car02]): 80.72% subject for the null pronoun, 83.33% object for the overt one.

Equations

• KwonLee2026.italian = { study := "Italian", nullSubject := 81, overtSubject := 17 }

def KwonLee2026.spanish : CrossLingProfile

Spanish ([CDD21]): 62% subject for the null pronoun, 58% object for the overt one.

Equations

• KwonLee2026.spanish = { study := "Spanish", nullSubject := 62, overtSubject := 42 }

def KwonLee2026.chinese : CrossLingProfile

Chinese ([ZK22]): 84% and 65.3% subject.

Equations

• KwonLee2026.chinese = { study := "Chinese", nullSubject := 84, overtSubject := 65 }

def KwonLee2026.korean : CrossLingProfile

Korean with kyay, Experiment 3.

Equations

• KwonLee2026.korean = { study := "Korean", nullSubject := KwonLee2026.exp3_pro.subjectPercent, overtSubject := KwonLee2026.exp3_overt.subjectPercent }

def KwonLee2026.koreanKweon : CrossLingProfile

Korean with ku and kunye ([Kwe11]): 81.1% and 31.4% subject.

Equations

• KwonLee2026.koreanKweon = { study := "Korean (Kweon 2011)", nullSubject := 81, overtSubject := 31 }

def KwonLee2026.koreanChoe : CrossLingProfile

Korean with ku and kunye ([Cho21]): 91% and 73% subject.

Equations

• KwonLee2026.koreanChoe = { study := "Korean (Choe 2021)", nullSubject := 91, overtSubject := 73 }

def KwonLee2026.profiles : List CrossLingProfile

The studies compared.

Equations

• KwonLee2026.profiles = [KwonLee2026.italian, KwonLee2026.spanish, KwonLee2026.chinese, KwonLee2026.korean, KwonLee2026.koreanKweon, KwonLee2026.koreanChoe]

theorem KwonLee2026.null_gt_overt_universally (p : CrossLingProfile) : p ∈ profiles → p.overtSubject < p.nullSubject

The relative ordering is universal: in every study the null pronoun is more subject-biased than the overt one.

def KwonLee2026.CrossLingProfile.spread (p : CrossLingProfile) : ℕ

The spread between the two pronouns.

Equations

• p.spread = p.nullSubject - p.overtSubject

theorem KwonLee2026.italian_widest_spread : spanish.spread < italian.spread ∧ chinese.spread < italian.spread ∧ korean.spread < italian.spread

Italian divides the labour most sharply; Spanish, Chinese, and Korean calibrate the same ordering with a smaller spread.

theorem KwonLee2026.overt_object_biased_as_kweon : korean.overtSubject < 50 ∧ koreanKweon.overtSubject < 50 ∧ 50 < koreanChoe.overtSubject

The overt pronoun is object-biased, as in [Kwe11] and unlike [Cho21].

def KwonLee2026.biasSpread (a b : AntecedentChoice) : ℕ

The spread in subject bias between two forms of Experiment 3.

Equations

• KwonLee2026.biasSpread a b = max a.subjectPercent b.subjectPercent - min a.subjectPercent b.subjectPercent

theorem KwonLee2026.null_nonnull_cliff : 3 * biasSpread exp3_overt exp3_fullNP < biasSpread exp3_pro exp3_overt

The primary contrast is between null and non-null forms: the null-versus-overt step in subject bias is more than three times the overt-versus-full-NP step.