What should we do with classical theorems in iset.mm?

[jkingdon]

Right now, ax-3 is present but marked with "New usage is discouraged". The whole point, of course, of iset.mm is that we can develop logic without ax-3.

Currently, 414 theorems use ax-3 according to show usage ax-3/recursive, so we should either delete them (and ax-3), or put "(New usage discouraged.)" in them.

The arguments for retaining ax-3 and theorems derived from it are to contrast classical logic with intuitionistic logic (sort of like ax-groth, I guess, although there is probably less danger of accidentally overusing ax-groth or getting confused by its presence). Ideally, there would be a better way to express how different axiom sets relate to each other - like http://wikiproofs.org/w/index.php?title=From_intuitionistic_to_classical_propositional_logic - but in the absence of something like ghilbert-style modules, we're left with approaches like the way we handle the various sets of predicate logic axioms (ax12o and all that stuff). Having said all that, I'd probably lean towards deleting all the classical theorems. How would we refer to classical theorems from the intuitionistic pages if we did that? Would we just link to URLs like http://us.metamath.org/mpeuni/anor.html ?

[digama0]

The classical theorems are there for a reason, to show that we can derive all the original stuff with ax-3, and also to mark theorems that are either known to require classical reasoning, or haven't yet been "intuitionized". I don't think any marking is necessary, we already have ax-3 tracking in the HTML, although mentioning it in the text when the usage is deliberate is fine. If we insist on an explicit annotation then of course (New usage is discouraged.) should do the trick.

[nmegill]

On 11/25/17 9:21 PM, Jim Kingdon wrote:

Having said all that, I'd probably lean towards deleting all the classical theorems. How would we refer to classical theorems from the intuitionistic pages if we did that? Would we just link to URLs like http://us.metamath.org/mpeuni/anor.html ?

That would be a little ugly, although a possibility.

Another possibility is to move ax-3 and all that depends on it to the end of iset.mm, kind of like we postpone introducing ax-ac in set.mm. We could keep all the current ax-3-dependent theorems, or we could just include those like anor that we need to reference. In any case, we wouldn't need "(New usage is discouraged.)" anywhere because there will be no intuitionistic theorems in that section that could be contaminated. (Well, at least until we introduce mathboxes, but I doubt that will happen soon.)

Norm

[jkingdon]

Moving ax-3 later in the file is also something which occurred to me.

I'm trying to make the whole file clearer about things like the difference between "known to require classical reasoning" and "haven't yet been intuitionized". But I am open to a variety of ways to get there.

[jkingdon]

My current thinking is roughly this:

1. Remove stuff which is easy to remove and doesn't accomplish anything in iset.mm. I'm thinking of things like Nicod's axioms (which are an alternative axiomization of classical propositional logic, not intuitionistic propositional logic).

2. Start chipping away at predicate logic by trying to decide whether things like ax12o (and others which depend on ax-3) can just be removed (and their usages replaced with other theorems), or proved intuitionistically, or what. Much of the ax-*o stuff makes sense in terms of a classical history and trying to carry it over to intuitionistic logic doesn't make much sense to me, but the details here will depend on seeing where it is used.

3. At some point in this process (after step 1 and maybe after some of step 2), move ax-3 (and everything which still depends on it) to the end of the file.

[nmegill]

I think this plan is fine.

Some optional things:

1. There have been a number of label changes in the set.mm file from which the initial version was taken. You can see them at the top of set.mm in reverse order by date. You might want to apply them to iset.mm in order to be closer to the set.mm names, making it somewhat more familiar to people used to set.mm. This is just a cosmetic improvement, though, and entirely optional.

David A. Wheeler has a bash script to apply these changes: https://groups.google.com/d/msg/metamath/HDQXr196Yo0/5Oin28nvBgAJ

2. You can clear the list of recent label changes at the top since it really applies to set.mm. Maybe leave the top entry, "28-Jan-15 strssd", so we can know where to start if we later want to apply the set.mm label changes.

3. You can add your name as a contributor to the contributor list. Possibly the list could be trimmed down to reflect the actual contributors.

Norm

On 11/29/17 12:34 PM, Jim Kingdon wrote:

My current thinking is roughly this:

1.

Remove stuff which is easy to remove and doesn't accomplish anything
in iset.mm. I'm thinking of things like Nicod's axioms (which are an
alternative axiomization of classical propositional logic, not
intuitionistic propositional logic).

2.

Start chipping away at predicate logic by trying to decide whether
things like ax12o (and others which depend on ax-3) can just be
removed (and their usages replaced with other theorems), or proved
intuitionistically, or what. Much of the ax-*o stuff makes sense in
terms of a classical history and trying to carry it over to
intuitionistic logic doesn't make much sense to me, but the details
here will depend on seeing where it is used.

3.

At some point in this process (after step 1 and maybe after some of
step 2), move ax-3 (and everything which still depends on it) to the
end of the file.

[jkingdon]

1. I like the idea of trying to use similar names in set.mm and iset.mm but even with that script it might be a bit labor intensive. Maybe I'll get the chance to take a closer look at a bulk rename at some time in the future, or maybe I'll just apply changes by hand when I notice them.

2. Submitted as https://github.com/metamath/set.mm/pull/169

3. I guess maybe I have a weak preference for full names rather than initials but if people are looking at the contributor list I can take a look at some point.

[jkingdon]

It will be a while before the work outlined above is done, but it is well underway, as people can see from all the recent changes to iset.mm. I'm going to close this issue as I think the path here is now pretty clear. Thanks to everyone for the comments and suggestions.