jkingdon
commented
6 years ago Hmm, if I gave some sketchy outlines, would that be enough for you to find references in iset.mm and turn it into documentation?
-
If you see pm2.61 you'll probably end up with two theorems for the two cases. In particular, if the cases were A e. _V and -. A e. _V you probably just care about the A e. _V case.
-
Non-empty almost always needs to be changed to inhabited.
-
If the original proof relied on propositional/predicate logic which isn't a theorem of intuitionistic logic, maybe there is a way of expressing it more directly. This is perhaps the hardest one to put in cookbook form: sometimes I just try some things and see if anything works.
3a. If the original proof relied on df-ex so that it could prove a theorem for A. and then get E. for free (or vice versa), instead go look at the original proof and try to come up the analogues to each step for the other quantifier (for example, cbvrexcsf , sbcrext , rexxpf ).
-
If you are dealing with a definition, try to find the best constructive definition from the literature (HoTT book, Stanford Encyclopedia of Philosophy, Bauer, etc). Once you pick a definition, that'll affect the proofs which rely on that definition.
-
If there is case elimination on whether variables are distinct, most of the time you just need the variant with distinct variables. Sometimes you can then remove the constraint with a temporary variable (e.g. the various sbco2* variants, nfrabya).
-
Sometimes one direction of a biconditional holds, or subset holds instead of equality. You might be able to keep the easy direction and worry about the other one later.
-
If your proof relies on dveeq2 try dveeq2or and likewise for the other things downstream of ax-i12 or ax-bnd .
7a. If you have a disjunction, be reluctant to turn it into an implication using ord and the like. Instead, show that each disjunct implies what you are trying to prove and use jaoi to join those two implications into something which can hook up to the disjunction.
7b. Disjunctive syllogism holds in intuitionistic logic but we don't have a lot of theorems to make it easy to apply. Unless we add those, you'll use ord or something similar followed by mpd or something similar.
-
If your proof is doing tricky things perhaps in the interest of shortness, try just expanding the definitions and applying logic in a straightforward way. See if this gets you a working (although perhaps longer) proof.
-
If your proof relies on a biconditional in set.mm which isn't in iset.mm, see if one direction is in iset.mm and see which direction your proof is using. For example 19.35-1 or exnalim .
-
If you are doing things with inhabited classes, you may be able to dig up some predicate logic you haven't used in a while (e.g. raaan).
-
Consider the possibility of giving up. Some things just won't have intuitionistic proofs. The more it looks like excluded middle or other non-intuitionistic statements, the more likely you are dealing with one of these. But it can be hard to have good intuition about this and rubrics like "can I use this statement to prove 'ph or not ph' for an arbitrary proposition" are not always easy to apply.
-
Switching between 2th and 2false might help (e.g. dfnul2 , dfnul3 , rab0 ).
-
In many cases statements which are equivalent in classical logic become several non-equivalent statements (e.g. xor, ordinals, non-empty versus inhabited, apartness versus negated equality). This is usually a good place to look for a literature reference, but don't be afraid to change the statement being proved to "what you really meant is X" as appropriate.
-
If a statement has multiple equivalences in set.mm (e.g. mo2 and mo3 , or dffun2 and dffun3 ) and only some of them in iset.mm, sometimes a pretty similar proof will work (that is, which one to use in the original proof may have been a fairly arbitrary choice).
-
If all else fails, ask Mario. I'm only half joking on this one.
On October 15, 2018 4:55:39 PM PDT, "David A. Wheeler" notifications@github.com wrote:
I would love to see the iset.mm documentation explain more about how to "intuitionize", including citations pointing to especially good books/papers and specific explanations of how to do it in metamath ("when you see X, you often need to convert to Y by following steps Z"). Pointing to a few examples of theorems that are especially good at explaining the changes (and how to do something similar) would be great.
This is probably especially a request to @jkingdon ... but anyone else's input would be welcome.
I am intrigued by intuitionistic logic, but I am hopelessly steeped in classical logic :-). A little more explanation of what you have to change would be helpful for me, and probably for others.
-- You are receiving this because you were mentioned. Reply to this email directly or view it on GitHub: https://github.com/metamath/set.mm/issues/594
david-a-wheeler
I would love to see the iset.mm documentation explain more about how to "intuitionize", including citations pointing to especially good books/papers and specific explanations of how to do it in metamath ("when you see X, you often need to convert to Y by following steps Z"). Pointing to a few examples of theorems that are especially good at explaining the changes (and how to do something similar) would be great.
This is probably especially a request to @jkingdon ... but anyone else's input would be welcome.
I am intrigued by intuitionistic logic, but I am hopelessly steeped in classical logic :-). A little more explanation of what you have to change would be helpful for me, and probably for others.