As a follow-up question: Metamath seems clearly limited in that it can't prove independence, or more generally that the only kind of statement it can express is that something is provable given the axioms. If we want to prove something like "ZFC does not prove CH" then it seems like we'd need an "outer axiomatic system" with its own framework of generic axioms that could take in a model of set theory and determine whether it proves some statement. Then a proof of, say, the independence of CH could be expressed in this outer model, since it clearly (I assume) can't be expressed in Metamath. Is this the right way to think about this, and if so what would those generic axioms be? Sorry if this is an obvious question or if I'm not expressing this clearly - my knowledge is mostly just from a lot of reading through the Metamath proof explorer and so I don't have much experience with other proof explorers/ways of doing set theory.
On Mon, Nov 25, 2024 at 11:11 AM Jim Kingdon <[email protected]> wrote: > This is a good summary. > > Another place to look is a treatment of the disjunction property such as > https://en.wikipedia.org/wiki/Disjunction_and_existence_properties or > https://plato.stanford.edu/entries/disjunction/ (search for "disjunction > property"). The original post seemed to implicitly assume the disjunction > property, which does not hold for ZFC. > On 11/25/24 07:49, 'Thierry Arnoux' via Metamath wrote: > > Given a set of axioms like ZFC: > > - some statements can be proven to be true, > - some statements can be proven to be false, > - some statements can be neither proven nor disproved. > > The last statements are said to be *independent* of the model. It does > not mean that they are both true and false or neither true or false, it > means that it does not matter whether you choose them to be true or false, > neither case will lead to inconsistencies/contradictions. The famous > example is that of the non-euclidean geometries: one might choose to assume > that there exist more than one line through a point parallel to the given > line - or exactly one - or none. It's not that those statement are both > true and false, or neither : you can choose them to be what you want - and > there are interesting developments in both cases. > > This is compatible with the law of excluded middle, which states that a > statement is either true or false: we might simply have not decided yet - > our set of axioms do not shed light so far and they are still in the dark, > behind our horizon. > > > That's the case for the Continuum Hypothesis: it is independent from ZFC, > in the sense that it cannot be proven nor disproved from ZFC. > In set.mm, the (generalized) Continuum Hypothesis is written `GCH = _V`, > for example in ~gch3 <https://us.metamath.org/mpeuni/gch3.html>. > In this statement ~gch3, it is not taken to be true or false, but an > equivalence is provided. In other cases, some of its implications are > found. In all cases, it is part of a broader statement. > While we can reason *about *it, no assumption is made about its truth > value. > > Because it is independent of ZFC, there can be no conflict. We could > choose to either assume it is true or false, and add the corresponding > axiom, and there would be no contradiction. > BR, > _ > Thierry > > > On 25/11/2024 15:23, Anarcocap-socdem 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/44fba649-7673-4418-bd96-9354224bfed8%40gmx.net > <https://groups.google.com/d/msgid/metamath/44fba649-7673-4418-bd96-9354224bfed8%40gmx.net?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/d653f50d-c912-4d2d-8168-bce2d56408d4%40panix.com > <https://groups.google.com/d/msgid/metamath/d653f50d-c912-4d2d-8168-bce2d56408d4%40panix.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/CABJcXbQ_bkB-Ef1do-1T%2Bm9pd979a42WhV_J08BuvqWZtCHczg%40mail.gmail.com.
