Gettier Witness

Abstract

A Gettier witness is justified true belief accompanied by an admissible same-evidence counterexample.

Definition 1.1 (Gettier witness).

$$\begin{gathered} \mathrm{gettier}\left(P,E,Bel,Just,Adm,a\right)⟺ \\ P\left(a\right)\wedge \\ \mathrm{Bel}\left(E,P,a\right)\wedge \\ \mathrm{Just}\left(E\left(a\right),P\right)\wedge \\ \exists x,\mathrm{Adm}\left(x\right)\wedge E\left(x\right)=E\left(a\right)\wedge \neg P\left(x\right). \end{gathered}$$

Formalization. D5/S3/ConceptDynamics/Epistemic/GettierWitness.gettier (✓ std3).

Source. Repository-derived.

Commentary.

Let X be a state type and B an evidence type. Fix a state predicate P, evidence map E, evidence-indexed belief operator Bel, justification predicate Just, admissibility predicate Adm, and anchor a.

The anchor satisfies P, Bel receives E and affirms P at a, and Just affirms P for E(a). In addition, an admissible witness x has exactly the same evidence as a while P(x) is false.

The source ends immediately after the displayed definition. No conclusion after that truncation is supplied here.

Theorem 1.2 (Concrete positive and negative instances).

$$\begin{array}{c}P\left(n\right)⟺n=0,E\left(n\right)=7,\\ \left(Be{l}_0\right)\left(E,P,n\right)⟺n=0,\left(Be{l}_1\right)\left(E,P,n\right)⟺n=1,\\ \mathrm{Just}\left(e,P\right)⟺e=7,\mathrm{Adm}\left(n\right)⟺n=1,\\ \mathrm{gettier}\left(P,E,Be{l}_0,Just,Adm,0\right)\wedge \neg \mathrm{gettier}\left(P,E,Be{l}_1,Just,Adm,0\right).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Epistemic/GettierWitness.gettier_concrete_examples (✓ std3). ∎

Source. Repository-derived.

Commentary.

Take natural-number states with P true exactly at 0, constant evidence E(n) = 7, justification true exactly for evidence 7, and admissibility true exactly at state 1.

When belief is true exactly at anchor 0, state 1 is the required admissible counterexample: E(1) = E(0) = 7 and P(1) is false, while all three anchor clauses hold.

Keeping every other component fixed but requiring belief at state 1 breaks the belief clause at anchor 0, since 0 is not 1. Thus the first instance satisfies gettier and the second does not.

References

• Truth anchor: D5/S3/ConceptDynamics/Epistemic/GettierWitness.gettier
• Truth anchor: D5/S3/ConceptDynamics/Epistemic/GettierWitness.gettier_concrete_examples