Positive-Support Non-Explosion

Abstract

Both-supported evidence supplies a countermodel to positive-support explosion.

Theorem 1.1 (Both-supported premises do not entail an unsupported conclusion).

$\forall F or m u l a \in Type (), p ro p os i t i o n \in F or m u l a, n e g a t e d P ro p os i t i o n \in F or m u l a, co n c l u s i o n \in F or m u l a, (p ro p os i t i o n \neq = n e g a t e d P ro p os i t i o n \land (co n c l u s i o n \neq = p ro p os i t i o n \land co n c l u s i o n \neq = n e g a t e d P ro p os i t i o n)) \Rightarrow let p os i t i v e l y E n t ai l s : P ro p = \forall c an d i d a t e Va l u a t i o n \in F or m u l a \to EvidenceValue (), c an d i d a t e Va l u a t i o n (n e g a t e d P ro p os i t i o n) = swap (c an d i d a t e Va l u a t i o n (p ro p os i t i o n)) \Rightarrow ((fst (c an d i d a t e Va l u a t i o n (p ro p os i t i o n)) = t r u e \land fst (c an d i d a t e Va l u a t i o n (n e g a t e d P ro p os i t i o n)) = t r u e) \Rightarrow fst (c an d i d a t e Va l u a t i o n (co n c l u s i o n)) = t r u e), \exists v a l u a t i o n \in F or m u l a \to EvidenceValue (), v a l u a t i o n (p ro p os i t i o n) = bothSupported () \land (v a l u a t i o n (n e g a t e d P ro p os i t i o n) = swap (v a l u a t i o n (p ro p os i t i o n)) \land (fst (v a l u a t i o n (p ro p os i t i o n)) = t r u e \land (fst (v a l u a t i o n (n e g a t e d P ro p os i t i o n)) = t r u e \land (v a l u a t i o n (co n c l u s i o n) = (f a l se, f a l se) \land (fst (v a l u a t i o n (co n c l u s i o n)) = f a l se \land ((\neg EvidenceConsistent (v a l u a t i o n (p ro p os i t i o n))) \land (\neg p os i t i v e l y E n t ai l s)))))))$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Evidence/PositiveSupportNonexplosion.positive_support_nonexplosion (✓ std3). ∎

Source. Repository-derived.

Commentary.

Over an arbitrary formula carrier, choose any distinct proposition, its negation, and conclusion. The proposition receives the canonical both-supported value, while the value of its negation is obtained by swapping the two support coordinates.

Both premises therefore have positive support. The arbitrary conclusion receives neither positive nor negative support, while every other formula may receive the same unsupported value. This valuation refutes positive-support entailment of that conclusion.

The same witness has inconsistent premise evidence while the consequence relation remains non-explosive: an unsupported conclusion is not made supported merely by the conflict.

References

Truth anchor: D5/S3/ConceptDynamics/Evidence/PositiveSupportNonexplosion.positive_support_nonexplosion
Dependency: D5/S3/ConceptDynamics/Evidence/ConflictingEvidenceAggregation

Keyboard shortcuts

trureturing Blueprint

Positive-Support Non-Explosion

Abstract

References