Add note about df-clel , df-cleq and df-clab #3375
Conversation
set.mm
Outdated
| and moving them up to the ~ ax-4 through ~ ax-9 section. | ||
| and moving them up to the ~ ax-4 through ~ ax-9 section.</p> | ||
| <p>For these purposes, ~ df-clel , ~ df-cleq , | ||
| and ~ df-clab should be considered axioms rather than definitions. |
There was a problem hiding this comment.
df-clab is actually conservative
proof: wcel is only used by wel at the time of df-clab. df-clab is not ambiguous with wel, so wcel can be considered to have a piecewise definition with wel and df-clab (at the point of df-clab)
There was a problem hiding this comment.
OK, I wasn't sure whether to include df-clab just because the definition checker can't check it, or omit it because I had no knowledge of an interaction with axiom usage.
I've updated this pull request to omit it.
There was a problem hiding this comment.
This is indeed the kind of text we would have to write if we keep df-cleq and df-clel unchanged. Introducing particular cases adds complexity, so hopefully the changes mentioned in #3199 (comment) will make this not needed.
jkingdon
force-pushed
the
conventions-clel
branch
from
fe2bca0 to
d78e041
Compare
This is in the conventions where we describe reducing use of axioms.
jkingdon
force-pushed
the
conventions-clel
branch
from
d78e041 to
ac3d7c3
Compare
Ah. I ran the rewrap script but forgot that it doesn't touch anything inside HTML tags. I have done a manual rewrap. |
|
Could you then push the result? |
I pushed up everything I did. The text I added is pretty well wrapped, isn't it? In general, I think we should mostly limit our concern for style and formatting to what we can check automatically. |
|
Feel free to close #3199 after this is merged. |
|
Whether this text ends up being here for a short time or for longer depends on whether we make other changes to df-clel and df-cleq, but that doesn't seem like a reason not to merge it. |
This is in the conventions where we describe reducing use of axioms.
There's a whole lot more background at #3199 (comment) and in some of the pages a click or two away from the text I'm adding, but the short summary is that whatever we want to do about these definitions/axioms in the future, we might as well describe what is going on now.