The Coq mailing list

[Ken Kubota <mail AT kenkubota.de>]

Set theory *is* dependent set theory.

This is – as an answer to José's question "that matrices should be dependently typed" – incorrect.

He was asking this question since "Metamath does not use dependent type theory".

Many things can be expressed via the circumlocation of encoding.

But the concept of type theory is to express mathematical ideas naturally (*without* encoding).

Andrews: "allowing mathematical ideas to be expressed precisely with a minimum of circumlocutions"

http://www.owlofminerva.net/files/fom.pdf, p. 5

The key concept of type theory is to represent such dependencies within the syntax (the grammar)

as part of the formal language instead of using artificial constructions such as encoding on top of an existing invariable syntax.

Andrews: "The discussion turns to finding as simple, natural, and expressive a formulation of type theory as possible."

http://www.owlofminerva.net/files/fom.pdf, p. 5

For the same reason, I had argued similarly in the context of Coq in February 2017:

"A second aspect is the question of classical vs. constructive foundations. All 

constructive foundations, including Coq, use the encoding of proofs based on 

the Curry-Howard isomorphism. But the concept of expressiveness yields the 

_natural_ _expression_ of mathematics, hence the desire is not an _encoded_, but 

an _unencoded_ (direct) form of _expression_. With Q0/R0, one can express 

mathematical concepts very naturally."

https://sourceforge.net/p/hol/mailman/message/35648326/

https://sympa.inria.fr/sympa/arc/coq-club/2017-02/msg00024.html

Kind regards,

Ken Kubota

____________________________________________________

Ken Kubota

http://doi.org/10.4444/100

Am 23.12.2018 um 23:40 schrieb Mario Carneiro <di.gama AT gmail.com>:

Set theory *is* dependent set theory. There is no problem encoding dependent types in set theory, and matrix multiplication depends on all the dimensions of the arguments as well as the arguments themselves. A dependent pi type in metamath is df-ixp (the indeced cartesian product), and dependent sigma doesn't have a name but is idiomatically represented in theorems like eliunxp as ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) .

On Sun, Dec 23, 2018 at 3:22 AM José Manuel Rodriguez Caballero <josephcmac AT gmail.com> wrote:

Hello,

There is an argument that matrices should be dependently typed, specially in the case of quantum programs: http://www.cs.umd.edu/~rrand/coqpl_2018.pdf

My question are: 

1) Do you agree with this argument?

2) How does Metamath deals with this problem, because as far as I know, Metamath does not use dependent type theory?

For further information, see section 4.7 in  Robert Rand's PhD thesis: http://www.cs.umd.edu/~rrand/thesis.pdf

Kind Regards,

José M.

--
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 AT googlegroups.com.
To post to this group, send email to metamath AT googlegroups.com.
Visit this group at https://groups.google.com/group/metamath.
For more options, visit https://groups.google.com/d/optout.

--
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 AT googlegroups.com.
To post to this group, send email to metamath AT googlegroups.com.
Visit this group at https://groups.google.com/group/metamath.
For more options, visit https://groups.google.com/d/optout.