This is actually a property shared with every formal system, it's a necessary consequence of having a precise derivation mechanism that you can only derive the things that are derivable, you can't derive that things are not derivable or else they would be derivable. You have to use a "metalogic" within which to perform reasoning about non-derivability in an object logic. In ZFC, this is done by passing to a metalogic which is usually another set theory (a stronger one, because it will generally contain a model of ZFC).
You can use Metamath as a metalogic though, and then you would be proving theorems about derivability and non-derivability with respect to a different logic, explicitly encoded via proof rules. For example (an example so trivial that it may actually be confusing to think about), you can view the natural numbers as a formal system whose proofs are numbers and where there is one axiom "zero is a number" and one inference rule "the successor of a number is a number". So when you prove `n e. NN0`, you are proving that `n` is a proof in this formal system, and since -1 is negative we can prove `-1 e/ NN0` and hence we can prove that -1 is unprovable in this formal system (no amount of adding successors to zero will obtain -1). I've been working on using Metamath as a metalogic pretty heavily, but most of my work has shifted to using Metamath Zero instead (which was designed to make this kind of thing a bit easier). For example https://github.com/digama0/mm0/blob/master/examples/mm0.mm0 is a formalization of the MM0 formal system, using PA as the metalogic and MM0 as the object logic (and MM0 as the framework within which to do proofs in PA). On Tue, Nov 26, 2024 at 10:50 AM Noam Pasman <[email protected]> wrote: > 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 > <https://groups.google.com/d/msgid/metamath/CABJcXbQ_bkB-Ef1do-1T%2Bm9pd979a42WhV_J08BuvqWZtCHczg%40mail.gmail.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/CAFXXJSvcoRVOfBJZk5w11diH2tRxPZ-xjGp_XpWVK4U6axFHoQ%40mail.gmail.com.
