Law of excluded middle

[Anarcocap-socdem]

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!

[Thierry Arnoux]

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.
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

--
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 metamath+u...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/metamath/f3de6454-93b6-4ae1-856a-ceb4bb88c0abn%40googlegroups.com.

[Jim Kingdon]

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.

To view this discussion visit https://groups.google.com/d/msgid/metamath/44fba649-7673-4418-bd96-9354224bfed8%40gmx.net.

[Noam Pasman]

Hi,

I think I can help, but this might be slightly off:

If you apply the law of excluded middle to the continuum hypothesis you would get (CH or (not CH)), which is a true statement. However, CH is not provable and (not CH) is not provable. So we can prove that one of the two statements are true, but we can't prove that the first one is true and we can't prove that the second one is true. That seems weird to think about but technically there's no logical contradiction there.

Another way to think about this is that LEM says that either CH or (not CH) is true, not that either CH or (not CH) is provable. That would be a different statement: turnstile((turnstile CH) or (turnstile (not CH))) which is not possible to do in metamath (and to my knowledge isn't very practical anywhere).

I am very much not an expert but hopefully this clarifies it a bit.

--

[Noam Pasman]

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.

To view this discussion visit https://groups.google.com/d/msgid/metamath/d653f50d-c912-4d2d-8168-bce2d56408d4%40panix.com.

[Mario Carneiro]

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).

To view this discussion visit https://groups.google.com/d/msgid/metamath/CABJcXbQ_bkB-Ef1do-1T%2Bm9pd979a42WhV_J08BuvqWZtCHczg%40mail.gmail.com.

[Noam Pasman]

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?

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.

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?

To view this discussion visit https://groups.google.com/d/msgid/metamath/CAFXXJSvcoRVOfBJZk5w11diH2tRxPZ-xjGp_XpWVK4U6axFHoQ%40mail.gmail.com.

[Mario Carneiro]

On Tue, Nov 26, 2024 at 4:30 PM Noam Pasman <noam....@gmail.com> 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.

 

To view this discussion visit https://groups.google.com/d/msgid/metamath/CABJcXbRYQErAK5kU2Qw3j6%2BoNBtOnLCfYLXu7zyfOgq_5CBsAA%40mail.gmail.com.

[Noam Pasman]

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?

To view this discussion visit https://groups.google.com/d/msgid/metamath/CAFXXJSsrTWnsA67iYBtmvOAYSJ2FhdexVJMQ-wxFcrtVwYoaqw%40mail.gmail.com.

[Mario Carneiro]

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.

To view this discussion visit https://groups.google.com/d/msgid/metamath/CABJcXbRuEnxwNUuUK_bru%2B%3Dw58gQpc5VN8%3DdXxFuknm7nYBBFQ%40mail.gmail.com.

[Noam Pasman]

Ok, thank you! I'll probably try and get a bit more acquainted with this and then think about it a bit more.

To view this discussion visit https://groups.google.com/d/msgid/metamath/CAFXXJSvCKOkZnXGOP-b2QrhjVpkxz4aigoLz76-3Q06N1oQjPw%40mail.gmail.com.