How to express a quadratic form over a vector space

[Mingli Yuan]

Hi, folks,

I am a newbie and I have a question about expressing a quadratic form over a vector space.

Just follow cases in set.mm, I give below definition of a quadratic form

```metamath
$( 

=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
Quadratic Form
=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=

A quadratic form over a field K is
a map q: V -> K from a finite-dimensional K-vector space to K
such that q(av) = a^2 q(v) for all a \in K, v \in V.

$)

$c QFrm $.

$( Extend class notation with class of all quadratic forms. $)
cqfrm $a class QFrm $.

df-qfrm $a |- QFrm = { V --> ( Scalar ` V ) | V e. LVec /\
q e. V --> ( Scalar ` V ) /\ v e. V /\ a e. ( Scalar ` V ) /\
q ` ( a .x. v ) = ( a * a ) .x. v }
$.

```

But I found it is difficult to express special quadratic forms over R^3

In Haskell or similar languages which support algebraic data types, we can define

```haskell
data Tree a = Tip | Node (Tree a) a (Tree a)
```

Here a is a type parameter.

So my questions are:

(1) Is the definition of Quadratic Form correct?

(2) How can we express something like a type with parameter and the initialization of a type with parameter.

Thanks a lot.

Mingli

[Alexander van der Vekens]

Hi Mingli,

welcome to the Metamath community!

You started with an interesting topic, and I hope I can assist you with your "project".

Here is a definition that would be valid (checked nby the metamath verifier) and hopefully fullfils your expectations:

  ${
    $d a q v $.
    $( The definition of a "quadratic form".  (Contributed by ...,
       5-Feb-2022.) $)
    df-qfrm $a |- QFrm = { q e. ( ( Base ` ( Scalar ` V ) ) ^m ( Base ` V ) ) |
                A. v e. ( Base ` V ) A. a e. ( Base ` ( Scalar ` V ) )
                ( q ` ( a ( .s ` V ) v ) ) = ( ( a ( .r ` ( Scalar ` V ) ) a ) ( .s ` V ) ( q ` v ) ) } $.
  $}

I also proved some basic theorems for this definition:

  ${
    isqfrm.b $e |- B = ( Base ` V ) $.
    isqfrm.m $e |- .x. = ( .s ` V ) $.
    isqfrm.s $e |- S = ( Scalar ` V ) $.
    isqfrm.k $e |- K = ( Base ` S ) $.
    isqfrm.t $e |- .X. = ( .r ` S ) $.
    $( The predicate "is a quadratic form".  (Contributed by ...,
       5-Feb-2022.) $)
    isqfrm $p |- ( Q e. QFrm <-> ( Q e. ( K ^m B ) /\ A. v e. B A. a e. K
                    ( Q ` ( a .x. v ) ) = ( ( a .X. a ) .x. ( Q ` v ) ) ) ) $=
     ? $.

    $( A quadratic form is a function from a class ` B ` (usually the base set
       of a vector space) to the base set ` K ` of its scalars ` S ` (usually a
       field).  (Contributed by ..., 5-Feb-2022.) $)
    qfrmf $p |- ( Q e. QFrm -> Q : B --> K ) $=
      ?$.

    $( The property of a quadratic form as a function from a class ` V `
       (usually a vector space) to its scalars ` S ` (usually a field).
       (Contributed by ..., 5-Feb-2022.) $)
    qfrmprop $p |- ( ( Q e. QFrm /\ X e. B /\ A e. K )
                    -> ( Q ` ( A .x. X ) ) = ( ( A .X. A ) .x. ( Q ` X ) ) ) $=
      ? $.
  $}

Maybe you want to prove them by yourself as an exercise...

Here some remarks you should consider:

* The definition does not require V to be a vector space. It can also be a left module or anything else having scalars. If it is important that V is a vector space for a specific theorem, it must be provided as antecedent, e.g., ( ( V e. LVec /\ Q e. QFrm ) -> ...)

* In set.mm, we distingush between groups, rings, fields, etc. (as tuples of a base set and several operations, represented by "extensible structures") and the set of their elements (the base set). Example: if Q = ( B , + , * ) is the field of the rational numbers, then B is the set of the rational numbers. QFrm should be a function mapping the elements of a structure V (e.g., the vectors of a vector space)  to the elements of the scalar structure, therefore we use

the notation `( Base ``V )` resp.  `( Base `` S )` for the domain and the codomain of QFrm.

* In a definition, we usually have to use all required construct explicitly (that's why it looks so complicated), whereas in theorems we can use class variables to abbreviate complex constructs, e.g., K = ( Base ` S )= ( Base `  ( Scalar ` V ) ) as the base set of the scalar (field) S of (the vector space) V. Theorem ~isqfrm is a direct translation of the definition, using such class variables. As you can see, this is much better to comprehend. In practice, the definition itself would mostly be used in such basic theorems only, and the basic theorems would be used in the following.

If you have further questions, don't hesitate to ask then in this forum. Maybe others can share their experiences and opinions here, too.

By the way, in Wikipedia I read "A quadratic form over a field  K is a map q : V -> K from a finite-dimensional K-vector space to K such that q(av) = (a^2)q(v) for all a in K, v in V and the function q(u+v)-q(u)-q(v) is bilinear." Is the first condition really sufficient for your purposes, or do you need the bilinearity, too?

Regarding your second question: maybe someone else has an answer for it.

Alexander

[vvs]

Hi Mingli,

(2) How can we express something like a type with parameter and the initialization of a type with parameter.

I'm not an expert, so don't take my word for it. But let me guess. Haskell is based on simple type theory while set.mm is ZFC, i.e. set theory. They are different beasts. You can embed type theory, of course, but that would not be set.mm anymore, IMHO.

But maybe some real expert will say that I'm telling nonsensicality and this should be easy to do :) 

[Mingli Yuan]

Thanks, Alex and vvs

Quadratic form is widely used, but looks like it is still missing in metamath.

I guess I need the bilinear condition but I'm not sure about it. In fact, following paper[1], I am trying to solve Pascal's Hexagon theorem.

If not wrong, I did not see too many obstacles for the formalization of the simple proof.

The next step is to introduce homogeneous coordinates which connect conic sections in 2d with quadratic form in 3d.

And then by some algebraic property of cross product in 3d space to prove the theorem.

(we still do not have cross product in 3d?)

Maybe difficult for a newbie to solve, at least it is a good chance for exercises.

So far the learning curve is a little bit steep because a lot of conventions are not documented?

But the community is very nice, which reminds me of Norm.

[1]: A very simple proof of Pascal’s hexagon theorem and some applications by Nedeljko Stefanovic and Milos Milosevic

--
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.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/4bef40e5-3ab7-402d-850c-e08aaeb0edcan%40googlegroups.com.

[Mario Carneiro]

On Sat, Feb 5, 2022 at 6:10 PM vvs <vvs...@gmail.com> wrote:

Hi Mingli,

(2) How can we express something like a type with parameter and the initialization of a type with parameter.

I'm not an expert, so don't take my word for it. But let me guess. Haskell is based on simple type theory while set.mm is ZFC, i.e. set theory. They are different beasts. You can embed type theory, of course, but that would not be set.mm anymore, IMHO.

But maybe some real expert will say that I'm telling nonsensicality and this should be easy to do :) 

That's nonsense, this should be easy to do. :) The equivalent of a type with a parameter in set.mm is a function from sets to sets. You use function application to represent the application of the type function to some particular type.

This has already appeared in this thread: in AV's code you have ( QFrm ` V ) as the type of all quadratic forms over V. Or rather it should read that: there appears to be an error in the code, and the code as written would have tripped the definition checker. Here's a revised version (still not checked though):

${
    $d a q v $.
    $( The definition of a "quadratic form".  (Contributed by ...,
       5-Feb-2022.) $)

    df-qfrm $a |- QFrm = ( w e. _V |-> { q e. ( ( Base ` ( Scalar ` w ) ) ^m ( Base ` w ) ) |
                A. v e. ( Base ` w ) A. a e. ( Base ` ( Scalar ` w ) )
                ( q ` ( a ( .s ` w ) v ) ) = ( ( a ( .r ` ( Scalar ` w ) ) a ) ( .s ` w ) ( q ` v ) ) } ) $.
  $}

  ${
    isqfrm.b $e |- B = ( Base ` V ) $.
    isqfrm.m $e |- .x. = ( .s ` V ) $.
    isqfrm.s $e |- S = ( Scalar ` V ) $.
    isqfrm.k $e |- K = ( Base ` S ) $.
    isqfrm.t $e |- .X. = ( .r ` S ) $.
    $( The predicate "is a quadratic form".  (Contributed by ...,
       5-Feb-2022.) $)

    isqfrm $p |- ( Q e. ( QFrm ` V ) <-> ( Q e. ( K ^m B ) /\ A. v e. B A. a e. K

                    ( Q ` ( a .x. v ) ) = ( ( a .X. a ) .x. ( Q ` v ) ) ) ) $=
     ? $.

    $( A quadratic form is a function from a class ` B ` (usually the base set
       of a vector space) to the base set ` K ` of its scalars ` S ` (usually a
       field).  (Contributed by ..., 5-Feb-2022.) $)

    qfrmf $p |- ( Q e. ( QFrm ` V ) -> Q : B --> K ) $=

      ?$.

    $( The property of a quadratic form as a function from a class ` V `
       (usually a vector space) to its scalars ` S ` (usually a field).
       (Contributed by ..., 5-Feb-2022.) $)

    qfrmprop $p |- ( ( Q e. ( QFrm ` V ) /\ X e. B /\ A e. K )

                    -> ( Q ` ( A .x. X ) ) = ( ( A .X. A ) .x. ( Q ` X ) ) ) $=
      ? $.

  $}


Sometimes, when it is important for the input to be a proper class, type level functions can also be written as term constructors from class to class instead. For example, the equivalent of Haskell's [a] type, the type of lists (let's ignore the infinite ones), is "Word A" in set.mm. An element of Word A is a finite list of elements drawn from A.

 

There is no particularly convenient way to define inductive datatypes in metamath as in Haskell, but it is possible to define a type of trees or other such things via a fixpoint construction. We should probably have a simpler mechanism for this.

[Alexander van der Vekens]

On Sunday, February 6, 2022 at 7:39:19 AM UTC+1 di....@gmail.com wrote:

...

This has already appeared in this thread: in AV's code you have ( QFrm ` V ) as the type of all quadratic forms over V. Or rather it should read that: there appears to be an error in the code, and the code as written would have tripped the definition checker. Here's a revised version (still not checked though):

Sorry for my mistake, and many thanks to Mario who detected it. It was a little late last night, and I only used metamath.exe to check the definition and the theorems, and not mmj2 which would have detected the mistake by its soundness checks. Of course, the class/vector space V should not be used directly in the definition, but should be made variable by defining QFrm as funktion mapping a set/vector space V to the set of the quadratic forms over this set/vector space.

I'll revise my definition and theorems according to Mario's suggestion (at least the distinct variable conditions must be adjusted, and some subtleties with V being a proper class must be considered) in the near future.

[Thierry Arnoux]

Hi Mingli,

Let me try to add up to / complete the other answers, starting from your own definition.

You write:

```metamath

df-qfrm $a |- QFrm = { V --> ( Scalar ` V ) | V e. LVec /\
q e. V --> ( Scalar ` V ) /\ v e. V /\ a e. ( Scalar ` V ) /\
q ` ( a .x. v ) = ( a * a ) .x. v }
$.

```

So your `QFrm` is in the form ` { A --> B | ph } `. Unfortunately, this syntax has not been defined in set.mm. A definition for a "class of something" has to take one of the following forms:

```metamath

cab $a class { x | ph } $.
crab $a class { x e. A | ph } $.
copab $a class { <. x , y >. | ph } $.
coprab $a class { <. <. x , y >. , z >. | ph } $.
```

The first two forms define "the set of `x` in `A` fulfilling `ph`", the third defines a relation (like '<'), the last also defines a relation, but with three elements.

Here, you want to define a set of mappings, so the second form is what we need. Something like ` QFrm = { q e. M | ph(q) } `, where `q e. M` would express "q is a mapping", and `ph(q)` would express "q is quadratic".

For "q e. M" to express "q is a mapping", we have ~df-map, and the operation `^m`: the set of all functions that map from ` B ` to ` A ` is written ` ( A ^m B ) `.

Here we want mappings from the base of a field V to the scalars of that field, so we have to write ` ( Base ` ( Scalar ` V ) ) ^m ( Base ` V ) `. Alexander has explained why we need to use the ` Base ` here.

Now, a quadratic form always relates to a specific vector space. Above, we have not defined what ` V ` is, and so our definition is not a closed form.

There are two ways around this: either we define ` QFrm ` as the set of all quadratic forms, regardless of the underlying vector space, or we first fix a specific vector space, and then define the class of quadratic forms over that specific vector space. I think the latter is usually better, and what you try to achieve. So here what we want is a function, mapping one vector space ` w ` to the class of quadratic forms over ` w `, ` ( QFrm ` w ) `. Later on, we will be able to state "` Q ` is a quadratic form over V" by writing `Q e. ( QFrm ` V )`.

We can use the "maps to" notation here: ` ( w e. Field |-> F(w) ) ` stands for "the function which maps the field `w` to `F(w)`.

Putting it together, this gives:

```metamath
df-qfrm $a |- QFrm = ( w e. Field |-> { q e. ( Base ` ( Scalar ` w ) ) ^m ( Base ` w ) | ph } ) $.

```

Of course I've still omitted `ph` here, which corresponds to your:

```metamath

v e. V /\ a e. ( Scalar ` V ) /\ q ` ( a .x. v ) = ( a * a ) .x. v

```

We have not introduced `v` and `a` yet though. Those are respectively any vector and any scalar, so we shall use "for all": ` A. a e. ( Base ` ( Scalar ` w ) ) A. v e. ( Base ` w ) ps `

Finally, ` .x. ` is just another class variable, like ` A `. In the theorems which make use of it, like ~ drngmcl, there is a hypothesis to give it a value. In your definition, we cannot use such a trick, so we have to use everything verbatim. The scalar multiplication operation of ` w ` is ` ( .s ` w ) `, so instead of ` ( a .x. v ) ` one has to write ` ( a ( .s ` w ) v ) `. This gives:

```metamath

( q ` ( a ( .s ` w ) v ) ) = ( ( a ( .r ` ( Scalar ` w ) ) a ) ( .s ` w ) ( q ` v ) )

```

It also looks like we need to express the fact that ` q(u+v) - q(u) - q(v) ` is bilinear. It is a mapping function of two variables `u` and `v`, so we can express it using ~ cmpt2:

```metamath
cmpt2 $a class ( x e. A , y e. B |-> C ) $.

```
Let's assume we have a similar definition for Bilinear Forms, `BFrm`. A statement "` Q ` is a bilinear form over ` w `" is expressed ` Q e. ( BFrm ` w ) `. This gives:

```metamath
( u e. ( Base ` w ) , v e. ( Base ` w ) |-> ( q ` ( u ( +g ` w ) v ) ( -g ` ( Scalar ` w ) ) ( ( q ` u ) ( +g ` ( Scalar ` w ) ) ( q ` v ) ) ) ) e. ( BFrm ` w )

```

Let's put everything together once again:

```metamath

${
    $d a q v w $.

    $( The definition of a "quadratic form".  (Contributed by ...,
       5-Feb-2022.) $)

    df-qfrm $a |- QFrm = ( w e. Field |-> { q e. ( ( Base ` ( Scalar ` w ) ) ^m ( Base ` w ) ) | (

                A. v e. ( Base ` w ) A. a e. ( Base ` ( Scalar ` w ) ) ( q ` ( a ( .s ` w ) v ) ) = ( ( a ( .r ` ( Scalar ` w ) ) a ) ( .s ` w ) ( q ` v ) )

                /\ ( u e. ( Base ` w ) , v e. ( Base ` w ) |-> ( q ` ( u ( +g ` w ) v ) ( -g ` ( Scalar ` w ) ) ( ( q ` u ) ( +g ` ( Scalar ` w ) ) ( q ` v ) ) ) ) e. ( BFrm ` w )
      ) } ) $.
$}

```

That shall be exactly Mario's answer, with the addition of the "bilinear form" part. That's quite complex, but the next theorems are going to be simpler... and Metamath forces us with some formalism (which is good!).

Actually, there is one little difference with Mario's definition. I've written ` ( w e. Field |-> ... ) `, but we usually prefer ` ( w e. _V |-> ... ) `. By using the universal class ` _V `, we do not force ` w ` to be a field, this allows us to be as general as possible, and define "what a quadratic form would be if ` w ` was a vector space".

In practice, as explained by Alexander, as soon as we will need any specific field or vector space property (say, distributivity), this will have to appear as a hypothesis, like ` ( W e. Field -> ... ) ` or ` ( W e. LVec -> ... `.

Of course, `BFrm`, the function mapping a field to the set of its bilinear forms, will need to be defined first: this is left as an exercise! ;-)

BR,

_
Thierry

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

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAGDRuAg4F%3Deb2qSTLBsXwX7yz05W7b6PBR%2BX%2B2Q-zCBB7E6RbA%40mail.gmail.com.

[Alexander van der Vekens]

Here is, as promised, the corrected theorem and related basic theorems, checked by metamath.exe as well as mmj2. Theorem qfrm  was added, which charaterizes the set of quadratic forms over a set/vector space V. See the remarks in its comment about the necessity of V to be a set. Of course, the bilinearity has to be added, as described by Thierry.

  ${
    $d a q v w $.
    $( The definition of a "quadratic form".  (Contributed by ...,
       5-Feb-2022.) $)

    df-qfrm $a |- QFrm = ( w e. _V

        |-> { q e. ( ( Base ` ( Scalar ` w ) ) ^m ( Base ` w ) ) |

              A. v e. ( Base ` w ) A. a e. ( Base ` ( Scalar ` w ) )
              ( q ` ( a ( .s ` w ) v ) )

              = ( ( a ( .r ` ( Scalar ` w ) ) a ) ( .s ` w ) ( q ` v ) ) } ) $.
  $}

  ${
    $d B q w $.  $d K q w $.  $d U w $.  $d V a q v w $.  $d .x. w $.
    $d .X. w $.

    qfrm.b $e |- B = ( Base ` V ) $.

    qfrm.m $e |- .x. = ( .s ` V ) $.

    qfrm.s $e |- S = ( Scalar ` V ) $.

    qfrm.k $e |- K = ( Base ` S ) $.

    qfrm.t $e |- .X. = ( .r ` S ) $.

    $( The set of quadratic forms over a set ` V `.  The assumption that ` V `
       must be a set (` V e. U `) is necessary, because if ` V ` was a proper
       class (` V e/ _V `) , then ` ( QFrm `` V ) = (/) ` (see ~ fvprc ), but
       the right hand side of the equation would be ` { (/) } =/= (/) `
       (see ~ mapdm0 and ~ ral0 ).  Usually, ` V ` will be a vector space
       (` U = LVec `, i.e. ` V e. LVec `).  (Contributed by ...,
       5-Feb-2022.) $)
    qfrm $p |- ( V e. U -> ( QFrm ` V ) = { q e. ( K ^m B ) |

                     A. v e. B A. a e. K

                     ( q ` ( a .x. v ) ) = ( ( a .X. a ) .x. ( q ` v ) ) } ) $=
      ? $.

    $d Q a q v $.  $d .x. q $.  $d .X. q $.
    $( The predicate "is a quadratic form".  (Contributed by ...,
       5-Feb-2022.) $)
    isqfrm $p |- ( V e. U -> ( Q e. ( QFrm ` V ) <-> ( Q e. ( K ^m B )

                /\ A. v e. B A. a e. K

                   ( Q ` ( a .x. v ) ) = ( ( a .X. a ) .x. ( Q ` v ) ) ) ) ) $=

     ? $.

    $( A quadratic form is a function from a class ` B ` (usually the base set
       of a vector space) to the base set ` K ` of its scalars ` S ` (usually a
       field).  (Contributed by ..., 5-Feb-2022.) $)
    qfrmf $p |- ( Q e. ( QFrm ` V ) -> Q : B --> K ) $=
      ? $.

   $d A a $.  $d B v $.  $d K a v $.  $d Q a v $.  $d X a v $.
   $d .x. a v $.  $d .X. a v $.

    $( The property of a quadratic form as a function from a class ` V `
       (usually a vector space) to its scalars ` S ` (usually a field).

       (Contributed by ..., 5-Feb-2022.) $)

[vvs]

That's nonsense, this should be easy to do. :) The equivalent of a type with a parameter in set.mm is a function from sets to sets. You use function application to represent the application of the type function to some particular type.

Very well, then.

Also, maybe I was looking in the wrong direction and this isn't relevant here, but function is still just an approximation and it is not a type, right? I mean, in case where you really want it to be different from set? Then it would be not enough to just define a function and you will need several theorems to prove that. And if you will use it too often then it might become annoying.

[Thierry Arnoux]

Hi Mingli,

It's very good that you have a paper to follow, and very good that you set yourself as a target to prove another of the "100 theorems"! Good luck, and don't hesitate to shout for help whenever you feel blocked, I'm sure you'll find many willing to help!

The title of the paper is "A very simple proof", but not everything is as simple as it claims ;-)

Very very quickly surveying what you might need:

It seems you're right that we do not have the 3D cross product in Metamath yet. That's probably a very good addition! (and absolutely necessary for that proof)

To express the Euclidean space in 3 dimensions, you can use ` ( EEhil ` 3 )` . It is defined as ` ( RR^ ( 1 ... 3 ) ) `, and that's a structure which is also a vector space. Then, for example, the set of quadratic forms over RR^3 will be ` ( QFrm ` ( EEhil ` 3 ) ) ` (once you've defined it!).

We already have quite some matrix algebra, defined by Stefan O'Rear and Alexander Van der Vekens.

Alexander has already introduced the concept of "linear dependency" as `linDepS` (see ~df-lindeps).

Norm has a whole chapter about projective geometry, but unfortunately I don't understand it, I can't tell whether it could be useful.

I hope this helps somehow!

BR,
_
Thierry

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAGDRuAhT3ZADrOrPF3%3D9nVv3SZCVj8ZVh5_Rv%3D%2BRZMErfqvHYQ%40mail.gmail.com.

[Mario Carneiro]

There isn't really any essential way that a type is different from a set, except that a type abstracts some encoding details that sets instantiate in a particular way. That means that if you have a type you want to model then sets are a way to do it, maybe not the only way. Of course the function giving the type family is only the beginning of the story: in haskell an inductive data type comes with constructors and pattern matching, and that corresponds to functions and a recursion principle in metamath.

[vvs]

There isn't really any essential way that a type is different from a set, except that a type abstracts some encoding details that sets instantiate in a particular way. That means that if you have a type you want to model then sets are a way to do it, maybe not the only way. Of course the function giving the type family is only the beginning of the story: in haskell an inductive data type comes with constructors and pattern matching, and that corresponds to functions and a recursion principle in metamath.

I'm thinking more about elements that may belong to many sets, while they can have only one type. Isn't that the main reason why type theory was invented in the first place? Yes, it's possible to use set theory with particular axioms like ZFC, but trying to model type theory inside it kinda defeats the purpose. Why not implement type theory in Metamath then?

[Mario Carneiro]

On Sun, Feb 6, 2022 at 11:11 AM vvs <vvs...@gmail.com> wrote:

There isn't really any essential way that a type is different from a set, except that a type abstracts some encoding details that sets instantiate in a particular way. That means that if you have a type you want to model then sets are a way to do it, maybe not the only way. Of course the function giving the type family is only the beginning of the story: in haskell an inductive data type comes with constructors and pattern matching, and that corresponds to functions and a recursion principle in metamath.

I'm thinking more about elements that may belong to many sets, while they can have only one type. Isn't that the main reason why type theory was invented in the first place? Yes, it's possible to use set theory with particular axioms like ZFC, but trying to model type theory inside it kinda defeats the purpose. Why not implement type theory in Metamath then?

Two things: (1) it's been done, see hol.mm or dtt.mm. (2) It's not necessary; type theory can be simulated in set.mm without straying very far from idiomatic style, and without a lot of overhead, so it amounts to a particular way of handling propositions in ZFC. I don't see why you are so eager to say "types are not quite sets" and therefore you may as well throw away the library and get another one if you want to use type-based reasoning. Type theory thinking can still be useful without the trappings of type theory itself, and in fact type theory simulated in set theory has some advantages over pure type theory in that you can bend the rules when it is advantageous to do so. In lean, there is a concept called "defeq", or definitional equality, and it is strictly stronger than regular equality: there are things that are propositionally equal but not defeq, like x + (y + z) and (x + y) + z. You can prove these two are equal, but if you have a type family indexed in natural numbers and an element in F ((x + y) + z) you can't just treat it as an element of F (x + (y + z)). In metamath you can; since the values are equal the sets are equal so any element of one is also an element of the other. Defeq is simply not a thing in metamath, and this is very freeing.

[Jim Kingdon]

On 2/6/22 11:47, Mario Carneiro wrote:

Two things: (1) it's been done, see hol.mm or dtt.mm.

At least in my email cilent these got linked funny. The references are to http://us.metamath.org/holuni/mmhol.html and https://github.com/digama0/dtt.mm respectively, as far as I know. Hope that helps people follow along in case anyone is unfamiliar.

[vvs]

I don't see why you are so eager to say "types are not quite sets"

I am not, I think. I don't really care. I'm trying to avoid being biased but fall in that trap over and over again.

But I know that such people exist and I don't know why someone should insist that they are wrong just because somebody else have a different opinion. This is also a philosophical difference, not just a practical one. But even from a practical point of view everyone have their own definition of feasibility. We can walk backwards or even upside down, that's certainly possible, but not everyone will find this quite feasible. And when I'm not sure what solution is feasible in this particular case, I prefer to reason conservatively. But maybe I'm overreacting sometimes.

 

Type theory thinking can still be useful without the trappings of type theory itself, and in fact type theory simulated in set theory has some advantages over pure type theory in that you can bend the rules when it is advantageous to do so.

And not everyone will like it. Should we say that there is only one single truth?

 

In lean, there is a concept called "defeq", or definitional equality, and it is strictly stronger than regular equality: there are things that are propositionally equal but not defeq, like x + (y + z) and (x + y) + z. You can prove these two are equal, but if you have a type family indexed in natural numbers and an element in F ((x + y) + z) you can't just treat it as an element of F (x + (y + z)). In metamath you can; since the values are equal the sets are equal so any element of one is also an element of the other. Defeq is simply not a thing in metamath, and this is very freeing.

Ok. But this is starting to sound like a preaching :) And don't take me wrong. If you feel so strongly about this issue I won't continue to try to dissuade you. Probably this discussion already turned into bikeshedding and I should stop arguing and do something useful instead :) I'm sorry.

[Mingli Yuan]

Thanks, Thierry,  Mario and Alex, I will follow your advice, and take the exercise. :-)

The community is so friendly! I will ask if I am blocked.

Mingli

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

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/14ce5c0a-44e9-4ee8-b6be-ac2d67848ac8n%40googlegroups.com.

[Benoit]

Sorry, I'm a bit late to the party.  As has been noted, you also need bilinearity of the associated symmetric form. Without it, you are simply defining homogeneous functions of degree two.

Also, quadratic forms should be defined in set.mm on (left) modules for wider applicability (even if some results might be funny over noncommutative rings).

As for the first point, the associated symmetric form is probably important enough that a definition would be useful.  Here is a proposal (I do not remember the names of the components of an extensible structure, so I put mnemonic ones):

$( Define the function associating with a function ` q ` from a magma to a group its "associated binary form". For its value, see ...  It is symmetric as soon as the magma and the group are commutative (with no condition on q), see ...  It is bilinear when the magma and the group are respectively a module and its ring of scalars and ` q ` is a quadratic form (this is actually part of the definiton of a quadratic form, see ~df-qform ). $)

df-assocbiform $a assoc_bi_form = ( m e. Magma , g e. Group |->

                         ( q e. ( ( Base `g ) ^m ( Base ` m ) ) |->

                            ( x , y e. ( Base ` m ) |-> ( ( q ` ( x ( Plus ` m ) y ) )

                                                                                         ( Plus ` g )

                                                            ( ( Opposite ` g ) ` ( ( q ` x ) ( Plus ` g ) ( q ` y ) ) ) ) ) ) ) $.

If homogeneous functions are to be defined, then maybe (restricting to the case domain=codomain):

df-homog $a Homog = ( x e. ScalSet |-> ( d e. NN0 |-> { f e. ( ( Base ` x ) ^m ( Base ` x ) ) |

                                  A. a e. ( Base ` x ) A. s e. ( Base ` ( Scalar ` x ) ) ( f ` ( s ( scalmul ` x ) a ) ) = ( s^d ( scalmul ` x ) ( f ` a ) ) } ) ) $.

(s^d is probably defined somewhere in set.mm but I do not know the syntax, and ScalSet is the class of "sets with a magma of scalars", or "M-sets" if M is said magma, sometimes "sets with operators", as in group actions).

Then, quadratic forms can be defined by:

df-qform $a QForm = ( m e. LMod |-> { q e. ( ( Homog ` m ) ` 2 ) | ( ( M assoc_bi_form ( Scalar ` M ) ) ` q ) e. ( BilinForm ` m ) } ) $.

It remains to define the class of bilinear forms on a module:

df-bilinform $a BilinForm = ( m e. LMod |-> { q e. ( ( Base ` ( Scalar `m ) ) ^m ( ( Base ` m ) X. ( Base ` m ) ) ) |  [ the two partial functions are linear forms ] } ) $.

If notation becomes too heavy, one can use "local variables" in the form " [ z / ( Base ` x ) ] ... " as is done in a few other definitions in set.mm, if I recall correctly.

Benoît

[Mingli Yuan]

Hi, Benoit and others, thanks for your reply. Let me keep a weekly pace to learn metamath step by step.
I still stick to Alex's assignment :-)  - try to complete the proofs he left in the first reply.

Yes and of course, I was blocked by questions. I record the learning process and give comments and questions as below.

It is a little bit long and preliminary, but maybe the next newcomers can learn faster and easier.

I had read the manual - metamath by Norm, and I understood the RPN notion and the stack.
Also I checked several examples, e.g.,

```metamath
$( A field is a commutative division ring. (Contributed by Mario Carneiro,17-Jun-2015.) $)
isfld $p |- ( R e. Field <-> ( R e. DivRing /\ R e. CRing ) ) $=
( cdr ccrg cfield df-field elin2 ) ABCDEF $.

```

The proof here starts with cdr which is a class notion, and I understand here is one abstract layer based on the class notion.

And based on the abstract layer we can set up more advanced math. In my understanding,  it also means if we grasp several rules

above the layer we can safely ignore the detail beneath the layer. Those are the assumptions I started to explore.

I copy the definitions of field and elin2 for reference

```metamath

$c DivRing $.
$c Field $.

$( Extend class notation with class of all division rings. $)
cdr $a class DivRing $.

$( Class of fields. $)
cfield $a class Field $.

$( Define class of all division rings. A division ring is a ring in which
the set of units is exactly the nonzero elements of the ring.
(Contributed by NM, 18-Oct-2012.) $)
df-drng $a |- DivRing = { r e. Ring |
( Unit ` r ) = ( ( Base ` r ) \ { ( 0g ` r ) } ) } $.

$( A _field_ is a commutative division ring. (Contributed by Mario Carneiro,
17-Jun-2015.) $)
df-field $a |- Field = ( DivRing i^i CRing ) $.

```

```
${
elin2.x $e |- X = ( B i^i C ) $.
$( Membership in a class defined as an intersection. (Contributed by
Stefan O'Rear, 29-Mar-2015.) $)
elin2 $p |- ( A e. X <-> ( A e. B /\ A e. C ) ) $=
( wcel cin wa eleq2i elin bitri ) ADFABCGZFABFACFHDLAEIABCJK $.
$}

```

In order to understand how proof of isfld works, I use below command to show

```

MM > show proof isfld /renumber /lemmon
1 df-field       $a |- Field = ( DivRing i^i CRing )
2 1 elin2       $p |- ( R e. Field <-> ( R e. DivRing /\ R e. CRing ) )

```

and

```

MM> show proof isfld
5   elin2.x=df-field $a |- Field = ( DivRing i^i CRing )
6 isfld=elin2      $p |- ( R e. Field <-> ( R e. DivRing /\ R e. CRing ) )

```

My questions here are:

1.  In the manual by Norm, a simple example was given at page 137, it pushes several $f or $ e into the stack,

and when it meets assertions, it will match and substitute. 

Considering proof

```metamath
( cdr ccrg cfield df-field elin2 ) ABCDEF $.

```

So the question here is: cdr, ccrg, cfield, df-field are all $a, and only elin2 is a $p, where are the $f or $ e?

2. Fortunately, I check the manual and found a /all option and mention about syntax construction, so we have

```

MM> show proof isfld /all
1   cA=cR            $f class R
2   cB=cdr           $a class DivRing
3   cC=ccrg          $a class CRing
4   cX=cfield        $a class Field
5   elin2.x=df-field $a |- Field = ( DivRing i^i CRing )
6 isfld=elin2      $p |- ( R e. Field <-> ( R e. DivRing /\ R e. CRing ) )

```

But where does step 1 come from? and when the verifier reads cdr in step 2, what does it happen?

It seems I should understand how class notions take effect precisely?

3. If we could ignore the class notions here as an abstraction layer, maybe we can understand the proof as process below

```

1. cdr            a label and class of DivRing, left it in scope

2. ccrg          a label and class of CRing, left it in scope

3. cfield         a label and class of Field, left it in scope

4. df-field       construct class by defined constructions and assigned it to label Field, left it in scope

5. elin2.x       matched by Field

6. elin2          takes effect by elin2 and QED.

```

I know this understanding is only roughly true but not precisely.

Thanks in advance.

Mingli

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/c9b002d5-1182-4ddc-b4cd-8e6502a2ad66n%40googlegroups.com.

[Benoit]

The proofs in set.mm are written in the "compressed" format (described in an appendix of the book).  If you want to see the "normal" uncompressed format, which best permits to understand the proof stack, type

MM> show proof isfld /normal
Proof of "isfld":
---------Clip out the proof below this line to put it in the source file:
    cR cdr ccrg cfield df-field elin2 $.
---------The proof of "isfld" (33 bytes) ends above this line.

I think with this, you'll understand how this works.

That being said, understanding the proof verification mechanism will not help you (or only very remotely) in understanding the math, and conversely.  You can learn them separately.

Benoît

[Thierry Arnoux]

Hi Mingli,

You're trying to understand how a proof is stored and verified.

There's absolutely nothing wrong with that, but I just wanted to state that it's not mandatory that you understand those.

I think when I first started with Metamath, I focused on understanding simple proofs on the website, or on MMJ2 (both are similar), created my first proofs and let the tool (MMJ2) store and verified the proof for me. I consider the compressed proof format like a kind of "binary executable" which we don't absolutely need to understand and read.

MMJ2 and the website both hide some steps of the proof (syntactical steps) and allows you focus on the more important ones (logical steps).

1. So the question here is: cdr, ccrg, cfield, df-field are all $a, and only elin2 is a $p, where are the $f or $ e?

Like all proofs in set.mm, the proof you chose is provided in compressed format. That format favors space over readability, so as few information as possible is included.

The $f and $e hypotheses which are "in scope" are known, so they do not need not repeated in the statement list in parentheses. That format is described in appendix B. of the Metamath Book, which states:

If the statement being proved has m mandatory hypotheses, integers 1 through m correspond to the labels of these hypotheses in the order shown by the show statement ... / full command, i.e., the RPN order of the mandatory hypotheses.

Here is the output of that command:

67962 isfld $p |- ( R e. Field <-> ( R e. DivRing /\ R e. CRing ) ) $= ... $.
Its mandatory hypotheses in RPN order are:
  cR $f class R $.

So there is a single mandatory hypothesis, which is `cR`, referred to by a `A` in the compressed proof (here A encodes to integer 1).

MM> show proof isfld /all
1   cA=cR            $f class R
2   cB=cdr           $a class DivRing
3   cC=ccrg          $a class CRing
4   cX=cfield        $a class Field
5   elin2.x=df-field $a |- Field = ( DivRing i^i CRing )
6 isfld=elin2      $p |- ( R e. Field <-> ( R e. DivRing /\ R e. CRing ) )

```

2. But where does step 1 come from? and when the verifier reads cdr in step 2, what does it happen?

It seems I should understand how class notions take effect precisely?

...and that's where the `cR` comes from, since `A` is the first character of the compressed proof (ABCDEF).

What happens is that the statement with a single "class R" is stored on the proof stack.

Here is how I would describe the rest of the verification process:

Next, `B` is read, which refers to `cdr`. This pushes "class DivRing" on the stack, which now contains "class R / class DivRing".

And so on until step 5, where the stack contains "class R / class DivRing / class CRing / class Field / |- Field = ( DivRing i^i CRing )".

Then, at step 6, `elin2` in invoked, which requires 4 variables : A, X, B and C, and an hypothesis ~elin2.x of the form `|- X = ( B i^i C ) `.

All 5 items are popped from the stack, in the order in which they are declared:

• A, which is substituted by R
• B, substituted by DivRing
• C, substituted by CRing
• X, substituted by Field
• |- X = ( B i^i C ), substituted by Field = ( DivRing i^i CRing ). The verifier checks that this substitution matches.
  

Finally, the statement of elin2 is pushed on the stack: |- ( A e. X <-> ( A e. B /\ A e. C ) )

Which, when substituted, results in |- ( R e. Field <-> ( R e. DivRing /\ R e. CRing ) ).

That is the final and only expression remaining on the proof stack, and the verifier finally verifies that this matches with the statement of ~isfld.

And that's it! Luckily this was a very short proof!

In practice, if you had used MMJ2 or checked the website proof of isfld, you can see that that proof only has 2 steps: 1-4 are hidden, and only 5-6 are shown.

That's because steps 1-4 only deal with "syntactically" building the expressions which will later be used in substitutions, not deriving new true statements.

I hope this helps and clarifies!...

BR,
_
Thierry

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAGDRuAjAUAtf9Mvz%3D7TRK3%3DtjAHPp1e0%2BWEmX61n4%2BUuqT%3DsFw%40mail.gmail.com.

[Mingli Yuan]

Hi, Thierry and Benoit,

I had read the lines in set.mm

```

$c class $.

$( Add 'class' as a typecode. $)
$( $j syntax 'class'; $)

```

So I guess the class notion is a kind of syntax sugar. I did not know mmj can simplify the development, that is why I want to understand how this mechanism works.

Right now, I know mmj and the webpage is more important for development.

Thanks

Mingli

[Benoit]

Mingli, you wrote:

> So far the learning curve is a little bit steep because a lot of conventions are not documented?

We are striving to keep documentation up-to-date and to document our conventions.  For the moment, documentation is not very centralized: there is the website (e.g., http://us2.metamath.org/mpeuni/mmset.html), the github pages (like README.md and CONTRIBUTING.md), the help of the metamath program (obtained by typing MM> help [command]), the statement ~conventions in set.mm (http://us2.metamath.org/mpeuni/conventions.html#uniprg) for set.mm-specific conventions, searching within this google group.

Can you keep a log of what seems undocumented to you, and share it here once you've verified it is undocumented, so that we can add it ?

Thanks in advance.

Benoît