Add theorems dcfrom (iset.mm)

[ducourtial]

In the propositional calculus section of iset.mm, the theorems notnotrdc, condc, and peircedc can be viewed as establishing (instances of) classical principles under the assumption that the law of excluded middle (or in other words, decidability) holds of suitable propositions occurring in the principles. The aim of this PR is to introduce three analogous theorems, dcfromnotnotr, dcfromcon, and dcfrompeirce, that derive (an instance of) the law of excluded middle given (a suitable instance of) the classical principle in question.

From a bird's-eye view, the theorems notnotrdc, condc, and peircedc indirectly show that, as schemas, excluded middle implies double negation elimination (DNE), contraposition, and Peirce's law, respectively. Conversely, the theorems added in this PR show that, as schemas, DNE, contraposition, and Peirce's law each imply the law of excluded middle. The treatment of propositional calculus in iset.mm (and related databases) does not allow us to formalize these results about schemas directly, at least not without introducing the schemas as axioms.

I imagine that the placement of the new theorems, under "Logical implication (continued)", is not entirely appropriate, and I'm open to discussing alternatives. Note that they cannot a priori be placed under §1.2.10, "Miscellaneous theorems", as their statements invoke the logical constants T. and F., which are defined later. Otherwise, placing them in a mathbox of my own is always a possibility.

[jkingdon]

Mathbox is of course an option and I guess more appealing the more we consider these to be exploratory or just one way to do it.

Part of me wonders whether something like Peirce's law can be expressed in terms of subsets of 1o (sometimes known as subsingletons), as we do for https://us.metamath.org/ileuni/df-exmid.html . That has worked out for things like Shroeder-Bernstein ( https://us.metamath.org/ileuni/exmidsbth.html ) but I haven't tried to work out what that would look like for propositional logic statements like the one in this pull request.

I don't have a lot of firm conclusions (at least yet). We should be able to get something merged, but let's hear your thoughts on the above (and see if anyone else wants to weigh in, I hope they aren't all waiting for me).

[ducourtial]

That's an interesting proposal. Looking at df-exmid, I'd imagine an analogous phrasing of Peirce's law looking something like

|- ( PEIRCE <-> A. x A. y ( ( x C_ { (/) } /\ y C_ { (/) } ) -> ( ( ( (/) e. x -> (/) e. y ) -> (/) e. x ) -> (/) e. x ) ) )

Here, (/) e. x and (/) e. y are stand-ins for the propositions ph and ps. Is that what you were thinking about?

This approach is less pure in that it makes use of concepts and principles (e.g., Separation) that go beyond propositional logic. On the other hand, as you suggest, it might enable us to prove |- ( EXMID <-> PEIRCE ) and the like (using the definition of PEIRCE above); establishing something akin to exmidexmid (i.e., that PEIRCE implies every instance of Peirce's law) would then allow us to move back into propositional logic (though this is only a one-way ticket).

In the context of IZF, I think this is a nice approach if it can be made to work, since we'd be working with universal statements (EXMID, PEIRCE) rather than, say, introducing axiom schemes.

Mathbox is of course an option and I guess more appealing the more we consider these to be exploratory or just one way to do it.

My impression is that the consequences of the law of excluded middle (over intuitionistic set theory) are well represented in iset.mm, but that results such as exmidsbth are relatively more scarce. As the implications between various non-intuitionistic principles are well-understood, I thought it might be relevant to fill out the landscape a bit more (here in propositional logic).

[jkingdon]

Here, (/) e. x and (/) e. y are stand-ins for the propositions ph and ps. Is that what you were thinking about?

Yup, that's about it. In https://us.metamath.org/ileuni/exmid1dc.html we use 𝑥 = {∅} for "x is true" but I think ∅ ∈ x should behave the same way.

This approach is less pure in that it makes use of concepts and principles (e.g., Separation) that go beyond propositional logic.

For this reason I'm not sure we need to completely abandon techniques such as the one in this pull request. Although I will admit that now that I've been working with EXMID for a while, and learned some of the tricks, it does feel like it does behave as expected.

On the other hand, as you suggest, it might enable us to prove |- ( EXMID <-> PEIRCE ) and the like (using the definition of PEIRCE above)

Yup! I suppose we'd find a way to avoid defining a PEIRCE notation but let's not get tangled up in that detail just yet.

; establishing something akin to exmidexmid (i.e., that PEIRCE implies every instance of Peirce's law) would then allow us to move back into propositional logic (though this is only a one-way ticket).

This was the most surprising thing to me - it isn't a one-way ticket! At least in the sense of something like https://us.metamath.org/ileuni/exmidonfin.html where https://us.metamath.org/ileuni/exmidonfinlem.html can be expressed in terms of propositions - that is use 𝜑 for a proposition without extra notational overhead.

My impression is that the consequences of the law of excluded middle (over intuitionistic set theory) are well represented in iset.mm, but that results such as exmidsbth are relatively more scarce. As the implications between various non-intuitionistic principles are well-understood, I thought it might be relevant to fill out the landscape a bit more (here in propositional logic).

Definitely more to do. In case you haven't noticed it we also have https://us.metamath.org/ileuni/mmil.html#flavors which has various principles which are between IZF and ZFC in strength. That table doesn't try to list all of the consequences of EXMID, or equivalents (or the others listed), but it at least gives something to search for (using the search command in metamath-exe, or one's favorite technique).

And even in the realm of propositional logic there are probably more ways to express the various excluded middle equivalents.

Anyway, lots of interesting topics but let me bring it back to this pull request. I'd propose to merge it as-is, largely on the grounds that we can always move things around later.

[ducourtial]

This was the most surprising thing to me - it isn't a one-way ticket!

Interesting — I guess that lemma expresses (the semantics of) a proposition 𝜑 in terms of a class 𝐴. Thanks for the pointer.