Can this be proved?: ( A e. ( B \ { C , D } ) <-> ( A e. B /\ A =/= C /\ A =/= D ) )

[David A. Wheeler]

Question: Can this be proved (& if so how)?:
( A e. ( B \ { C , D } ) <-> ( A e. B /\ A =/= C /\ A =/= D ) )

This *seems* like an easy theorem to prove & is a clear analogy to eldifsn:
( A e. ( B \ { C } ) <-> ( A e. B /\ A =/= C ) )

I started to prove this using eldif:
( A e. ( B \ C ) <-> ( A e. B /\ -. A e. C ) )

But then I found that relevant supporting theorems tended to be
one-way (-> not <->), like elpri:
( A e. { B , C } -> ( A = B \/ A = C ) )

Or that many relevant theorems have additional requirements
on A, e.g., like elprg:
( A e. V -> ( A e. { B , C } <-> ( A = B \/ A = C ) ) )

I'm probably stuck on something stupid & obvious. However, perhaps
that some of the theorems I listed above could be generalized
(if they were more general it'd be easy).
Or maybe I'm trying to prove something too general.
This structure comes up with logb, because of the condition
" x e. ( CC \ { 0 , 1 } ) ", but clearly this is a much more general
construct.

Thanks!

--- David A. Wheeler

[Mario Carneiro]

Writing a complete proof since it is easier than an explanation:

50::elprg              |- ( A e. B -> ( A e. { C , D } <-> ( A = C \/ A = D ) ) )
51:50:notbid          |- ( A e. B -> ( -. A e. { C , D } <-> -. ( A = C \/ A = D ) ) )
52::neanior           |- ( ( A =/= C /\ A =/= D ) <-> -. ( A = C \/ A = D ) )
53:51,52:syl6bbr     |- ( A e. B -> ( -. A e. { C , D } <-> ( A =/= C /\ A =/= D ) ) )
54:53:pm5.32i       |- ( ( A e. B /\ -. A e. { C , D } ) <-> ( A e. B /\ ( A =/= C /\ A =/= D ) ) )
55::eldif           |- ( A e. ( B \ { C , D } ) <-> ( A e. B /\ -. A e. { C , D } ) )
56::3anass          |- ( ( A e. B /\ A =/= C /\ A =/= D ) <-> ( A e. B /\ ( A =/= C /\ A =/= D ) ) )
qed:54,55,56:3bitr4i
                   |- ( A e. ( B \ { C , D } ) <-> ( A e. B /\ A =/= C /\ A =/= D ) )

The secret sauce you needed was pm5.32i.

Mario

--- David A. Wheeler

--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+unsubscribe@googlegroups.com.
To post to this group, send email to meta...@googlegroups.com.
Visit this group at https://groups.google.com/group/metamath.
For more options, visit https://groups.google.com/d/optout.

[Thierry Arnoux]

I would try to use ~ difundi :

df-pr $a |- { A , B } = ( { A } u. { B } ) $.

difundi $p |- ( A \ ( B u. C ) ) = ( ( A \ B ) i^i ( A \ C ) ) $=

elin $p |- ( A e. ( B i^i C ) <-> ( A e. B /\ A e. C ) ) $=

[Thierry Arnoux]

...and I thought I was answering fast! ;-)

My method ultimately leads to a proof longer than Mario's:

10::df-pr          |- { C , D } = ( { C } u. { D } )
20::difundi        |- ( B \ ( { C } u. { D } ) ) = ( ( B \ { C } ) i^i ( B \ { D } ) )
25:10:difeq2i      |- ( B \ { C , D } ) = ( B \ ( { C } u. { D } ) )
26:25,20:eqtri     |- ( B \ { C , D } ) = ( ( B \ { C } ) i^i ( B \ { D } ) )
29:26:eleq2i       |- ( A e. ( B \ { C , D } ) <-> A e. ( ( B \ { C } ) i^i ( B \ { D } ) ) )
30::elin           |- ( A e. ( ( B \ { C } ) i^i ( B \ { D } ) ) <-> ( A e. ( B \ { C } ) /\ A e. ( B \ { D } ) ) )
40::eldifsn        |- ( A e. ( B \ { C } ) <-> ( A e. B /\ A =/= C ) )
50::eldifsn        |- ( A e. ( B \ { D } ) <-> ( A e. B /\ A =/= D ) )
60:40,50:anbi12i   |- ( ( A e. ( B \ { C } ) /\ A e. ( B \ { D } ) ) <-> ( ( A e. B /\ A =/= C ) /\ ( A e. B /\ A =/= D ) ) )
70::anandi         |- ( ( A e. B /\ ( A =/= C /\ A =/= D ) ) <-> ( ( A e. B /\ A =/= C ) /\ ( A e. B /\ A =/= D ) ) )
80::3anass         |- ( ( A e. B /\ A =/= C /\ A =/= D ) <-> ( A e. B /\ ( A =/= C /\ A =/= D ) ) )
90:29,30,60:3bitri |- ( A e. ( B \ { C , D } ) <-> ( ( A e. B /\ A =/= C ) /\ ( A e. B /\ A =/= D ) ) )
qed:70,80,90:3bitr4ri |- ( A e. ( B \ { C , D } ) <-> ( A e. B /\ A =/= C /\ A =/= D ) )

To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.

[David A. Wheeler]

On Tue, 18 Jul 2017 16:35:45 +0100, Mario Carneiro <di....@gmail.com> wrote:
> Writing a complete proof since it is easier than an explanation:

Awesome, and thanks. I'll add & give you credit.

The 1-element version is "eldifsn"; should I call this "eldifsn2"?:

> |- ( A e. ( B \ { C , D } ) <-> ( A e. B /\ A =/= C /\ A =/= D ) )

We should probably have the 3-element version, perhaps calling it "eldifsn3":

> |- ( A e. ( B \ { C , D , E } ) <-> ( A e. B /\ ( A =/= C /\ A =/= D /\ A =/= E ) ) )

--- David A. Wheeler

[Mario Carneiro]

That would be eldifpr and eldiftp.

Mario

--- David A. Wheeler

[David A. Wheeler]

On Tue, 18 Jul 2017 19:49:53 +0100, Mario Carneiro <di....@gmail.com> wrote:
> That would be eldifpr and eldiftp. [in addition to eldifsn]

Okay. Given that "eldifsn" is:
> ( A e. ( B \ { C } ) <-> ( A e. B /\ A =/= C ) )

I'm trying to decipher the naming convention used here.
I'm guessing the initial "el" is "element member of" (e.),
"dif" is "difference", and the last 2 letters
are sn->singleton, pr->pair, tp->triple.

Is that right? Or is "d" used for difference, followed by "if"?
If so, that seems odd; "if" is often used for inference "->", but this is a
biconditional.

I'd like to document in comments where some of the
names "come from", to help make the naming conventions more obvious.
Something like this:
The name of this theorem ("eldifsn") is derived from
"el" (element member of) + "dif" (difference) + "sn" (singleton).

--- David A. Wheeler

[Mario Carneiro]

On Tue, Jul 18, 2017 at 10:19 PM, David A. Wheeler <dwhe...@dwheeler.com> wrote:

On Tue, 18 Jul 2017 19:49:53 +0100, Mario Carneiro <di....@gmail.com> wrote:
> That would be eldifpr and eldiftp. [in addition to eldifsn]

Okay.  Given that "eldifsn" is:
> ( A e. ( B \ { C } ) <-> ( A e. B /\ A =/= C ) )

I'm trying to decipher the naming convention used here.
I'm guessing the initial "el" is "element member of" (e.),
"dif" is "difference", and the last 2 letters
are sn->singleton, pr->pair, tp->triple.

Is that right?  Or is "d" used for difference, followed by "if"?
If so, that seems odd; "if" is often used for inference "->", but this is a
biconditional.

You were right the first time. "el" means e. , "dif" means \ , "sn" means { A } . Put them together and you have the property on the left that we are trying to characterize. "if" means if ( ph, A, B ). We don't use it for inference (although it might occur as a suffix "i" + "f" if we had an inference theorem that also had F/ hypotheses).
 

I'd like to document in comments where some of the
names "come from", to help make the naming conventions more obvious.
Something like this:
  The name of this theorem ("eldifsn") is derived from
  "el" (element member of) + "dif" (difference) + "sn" (singleton).

I'm not opposed to this, but I don't know how best to present and store the information.

Mario

[David A. Wheeler]

On Tue, 18 Jul 2017 22:45:52 +0100, Mario Carneiro <di....@gmail.com> wrote:
> I'm not opposed to this, but I don't know how best to present and store the
> information.

I think putting a list in "conventions" of some more-common abbrevations used in
names would be a good start. It should show both the longer name (to help
remember it) and its symbol(s) where relevant.
I'd also add examples, to put them in context, and
sort them alphabetically so a mysterious name might be decodable.
In short, add this to "conventions":

Common abbreviations used in theorem names are:
* "dif": difference ( ` \ ` ). Example: ~ eldifsn
* "el": element member of ( ` e. ` ). Example: ~ eldifsn
* "mp": modus ponens
* "sn": singleton ( ` { A } ` ). Example: ~ eldifsn
* "syl": syllogism

There's no need to list them *all* for the list to be useful.
A decoder for simply the more common abbreviations would be helpful.

In addition, I'd add comments for at least a few theorems like "eldifsn",
particularly if they're being used as naming examples. That would help
reinforce understanding.

I can cobble up a starting list. In fact, if there's no objection,
I can just add a short list to the "conventions" section.
There's no harm in having a short list there,
and we can then discuss if adding more entries would be useful.

--- David A. Wheeler

[Mario Carneiro]

On Tue, Jul 18, 2017 at 10:59 PM, David A. Wheeler <dwhe...@dwheeler.com> wrote:

> On Tue, Jul 18, 2017 at 10:19 PM, David A. Wheeler <dwhe...@dwheeler.com> wrote:
> > I'd like to document in comments where some of the
> > names "come from", to help make the naming conventions more obvious.
> > Something like this:
> >   The name of this theorem ("eldifsn") is derived from
> >   "el" (element member of) + "dif" (difference) + "sn" (singleton).

On Tue, 18 Jul 2017 22:45:52 +0100, Mario Carneiro <di....@gmail.com> wrote:
> I'm not opposed to this, but I don't know how best to present and store the
> information.

I think putting a list in "conventions" of some more-common abbrevations used in
names would be a good start. It should show both the longer name (to help
remember it) and its symbol(s) where relevant.
I'd also add examples, to put them in context, and
sort them alphabetically so a mysterious name might be decodable.
In short, add this to "conventions":

Common abbreviations used in theorem names are:
* "dif": difference ( ` \ ` ).  Example: ~ eldifsn
* "el": element member of ( ` e. ` ).  Example: ~ eldifsn
* "mp": modus ponens
* "sn": singleton ( ` { A } ` ).  Example: ~ eldifsn
* "syl": syllogism

I would distinguish "mp" and "syl" from the others in this list. Even though "mp" is often used as a label abbreviation with this meaning, it doesn't attach specifically to a syntax constructor as the others do. Basically every syntax in Metamath has a label fragment associated to it, and there's even a simple rule that will tell you what it is in 99% of cases (and let me know if you see any exceptions so I can fix it): the name of the definition will be df-<label fragment> for that syntax. That is, the definition of the singleton is df-sn, the definition of difference is df-dif. (Unfortunately this rule doesn't work for elementhood, since it is primitive and so has no definition df-el as you would expect from this rule).

I put "mp" and "syl" in a more ad-hoc category of label framgents, when the syntax alone is insufficient to distinguish the 100+ different implication-exclusive theorems we have. It's not a bad idea to collect these as well, but the rules for application of these is not as formulaic as the other category.

Mario

[Norman Megill]

On Tuesday, July 18, 2017 at 5:19:31 PM UTC-4, David A. Wheeler wrote:

On Tue, 18 Jul 2017 19:49:53 +0100, Mario Carneiro wrote:
> That would be eldifpr and eldiftp. [in addition to eldifsn]

Okay.  Given that "eldifsn" is:
> ( A e. ( B \ { C } ) <-> ( A e. B /\ A =/= C ) )

I'm trying to decipher the naming convention used here.
I'm guessing the initial "el" is "element member of" (e.),  

"dif" is "difference", and the last 2 letters
are sn->singleton, pr->pair, tp->triple.

Right.
 

Is that right?  Or is "d" used for difference, followed by "if"?

Not in the context of this theorem.  It might be the case for some other theorem.

In particular, "el", "dif", "sn", "pr", "tp" are pretty much universally used to abbreviate element of, difference, singleton, pair, triple.  So if you search for labels matching *dif* you will get essentially all of the theorems that involve difference as their focus.  You may also get a few irrelevant ones if they contain an abbreviation ending with "d" juxtaposed with another beginning with "if".

Labels are intended to be easy to remember hints about theorem content, not a 1-1 mapping.  An attempt to make say "dif" correspond uniquely to theorems about difference is a losing battle.  You would end up with very long names that would be difficult to remember and tedious to type.  Recall this post:

https://groups.google.com/d/msg/metamath/ZD_kEVSepj0/5M51W6eBCwAJ

 

If so, that seems odd; "if" is often used for inference "->", but this is a
biconditional.

I'd like to document in comments where some of the
names "come from", to help make the naming conventions more obvious.
Something like this:
  The name of this theorem ("eldifsn") is derived from
  "el" (element member of) + "dif" (difference) + "sn" (singleton).

I would strongly discourage putting such an explanation in the theorem's content, because we often change labels, or even naming schemes involving many theorems, when better ones are suggested.  This is evident from the label change list at the top of set.mm, which historically has been an attempt toward more uniform naming conventions over time as people make suggestions or point out inconsistencies.

I would be open to having a general description for our most common label conventions in a single place (not scattered in theorem comments), but someone would have to maintain it.  For example, in this text file:
http://us.metamath.org/mpegif/mmnotes2004.txt (search for "13-May-04")
I made an attempt to describe some of the thinking behind labels using ax-4 variants as an example.

(As a semi-related aside, I want to change "*a4*", which means "related to ax-4", to become "sp", standing for "specialization", because tying the abbreviation to ax-4 would make a later change of axiom names confusing.  There aren't any conflicts with "sp" in the pred. calc. section, only later on where it means "span" and a few other things, but we tolerate such conflicts outside of context.)

Norm

[David A. Wheeler]

On Tue, 18 Jul 2017 15:21:59 -0700 (PDT), Norman Megill <n...@alum.mit.edu> wrote:
> I would be open to having a general description for our most common label
> conventions in a single place (not scattered in theorem comments), but
> someone would have to maintain it.

In a new branch I've modified the "conventions" section to describe the
common label conventions as I understand them. If they're incorrect or
have a serious omission, we can now add to them.

You can see the changes here:
> https://github.com/metamath/set.mm/pull/126/files
and discuss it here:
> https://github.com/metamath/set.mm/pull/126

--- David A. Wheeler

[Norman Megill]

On Tuesday, July 18, 2017 at 6:21:59 PM UTC-4, Norman Megill wrote:

...

(As a semi-related aside, I want to change "*a4*", which means "related to ax-4", to become "sp", standing for "specialization", because tying the abbreviation to ax-4 would make a later change of axiom names confusing.  There aren't any conflicts with "sp" in the pred. calc. section, only later on where it means "span" and a few other things, but we tolerate such conflicts outside of context.)

I did this in develop commit 62d5c5b, changing *cla4* and *a4* (no cl) to *spc* and *sp*
respectively.  Searching for labels sp*, rsp*, and *spc* will match very closely what was *a4* before in the predicate calculus and early set theory sections.

This paves the way for the subject headline of this post:

The pred calc axioms in set.mm are somewhat disorganized, which is a consequence of various simplifications and redundances discovered over the past decade or so, leading to gaps in the numbering among other things.

I don't think any more simplifications or redundancies will be found (though I'd be thrilled to be proved wrong), so I think the current axioms are stable, giving us the opportunity to reorganize and rename them.

An old philosophy still in place to a certain extent in set.mm was to prove as much as possible without any $d's, then introduce axiom(s) needing $d's.  However, a number of the original $d-free axioms were shown redundant, but their proofs typically involved ax-17, so it doesn't really make sense to organize them this way anymore.

I think the cleanest reorganization would be the following:

1. Introduce Tarski's 6 axiom schemes first, providing a logically complete system (but one without much power to derive useful schemes).  The work described in http://us.metamath.org/mpegif/equidK.html will be moved to this section, proving as much as we can from these 6 axiom schemes alone.  These 6 schemes can emulate all valid object-language theorems, so in principle they suffice for translation to and from other proof languages that work with the object language rather than our metalanguage.

2. Add the 4 set.mm-specific technical schemes that allow us to prove all possible schemes involving wff metavariables and bundled set metavariables (metalogical completeness).

3. Add a standalone section showing proofs to and from the obsolete axioms ax-*o and redundant ones such as ax-10.  Most of these are in my 1995 paper and are called C<nn>'.  I will rename them ax-c4, ax-c5, etc. for easier correspondence with the paper.  Showing that the ones in the paper are equivalent shows that metalogical completeness also holds for the current official ones.  However, the use of anything requiring the obsolete axioms will be "discouraged", so ax-b* won't be used outside of that section..


I thought long and hard about whether to give the axioms numeric or mnemonic names.  I have concluded that numeric names are better for these axiom schemes:  you can recognize at once what axiom group they fall under (prop calc, Tarski, or technical), you know how many axioms there are without counting, and it is much easier to check that you haven't forgotten one when working with them as a collection (since there are no gaps in the numbering sequence).

I did try giving them short mnemonic names as an experiment, and I didn't like it.  It just felt uncomfortable somehow, for the reasons above.

In ZFC, the axioms are given names (union, choice, etc.) because they have clear, well-defined purposes.  It is often of interest to see what can be proved without depending on, say, choice.  But in pred calc, the English description may only vaguely indicate what the axiom is for.  Unlike ZFC, I don't think it is that interesting to omit an axiom from our predicate calculus ones, because they work together synergistically.

Almost all textbooks follow this labeling convention, using numbers for prop and pred calc axioms, but using names or abbreviations for ZFC axioms.

Numbering might be a problem if the axioms were in a state of flux with the numbers constantly changing, but I think the axioms are going to be stable at this point, so this should be a one-time change.

Most people will be unaffected by this change because it is not common for the axioms to be referenced directly in proofs.  In the few cases where they are commonly used directly, we can restate them with an alternate more meaningful name; for example, hbn1 is exactly ax-6, but named as a member of the hb* family of theorems.

Below is the reorganization and renaming I propose.

     Current New   Description
     name    name


     Propositional calculus

     ax-1   ax-1   Simplification
     ax-2   ax-2   Frege
     ax-3   ax-3   Transposition
     ax-mp  ax-mp  Rule of modus ponens


     Tarski's axiom schemes (for logical completeness)  ax-4 through ax-9

     ax-5   ax-4   Quantified Implication
     ax-17  ax-5   Quantifier Introduction
     ax-9   ax-6   Existence
     ax-8   ax-7   Equality
     ax-13  ax-8   Equality
     ax-14  ax-9   Equality
     ax-gen ax-gen Rule of Generalization


     Technical schemes (for metalogical completeness) ax-10 through ax-13

     ax-6   ax-10  Quantified Negation
     ax-7   ax-11  Quantifier Commutation
     ax-11  ax-12  Substitution
     ax-12  ax-13  Quantified Equality
    
     Obsolete or redundant

     ax-4   ax-c5   Specialization
     ax-5o  ax-c4   Quantified Implication
     ax-6o  ax-c7   Quantified Negation
     ax-9o  ax-c10  Existence
     ax-10  ax-c11n Quantifier Substitution (c11n means newer c11)
     ax-10o ax-c11  Quantifier Substitution
     ax-11o ax-c15  Variable Substitution
     ax-12o ax-c9   Quantifier Introduction
     ax-15  ax-c14  Quantifier Introduction
     ax-16  ax-c16  Distinct Variables

Note:  ax-6 (old ax-9) will be stated without a $d, but its direct use will be "discouraged".  Instead, it will be used only to prove Tarksi's weaker version ax6v (old ax9v) with a 1-step proof, and all other references will trace back to ax6v (old ax9v).

Norm

[Mario Carneiro]

I'm okay with all this, although separating ax-9, ax-11 and especially ax-17 from these numbers will take some re-learning. (I've also referred to them by these names in various papers, which will now be obsolete. Not sure how much of a concern this is.)

Most people will be unaffected by this change because it is not common for the axioms to be referenced directly in proofs.

It's good, then, that we introduced nfv as an alternative to ax-17. Pretty sure none of the others have more than a handful of direct uses.

Mario

[Norman Megill]

On Friday, July 28, 2017 at 6:41:56 PM UTC-4, Mario Carneiro wrote:

I'm okay with all this, although separating ax-9, ax-11 and especially ax-17 from these numbers will take some re-learning. (I've also referred to them by these names in various papers, which will now be obsolete. Not sure how much of a concern this is.)

Well, ax-9 and ax-11 could keep their names if we reordered axioms within their groups (Tarski and technical); they would each remain in the right group.  But right now the ordering for Tarski's schemes is the same as Tarski's, which is a nice but not essential thing to have, and that would no longer be case.

Alternately, no matter what ax-9 and ax-11 end up being, we could include a comment on the ax-9 and ax-11 descriptions referencing your paper and saying the name was changed, along with a link to the correct one.  I would probably prefer to do that so as to have control over the order that I want.

If you displayed the actual ax-9,11,17 in the paper, the reader should be able to figure it out the renaming if they look at the axiom list on the MPE home page.  I could also mention the renaming prominently on that page and others.

Do you have a list of what links you are depending on in your papers and presentations?

Most people will be unaffected by this change because it is not common for the axioms to be referenced directly in proofs.

It's good, then, that we introduced nfv as an alternative to ax-17. Pretty sure none of the others have more than a handful of direct uses.

Mario

I won't do the renaming right away, just the reorganization, so there will be time to discuss the best way to approach it.  The actual renaming is just running a simple script and can be done anytime.  (I will likely rename the obsolete axioms to match my 1995 paper since they don't affect anyone.)

 Norm