Definition of the universal class

[Benoit]

I propose below to redefine the universal class to be { x | T. } instead of the current { x | x = x }. The proposed definition is more economical, it has a shorter justification (see below vjust-ALT versus vjust), and it emphasizes the fact that the Boolean algebra of classes mirrors the Boolean algebra of formulas. Similarly for the empty class (set), one can define (/) = { x | F. } (not written below). Or if one whishes to keep the definition (/) = V \ V, then one can add the theorems -. ph => (/) = { x | ph } and ph => |- (/) = { x | -. ph } and (/) = { x | F. }. What do you think?

$( Proposal of redefinition of _V. Here, I define _V-ALT and prove from this definition the definition of _V. $)
$( The definition of -V-ALT does not use dummy variables and emphasizes the fact that
the Boolean algebra of classes "mirrors" the Boolean algebra of formulas.
$)

$c _V-ALT $.

cvv-ALT $a class _V-ALT $.

${
  $( Justification of df-v-ALT. $)
  $d z x $.  $d z y $.
  vjust-ALT $p |- { x | T. } = { y | T. } $= ( vz wtru cab wsb cv wcel trusb 2th df-clab 3bitr4i eqriv ) CDAEZDBEZDACFZDBCFZCGZNHROHPQACIBCIJDCAKDCBKLM $.
$}

$( compare:
vjust-ALT: ( vz wtru cab wsb cv wcel trusb 2th df-clab 3bitr4i eqriv ) CDAEZDBEZDACFZDBCFZCGZNHROHPQACIBCIJDCAKDCBKLM $.
vjst     : ( vz cv wceq cab wsb wcel equid sbt 2th df-clab 3bitr4i eqriv ) CADZOEZAFZBDZREZBFZPACGZSBCGZCDZQHUCTHUAUBPACAIJSBCBIJKPCALSCBLMN $.
$)

df-v-ALT $a |- _V-ALT = { x | T. } $.

${
  $( Any true wff determines the universal class. $)
  vtr.1 $e |- ph $.
  vtr   $p |- _V-ALT = { x | ph } $= ( cvv-ALT wtru cab df-v-ALT tru 2th abbii eqtri ) DEBFABFBGEABEAHCIJK $.
$}

$( An alternate definition of the universal class. $)
vtru $p |- _V-ALT = { x | x = x } $= ( weq equid vtr ) AABAACD $.

$( Prove vex from the proposed definition df-V-ALT. $)
vex-ALT $p |- x e. _V-ALT $= ( cv cvv-ALT wcel wtru tru df-v-ALT abeq2i mpbir ) ABCDEFEACAGHI $.

$( compare:
vex-ALT: ( cv cvv-ALT wcel wtru tru  df-v-ALT abeq2i mpbir ) ABCDEFEACAGHI $.
vex    : ( cv cvv     wcel wceq eqid df-v     abeq2i mpbir ) ABZCDJJEZJFKACAGHI $.
(same proofs with tru in place of eqid (which could be equid, by the way)
$)

[Mario Carneiro]

I don't see any issue with this. I believe that the usage of { x | x = x } is historical, because T. was defined later than the rest of prop & pred calc. The definition of T. is somewhat suspect in some logics, while using x = x (where x is an available free variable) is a perfectly sensible, so that may be a reason to use it. I think the definition of (/) = ( _V \ _V ) is to minimize the number of dummy variables in the definitions (because these don't require justification like df-v). Of course, we quickly stop justifying dummy variables after df-v (the df-v justification theorem should really be viewed as a schema for how to justify dummies in general), and mmj2 implements a general mechanism for checking such definitions anyway, so it's not essential, but it's still a bit easier to work with expressions that don't require introducing new bound variables.

Mario

--
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.

[Norman Megill]

The current definitions are the ones used in the literature, as referenced in their comments, and I don't recall ever seeing {x | T.} or {x | F.}.

The "T." and "F." constants are not ordinarily used by mathematicians, only by some logicians and maybe computer scientists.  Takeuti and Zaring, and most other set theory books I think, do not use these symbols.  They were added quite late to set.mm.

So I would vote against changing the definitions, so that we keep as close to the literature as possible, which was one of my goals with the early set theory in particular.

Norm

[Benoit]

Ok, I understand the argument of keeping close to the literature, and I have never seen { x | T. } me neither.

The following are just some explanations, but I'm fine with the current situation with no change.

To me, the traditional definition { x | x = x } came to be because one was looking for a formula "as true as possible", and "x = x" was obviously a good candidate. But "T." is precisely defined to be "the" true formula. Imagine that one specific x0 was not equal to isfelf (as in http://us.metamath.org/award2003.html#16), then it would be necessary to use T. This is just paraphrasing what I wrote above about the Boolean algebras of classes and of formulas, namely, (or, and, F, T, not) <-> (union, intersection, empty class, universal class, complement): the present case is about the greatest element.

And to reply to Mario, I think the people suspicious about T. are litteraly scared by "x = x" ! It suffices to look at the respective positions in set.mm of tru (1312, in prop calc, and actually intuitionistic) and eqid (1645, in "non-pure" predicate calculus). As for the empty class, I saw the dummy-variable issue, and that's why I proposed to simply add a theorem that (/) = { x | F }.

--
Benoit

[Norman Megill]

Mario is correct that df-nul was chosen to eliminate the dummy variable.  I haven't seen it defined this way in the literature, but as least it appears as an exercise, which I considered acceptable.  Another example is df-ss and dfss2.  In both cases I was somewhat torn about not matching the textbook definition page, but in the end not having the dummy variable won out.

What I suggest you do is to add theorems dfv2 and dfnul4 to your mathbox for now.  If these theorems result in shortening of any existing proofs, that would be more motivation to make them official.

Norm

[Ken Kubota]

Hi Norman,

This is not fully correct.

"T" and "F" are definitely used by mathematicians, see for example,

as a prominent case, [Andrews 2002 (ISBN 1-4020-0763-9), p. 212].

These definitions are also available online at

https://plato.stanford.edu/entries/type-theory-church/#ForBasEqu

Moreover, I used his definitions from Q0 (with a minor modification) in R0, see p. 359 at

http://www.owlofminerva.net/files/formulae.pdf

The definition of the universal class as suggested by Benoit is actually used

in R0, expressed in lambda notation as [ λx . T ], see the definition of

the universal set on p. 361.

The same holds for the definition of the empty class (set), cf. ibid.: [ λx . F ].

Note that omega denotes the universal type, hence all mathematical

objects (entities) are member of the universal set.

Ken

____________________________________________________

Ken Kubota

http://doi.org/10.4444/100

[Norman Megill]

Type theory is a kind of logic, with applications in computer science, so that would fall in the category of logicians and computer scientists that I mentioned.

What I meant was that it is not often used in other areas of mathematics.  I don't recall seeing T and F defined in any book on set theory, calculus, topology, algebra, or functional analysis, for example.

Norm

[Marnix Klooster]

Hi Norm,

It may not be commonplace, but this discrete math textbook has 'true' and 'false' and uses them regularly: Gries, Schneider, "A Logical Approach to Discrete Math".

http://www.springer.com/gp/book/9780387941158

See also the pictures from some lecture notes used with this book (or something closely related): https://math.stackexchange.com/q/751922/11994

Just a data point I wanted to throw out...

-Marnix

--
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+u...@googlegroups.com.