Timeline for Has anyone ever studied which proof types are feasible for which theorems in mathematics? If not, why not?
Current License: CC BY-SA 4.0
22 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Aug 10 at 16:55 | comment | added | J Kusin | I think it’s worth pointing out before going all the way down to the foundational level, most theorems belong to certain archetypes, which have common proof approaches within their foundations. Want to prove a theorem with form A v B, prove A or B individually (in classical math), want to prove A iff B, one way is to prove A -> B and B -> A. This is taught very early on and often there are appendices of several dozen of these techniques. It’s one way to understand the OP’s question. | |
| Aug 10 at 13:23 | comment | added | user21820 | @user509184: I have expanded on your comment in my answer. =) | |
| Aug 10 at 13:21 | answer | added | user21820 | timeline score: 3 | |
| Jul 15 at 17:45 | comment | added | Bumble | Let us continue this discussion in chat. | |
| Jul 15 at 10:50 | comment | added | Julio Di Egidio | P.S. I won't add more... except for mentioning that the Drinker's Paradox is prototypical of the actual underlying assumptions: I have an analysis and a formalization in Coq but I have not yet published it, will post a link at the first occasion when I do. | |
| Jul 15 at 10:42 | comment | added | Julio Di Egidio | @Bumble "if you don't see that it is not raining, you can conclude that it is raining": if you don't see how problematic that is, yes, maybe we should talk about it sooner than later (no kidding): my understanding is that these are the days we might build something better, or never again. I won't add more in these comments. | |
| Jul 15 at 10:37 | comment | added | Bumble | @JulioDiEgidio In that case, I'm interested to know what you think are the more serious problems with classical logic and mathematics. Maybe a subject for another question. | |
| Jul 15 at 10:33 | comment | added | Julio Di Egidio | @Bumble I don't see a distinction there: classical mathematics is built on classical logic principles, and I am trying to point out that "a non-constructive (namely, classical) proof doesn't give us a witness" is the least of the problems with classical logic and mathematics... | |
| Jul 15 at 10:20 | comment | added | Bumble | @JulioDiEgidio If the question is asking about logical pluralism, I agree. There are many logics and they have different proof systems. However, the question asks specifically about mathematical theorems, so it may be that we are meant to hold the choice of logic constant. | |
| Jul 15 at 10:07 | comment | added | Julio Di Egidio | @Bumble IMO the difference is deeper than that and the real trouble comes with the very logic: e.g. that "if you don't see that it is not raining, you can conclude that it is raining"... | |
| Jul 15 at 5:43 | comment | added | Bumble | Typically, constructive proofs are better than nonconstructive ones, because it is nice to be shown a solution rather than told that there is one but we don't know what it looks like. So, many people prefer direct proofs to indirect ones that rely on proof by contradiction. But it also depends on your approach to the concept of mathematical truth. For the classical logician, the difference ultimately is not important. For the intuitionist, nonconstructive proofs are not legitimate. | |
| Jul 14 at 20:00 | comment | added | Double Knot | All already proved or provable math theorems have been or will be proved as computably enumerable (ce, or re) sets, ergo insofar as the proof steps or sequents are of the types of correct, normalized, subformulaed and cut appropriately, they're not useful, not to mention the unprovable Godel like statements... | |
| Jul 14 at 8:19 | comment | added | Alexis | Andrej Bauer has written a post describing the difference between proof of negation and proof by contradiction. | |
| Jul 14 at 1:21 | comment | added | emesupap | echoing @NaïmFavier this is better called a proof by negation. for proofs that rely on contradiction, see constructive/intuitonistic math vs classical. | |
| Jul 13 at 21:29 | comment | added | user509184 | en.wikipedia.org/wiki/Reverse_mathematics | |
| Jul 13 at 19:21 | comment | added | J D | Welcome! I would say you might want to start by reading the SEP's article on Proof Theory. Then, once you get a good idea, take a look at Model Theory. The former is about immediately about proofs, and the latter is about understanding proofs as linguistic entities within a Tarskian framework of truth-conditional semantics. | |
| Jul 13 at 19:18 | history | edited | J D |
edited tags
|
|
| Jul 13 at 18:47 | history | edited | asdf555 | CC BY-SA 4.0 |
deleted 15 characters in body
|
| Jul 13 at 16:14 | comment | added | Naïm Favier | "√2 is irrational" is a negative statement, so the only way to prove it is by assuming that √2 is rational and deriving a contradiction. This is not a proof by contradiction in the sense of constructive mathematics. | |
| Jul 13 at 16:11 | comment | added | Rushi | There's something to be said for direct proofs for irrationality of sqrt(2)) See . | |
| Jul 13 at 16:07 | comment | added | Rushi | This will get better answers on math SE | |
| Jul 13 at 15:55 | history | asked | asdf555 | CC BY-SA 4.0 |