Improvement to the new structure pattern

[fl]

The new structure pattern used by Norm might be a bit improved in my
opinion.

Let's recall a topological group is a group where the addition and the
inverse function
are continuous and a topological ring is a ring where the addition,
the multiplication
and the inverse function are continuous.

Thus a topological ring should be considered as a ring or as a
topological
group.

But with the current structure it is not possible to do this since at
the third poisition in the
sequence you put the multiplication in the case of the ring or a
topology in the case
of the topological group.

I suggest instead of a sequence we use distinct "symbolic" constants.
For instance the constants base, add, mult, top.

Then one might write things like:

G = { <. base, ZZ >. , <. add , + >. } and G e. GrpNEW

T = { <. base, ZZ >. , <. add , + >. , <. top , ~P ZZ >. } and T e.
GrpTopNEW

R = { <. base, ZZ >. , <. add , + >. , <. mul , . >. } and R e.
RingNEW

U = { <. base, ZZ >. , <. add , + >. , <. mul , . >. , <. top , ~P ZZ
>. } and U e. RingTopNEW

and we would have the nice property that U e. RingNEW and U e.
GrpTopNEW

--
FL

[fl]

[Norman Megill]

On Nov 11, 6:12 am, fl <frederic.l...@laposte.net> wrote:
...

> I suggest instead of a sequence we use distinct "symbolic" constants.
> For instance the constants base, add, mult, top.

As I understand it, you are proposing to define base = 1,
add = 2, mult = 3, etc. - is that right?

Right now we are using "base" etc. to extract the components
rather than to specify them. This makes them uniform with
other symbols that specify defined operations,
so that the base is specified in a hypothesis as
"$e |- B = ( base ` R )". With your method, as I understand
it, we would instead say "$e |- B = ( R ` base )".

One issue is that the primitive operations of structures can
be different depending on how they are defined. For
example, a lattice can be defined with either a partial
order or with join, meet operations. In the first case,
join and meet would be defined; in the second case the
partial order would be defined. With the current method,
though, regardless of the definition we can say

$e |- L = ( le ` K )
$e |- J = ( join ` K )
$e |- M = ( meet ` K )

and if the definition is changed, theorems would not have to
be changed (only some early proofs from the new definition).

With your method, as I understand it, we would say

$e |- L = ( K ` le )
$e |- J = ( join ` K )
$e |- M = ( meet ` K )

in the first case and

$e |- L = ( le ` K )
$e |- J = ( K ` join )
$e |- M = ( K ` meet )

in the second. This seems a little confusing, and would
require all theorems to be changed if the definition was
changed in the future.

> Then one might write things like:
>
> G = { <. base, ZZ >. , <. add , + >. } and G e. GrpNEW
>
> T = { <. base, ZZ >. , <. add , + >. , <. top , ~P ZZ >. } and T e.
> GrpTopNEW
>
> R = { <. base, ZZ >. , <. add , + >. , <. mul , . >. } and R e.
> RingNEW
>
> U = { <. base, ZZ >. , <. add , + >. , <. mul , . >. , <. top , ~P ZZ
>
> >. } and U e. RingTopNEW
>
> and we would have the nice property that U e. RingNEW and U e.
> GrpTopNEW

I don't see how this is any different from the current
method except that you are using names base, add,... to
represent numbers 1, 2,... Perhaps I am misunderstanding.
Are you also proposing that df-struct be changed somehow?

Norm metamath.org

[Norman Megill]

On Nov 16, 8:39 am, fl <frederic.l...@laposte.net> wrote:
> X-No-Archive: yes

...

> > $e |- L = ( le ` K )
> > $e |- J = ( join ` K )
> > $e |- M = ( meet ` K )
>

> But that means that le, join and meet are overloaded, aren't they.

I don't know what you mean by overloaded. They aren't in the
usual sense; each has a single, specific definition. What is
it that you mean, and why is it a problem?

...

> But with the current method you couldn't say that
>
> |- ( U e. RingTopNew -> U e. RingNEW )
>
> and that
>
> |- ( U e. RingTopNew -> U e. GrpTopNEW )
>
> could you ?

You can't with your method either, unless you are proposing
a new definition of df-struct, which you haven't given.

Anyway, with the present definition this could be handled
(somewhat inelegantly) with a dummy operation in either
RingNEW or GrpTopNEW. A question is how often does this
problem occur in practice. Even if it does, this is only
an "issue" in the initial definition of the structure,
which goes away after the operations are abstracted out
for use with actual theorems later, as the ones in
my mathbox show. Almost nothing references the original
structure directly.

Norm

[fl]

> > But with the current method you couldn't say that
>
> > |- ( U e. RingTopNew -> U e. RingNEW )
>
> > and that
>
> > |- ( U e. RingTopNew -> U e. GrpTopNEW )
>
> > could you ?
>
> You can't with your method either, unless you are proposing
> a new definition of df-struct, which you haven't given.

Yes that's it we would have:

|- Struct(N, f, ph) = {f | (E.m e. N f Fn N /\ ph)}


With N a finite set. For instance { base, top, plus, mul }
for a topological ring or {base, plus, top} for a topological
group.

> Anyway, with the present definition this could be handled
> (somewhat inelegantly) with a dummy operation in either
> RingNEW or GrpTopNEW.

That's the probleme with the current definition you need
to add "holes".

> A question is how often does this
> problem occur in practice.

I don't know but it is frequent to add a topology over an
algebraic structure or to mix orders with algebraic
structures.

I remember that there was somebody that had begun to give
a collection of all the structures that he had found but I
can't rememeber whom and on which site.


Here it is. His name is Chapman:

http://math.chapman.edu/cgi-bin/structures

302 structures. Impressive. Geometries are missing. Things
such as grammars, automata, logics are missing,

> Even if it does, this is only
> an "issue" in the initial definition of the structure,
> which goes away after the operations are abstracted out
> for use with actual theorems later, as the ones in
> my mathbox show.  Almost nothing references the original
> structure directly.

Well I don't still understand the new definition very well. I had
understood that theorems such as:

|- ( U e. RingTopNew -> U e. RingNEW )

|- ( U e. RingTopNew -> U e. GrpTopNEW )

are those that you wanted when you decided to change the definition
of the structure. But Maybe I'm wrong.

--
FL

[fl]

> |- Struct(N, f, ph) = {f | (E.m e. N  f Fn N /\ ph)}

Well the quantifier is useless:

|- Struct(N, f, ph) = {f | (f Fn N /\ ph)}

--
FL

[fl]

> One issue is that the primitive operations of structures can
> be different depending on how they are defined.  For
> example, a lattice can be defined with either a partial
> order or with join, meet operations.  In the first case,
> join and meet would be defined; in the second case the
> partial order would be defined.  With the current method,
> though, regardless of the definition we can say
>
>    $e |- L = ( le ` K )
>    $e |- J = ( join ` K )
>    $e |- M = ( meet ` K )

Currently lattices are defined using posets.

http://us2.metamath.org:88/mpegif/df-lat.html

Could you give us the alternate definition with
the two operations meet and join so that I understand why
overloading is not used.

(Well I think I understand what you mean: one might replace
one definition by the other BUT not add both in the same file.)

--
FL

[fl]

> Here it is. His name is Chapman:

Hi name is Peter Jipsen. (Chapman is the name is the university.)

--
FL

[Norman Megill]

On Nov 16, 4:13 pm, fl <frederic.l...@laposte.net> wrote:

> Well I don't still understand the new definition very well. I had
> understood that theorems such as:
>
> |- ( U e. RingTopNew -> U e. RingNEW )
>
> |- ( U e. RingTopNew -> U e. GrpTopNEW )
>
> are those that you wanted when you decided to change the definition
> of the structure. But Maybe I'm wrong.

Yes, something like that is a goal.

When a series of successively more specialized structures
form a chain, the goal is accomplished: any member of a
more specialized structure is also a member of any more
general structure. For example, U e. Ring -> U e. Grp
(theorem ringgrpNEW).

Where there is branching back to two general
structures (i.e. not a chain) like in your example, the
existing definition does not accomplish that goal perfectly
without using a trick like a dummy operation to account for
the branching.


But with your definition,

> |- Struct(N, f, ph) = {f | (f Fn N /\ ph)}
>

> With N a finite set. For instance { base, top, plus, mul }
> for a topological ring or {base, plus, top} for a topological
> group.

each group would be a function on two members (a type of
ordered pair) and each ring would be a function on 3
members (ordered triple).

Thus, U e. Ring -> U e. Grp would be false with your
definition, since no ordered triple is an ordered pair.

...

> > $e |- L = ( le ` K )
> > $e |- J = ( join ` K )
> > $e |- M = ( meet ` K )
>
> Currently lattices are defined using posets.

Actually lattices and posets have the same structure, both
having a base set and an ordering operation. The meet and
join in the definition are not new operations but are
defined from the base set and ordering. Their appearance
in the lattice definition merely specializes the poset
definition further. If desired, the meet and join could be
eliminated by expanding them out into base set and
ordering.

A third structure member (orthocomplement) is first
introduced in orthoposets (df-oposet).

> http://us2.metamath.org:88/mpegif/df-lat.html
>
> Could you give us the alternate definition with
> the two operations meet and join so that I understand why
> overloading is not used.

I could, but it would take time to work it out.

> (Well I think I understand what you mean: one might replace
> one definition by the other BUT not add both in the same file.)

That's correct, we would not use them both in the same
file, so there is no overloading.

Norm

[fl]

> Thus, U e. Ring -> U e. Grp would be false with your
> definition, since no ordered triple is an ordered pair.

It is not fair from them I dare say.

--
FL

[Norman Megill]

The current Struct definition is

df-struct $a |- Struct ( N , f , ph ) = { f | ( E. m e. NN
( N <_ m /\ f Fn ( 1 ... m ) ) /\ ph ) } $.

This can be generalized to accomplish what you want:

df-structNEW $a |- StructNEW ( S , f , ph ) = { f | Fun f
/\ ( S C_ dom f /\ E. m e. NN dom f C_ ( 1 ... m ) )
/\ ph } $.

Essentially, the set S is an set of positive integers which
may have gaps in the numbering. You could of course assign
names to the integers if you want.

By setting S = ( 1 ... N ) i.e. a sequence of integers
without gaps, the current definition would be a special
case of this:

Struct ( N , f , ph ) = StructNEW ( ( 1 ... N ) , f , ph )

I haven't looked at the impact of StructNEW on the
subsequent theorems involving Struct and StrBldr, or how
StrBldr might have to be redefined. (Do "MM> search *
Struct/j" and "sea * StrBldr/j" to see them.) I fear some
of the "nice" theorems such as eustrdif, used to help out
the StrBldr, may become awkward. Perhaps you would want to
look at how StructNEW would affect those theorems.

The StrBldr is useful for specifying structures
symbolically (rather than numbers) using (my) "base",
"+g", etc. component extractors as in cnaddablNEW. We can
alternately specify structures as e.g.

"{ <. 1 , CC >. , < 2 , + >. }"

Or we could use

"{ <. base-index , CC >. , < +g-index , + >. }"

as you propose, but this requires _two_ sets of constant
symbols, the "base" and "+g" functions to extract the
structure components (used in hypotheses of most theorems)
and "base-index" and "+g-index" to represent the structure
entry integer indexes 1 and 2. If possible, I think it
would be nicer to have only one set of new symbols.

Norm

[Norman Megill]

I wrote:
> Or we could use
>
> "{ <. base-index , CC >. , < +g-index , + >. }"
>
> as you propose, but this requires _two_ sets of constant
> symbols, the "base" and "+g" functions to extract the
> structure components (used in hypotheses of most theorems)
> and "base-index" and "+g-index" to represent the structure
> entry integer indexes 1 and 2. If possible, I think it
> would be nicer to have only one set of new symbols.

To avoid two sets of symbols, notice that

( base ` ( _I |` NN ) ) = 1
( +g ` ( _I |` NN ) ) = 2

etc. We can define a single new symbol

ndx = ( _I |` NN )

Then the above becomes

"{ <. ( base ` ndx ) , CC >. , < ( +g ` ndx ) , + >. }"

so that maybe we can get by without StrBldr and without
having to have two sets of symbols, while maintaining
the goal of independence from the structure details
that could change in the future. (An example of such
a change would be to use finite ordinals instead of NN,
in order to more clearly see what ZF axioms are
actually needed. Or we might re-order the indices for
better compatibility with related structures.) And we
would have automatic compatibility with a different
definition such as StructNEW.

Norm