Target Completion and Noncircular Distinction

Abstract

Target completion preserves old cases but need not supply an independent permitted reason.

Theorem 1.1 (Formal target completion does not supply a noncircular reason).

$$(\forall X,C,Y:\mathrm{Type},A:\mathrm{Set}(X),q:X\to C,J_0,J_1:X\to Y,\mathrm{EqOn}(J_1,J_0,A)\Rightarrow \exists d:C\times Y\to Y,J_1=d\circ \mathrm{conceptJoin}(q,J_1)\wedge \mathrm{EqOn}(d\circ \mathrm{conceptJoin}(q,J_1),J_0,A))\wedge (\exists E:\mathrm{Set}(Bool\to Bool),(\lambda b:Bool,false)\in E\wedge (\forall D:Bool\to Bool,D\in E\Rightarrow D(false)=D(true))\wedge \mathrm{EqOn}(id,(\lambda b:Bool,false),\{false\})\wedge (\exists d:Bool\times Bool\to Bool,id=d\circ \mathrm{conceptJoin}((\lambda b:Bool,false),id)\wedge \mathrm{EqOn}(d\circ \mathrm{conceptJoin}((\lambda b:Bool,false),id),(\lambda b:Bool,false),\{false\}))\wedge (\neg (\exists D:Bool\to Bool,D\in E\wedge \mathrm{Refines}(id,\mathrm{conceptJoin}((\lambda b:Bool,false),D))))\wedge \neg ((\mathrm{EqOn}(id,(\lambda b:Bool,false),\{false\})\wedge \exists d:Bool\times Bool\to Bool,id=d\circ \mathrm{conceptJoin}((\lambda b:Bool,false),id)\wedge \mathrm{EqOn}(d\circ \mathrm{conceptJoin}((\lambda b:Bool,false),id),(\lambda b:Bool,false),\{false\}))\Rightarrow \exists D:Bool\to Bool,D\in E\wedge \mathrm{Refines}(id,\mathrm{conceptJoin}((\lambda b:Bool,false),D)))).$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/PrecedentTargetCompletion.target_completion_formal_distinction_not_noncircular (✓ std3). ∎

Source. Repository-derived.

Commentary.

For arbitrary case states, old facts, and verdicts, agreement on the old case set yields a decision through the canonical join of the old facts with the new verdict. The resulting decision still agrees with the old verdict on every old case.

The public countermodel uses Boolean cases. The permitted doctrine is nonempty and every permitted fact has the same value on the two cases, so it is specified without consulting the target verdict.

The target-completed interface decides the identity verdict, while no permitted fact joined with the constant old fact can do so. The final public conjunct is the resulting failure of the implication from formal distinction to a permitted noncircular reason.

The formal-completion clause directly applies the repository theorem concept_join_universal; repository and pinned-library searches found no theorem packaging it with old-case preservation and the doctrine countermodel.

References

• Truth anchor: D5/S3/ConceptDynamics/PrecedentTargetCompletion.target_completion_formal_distinction_not_noncircular
• Dependency: D5/S3/ConceptDynamics/ConceptJoinUniversal