Hi, I think I can help, but this might be slightly off: If you apply the law of excluded middle to the continuum hypothesis you would get (CH or (not CH)), which is a true statement. However, CH is not provable and (not CH) is not provable. So we can prove that one of the two statements are true, but we can't prove that the first one is true and we can't prove that the second one is true. That seems weird to think about but technically there's no logical contradiction there. Another way to think about this is that LEM says that either CH or (not CH) is true, not that either CH or (not CH) is provable. That would be a different statement: turnstile((turnstile CH) or (turnstile (not CH))) which is not possible to do in metamath (and to my knowledge isn't very practical anywhere).
I am very much not an expert but hopefully this clarifies it a bit. On Mon, Nov 25, 2024 at 9:23 AM Anarcocap-socdem < [email protected]> wrote: > I would like that somebody could point out the failure of the following > argument: > > - The law of excluded middle is a theorem in Metamath: > https://us.metamath.org/mpeuni/exmid.html > > - However, the Continuum Hypothesis is a counterexample of the law of > excluded middle in ZFC, since it is neither true nor wrong. > > How to avoid this conflict? > > Thanks! > > -- > You received this message because you are subscribed to the Google Groups > "Metamath" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to [email protected]. > To view this discussion visit > https://groups.google.com/d/msgid/metamath/f3de6454-93b6-4ae1-856a-ceb4bb88c0abn%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/f3de6454-93b6-4ae1-856a-ceb4bb88c0abn%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion visit https://groups.google.com/d/msgid/metamath/CABJcXbTt%2BSPyLQNwCETSXt1imHMMEEzHrLkdTej6eZPYh2Na1A%40mail.gmail.com.
