Gärtner & Gyuris (2017): Delimiting the Space of Bias Profiles

@cite{gartner-gyuris-2017}

Formalization of the bias profile framework from @cite{gartner-gyuris-2017}, which defines bias profiles as non-empty power-set choices from {+, −, %} for evidential and epistemic dimensions across PPQ/IN-NPQ/ON-NPQ forms.

Key Results

• Space size: 7³ × 7³ = 117649 total profiles
• 7 delimiting principles (§2) reduce the space progressively:
  1. No Uniformity (§2.1)
  2. PPQ ≠ NPQ (§2.2)
  3. Markedness (§2.3)
  4. Polarity Match / QA Alignment (§2.4)
  5. Convexity (§2.5)
  6. Narrow Epistemic Choice (§2.6)
  7. Static Complementarity (§2.7)
• Final reduction: Convexity + Narrow Epistemic Choice + Static Complementarity together yield (4 × 2)³ = 512 permissible profiles.

Cross-Linguistic Data (Appendix A)

Six bias profiles from English, Japanese, and Hungarian are encoded and verified against the delimiting principles.

inductive GartnerGyuris2017.BiasValue : Type

Bias values: positive (+), negative (−), neutral (%).

• pos : BiasValue
• neg : BiasValue
• neut : BiasValue

@[implicit_reducible]

instance GartnerGyuris2017.instDecidableEqBiasValue : DecidableEq BiasValue

Equations

• GartnerGyuris2017.instDecidableEqBiasValue x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def GartnerGyuris2017.instReprBiasValue.repr : BiasValue → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance GartnerGyuris2017.instReprBiasValue : Repr BiasValue

Equations

• GartnerGyuris2017.instReprBiasValue = { reprPrec := GartnerGyuris2017.instReprBiasValue.repr }

def GartnerGyuris2017.BiasChoice : Type

A bias choice is a non-empty subset of {+, −, %}. There are 2³ − 1 = 7 such subsets. We represent them as sorted lists for decidable equality and enumeration.

Equations

• GartnerGyuris2017.BiasChoice = List GartnerGyuris2017.BiasValue

@[implicit_reducible]

instance GartnerGyuris2017.instBEqBiasChoice : BEq BiasChoice

Equations

• GartnerGyuris2017.instBEqBiasChoice = { beq := GartnerGyuris2017.instBEqBiasChoice._aux_1 }

@[implicit_reducible]

instance GartnerGyuris2017.instDecidableEqBiasChoice : DecidableEq BiasChoice

Equations

• GartnerGyuris2017.instDecidableEqBiasChoice = GartnerGyuris2017.instDecidableEqBiasChoice._aux_1

@[implicit_reducible]

instance GartnerGyuris2017.instReprBiasChoice : Repr BiasChoice

Equations

• GartnerGyuris2017.instReprBiasChoice = { reprPrec := GartnerGyuris2017.instReprBiasChoice._aux_1 }

def GartnerGyuris2017.allBiasChoices : List BiasChoice

The 7 non-empty subsets of {+, −, %}.

Equations

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

theorem GartnerGyuris2017.seven_bias_choices : allBiasChoices.length = 7

inductive GartnerGyuris2017.BiasDimension : Type

Bias dimension: evidential vs epistemic.

• evidential : BiasDimension
• epistemic : BiasDimension

@[implicit_reducible]

instance GartnerGyuris2017.instDecidableEqBiasDimension : DecidableEq BiasDimension

Equations

• GartnerGyuris2017.instDecidableEqBiasDimension x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def GartnerGyuris2017.instReprBiasDimension.repr : BiasDimension → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance GartnerGyuris2017.instReprBiasDimension : Repr BiasDimension

Equations

• GartnerGyuris2017.instReprBiasDimension = { reprPrec := GartnerGyuris2017.instReprBiasDimension.repr }

inductive GartnerGyuris2017.GGPQForm : Type

G&G's PQ form typology: PPQ, IN-NPQ, ON-NPQ. These map to Romero's PosQ, LoNQ, HiNQ respectively.

• PPQ : GGPQForm
• IN_NPQ : GGPQForm
• ON_NPQ : GGPQForm

@[implicit_reducible]

instance GartnerGyuris2017.instDecidableEqGGPQForm : DecidableEq GGPQForm

Equations

• GartnerGyuris2017.instDecidableEqGGPQForm x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance GartnerGyuris2017.instReprGGPQForm : Repr GGPQForm

Equations

• GartnerGyuris2017.instReprGGPQForm = { reprPrec := GartnerGyuris2017.instReprGGPQForm.repr }

def GartnerGyuris2017.instReprGGPQForm.repr : GGPQForm → ℕ → Std.Format

Equations

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

def GartnerGyuris2017.GGPQForm.toRomero : GGPQForm → Semantics.Modality.BiasedPQ.PQForm

Map G&G forms to Romero's typology.

Equations

• GartnerGyuris2017.GGPQForm.PPQ.toRomero = Semantics.Modality.BiasedPQ.PQForm.PosQ
• GartnerGyuris2017.GGPQForm.IN_NPQ.toRomero = Semantics.Modality.BiasedPQ.PQForm.LoNQ
• GartnerGyuris2017.GGPQForm.ON_NPQ.toRomero = Semantics.Modality.BiasedPQ.PQForm.HiNQ

structure GartnerGyuris2017.BiasCell : Type

A cell in the bias profile grid: one PQ form × one bias dimension.

• form : GGPQForm
• dim : BiasDimension

@[implicit_reducible]

instance GartnerGyuris2017.instDecidableEqBiasCell : DecidableEq BiasCell

Equations

• GartnerGyuris2017.instDecidableEqBiasCell = GartnerGyuris2017.instDecidableEqBiasCell.decEq

def GartnerGyuris2017.instDecidableEqBiasCell.decEq (x✝ x✝¹ : BiasCell) : Decidable (x✝ = x✝¹)

Equations

• GartnerGyuris2017.instDecidableEqBiasCell.decEq { form := a, dim := a_1 } { form := b, dim := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

def GartnerGyuris2017.instReprBiasCell.repr : BiasCell → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance GartnerGyuris2017.instReprBiasCell : Repr BiasCell

Equations

• GartnerGyuris2017.instReprBiasCell = { reprPrec := GartnerGyuris2017.instReprBiasCell.repr }

structure GartnerGyuris2017.BiasProfile : Type

A bias profile assigns a non-empty bias choice to each of 6 cells (3 PQ forms × 2 bias dimensions).

• ppqEv : BiasChoice
• ppqEp : BiasChoice
• inNpqEv : BiasChoice
• inNpqEp : BiasChoice
• onNpqEv : BiasChoice
• onNpqEp : BiasChoice

def GartnerGyuris2017.instDecidableEqBiasProfile.decEq (x✝ x✝¹ : BiasProfile) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance GartnerGyuris2017.instDecidableEqBiasProfile : DecidableEq BiasProfile

Equations

• GartnerGyuris2017.instDecidableEqBiasProfile = GartnerGyuris2017.instDecidableEqBiasProfile.decEq

@[implicit_reducible]

instance GartnerGyuris2017.instReprBiasProfile : Repr BiasProfile

Equations

• GartnerGyuris2017.instReprBiasProfile = { reprPrec := GartnerGyuris2017.instReprBiasProfile.repr }

def GartnerGyuris2017.instReprBiasProfile.repr : BiasProfile → ℕ → Std.Format

Equations

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

def GartnerGyuris2017.BiasProfile.get (bp : BiasProfile) : BiasCell → BiasChoice

Access a bias profile by cell.

Equations

• bp.get { form := GartnerGyuris2017.GGPQForm.PPQ, dim := GartnerGyuris2017.BiasDimension.evidential } = bp.ppqEv
• bp.get { form := GartnerGyuris2017.GGPQForm.PPQ, dim := GartnerGyuris2017.BiasDimension.epistemic } = bp.ppqEp
• bp.get { form := GartnerGyuris2017.GGPQForm.IN_NPQ, dim := GartnerGyuris2017.BiasDimension.evidential } = bp.inNpqEv
• bp.get { form := GartnerGyuris2017.GGPQForm.IN_NPQ, dim := GartnerGyuris2017.BiasDimension.epistemic } = bp.inNpqEp
• bp.get { form := GartnerGyuris2017.GGPQForm.ON_NPQ, dim := GartnerGyuris2017.BiasDimension.evidential } = bp.onNpqEv
• bp.get { form := GartnerGyuris2017.GGPQForm.ON_NPQ, dim := GartnerGyuris2017.BiasDimension.epistemic } = bp.onNpqEp

theorem GartnerGyuris2017.total_space_size : 7 ^ 6 = 117649

Total space: 7 choices per cell, 6 cells = 7⁶ = 117649.

def GartnerGyuris2017.noUniformity (bp : BiasProfile) : Bool

No Uniformity: a bias profile is not entirely uniform, i.e., not all 6 cells have exactly the same bias choice.

"none of them consist of exactly the same choice, e.g., {+}, for each of its 6 dimensions."

Equations

• GartnerGyuris2017.noUniformity bp = !(bp.ppqEv == bp.ppqEp && bp.ppqEp == bp.inNpqEv && bp.inNpqEv == bp.inNpqEp && bp.inNpqEp == bp.onNpqEv && bp.onNpqEv == bp.onNpqEp)

theorem GartnerGyuris2017.noUniformity_removes : 117649 - 7 = 117642

No Uniformity removes exactly 7 profiles (one per uniform choice).

def GartnerGyuris2017.ppqNeqNpq (bp : BiasProfile) : Bool

PPQ ≠ NPQ: Negation has an impact on bias. Both the evidential AND epistemic choices of PPQ must differ from those of each NPQ form.

"PPQ ≠ NPQ (interpreted more precisely as PPQ^ev ≠ NPQ^ev & PPQ^ep ≠ NPQ^ep)" — §2.2.

Equations

• GartnerGyuris2017.ppqNeqNpq bp = (bp.ppqEv != bp.inNpqEv && bp.ppqEp != bp.inNpqEp && (bp.ppqEv != bp.onNpqEv && bp.ppqEp != bp.onNpqEp))

theorem GartnerGyuris2017.ppqNeqNpq_space : 7 * 7 * 6 * 6 * 6 * 6 = 63504

PPQ ≠ NPQ reduces the space to 7² × 6² × 6² = 63504.

def GartnerGyuris2017.markednessDistributive (bp : BiasProfile) : Bool

Quantitative Markedness (distributive, §2.3 eq. 11a): expressing marked (negative) meanings does not lead to more options than expressing their unmarked (positive) counterpart.

|PPQ^ev| ≥ |IN-NPQ^ev| & |PPQ^ev| ≥ |ON-NPQ^ev| & |PPQ^ep| ≥ |IN-NPQ^ep| & |PPQ^ep| ≥ |ON-NPQ^ep|

Equations

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

def GartnerGyuris2017.markednessCollective (bp : BiasProfile) : Bool

Quantitative Markedness (collective, §2.3 eq. 11b): |PPQ^ev| + |PPQ^ep| ≥ |IN-NPQ^ev| + |IN-NPQ^ep| & |PPQ^ev| + |PPQ^ep| ≥ |ON-NPQ^ev| + |ON-NPQ^ep|

Equations

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

theorem GartnerGyuris2017.markedness_distributive_space : Nat.mul 184 184 = 33856

Distributive Markedness yields 33856 profiles (Appendix B [1]). Per dimension: 3×3² + 3×6² + 1×7² = 184 (PPQ,NPQ) triples. Two independent dimensions: 184² = 33856.

theorem GartnerGyuris2017.markedness_collective_space : ((((Nat.mul 9 81).add (Nat.mul 18 729)).add (Nat.mul 15 1764)).add (Nat.mul 6 2304)).add (Nat.mul 1 2401) = 56536

Collective Markedness yields 56536 profiles (Appendix B [2]): 9×9² + 18×27² + 15×42² + 6×48² + 1×49² = 56536, summed over |PPQ^ev|+|PPQ^ep| = 2..6, counting NPQ pairs with sum ≤ PPQ sum.

def GartnerGyuris2017.avoidDisagreement (bp : BiasProfile) : Bool

Avoid Disagreement: − ∉ PPQ and + ∉ NPQ. The polarity of the question and the direction of bias should not totally contradict each other.

Equations

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

def GartnerGyuris2017.dontRuleOutAgreement (bp : BiasProfile) : Bool

Don't Rule Out Agreement: each cell of PPQ must contain +, and each cell of NPQ must contain −. The constraint applies per-cell, not per-row.

This yields 4 choices per cell (subsets containing the matching polarity), so 4⁶ = 4096 total (§2.4, chart (19)).

Equations

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

theorem GartnerGyuris2017.avoidDisagreement_space : 3 ^ 6 = 729

Avoid Disagreement yields 3⁶ = 729 profiles.

theorem GartnerGyuris2017.dontRuleOutAgreement_space : 4 ^ 6 = 4096

Don't Rule Out Agreement yields 4⁶ = 4096 profiles.

def GartnerGyuris2017.isConvex (bc : BiasChoice) : Bool

A bias choice is convex if it doesn't "skip" intermediate values in the Hasse ordering + > % > −. Concretely, {+, −} is ruled out because it crosses over % without including it.

The convex non-empty subsets of {+, %, −} are: {+}, {−}, {%}, {+,%}, {%,−}, {+,%,−} — six options.

Equations

• GartnerGyuris2017.isConvex bc = !(List.contains bc GartnerGyuris2017.BiasValue.pos && List.contains bc GartnerGyuris2017.BiasValue.neg && !List.contains bc GartnerGyuris2017.BiasValue.neut)

def GartnerGyuris2017.convexity (bp : BiasProfile) : Bool

A bias profile satisfies Convexity if all 6 cells are convex.

Equations

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

theorem GartnerGyuris2017.pos_neg_not_convex : isConvex [BiasValue.pos, BiasValue.neg] = false

{+, −} is ruled out by Convexity.

theorem GartnerGyuris2017.singletons_convex : isConvex [BiasValue.pos] = true ∧ isConvex [BiasValue.neg] = true ∧ isConvex [BiasValue.neut] = true

All singletons are convex.

theorem GartnerGyuris2017.adjacent_pairs_convex : isConvex [BiasValue.pos, BiasValue.neut] = true ∧ isConvex [BiasValue.neut, BiasValue.neg] = true

{+, %} and {%, −} are convex.

theorem GartnerGyuris2017.full_set_convex : isConvex [BiasValue.pos, BiasValue.neut, BiasValue.neg] = true

{+, %, −} is convex (the full set).

theorem GartnerGyuris2017.convexity_space : 6 ^ 6 = 46656

Convexity yields 6⁶ = 46656 profiles.

def GartnerGyuris2017.narrowEpistemicChoice (bc : BiasChoice) : Bool

Narrow Epistemic Choice: epistemic bias is either {+^ep} or {+^ep, −^ep, %^ep} (the full set).

"the number of epistemic bias options is rather narrow, that is, we predominantly find {+^ep} or {+^ep,−^ep,%^ep}"

Equations

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

def GartnerGyuris2017.narrowEpistemic (bp : BiasProfile) : Bool

A bias profile satisfies Narrow Epistemic Choice if all 3 epistemic cells use either {+} or {+,%,−}.

Equations

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

theorem GartnerGyuris2017.narrowEpistemic_space : (7 * 2) ^ 3 = 2744

Narrow Epistemic Choice alone yields (7 × 2)³ = 2744 profiles.

def GartnerGyuris2017.staticComplementarityEvChoices : List BiasChoice

The 4 evidential options surviving Static Complementarity + Convexity: {+,%}, {%,−}, {%}, {−}.

These are the convex subsets minus {+}, {+,%,−} (which are the epistemic options) and minus {+,−} (non-convex).

Equations

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

def GartnerGyuris2017.isStaticComplementaryEv (bc : BiasChoice) : Bool

A bias profile satisfies Static Complementarity if:

• Epistemic cells use {+} or {+,%,−} (Narrow Epistemic Choice)
• Evidential cells use {+,%}, {%,−}, {%}, or {−}

Equations

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

def GartnerGyuris2017.staticComplementarity (bp : BiasProfile) : Bool

Equations

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

theorem GartnerGyuris2017.staticComplementarity_space : (4 * 2) ^ 3 = 512

Static Complementarity + Convexity yields (4 × 2)³ = 512 profiles.

def GartnerGyuris2017.englishV1 : BiasProfile

[1] English V1-Interrogative (Appendix A [1], from Sudo 2013:284).

PPQ: ⟨{+, %}, {+, −, %}⟩ IN-NPQ: ⟨{−}, {+}⟩ ON-NPQ: ⟨{−, %}, {+}⟩

Equations

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

def GartnerGyuris2017.japaneseNull : BiasProfile

[2] Japanese ∅-Interrogative (Appendix A [2], from Sudo 2013:285).

PPQ: ⟨{%}, {+, −, %}⟩ IN-NPQ: ⟨{−}, {+, −, %}⟩ ON-NPQ: ⟨{+, %}, {+}⟩

Equations

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

def GartnerGyuris2017.japaneseNo : BiasProfile

[3] Japanese no-Interrogative (Appendix A [3], = ex. (4), from Sudo 2013:288).

PPQ: ⟨{+}, {+, −, %}⟩ IN-NPQ: ⟨{−}, {+}⟩ ON-NPQ: ⟨{+, −, %}, {+}⟩

Equations

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

def GartnerGyuris2017.japaneseDesho : BiasProfile

[4] Japanese desho-Interrogative (Appendix A [4], = ex. (23), from Sudo 2013:290).

PPQ: ⟨{+, −, %}, {+}⟩ IN-NPQ: ⟨{+, −, %}, {−}⟩ ON-NPQ: ⟨{−, %}, {−}⟩

Equations

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

def GartnerGyuris2017.hungarianWedge : BiasProfile

[5] Hungarian ∧-Interrogative (Appendix A [5], from Gyuris 2017: Section 4).

PPQ: ⟨{+, %}, {+, −, %}⟩ IN-NPQ: ⟨{−}, {+}⟩ ON-NPQ: ⟨{−, %}, {+}⟩

Equations

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

structure GartnerGyuris2017.PartialBiasProfile : Type

[6] Hungarian e-Interrogative (Appendix A [6], = ex. (10), from Gyuris 2017: Section 4). IN-NPQ is not expressible.

PPQ: ⟨{%}, {+, −, %}⟩ ON-NPQ: ⟨{%}, {+}⟩

• ppqEv : BiasChoice
• ppqEp : BiasChoice
• onNpqEv : BiasChoice
• onNpqEp : BiasChoice

def GartnerGyuris2017.instReprPartialBiasProfile.repr : PartialBiasProfile → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance GartnerGyuris2017.instReprPartialBiasProfile : Repr PartialBiasProfile

Equations

• GartnerGyuris2017.instReprPartialBiasProfile = { reprPrec := GartnerGyuris2017.instReprPartialBiasProfile.repr }

def GartnerGyuris2017.hungarianE : PartialBiasProfile

Equations

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

theorem GartnerGyuris2017.englishV1_noUniformity : noUniformity englishV1 = true

English V1 satisfies No Uniformity.

theorem GartnerGyuris2017.englishV1_ppqNeqNpq : ppqNeqNpq englishV1 = true

English V1 satisfies PPQ ≠ NPQ.

theorem GartnerGyuris2017.englishV1_convexity : convexity englishV1 = true

English V1 satisfies Convexity.

theorem GartnerGyuris2017.englishV1_narrowEpistemic : narrowEpistemic englishV1 = true

English V1 satisfies Narrow Epistemic Choice.

theorem GartnerGyuris2017.englishV1_staticComplementarity : staticComplementarity englishV1 = true

English V1 satisfies Static Complementarity.

theorem GartnerGyuris2017.hungarianWedge_eq_englishV1 : hungarianWedge = englishV1

Hungarian ∧-Interrogative has the same bias profile as English V1 (Appendix A: [5] = [1]).

theorem GartnerGyuris2017.japaneseNull_noUniformity : noUniformity japaneseNull = true

Japanese ∅-Interrogative satisfies No Uniformity.

theorem GartnerGyuris2017.japaneseNull_violates_ppqNeqNpq : ppqNeqNpq japaneseNull = false

Japanese ∅-Interrogative violates PPQ ≠ NPQ: PPQ^ep = IN-NPQ^ep = {+,−,%}. Under the AND interpretation (both ev and ep must differ), identical epistemic values suffice to violate the constraint.

theorem GartnerGyuris2017.japaneseNull_convexity : convexity japaneseNull = true

Japanese ∅-Interrogative satisfies Convexity.

theorem GartnerGyuris2017.japaneseNull_staticComplementarity : staticComplementarity japaneseNull = true

Japanese ∅-Interrogative satisfies Static Complementarity: all ev cells ∈ {{+,%},{%,−},{%},{−}} and all ep cells ∈ {{+},{+,−,%}}. Despite violating PPQ ≠ NPQ, its profile is within the 512-profile SC-permissible space.

theorem GartnerGyuris2017.japaneseNo_noUniformity : noUniformity japaneseNo = true

Japanese no-Interrogative satisfies No Uniformity.

theorem GartnerGyuris2017.japaneseNo_ppqNeqNpq : ppqNeqNpq japaneseNo = true

Japanese no-Interrogative satisfies PPQ ≠ NPQ.

theorem GartnerGyuris2017.japaneseNo_violates_distributiveMarkedness : markednessDistributive japaneseNo = false

Japanese no-Interrogative violates Distributive Markedness: |PPQ^ev| = 1 < |ON-NPQ^ev| = 3. This is a known counterexample noted by §2.3.

theorem GartnerGyuris2017.japaneseNo_violates_staticComplementarity : staticComplementarity japaneseNo = false

Japanese no-Interrogative violates Static Complementarity: ON-NPQ^ev = {+,−,%} which is not in the static complementarity set of evidential options.

theorem GartnerGyuris2017.japaneseDesho_violates_avoidDisagreement : avoidDisagreement japaneseDesho = false

Japanese desho-Interrogative violates Avoid Disagreement: IN-NPQ^ev contains + and PPQ^ev contains −.

theorem GartnerGyuris2017.japaneseDesho_violates_narrowEpistemic : narrowEpistemic japaneseDesho = false

Japanese desho-Interrogative violates Narrow Epistemic Choice: IN-NPQ^ep and ON-NPQ^ep select {−}, which is neither {+} nor {+,%,−}.

theorem GartnerGyuris2017.japaneseDesho_violates_ppqNeqNpq : ppqNeqNpq japaneseDesho = false

Japanese desho-Interrogative violates PPQ ≠ NPQ: PPQ^ev = IN-NPQ^ev = {+,−,%}.

theorem GartnerGyuris2017.japaneseDesho_violates_staticComplementarity : staticComplementarity japaneseDesho = false

Japanese desho-Interrogative violates Static Complementarity (via narrowEpistemic failure).

theorem GartnerGyuris2017.englishV1_violates_avoidDisagreement : avoidDisagreement englishV1 = false

English V1 violates Avoid Disagreement: PPQ^ep = {+,−,%} contains −, and IN-NPQ^ep = {+} contains +. This exemplifies the systematic incompatibility between Narrow Epistemic Choice and Polarity Match for epistemic cells (§3.1.2).

theorem GartnerGyuris2017.englishV1_violates_dontRuleOutAgreement : dontRuleOutAgreement englishV1 = false

English V1 violates Don't Rule Out Agreement: IN-NPQ^ep = {+} does not contain −. Again, the epistemic dimension conflicts with NEC-derived empirical patterns (§3.1.2).

theorem GartnerGyuris2017.englishV1_markednessDistributive : markednessDistributive englishV1 = true

English V1 satisfies Distributive Markedness.

theorem GartnerGyuris2017.englishV1_markednessCollective : markednessCollective englishV1 = true

English V1 satisfies Collective Markedness.

def GartnerGyuris2017.evidentiallyCompatible (bc : BiasChoice) (ce : Core.Discourse.Commitment.ContextualEvidence) : Bool

Map G&G's evidential bias choice to Romero/BiasedPQ ContextualEvidence compatibility. A bias choice lists which evidence types are felicitous.

Equations

• GartnerGyuris2017.evidentiallyCompatible bc Core.Discourse.Commitment.ContextualEvidence.forP = List.contains bc GartnerGyuris2017.BiasValue.pos
• GartnerGyuris2017.evidentiallyCompatible bc Core.Discourse.Commitment.ContextualEvidence.neutral = List.contains bc GartnerGyuris2017.BiasValue.neut
• GartnerGyuris2017.evidentiallyCompatible bc Core.Discourse.Commitment.ContextualEvidence.againstP = List.contains bc GartnerGyuris2017.BiasValue.neg

def GartnerGyuris2017.epistemicallyCompatible (bc : BiasChoice) (ob : Semantics.Modality.BiasedPQ.OriginalBias) : Bool

Map G&G's epistemic bias choice to Romero/BiasedPQ OriginalBias compatibility.

Equations

• GartnerGyuris2017.epistemicallyCompatible bc Semantics.Modality.BiasedPQ.OriginalBias.forP = List.contains bc GartnerGyuris2017.BiasValue.pos
• GartnerGyuris2017.epistemicallyCompatible bc Semantics.Modality.BiasedPQ.OriginalBias.neutral = List.contains bc GartnerGyuris2017.BiasValue.neut
• GartnerGyuris2017.epistemicallyCompatible bc Semantics.Modality.BiasedPQ.OriginalBias.againstP = List.contains bc GartnerGyuris2017.BiasValue.neg

theorem GartnerGyuris2017.englishV1_inNpq_evidence_matches_romero : evidentiallyCompatible englishV1.inNpqEv Core.Discourse.Commitment.ContextualEvidence.forP = false ∧ evidentiallyCompatible englishV1.inNpqEv Core.Discourse.Commitment.ContextualEvidence.neutral = false ∧ evidentiallyCompatible englishV1.inNpqEv Core.Discourse.Commitment.ContextualEvidence.againstP = true

English V1 IN-NPQ (= Romero's LoNQ) requires evidence against p, matching Romero's Table 2 prediction.

theorem GartnerGyuris2017.englishV1_onNpq_epistemic_matches_romero : epistemicallyCompatible englishV1.onNpqEp Semantics.Modality.BiasedPQ.OriginalBias.forP = true ∧ epistemicallyCompatible englishV1.onNpqEp Semantics.Modality.BiasedPQ.OriginalBias.neutral = false ∧ epistemicallyCompatible englishV1.onNpqEp Semantics.Modality.BiasedPQ.OriginalBias.againstP = false

English V1 ON-NPQ (= Romero's HiNQ) has epistemic bias for p only, matching Romero's requirement that HiNQ conveys original bias for p.

theorem GartnerGyuris2017.englishV1_ppq_evidence_matches_romero : evidentiallyCompatible englishV1.ppqEv Core.Discourse.Commitment.ContextualEvidence.forP = true ∧ evidentiallyCompatible englishV1.ppqEv Core.Discourse.Commitment.ContextualEvidence.neutral = true ∧ evidentiallyCompatible englishV1.ppqEv Core.Discourse.Commitment.ContextualEvidence.againstP = false

English V1 PPQ (= Romero's PosQ) is compatible with evidence for p or neutral evidence, matching Romero's Table 2.

theorem GartnerGyuris2017.hungarianE_ppq_antibias : hungarianE.ppqEv = [BiasValue.neut]

Hungarian e-Interrogative has evidential "anti-bias" {%^ev} for PPQ: requiring neutral evidence only. This is the key counterexample to PPQ ≠ NPQ noted by §2.2.

This contrasts with standard PPQs which admit positive evidence.

def GartnerGyuris2017.czechV1 : BiasProfile

Czech bias profile in G&G format, derived from @cite{simik-2024} Table 2 via czechBiasProfile.

Czech V1-Interrogative (InterPPQ/InterNPQ as PPQ/ON-NPQ):

• InterPPQ = PPQ: ev={%}, ep={+,%}
• DeclNPQ = IN-NPQ: ev={−}, ep={+,%}
• InterNPQ = ON-NPQ: ev={+,%,−}, ep={+,%}

Equations

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

theorem GartnerGyuris2017.czechV1_ppq_ev : czechV1.ppqEv = [BiasValue.neut]

Czech PPQ (InterPPQ) admits only neutral evidence — narrower than English V1 PPQ. Czech InterPPQ is the default unbiased PQ, felicitous only when there is no compelling evidence either way.

theorem GartnerGyuris2017.czechV1_onNpq_ev : czechV1.onNpqEv = [BiasValue.pos, BiasValue.neut, BiasValue.neg]

Czech ON-NPQ (InterNPQ) has broader evidential distribution than English — it admits +, %, and − evidence, reflecting FALSUM^CZ's weaker requirements (@cite{simik-2024} §5).

theorem GartnerGyuris2017.czechV1_onNpq_ep : czechV1.onNpqEp = [BiasValue.pos, BiasValue.neut]

Czech ON-NPQ (InterNPQ) epistemic bias admits + and % (speaker believes p or is neutral). Unlike English HiNQ which requires bias for p, Czech InterNPQ is also felicitous in explanation-seeking contexts (neutral epistemic bias, @cite{simik-2024} §5.2).

theorem GartnerGyuris2017.czechV1_noUniformity : noUniformity czechV1 = true

Czech V1 profile satisfies No Uniformity.

theorem GartnerGyuris2017.czechV1_violates_ppqNeqNpq : ppqNeqNpq czechV1 = false

Czech V1 profile violates PPQ ≠ NPQ: PPQ^ep = IN-NPQ^ep = {+,%}. Czech InterPPQ and DeclNPQ share the same epistemic bias distribution, reflecting that both forms are felicitous when the speaker either believes p or is neutral.

theorem GartnerGyuris2017.czechV1_convexity : convexity czechV1 = true

Czech V1 profile satisfies Convexity.

theorem GartnerGyuris2017.czechV1_violates_staticComplementarity : staticComplementarity czechV1 = false

Czech ON-NPQ evidential {+,%,−} violates Static Complementarity — this is expected because Czech FALSUM^CZ has broader distribution than English FALSUM, allowing all evidence types. The G&G framework was designed for English/Japanese/Hungarian where ON-NPQ evidence is narrower.

theorem GartnerGyuris2017.czech_vs_english_onNpq_evidence : evidentiallyCompatible czechV1.onNpqEv Core.Discourse.Commitment.ContextualEvidence.forP = true ∧ evidentiallyCompatible englishV1.onNpqEv Core.Discourse.Commitment.ContextualEvidence.forP = false

The key Czech vs English difference: Czech ON-NPQ admits positive evidence while English ON-NPQ does not. This is the empirical core of @cite{simik-2024}'s FALSUM^CZ proposal.

theorem GartnerGyuris2017.czech_hungarian_shared_antibias : czechV1.ppqEv = hungarianE.ppqEv

Czech InterPPQ shares the "anti-bias" evidential pattern {%^ev} with Hungarian e-interrogatives — both require neutral evidence only. This parallel is striking given that Czech InterPPQ and Hungarian e-PPQ serve different functions: Czech InterPPQ is the default unbiased PQ, while Hungarian e-PPQ carries positive epistemic bias.