Countermodel Repair Underdetermination

Abstract

One countermodel supports assumption restriction and conclusion enlargement without selecting between them.

Theorem 1.1 (A countermodel diagnoses failure without uniquely prescribing repair).

$$\begin{gathered} \forall M:\mathrm{Type},A,P:\mathrm{Set}\left(M\right),R:\mathrm{Set}\left(M\right)\to \mathrm{Set}\left(M\right)\to Prop,m:M, \\ m\in A\setminus P\Rightarrow \\ (\neg (m\in P)\vee \\ \neg (A\subseteq P)\vee \\ (\exists Aprime:\mathrm{Set}\left(M\right),Aprime\subset A\wedge \neg (m\in Aprime))\vee \\ (\mathrm{Derives}\left(R,A,P\right)\wedge \neg (A\subseteq P)))\wedge \\ (\{x\mid x\in A\wedge x\ne m\}\subset A\wedge \\ (\{x\mid x\in A\wedge x\ne m\}\setminus P)\subset A\setminus P\wedge \\ P\subset \{x\mid x\in P\vee x=m\}\wedge \\ (A\setminus \{x\mid x\in P\vee x=m\})\subset A\setminus P). \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Audits/CountermodelRepairUnderdetermination.countermodel_diagnosis_is_underdetermined (✓ std3). ∎

Source. Repository-derived.

Commentary.

A state in the assumption-minus-conclusion set witnesses the advertised four-way diagnosis: the conclusion fails there, the assumptions do not entail it, the state may be excluded by a stricter assumption set, or a purported derivation of the invalid entailment is refuted.

Restricting the assumptions away from the witness and enlarging the conclusion to include it are both strict changes. Each construction strictly reduces the corresponding countermodel set, so the original countermodel alone does not choose the repair direction.

References

• Truth anchor: D5/S3/ConceptDynamics/Audits/CountermodelRepairUnderdetermination.countermodel_diagnosis_is_underdetermined