> Algorithms can be enumerated. Proofs can be enumerated.
How exactly do you do this?
How exactly do you do this?
That's not true. Curry-Howard says that determining if a proof is correct has the same complexity as programs in general. Even if P=NP, there are still complexity classes strictly larger than P; say EXP, that would result in a proof requiring exponential time to check for validity. That's assuming that "validity" here means true/false-ness, rather than syntactical validity, which is much less useful.
* Types = formulae
* Programs = proofs
* Beta-reduction = cut-elimination
Checking whether a string is a proof in a given logic is a simple computation.
Point is that, according to Curry-Howard, validating a proof is equivalent to type checking the program, not actually running it to halting. Type checking (<-> validating a proof) is polynomial.
Given an instance x of some NP relation R:
1. Enumerate all (TM, π) pairs until we encounter a π which proves that TM is a correct polynomial time solution to R.
2. Simulate TM on the given instance x.
Yes.
I’m not sure I’d call that “constructive”.
The method for constructing the algorithm is given!