Thanks! And would MM0 (and therefore just having PA as a metatheory) be enough to prove theorems such as independence of CH or other incompleteness theorems?
On Tue, Nov 26, 2024 at 12:57 PM Mario Carneiro <[email protected]> wrote: > > > On Tue, Nov 26, 2024 at 4:30 PM Noam Pasman <[email protected]> wrote: > >> Ok, so if I understand this correctly the goal is to find a reasonable >> set of axioms that let you construct a model of ZFC and then try to prove >> derivability results about ZFC in that wider set theory. The first thing >> that comes to mind is the Tarski-Grothendieck Axiom, so (not sure if this >> is the right way to think about this) what would a statement that CH isn't >> derivable in ZFC look like in that system? >> > > Well in any system the statement that CH isn't derivable in ZFC looks > about the same: it consists of defining what a proof in ZFC is, by defining > formulas and substitution, the logical axioms and rules of inference, and > then the non-logical axioms and rules of inference of ZFC itself. Then the > assertion that CH is not derivable is saying that CH when encoded > appropriately as a formula does not have a proof in ZFC. You can do all of > this in PA or ZFC itself, you don't need the system to be strong to define > what a proof is. > > The hard part is proving this theorem, not stating it. It is a theorem of > Goedel that you can't prove *any* non-derivability theorem about an axiom > system such as ZFC unless the metatheory is stronger than ZFC, because one > particular non-derivability claim, "ZFC does not prove false", is > equivalent to "there is some statement that ZFC does not prove", and ZFC > cannot prove this statement (called Con(ZFC), aka "ZFC is consistent"). > > I definitely hadn't thought about that example and I think I somewhat >> understand it? I can imagine this proof of 3 for example: >> |- 1 (by A1) >> |- (1+1) (by A2) >> |- (1+(1+1)) (by A2) >> My one point of confusion is that I don't know how I'd even express -1 >> as a statement in this system, beyond proving it. >> > > That's fair. We can say that the language of statements in this system is > ZZ (each individual number is a separate proposition), but the proofs are > still NN0 and there is a family of inference rules saying that "n is a > natural number implies n+1 is a natural number" for each natural number n. > Then -1 will be a statement in the system, but it has no proof. > > >> I'm a bit confused about what Metamath Zero is doing (I'm not so good >> with github to be honest). Are you taking statements about set theory as >> your objects and then constructing proofs about what is provable using the >> Peano Axioms? >> > > In this case the object logic is Metamath zero itself, and the peano > axioms form the metatheory. So that means that we have to define in PA what > is a proof in the style of MM0, which is why the file is defining > expressions and theorems and proofs. The very last definition defines what > it means for a MM0 file to be provable (i.e. it asserts a statement that is > derivable from the axioms, which are also part of the statement in this > setting). This is a particularly grungy definition because it defines > parsing from strings, plus it works at a higher level than expressions, an > MM0 file (like a metamath file) consists of axioms and theorems that follow > from those axioms, so correctness is saying that the theorems follow from > the axioms. You don't have to pay too much attention to this reference, the > main point I wanted to make is that it is possible to scale this up to > formalizations of "real world" formal systems. > > >> >> On Tue, Nov 26, 2024 at 5:02 AM Mario Carneiro <[email protected]> wrote: >> >>> 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 >>> <https://groups.google.com/d/msgid/metamath/CAFXXJSvcoRVOfBJZk5w11diH2tRxPZ-xjGp_XpWVK4U6axFHoQ%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/CABJcXbRYQErAK5kU2Qw3j6%2BoNBtOnLCfYLXu7zyfOgq_5CBsAA%40mail.gmail.com >> <https://groups.google.com/d/msgid/metamath/CABJcXbRYQErAK5kU2Qw3j6%2BoNBtOnLCfYLXu7zyfOgq_5CBsAA%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/CAFXXJSsrTWnsA67iYBtmvOAYSJ2FhdexVJMQ-wxFcrtVwYoaqw%40mail.gmail.com > <https://groups.google.com/d/msgid/metamath/CAFXXJSsrTWnsA67iYBtmvOAYSJ2FhdexVJMQ-wxFcrtVwYoaqw%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/CABJcXbRuEnxwNUuUK_bru%2B%3Dw58gQpc5VN8%3DdXxFuknm7nYBBFQ%40mail.gmail.com.
