The Coq mailing list

[Mario Carneiro <di.gama AT gmail.com>]

One thing which set-theory-based foundations afford (arguably you can do this in type theoretic foundations as well but it's not done conventionally) is a decreased reliance on the exact form of a definition. Definitional equality is a really important concept in dependent type theory, and it prevents the ability to say "here is an encoding, now let's forget about it henceforth" because you can always unfold the definitions. There is a lack of encapsulation. And what's more, certain theorems that are true under one definition are not well typed(!) under another, equal, definition, even if one proves all the analogous theorems for the new definition. This means a lack of modularity. Of course one can always say that it is bad practice to use definitional equality like this, but it's only a gentleman's agreement at best.

Set theory, by contrast, thrives on making encodings and forgetting about them. You might say that it's a loss to have to go to such lengths to get a basic concept inside the theory, and wouldn't it be better if the concept was built in? and I would say that this shows that the original foundations were good enough already, and we need not make an unnecessary assumption. Obligatory quote:

"The advantages of the method of postulation are great; they are the same as the advantages of theft over honest toil." -Bertrand Russell

Once a concept is suitably encoded, and a short definition is made to refer to it, there is no loss in comfort or convenience to make use of it; indeed one of the most important properties of systems like metamath is that axioms and theorems are indistinguishable at point of use. The dependent type theory analogue of this would be to say that all theorems are opaque; this would be a problem for the objects of study, but we don't have propositions as types here - the proofs are not objects of (internal) study, they are strictly metatheoretic in nature.

If the foundation is chosen specifically to model the objects of study, no more no less, then this means that the foundation will shift as the objects of study change, once one attempts to formalize diverse subjects in the same theory. If the foundation never stops shifting then it's not much of a foundation, and if it does then eventually you fall back on encodings once more, and you will not have gained what you set out to gain. This latter situation is what you find in general purpose systems based on dependent type theory such as Coq; the foundations, though much more complicated than set theory, are still tiny compared to the breadth of what has been formalized, and in those formalizations you see encodings of all the things that the foundation didn't hand you specifically. Natural numbers are handed to you by fiat, but integers and real numbers have to be constructed. Compared to this, it is much more uniform to just say "construct everything" and make the foundation as parsimonious as possible.

Mario Carneiro

On Mon, Dec 24, 2018 at 6:32 AM Ken Kubota <mail AT kenkubota.de> wrote:

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.

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