search

metamath / set.mm

Metamath source file for logic and set theory
Other
254 stars 88 forks source link

Prove sbco2, hbsb, sbco3 and related theorems in iset.mm #339

Closed jkingdon closed 6 years ago

jkingdon commented 6 years ago

We are one distinct variable constraint away from having these. See sbco2v, hbsbv, and sbco3v for versions with the extra constraint. In classical logic, it is possible to prove two cases, where a pair of variables are identical or where they are distinct, and use pm2.61 to get the desired result. In intuitionistic logic, one needs a disjunction (a la nfsb2or), direct application of ax-i12, or some other technique.

We can also add sbcom to the list of theorems in this family; see #348 for the connection with sbco3.

Feel free to ask me (@jkingdon) for more background on what I have tried or discovered. But also feel free to try new things, because so far the breakthroughs have come in ways that have been hard for me, at least, to anticipate.

Oh, and if you do make progress, submitting frequent pull requests is encouraged. There may be other people working on this or closely related things.

jkingdon commented 6 years ago

This is done, at least assuming ax-bnd. See #364 and related issues and pull requests.

And note that the theorems in the subject line are (along with every predicate logic theorem which hasn't been moved to the end of the file) proved intuitionistically in iset.mm, as can be seen by running show usage ax-3/recursive.