Constructing Hilbert-style proofs without "assume" structure

Question

According to the definition of Hilbert-style systems, proofs should be constructed only by applying axioms and rules of inference.

In practice, most proof that I have seen use the 'suppose' or 'assume' construct. That is, they check the cases in which a given variable is true or false.

For example take the following proof that (p → q) → (¬p ∨ q)

if p

   q (p → q)

   -p ∨ q ( a → a ∨ b)

if -p 
   -p ∨ q ( a → a ∨ b)

Two questions regarding this:

1 Is this rule permitted to be used in Hilbert systems.

2a And if it is, why is it missing from the descriptions?

2b If it is not, is there a way to do the same thing with axioms and rules of inference (you can use the abore theorem as an example)?

Answer 1

Let me explain one by one. First, in mathematical logic, for example, first order logic, there are two kinds of proofs in fact: one is called proof and used for theorems of the form $\vdash\varphi$, another is called deduction of the form $\Gamma\vdash\varphi$ of which formulas may be called assumptions or premisis. Although the second kind has a different name, both kinds are called proof in mathematical practice.

For your question 1, in fact any rule preserving truth could be added into the set of inference rules only if it is intuitive and simple enough. Or equivalently, any valid formula could be transform into a rule to be used as an inference rule only if it is intuitive and simple enough. In this way, the proof and deduction sequences could be simplified a lot. In fact, we have done so in mathematical logic, and some meta theorems about deduction and deduction rules are proved towards that purpose.

For your question 2a, there are possibly two reasons that why such rules are not added into the set of inference rules in mathematical logic: (1) such rules are not as intuitive and simple as $\mathsf{MP}$ (most of textbooks choose $\mathsf{MP}$ only) although they are seems to be quite intuitive and simple; (2) if we add many rules into the set of inference rules, then the proof (not the proof defined in first order logic but like the actual proof in mathematical practice) to some meta theorems (for example, the soundness theorem) about mathematical logic would become quite complicated and the basic textbooks about mathematical logic would have more pages.

Now, for your question 2b, the answer is certainly YES. But when you do this, please make sure that it should be appropriate for your actual purpose.

---

By the way, my book about mathematical logic which isn't written in English unfortunately talks a lot about questions of such kind.

Answer 2

"Is this rule permitted to be used in Hilbert systems."

If this question is meant to ask if such a rule can always get used in Hilbert Systems, the answer is no. The rule you describe goes by the name of 'conditional introduction'. For that to hold as a rule of inference in a Hilbert system, a deduction meta-theorem has to get proved first. As an example, for the axiom set (in Polish notation) preferred by Lukasiewicz in two of his books, {CCpqCCqrCpr, CCNppp, CpCNpq}, the deduction meta-theorem, so far as I know, has never gotten proved from first principles. Lukasiewicz doesn't give it to you in those books also. That consists of a system where it could get proved, but since no one has proved the deduction meta-theorem for that system it seems (and it's proof isn't simple, nor easy in that system), using a rule of conditional introduction isn't permissible. Also, the deduction meta-theorem doesn't in detail say that using a rule of conditional introduction is permissible exactly, but rather details an algorithm by which a deduction can get transformed into an axiomatic proof given that we have enough space and resources for such a conversion. I mention this here, because for a system with the three Lukasiewicz axioms above, that conversion process would be very lengthy. The conversion process could outstrip the power of the computer/memory in some computational contexts, and thus the algorithm becomes even more theoretical.

Also, and perhaps better, there exist Hilbert type systems where there is no deduction meta-theorem whatsoever. For example, Lukasiewicz three-valued logic with axioms of {CpCqp, CCpqCCqrCpr, CCNpNqCqp, CCCpNppp} and C-detachment {C$\alpha$$\beta$, $\alpha$} $\vdash$ $\beta$ has no deduction meta-theorem, and thus using a rule of conditional introduction could lead us to start with correct premises and draw an incorrect conclusion, even if we adhered to the vert last detail of the formal system.

"And if it is, why is it missing from the descriptions?"

In the context of an axiomatic or "Hilbert" type system, what comes as missing is that the following rules of inference (in Polish notation) need to get shown as correct meta-logically using only the axioms of the formal system:

$\alpha$$\vdash$C$\beta$$\alpha$

{C$\alpha$C$\beta$$\gamma$, C$\alpha$$\beta$} $\vdash$ C$\alpha$$\gamma$.

This is why you'll often see the pair of axiom schema ($\alpha$$\rightarrow$($\beta$$\rightarrow$$\alpha$)) and (($\alpha$$\rightarrow$($\beta$$\rightarrow$$\gamma$))$\rightarrow$(($\alpha$$\rightarrow$$\beta$)$\rightarrow$($\alpha$$\rightarrow$$\gamma$))) in textbooks, since they lead to the shortest algorithms corresponding with the above two rules of inference.

OR that $\alpha$$\vdash$$\beta$ implies ($\alpha$$\rightarrow$$\beta$), but showing that the above two rules of inference hold consists of the quickest path of doing that.

"If it is not, is there a way to do the same thing with axioms and rules of inference (you can use the abore theorem as an example)?"

No. The above would not be convincing as a demonstration when studying Lukasiewicz three-valued logic or some other system where proving the deduction meta-theorem is not possible. And such reasoning could lead to an error for understanding that or some other system of logic.