Timeline for Blackbox Theorems
Current License: CC BY-SA 3.0
8 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jun 30, 2012 at 16:29 | comment | added | Kevin O'Bryant | This is often invoked informally in my field in the following manner: this proof uses ultrafilters, but it doesn't really use "choice" because any theorem of arithmetic/combinatorics that has a proof with choice has a proof without choice. | |
| Jun 14, 2012 at 0:25 | comment | added | Noah Schweber | (cont'd) So I don't think that the relative consistency of ZFC is actually being invoked whenever Choice is used. | |
| Jun 14, 2012 at 0:24 | comment | added | Noah Schweber | In fact, building off of Michal, perhaps the consistency of the axioms of powerset, replacement, and separation would be better, since these are implicitly used whenever comprehension (forming the set of all $x$ such that $P(x)$) is used, and full comprehension actually is contradictory! But I still don't feel that these are good examples. Roughly speaking, either you're Platonist - in which case mere consistency of AC isn't sufficient to justify using it - or one is interested in proving theorems from axioms, in which case "ZFC proves X" is valuable even if ZFC isn't known to be consistent. | |
| Jun 13, 2012 at 23:41 | comment | added | Michal R. Przybylek | @Ralph: you may say the same about any axiom in any theory. | |
| Jun 13, 2012 at 22:56 | comment | added | Noah Schweber | @Ralph, I disagree. First, the independence of AC from ZF is not the same as the consistency of ZFC relative to ZF (indeed, the latter is very easy). Second, I'm not certain that even this is used frequently outside of set theory; when non-logicians use the axiom of choice, they are not tacitly assuming that it is consistent with ZF, they are tacitly assuming that it is part of some consistent set theory - for example, how many non-logicians know the ZF axioms off the top of their head? I think in practice the set theory that is actually used is generally some high-but-finite-order arithmetic. | |
| Jun 13, 2012 at 22:20 | comment | added | Ralph | Would you use AC if it contradicts ZF ? The magnitude of the independence theorem is that we use it implicitely whenever we apply AC, since it tells us that AC doesn't lead to logical contradictions that weren't already present in ZF. | |
| Jun 13, 2012 at 21:59 | comment | added | Jan Weidner | Is this theorem actually applied frequently inside or outside of set theory? | |
| Jun 13, 2012 at 21:45 | history | answered | Ralph | CC BY-SA 3.0 |