Proof of `Fagin’s theorem` (2nd statement)
groundedproofs/Lax678846Proofs/DefinableInNP.lean · lax-678846
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
Guess the characteristic tables of the existential relations. Their total length is polynomial in the original input length. The concrete verifier splits and decodes the pair, uses the Immerman–Vardi first-order evaluator, rejects malformed encodings, and returns its answer in polynomial TM2 time.