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.
