Timeline for Can we prove set theory is consistent?
Current License: CC BY-SA 2.5
13 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Mar 11, 2021 at 16:54 | comment | added | Timothy Chow | @Max I don't think so, because the Key Assumption states something about informal proofs and your proposal seems to talk only about formal proofs, formal computations, and informal computations. It seems one would additionally need something like a "Curry–Howard thesis" equating informal proofs with informal computations. | |
| Mar 11, 2021 at 15:29 | comment | added | Max | The "Key Assumption" may follow from the Curry–Howard correspondence (which says that formal proofs are equivalent to programs) together with, as mentioned above, the Church–Turing thesis. | |
| Apr 11, 2020 at 17:05 | comment | added | Timothy Chow | @user170039 : To be more precise, Detlefsen challenges the standard claim that Goedel's 2nd theorem kill's Hilbert's program to prove the consistency of mathematics by finitary means. He sets out his argument at length in his book Hilbert's Program: An Essay on Mathematical Instrumentalism. As for the Key Assumption itself, not long before Detlefsen died, I engaged him in an email conversation on this topic, but unfortunately we never finished the conversation. You can read the tail end of that conversation here. | |
| Apr 11, 2020 at 13:36 | comment | added | user57432 | This is an excellent answer! By the way, in which article/book Detlefsen challenged the standard claim that the string Con(ZFC) properly mimics the statement "ZFC is consistent" in the sense of the Key Assumption? | |
| Jul 25, 2019 at 1:17 | comment | added | Ronald Monson | ... Of course all of the above applies to any axiomatization so even arguing against ZFC as the preferred formalization one still has to contend with a generalized KA Key Assumption Generalized (KAG): "all mathematical proofs that mathematicians come up with can be mimicked by a single, formal proof system", a generalization that perhaps makes a belief in it either less compelling or even more alarming. | |
| Jul 25, 2019 at 1:16 | comment | added | Ronald Monson | ... KA, Con (ZFC) => humans cannot ever prove that a particular Diophantine equation has no solutions, or that KA, Con (ZFC) => humans cannot ever prove that a particular Turing Machine ever halts when started on a blank tape. And reflexively even more so when that Diophantine equation has 9 variables (and potentially fewer) or that Turing Machine has only 1919 states (and potentially fewer) ... | |
| Jul 25, 2019 at 1:07 | comment | added | Ronald Monson | @TimothyChow It is nice to see an articulation of this Key Assumption (KA): "all mathematical proofs that mathematicians come up with can be mimicked by formal proofs in ZFC". In regards to beliefs - we have KA, Con(ZFC) => humans cannot ever prove the consistency of mathematics where maintaining belief in KA seems reasonable given the conclusion's scope but also either less so or more alarmingly so when considering the also valid ... | |
| Jan 8, 2018 at 23:36 | comment | added | Timothy Chow | @Timothy : Having said that, I agree that you can quibble about whether ZFC is the correct foundation for mathematics. That's why I said at the outset "a certain formal system (ZFC, say)". If you don't like the axiom of choice then replace ZFC with ZF, or with whatever axioms you consider to be acceptable. | |
| Jan 8, 2018 at 23:34 | comment | added | Timothy Chow | @Timothy : Suppose a statement S is not provable in ZFC, but is "provable," presumably from some other axioms A. Then I claim that you're not going to see a published paper where S is touted as a "Theorem," without additional qualification. Instead, you'll see a footnote saying that A is needed to prove S, or else the actual "Theorem" being claimed will be "S follows from A," which is provable in ZFC. That's what I mean by "mathematically acceptable proof"---it will be considered an acceptable proof in a journal "as is" without any special footnotes about what axioms are needed. | |
| Jan 8, 2018 at 19:42 | comment | added | Timothy | I don't know what you mean by "any mathematically acceptable proof of the original mathematical statement can be mimicked to produce a formal proof of $S$ from the axioms of ZFC". Clearly, there exists statements that are provable but not provable in ZFC. Did you mean you can decide on a new meaning for all the strings of text that represent a statement in the formal system of ZFC? Also, I think ZFC can't be proven to be a true model because many people don't accept the axiom of choice as being true. | |
| Dec 2, 2014 at 23:12 | comment | added | isarandi | This "Key Assumption" sounds analogous to the Church-Turing thesis. It asserts a sort of correspondence between informal reality and formalized models. | |
| May 16, 2010 at 21:40 | comment | added | Dan Piponi | It's nice to see the 'Key Assumption' clearly articulated. I agree that I've found it glossed over in many places. | |
| May 16, 2010 at 19:34 | history | answered | Timothy Chow | CC BY-SA 2.5 |