6
$\begingroup$

The question Elimination rule for identity types in Martin-Lof Type Theory [closed] was recently closed for being off-topic.

While I agree it should have been closed for being a duplicate, I don't see how a question about Martin-Löf type theory, and hence dependent type theory, is off topic for a site about proof assistants.

$\endgroup$
0

2 Answers 2

Reset to default
4
$\begingroup$

It may sound strange, but from what I've seen before (on other Stack Exchange sites) closing a question as off topic is the typical close reason for a cross site post. Some sites like Unix.SE do have a custom close reason for things like these, and this also falls under the off topic category.

This should make sense, as the question may not fit the other close reasons. It could be a perfectly valid question that was simply just asked on multiple Stack Exchange sites and is not unclear, too broad, or opinionated.

$\endgroup$
4
$\begingroup$

In this particular instance, it does seem that the question was closed mainly due to its being answered on another site, and "off-topic" was just the least inapplicable of the official "close reasons".

However, it's not obvious to me that questions that are purely about some mathematical foundation should be on-topic here just because the foundation has been used in a proof assistant. If there is nothing at all about the question that relates to the proof assistant, but it is purely a mathematical question, wouldn't it be better to ask it on Math.SE or MathOverflow?

Dependent type theory is strongly associated with proof assistants in many people's minds, but there's no intrinsic reason for this. Some proof assistants use ZFC; are all questions about ZFC therefore also on-topic here? I wouldn't think so.

$\endgroup$
7
  • $\begingroup$ While I agree that not any question purely about mathematical foundations should be on topic, I disagree that type theory is just an arbitrary choice of foundation for proof assistants. For example, Mizar, metamath, and Isabelle/ZF, while all using set theory as the mathematical interface, are all based on some form of type theory. In fact I would argue no currently existing proof assistant uses set theory as it's foundation. $\endgroup$
    – Couchy
    Commented Feb 11, 2022 at 22:38
  • $\begingroup$ I don't know if I would be so parsimonious. The theoretical underpinnings of a theorem prover, in my mind, is "on topic" for PA.SE; plus, we don't know what the thread's author is doing, for all we know they could be stuck with some theoretical dilemma that's a thorn in some application. So I'm just not sure about excluding such questions... $\endgroup$
    – Alex Nelson
    Commented Feb 11, 2022 at 22:45
  • $\begingroup$ @Couchy One could similarly argue that mathematical ZFC itself is based on a form of type theory, namely single-typed first-order logic. So yes, type theory is not an arbitrary choice of foundation for proof assistant, but that's because it's not an arbitrary choice of foundation for mathematics either -- there's nothing special about its relationship to proof assistants. $\endgroup$
    – Mike Shulman
    Commented Feb 11, 2022 at 23:30
  • $\begingroup$ @AlexNelson I don't see how what the author is doing is relevant. Regardless of what their end goal is, if their question is just about mathematics, doesn't it belong on a mathematics SE? $\endgroup$
    – Mike Shulman
    Commented Feb 11, 2022 at 23:33
  • $\begingroup$ But by that reasoning, why wouldn't implementing a proof assistant belongs on stackoverflow? Or formalizing group theory in a proof assistant belongs of math.SE? $\endgroup$
    – Alex Nelson
    Commented Feb 11, 2022 at 23:46
  • $\begingroup$ If a question about formalizing group theory in a proof assistant is not really about the mathematics, but about the proof assistant, this would probably be a better place. But if it were fundamentally about group theory and just happened to arise during formalization, then I would say math.SE is a better place. Similarly, if a question about implementing a proof assistant were really just about programming (e.g. how to use some feature of the PL in question), then SO would make more sense; but if it were specific to proof assistants then a better response might be obtained here. $\endgroup$
    – Mike Shulman
    Commented Feb 12, 2022 at 0:11
  • $\begingroup$ In this case, the question mentioned by the OP has nothing directly to do with proof assistants; it is only about the mathematical formalism of type theory. $\endgroup$
    – Mike Shulman
    Commented Feb 12, 2022 at 0:12

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .