Soundness, Liveness, and Shape-Only Tests

Abstract

A concrete judge model separates soundness, liveness, and shape-only tests.

Theorem 1.1 (Soundness and liveness are independent of shape-only tests).

$so u n d ((t r u e, f a l se)) \land \neg l i v e ((t r u e, f a l se)) \land l i v e ((f a l se, t r u e)) \land \neg so u n d ((f a l se, t r u e)) \land s ha p e ((t r u e, f a l se)) = s ha p e ((t r u e, t r u e)) \land \neg (l i v e ((t r u e, f a l se)) \Leftrightarrow l i v e ((t r u e, t r u e))) \land \neg \forall j : J u d g e, so u n d (j) \Rightarrow l i v e (j) \land \neg \forall j : J u d g e, l i v e (j) \Rightarrow so u n d (j) \land \forall T : J u d g e \to P ro p, \forall j 1, j 2 : J u d g e, s ha p e (j 1) = s ha p e (j 2) \Rightarrow (T (j 1) \Leftrightarrow T (j 2)) \Rightarrow \neg \forall j : J u d g e, (T (j) \Leftrightarrow l i v e (j)) \land \forall Ot h er J u d g e, Ot h er S ha p e : Type, o t h er S ha p e : Ot h er J u d g e \to Ot h er S ha p e, o t h er L i v e : Ot h er J u d g e \to P ro p, \exists f i rs t, seco n d : Ot h er J u d g e, o t h er S ha p e (f i rs t) = o t h er S ha p e (seco n d) \land \neg (o t h er L i v e (f i rs t) \Leftrightarrow o t h er L i v e (seco n d)) \Rightarrow \forall t es t : Ot h er J u d g e \to P ro p, \forall f i rs t, seco n d : Ot h er J u d g e, o t h er S ha p e (f i rs t) = o t h er S ha p e (seco n d) \Rightarrow (t es t (f i rs t) \Leftrightarrow t es t (seco n d)) \Rightarrow \neg \forall j u d g e : Ot h er J u d g e, (t es t (j u d g e) \Leftrightarrow o t h er L i v e (j u d g e)) .$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Governance/SoundnessLivenessShapeOnlyIndependence.soundness_liveness_independent_of_shape_only_tests (✓ std3). ∎

Source. Repository-derived.

Commentary.

Judge is Bool x Bool. Soundness reads the first coordinate, liveness reads the second, and shape is the first coordinate itself.

The judges (true,false) and (false,true) witness both failed implications. The judges (true,false) and (true,true) have equal shape but opposite liveness.

Consequently every test family constant on equal-shape fibers fails to characterize liveness. The declaration also includes the general version for every model with a same-shape liveness split.

References

Truth anchor: D5/S3/ConceptDynamics/Governance/SoundnessLivenessShapeOnlyIndependence.soundness_liveness_independent_of_shape_only_tests

Keyboard shortcuts

trureturing Blueprint

Soundness, Liveness, and Shape-Only Tests

Abstract

References