Ok, thank you! I'll probably try and get a bit more acquainted with this and then think about it a bit more.
On Fri, Nov 29, 2024 at 4:41 PM Mario Carneiro <[email protected]> wrote: > No, you cannot prove ZFC |/- CH in PA. It's conceivable that you could > prove Con(ZFC) -> ZFC |/- CH in PA, but it would probably be quite > challenging and I am not sure anyone has ever worked it out. There are > certainly going to be some sufficient purely number theoretic assertions > one can make in PA which imply independence of CH but you might need more > than just consistency. > > On Fri, Nov 29, 2024, 20:10 Noam Pasman <[email protected]> wrote: > >> 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 >> <https://groups.google.com/d/msgid/metamath/CABJcXbRuEnxwNUuUK_bru%2B%3Dw58gQpc5VN8%3DdXxFuknm7nYBBFQ%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/CAFXXJSvCKOkZnXGOP-b2QrhjVpkxz4aigoLz76-3Q06N1oQjPw%40mail.gmail.com > <https://groups.google.com/d/msgid/metamath/CAFXXJSvCKOkZnXGOP-b2QrhjVpkxz4aigoLz76-3Q06N1oQjPw%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/CABJcXbRf0KczdnR%3DqH7uyrZU7VGCTEAVFMZO15CKN4qwaovAgA%40mail.gmail.com.
