Stock answer for questions relating to formal proof

Question

Lately there has been a slew of questions (see below) which basically say "how do I construct a formal proof of proposition X?" where $X$ is usually a tautology from propositional logic. These questions tend to be very low quality:

1. They often fail to give any description of what formal proof system should be used. The askers may be under the misconception that there is only one formal proof system, or that there is only one "Hilbert-style" proof system. In reality there are many systems in different books, and a "formal proof" in one would not be a "formal proof" in another.

2. There is a general method for obtaining these results, which is proved as the "completeness theorem" in the book the asker is using as a reference. So the situation is somewhat analogous to getting numerous questions about how to solve different specific systems of linear equations over $\mathbb{R}$, when there is a general method that will solve all of them. In this situation the method depends on the proof system, but it still applies to all provable formulas.

3. The questions are typically unmotivated, with no explanation at all for why the person is somehow interested in the proposition stated. Sometimes the asker explains that the problem is homework, which at least explains where it came from.

These questions seem to be an exact fit for the "too localized" closing option. An answer that works for the person asking the question is unlikely to work for anyone else, unless that person happens to be assigned the same problem from the same (unmentioned) book. I have started voting to close these for that reason.

Is it feasible to develop some sort of canonical answer for these questions (for example, a question of the form "How do I find a formal proof for a given proposition?"). We could then close new questions of this form as duplicates of that one. I think this was discussed for some algebra-related questions, but I don't know exactly what the outcome was.

Examples:

• Proving $(p \to (q \to r)) \to ((p \to q) \to (p \to r))$

• prove $(A \rightarrow B) \rightarrow (\neg B \rightarrow \neg A)$ in Hilbert System

• formal proof challenge

• find formal proof

• Derive: $(A \implies (B \wedge C)) \models (A\implies B)$

• How do I prove $\Gamma, A, B \vdash C \Rightarrow \Gamma, A \wedge B \vdash C\ $ in a Hilbert system?

• https://math.stackexchange.com/questions/102944/formal-proof-of-varphi-lor-psi-leftrightarrow-varphi-prime-lor-psi

• Prove$ \forall x (A(x) \to B(x)) \to (\forall xA(x) \to \forall xB(x))$ is logically valid

• How do I prove $\Gamma, A, B \vdash C \Rightarrow \Gamma, A \wedge B \vdash C\ $ in a Hilbert system?

• How does (wikipedia's axiomatization of) intuitionistic logic prove $p \rightarrow p$?

• Prove the proposition is a tautology

Answer 1

Not all of these questions are created equal.

I agree that there's not much to be done for questions that don't even specify which formal system they're working with. Even if the OP is asked to clarify in comments, the clarification often comes in a comment as well, meaning that the question is of limited usefulness later because one has to trawl through a comment thread to find out exactly what the answers (if any) are answers to.

On the other hand, for example, the first of the questions you link to is not one of those. There the OP explicitly stated the axioms he had to work with, and apparently didn't have any kind of completeness theorem to refer to, not even the deduction theorem. The answer thread was long and interesting, and I think we would have been worse off if that question had been closed with a pointer to a "figure it out yourself" stock answer.

It would be good to have a faq/stock answer to which we could redirect the incomplete questions of this kind. However, I don't think it should just direct the reader to refer to the completeness theorem in his textbook:

• Completeness might not hold at all for the formal system in question, such as if an intuitionistic proof is required.

• It is possible that the OP is asking for help for an exercise that the textbook uses as a stepping stone on the way to completeness.

• In extreme cases, there may not be a textbook involved at all. For example., the Op could be reading a quasi-popular description of how formal proof systems work and a bald assertion that "it can be proved that" such and such. (Imagine someone trying to learn formal logic from Wikipedia!) Or they could be working with an advanced text that presents a formal system in its "things you should already know" chapter, but uses different axioms from the ones the OP are used to.

So among the faq answers there should also be a guide for how to ask a complete question if the standard techniques don't work in the situation the reader find himself in. Probably that just means saying: be sure to state all the logical axioms and all the rules of deduction in your question, as well as any metaresults you have already proved that feel relevant (especially the deduction theorem, or other derived rules).

Answer 2

I can agree that those questions might be too localized, however

• Sometimes it's not pedagogically right to just go ahead and prove completeness theorem. Well, because during the proof you actually need to understand how are things proved in the formal systems. As Henning mentioned it might be a stepping stone.

• When I had troubles with proving some statements I used some techniques from mentioned questions, but that's just an anecdote.