KarpReducible

Read back from the Lean

This is a definition, not a theorem: it introduces the relation KarpReducible on pairs of alphabets and languages. For any types Γ and Γ' (viewed as alphabets), any language L : Language Γ over Γ, and any language L' : Language Γ' over Γ' (a "language" here is a predicate on words, i.e. on List Γ / List Γ', so that w ∈ L says the word w belongs to L), the proposition KarpReducible Γ Γ' L L' is defined to mean: There exists a function f : List Γ → List Γ' (a map from words over Γ to words over Γ') such that BOTH of the following hold: 1. Nonempty (Turing.TM2ComputableInPolyTime (id : List Γ → List Γ) (id : List Γ' → List Γ') f) — i.e. there is a witness that the (multi-tape) Turing-machine predicate Turing.TM2ComputableInPolyTime holds of the three arguments: the identity function on List Γ, the identity function on List Γ', and f. Informally this is the requirement that f be computable by a TM2 Turing machine within polynomial time, with both of the symbol's extra arguments fixed to the identity. 2. ∀ w : List Γ, w ∈ L ↔ f w ∈ L' — for every word w over Γ, w belongs to L exactly when its image f w belongs to L'. The binders are: ∃ f outermost, then a conjunction, the second conjunct of which is a universal statement over all words w : List Γ. The equivalence is a biconditional (both directions), so f is a many-one (Karp-style) reduction of L to L'. There is no claim of truth or provability; the declaration simply defines the reduction predicate.

Written by a model that saw only the Lean, never the English above. If the two disagree, that is worth a challenge.