Proof of `Undecidability of positive first-order definability`
groundedproofs/Lax503819Proofs/Undecidability.lean · lax-503819
What this proof establishes
no assumptions
Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.
Description
Theorem 6.1: a positive-definability decision algorithm would decide mortality via the proved computable reduction. Both prerequisites are proved in the proof package; no concept axiom is used in this composition.