Talk:Diaconescu's theorem

In the second formula, I changed "{0} to {1} if not P". Assuming U refers to the first set and V to the second, "not P" implies "x = 1" which rules out "V = {0}". MichaelShoemaker (talk) 21:22, 17 July 2009 (UTC)

I changed it back. On rereading, my interpretation was not correct. MichaelShoemaker (talk) 21:25, 17 July 2009 (UTC)

This proof is a strawman argument

IMHO, the correct intepretation of the AC is: given a family of sets $S_{i},i\in I,$ there exists a function $f$ such that $\forall i:f(i)\in S_{i}$. It is a much more reasonable interpretation: whenever we have choice involved in practice, we don't just have sets, we have sets in certain roles, here represented by the indices.

This way, if we took $I=\{0,1\},$ $S_{0}=U,$ $S_{1}=V,$ then $S_{0}=S_{1}$ would not imply $f(0)=f(1)$, i.e. we could still make different choices, and the truth of $P$ would not be recoverable.

The proof weasels in the otherwise completely unwarranted $U=V\implies f(U)=f(V)$ step by having the choice function act on the values and not on the roles. — Preceding unsigned comment added by 78.83.51.215 (talk) 23:06, 18 June 2011 (UTC)

Taken back. We can take the family to be $\{U_{U},V_{V}\}$, in which case $U=V\implies f(U)=f(V)$ would still be relevant. 78.83.51.215 (talk) 23:39, 18 June 2011 (UTC)

The proof still stinks though. We don't need AC to choose from two sets (or from any finite collection of sets, for that matter,) so, by this proof, excluded middle seems to be a tautology. 78.83.51.215 (talk) 00:00, 19 June 2011 (UTC)

You're right that, even constructively, we can make a choice function for two nonempty sets. The strange thing in the proof is that we don't know whether we have two sets or one set. If P holds then we have only one set, {0,1}. If P fails then we have two sets. In the set theories where this proof applies, the choice function has to be extensional: if U = V then it has to choose the same element from U and from V. That requirement is what lets the proof here go through. — Carl (CBM · talk) 00:25, 19 June 2011 (UTC)

All well, but if the proof goes through as it is, then it would go through without assuming AC, i.e. without any non-constructive assumptions, which in turn means that there's nothing non-constructive about excluded middle :) 78.83.51.215 (talk) 04:55, 25 June 2011 (UTC)

• It requires AC to choose from a "subfinite" set (subfinite: surjective image of a finite set, and finite: bijective with a natural number). By the law of the excluded middle, a subfinite set is finite, and as Carl says, we don't need AC to choose from a finite collection, classically or constructively. Basically we are using AC to prove that a subfinite set is finite. But I must agree that this isn't the "spirit" of AC at all. Some suspect there is a natural principle which is classically equivalent to AC but is constructively valid. The presentation axiom might already be it. We don't know how to prove AC from it, but all known classical models of it are models of AC. I hvae been meaning to fill out redlinks like these for a while now, but I never seem to get around to it. --Unzerlegbarkeit (talk) 04:28, 23 August 2011 (UTC)

I don't follow this part

I must be missing something.

"But since $P\to (U=V)$ (by the axiom of extensionality), therefore $P\to (f(U)=f(V))\,$, so

$(f(U)\neq f(V))\to \neg P.$"

Doesn't it beg the question? I mean, to get from

$A\to B$

to

$\neg B\to \neg A$

already assumes that either A is true or A is false, doesn't it? Suppose A is neither true nor false; then the sentence $A\to B$ ("B is true if A is true") is met regardless of whether B is true, false, or neither. If B happens to be false under this circumstance, it is not the case that $\neg B\to \neg A$. 70.187.173.242 (talk) 03:34, 8 November 2012 (UTC)

No; you need to read the negation intuitionistically. So $\lnot A$ means $A\to \bot$ and $\lnot B$ means $B\to \bot$. Assume $A\to B$. Then, if $B\to \bot$, modus ponens gives $A\to \bot$. Thus, if we assume $A\to B$, we can prove $\lnot B\to \lnot A$ constructively, using just modus ponens, without mentioning truth values in any way. This is generally the right way to think about intuitionistic logic; thinking about truth values is generally not helpful.

Separately, you seem to be thinking of three-valued logic (so A is true, false, or neither). But that is not the semantics that are used for intuitionistic logic. If you want to try to think about truth values in intuitionistic logic, you should think of the truth values as coming from some Heyting algebra, just as classical logic uses truth values that come from a Boolean algebra. — Carl (CBM · talk) 12:04, 8 November 2012 (UTC)