Timeline for Proof complexity of two directions of equivalency?
Current License: CC BY-SA 3.0
15 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Oct 22, 2017 at 10:53 | comment | added | Joel Adler | The equivalence in ZF of AC and the well-ordering principle should qualify as an example of a statement where one direction is much harder to prove than the other. I don't think it as been shown that the proof of one direction must be much longer / is much harder than the other as is requested in the question. | |
| Oct 22, 2017 at 4:13 | history | edited | Bjørn Kjos-Hanssen | CC BY-SA 3.0 |
deleted 16 characters in body
|
| May 18, 2014 at 16:38 | vote | accept | Ian Agol | ||
| May 18, 2014 at 1:25 | comment | added | Ian Agol | Right, I suppose it's really a metamathematical question, if the mathematical answers are trivial. | |
| May 18, 2014 at 1:19 | comment | added | Christian Remling | It seems to me they still work, after minor modifications (for example $\forall x (x=x \leftrightarrow A(x))$). I think Joel's examples show that no easy formal definition of equivalence captures what you "really" had in mind. | |
| May 18, 2014 at 1:09 | comment | added | Ian Agol | @ChristianRemling: Actually, a universal quantifier is probably better, to rule out the sort of trivial example in Joel David Hamkins comment to his answer. | |
| May 17, 2014 at 21:03 | comment | added | Carl Mummert | This sort of question comes up very naturally, but it is often hard to find precisely the notion we want to capture. The length of a formal proof is not a very interesting metric, because we don't normally look at formal proofs anyway (so the length is meaningless for practice) and because the length depends as much on the proof system as on the theorem being proved. Reverse Mathematics can capture the set-existence axioms required for each direction. But trying to capture how "easy" or "natural" each direction is to prove is a challenge that has not been solved. | |
| May 17, 2014 at 20:52 | answer | added | Bjørn Kjos-Hanssen | timeline score: 10 | |
| May 17, 2014 at 20:06 | comment | added | François G. Dorais | Not a fascinating example, but "a square matrix is invertible iff it has nonzero determinant" seems like an example. | |
| May 17, 2014 at 19:52 | history | edited | François G. Dorais |
edited tags
|
|
| May 17, 2014 at 19:51 | comment | added | Ryan Budney | There's aspects of ill-definition that could be concerning. For example, with Perelman's proof, one way to shorten it would be to adjust the axioms. Take the Poincare conjecture as an axiom, and both directions become pretty straightforward. | |
| May 17, 2014 at 19:50 | comment | added | Christian Remling | If by an equivalence you mean a sentence of the form $A\leftrightarrow B$, then your example is not ideal, because it has the structure $\forall M (A(M)\leftrightarrow B(M))$ | |
| May 17, 2014 at 19:50 | answer | added | Joel David Hamkins | timeline score: 9 | |
| May 17, 2014 at 19:41 | comment | added | Ian Agol | If users think this question is not formulated precisely enough, or belongs to another forum, then I'm happy to delete or move it. | |
| May 17, 2014 at 19:39 | history | asked | Ian Agol | CC BY-SA 3.0 |