0

Hello all,

I have an interest in proof reduction. If in the final theorem of a proof, some variables are filled in, then the proof might be reduced to a simpler proof. If all variables are filled, then (often) the proof can fully reduced. I am interested in examples were proof reduction is not possible.

Suppose we would encode Wiles proof in a formal logic. Does the proof reduce if you fill in the values for $a$, $b$, $c$ and $n$?

Suppose we take $a = 11$, $b = 14$, $c = 16$, $n = 3$, then a fully reduced proof would look like this:

$0 \neq 21 \Rightarrow 4075 \neq 4096 \Rightarrow 11^3 + 13^3 \neq 16^3$

If it is not possible to reduce Wiles proof step by step with filled in values, why not?

I don't know much about Wiles proof, but my question is about logic and proof reduction. If you take the Four Color Theorem, then if you a particular planar graph, then you will end up with a graph that is colored with 4 colors.

Regards,

Lucas

flag
Sorry, Wiles. (Andrew John Wiles). I edited the article. – Lucas K. Apr 7 2012 at 20:56
Why the vote down? There is not so much material and questions about proof reduction. Maybe I should have asked, if there is a natural example, where proof reduction is not possible, if all variables are filled in. – Lucas K. Apr 7 2012 at 21:04
1 
 I think my question was not stated properly. With proof reduction, I mean in the sequent logic with cut elimination rule. I was interested how that would work on a real theorem. – Lucas K. Apr 7 2012 at 21:29
1 
 There are a number of issues with this question (for instance, even after your clarification, I'm not clear what you mean by "proof reduction"). But FLT is a $\Pi_1$ statement, so if you fill in values for a,b,c,n values in FLT, you get a quantifier-free sentence---you can just evaluate it to see whether it's true or not. – Henry Towsner Apr 7 2012 at 22:01
1 
 I didn't say we can't prove that the reduction is guaranteed to work, I said we can't prove it in the same system we want to apply it to. I'm only guessing what you mean by "a natural example where this reduction is not working" (for instance, I still don't know what "this reduction" is), but why do you think there are any such examples at all? You can't prove, in Peano arithmetic, that every proof has a corresponding cut-free proof, but you won't find a counter-example, because every proof does have a cut-free version, and this can be proven...but in a stronger system. – Henry Towsner Apr 7 2012 at 23:22
show 6 more comments

closed as not a real question by Andres Caicedo, Mark Sapir, Ryan Budney, Gerald Edgar, Neil Strickland Apr 7 2012 at 21:05

Browse other questions tagged or ask your own question.