11
$\begingroup$

The tag currently has no tag wiki. In my opinion this might invite people to use the tag for any question asking for a (more or less formal) proof. Very similar to the way the tag was used before it got removed and blacklisted. My personal assumption, however, was that is more likely intended for questions on a way more formal level, where you are considering a strict formalism and how to perform low-level steps in a formal proof.

Currently, has 26 questions, half of them from this month. Several older questions are indeed related to formal questions, while recent examples are at a much less formal level.

  1. Do you agree that is not intended for any question where a proof is required, but only for questions where the formalization plays a major part?
  2. How does the tag differ from ? Is it that is intended for questions about a specific proof, while is on the meta level, speaking about (a family of) proofs?
  3. Do you have a specific wording to suggest for the tag wiki?
$\endgroup$
14
  • 5
    $\begingroup$ Proof theory is a mathematical field. $\endgroup$
    – Asaf Karagila Mod
    Oct 8, 2014 at 12:11
  • 2
    $\begingroup$ @Asaf I'm not an expert, but wouldn't it be like "set theory" vs. "sets"? One is the field, the other is the main object of study? We don't need a tag for both if that's the case. $\endgroup$
    – Najib Idrissi
    Oct 8, 2014 at 12:27
  • 1
    $\begingroup$ Most questions concerning sets are not set theory (or even elementary set theory for that matter). I agree that [formal-proofs] is not a great tag, at least without a specified range of subjects. Whether or not the questions there fall under proof theory, I can't say because (1) I don't know much about proof theory; and (2) I haven't looked at them. $\endgroup$
    – Asaf Karagila Mod
    Oct 8, 2014 at 12:28
  • 1
    $\begingroup$ This is the oldest question I see, where this tag is used. Maybe this is where the tag was created. I pinged the user, who added the tag to this question to let them know about the discussion on meta. Here is another question, where the tag was added about the same time. $\endgroup$
    – Martin Sleziak
    Oct 8, 2014 at 13:01
  • 1
    $\begingroup$ A question that could be tagged formal-proof but not proof-theory would be: Is there are formal proof of the Feit--Thompson theorem? (Answer: yes, by Gonthier, using Coq). $\endgroup$
    – quid Mod
    Oct 8, 2014 at 13:15
  • 3
    $\begingroup$ I created the tag (formal-proofs) with intent that it should be used when people are asking for a formal proof of something within a formal system, the most common occurrences of this are natural deduction and Hilbert system kind of proofs. It could perhaps be used sometimes in conjunction with (proof-theory) if people are trying to related a formal proof to its stance in the meta-theoretic context, but mainly it's independent of proof theory. All of the above is just what I intended for the tag. I don't think it is a bad tag and I most certainly feel that this or a similar one is required. $\endgroup$
    – Git Gud
    Oct 8, 2014 at 14:56
  • 1
    $\begingroup$ In the past I asked as a subquestion of this whether a the (formal-proofs) tag should be created. No one answered and I took it upon myself to create it and still stand by it. $\endgroup$
    – Git Gud
    Oct 8, 2014 at 14:58
  • $\begingroup$ "In my opinion this might invite people to use the tag for any question asking for a (more or less formal) proof" I agree, what I don't agree is that I should care of askers' ignorance. $\endgroup$
    – Git Gud
    Oct 8, 2014 at 15:00
  • 4
    $\begingroup$ @GitGud You should be concerned with the way the tag is used. I don't object to the idea, but implementation is weak (creating a tag with empty wiki? you should know better than that). How can we expect the students learning to write proofs by induction in their "Intro to abstract math class" to know that this tag is not for them? They have a question about a proof, so they look for a tag with proof in it. (formal-proof) comes up and looks just right to them. $\endgroup$
    – user147263
    Oct 8, 2014 at 15:05
  • 1
    $\begingroup$ @CareBear I don't disagree, but 1) I still think that tag with no wiki is better than no tag at all; 2) I believe what you say will happen (in fact it has happened, the OP posted one example of this) and I take it as occupational hazard. As a practical matter, I don't think a tag wiki is going to help much with this because I don't think people read them. $\endgroup$
    – Git Gud
    Oct 8, 2014 at 15:11
  • $\begingroup$ I just removed the tag (formal-proofs) from a number of questions in which it wasn't used as I intended. Just letting you all know. $\endgroup$
    – Git Gud
    Oct 8, 2014 at 15:15
  • $\begingroup$ @MartinSleziak: Thanks for filling in the wiki. Will you simply copy your wiki text here as an answer? $\endgroup$
    – MvG
    Oct 8, 2014 at 15:37
  • 1
    $\begingroup$ MvG: As I mentioned here, the tag-info (tag-wiki and tag-excerpt) is only very basic. (I suppose it could be expanded by someone more knowledgeable.) It is based on @GitGud comment explaining their intentions when creating the tag.) If you think that this comment and the newly created tag-wiki answer your question, feel free to post some parts of them as an answer. (BTW thanks for retagging the incorrectly tagged questions Git Gud.) $\endgroup$
    – Martin Sleziak
    Oct 8, 2014 at 15:45
  • 3
    $\begingroup$ @GitGud wrote: I don't think a tag wiki is going to help much with this because I don't think people read them. Personally, I try to help with correct tagging of posts on the main. If I am unsure about usage of a tag, I usually try to find more information in tag-info (=tag-wiki and tag-excerpt). $\endgroup$
    – Martin Sleziak
    Oct 9, 2014 at 16:11

1 Answer 1

Reset to default
6
$\begingroup$

Martin Sleziak created a tag wiki and excerpt, based on the comment by Git Gud, who originally introduced the tag (as proposed in this post). Currently the description reads:

For questions about proofs within a formal system, such as natural deduction or Hilbert system.

Judging from the comments, the current interpretation appears to be:

  1. Yes, the tag is only intended in connection with specific formal systems and proofs therein. So a question which simply states “prove that …” should not be tagged with this. It should not be tagged for that aspect at all.
  2. The tag is only loosely related to proof theory. I see my original distinction somewhat confirmed, even though it's formulated differently.
  3. We now have a tag wiki, and taggers (original posters and retaggers) can use that to decide whether the tag is appropriate for a given question.
$\endgroup$

You must log in to answer this question.

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