Timeline for Has a computer search for inconsistency of large cardinals been carried out before?
Current License: CC BY-SA 4.0
6 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Sep 8 at 12:59 | comment | added | Timothy Chow | @MonroeEskew Obligatory xkcd comic. | |
| Sep 8 at 5:04 | comment | added | Monroe Eskew | There’s a rumor that some top set theorists have actually found inconsistencies, but the arguments are so intricate that they can be mined for proofs of other results enough to make a long successful academic career. | |
| Sep 8 at 3:35 | comment | added | Timothy Chow | The situation could change if someone could come up with an idea for a targeted search for a proof of "false". There have been a few successes in automated theorem proving, when the search space is carefully designed. In today's era of machine learning, one could imagine training a learning algorithm on a corpus of inconsistent systems. The difficulty here might be coming up with a sufficiently large and rich corpus of inconsistent systems for the machine learning system to sink its teeth into. | |
| Sep 7 at 23:48 | comment | added | Andreas Blass | It seems to me that any proposal for such a search should first be checked on a known inconsistency, for example Reinhardt cardinals with ZFC. | |
| Sep 7 at 22:41 | comment | added | Alex Kruckman | The conventional wisdom is that the space of proofs is so vast that an open-ended computer search for a proof of any particular theorem is totally infeasible (a proof of inconsistency is a proof of the theorem "false"). So people are unlikely to have attempted such a search, for the same reason they are not searching for proofs of (say) the Riemann Hypothesis. | |
| Sep 7 at 21:42 | history | asked | C7X | CC BY-SA 4.0 |