Do inference rules mean the same in a Hilbert system and in a natural deductive system?

Question

Is it correct that Enderton's A Mathematical Introduction to Logic uses a Hilbert style system for first order logic?

On p110 in SECTION 2.4 A Deductive Calculus in Chapter 2: First-Order Logic

Our one rule of inference is traditionally known as modus ponens. It is usually stated: From the formulas $α$ and $α → β$ we may infer $β$ : $$\frac{α, α → β}{β}.$$

Which does the rule mean:

1. An instance of relation $\vdash$: $\{α, α → β\} \vdash β$.

2. An instance of a relation between the instances of $\vdash$: if $\vdash α$ and $\vdash α → β$, then $\vdash β$.

3. For a set $\Gamma$ of formulas, if $\Gamma \vdash α$ and $\Gamma \vdash α → β$, then $\Gamma \vdash β$. So the quote means to have $\Gamma$ but omits it, thinking that its readers will fill it in automatically. (Also see more below)

4. Something else?

Some thoughts, observations and questions:

• 2 and 3 are equivalent, because 2 implies 3 by the deductive theorem (or I am wrong because the deductive theorem is derived from the inference rules and axioms, so doesn't exist before the inference rules and axioms?).

• What makes me support 3 over 2 is that I saw in Wikipedia that the deductive theorem is regarded as an extended inference rule,

  Because Hilbert-style systems have very few deduction rules, it is common to prove metatheorems that show that additional deduction rules add no deductive power, in the sense that a deduction using the new deduction rules can be converted into a deduction using only the original deduction rules.

  Some common metatheorems of this form are: The deduction theorem, ...

  and in Enderton's book on p118

  DEDUCTION THEOREM If $\Gamma; \gamma \vdash ϕ$ , then $\Gamma \vdash ( γ → ϕ )$.

• Do inference rules mean the same in a Hilbert system and in a natural deductive system? No. 3 above is similar to 3.5 "Modus ponens" on p65 in IV Sequent Calculus (actually some natural deduction system) in Ebbinghuas' Mathematical Logic. Do the horizontal lines appearing in both mean "if ... then ..." at the metalanguage level?

  

• The reply to a related question says that inference rules may operate on formulas, if they are not written explicitly as operating on sequents (i.e. instances of $\vdash$). Is that incorrect? Inference rules always operate on instance of $\vdash$, even if they are written in a form which looks like they operate on formulas directly?

Thanks.

Answer 1

Do inference rules mean the same in a Hilbert system and in a natural deductive system?

YES.

See Rule of inference. The "canonical" representation is quite standard, but it is only a perspicuous symbolic representation.

We can describe it in words: a rule it is a “procedure” that takes as input one or two formulas of a specified form and produces as output a new formula.

So, they operate on formulas. And what is relevant is not “typographical shape” we use to represent it, but the fact that it is “formal”.

Modus Ponens rule is stated in the context of the definition of “formal deduction” that is meant to “mirror (in our model of deductive thought) the proofs made by the working mathematician” [see yesterday’s post].

A formal deduction is a sequence of formulas: at every stage we may write an assumption, a logical axiom or add a formula using the MP rule of inference that produce the "output" formula from two previously written formulas of the sequence.

Thus, an application of MP rule amount to the following inference: $\{ α, α → β \} ⊢ β$.

2 is simply a particular case of 3. The quote does not omit assumptions: they are the set $Γ$ in the definition of deduction of $\varphi$ from $Γ$ (page 111).

What are "assumptions" ? As already said, the definition of formal derivation is a formal model of mathematical practice: let $\Gamma$ the set of Euclid’s Elements axioms and let $\varphi$ Pythagoras theorem.

We have $Γ \vdash \varphi$.

---

Annex

Here is Enderton's Modus Ponens (Enderton's proof system is an Hilbert-style one):

$$\frac{α, α → β}{β}.$$

Here is the same rule (called Conditional Elimination) from a Natural Deduction popular textbook:

van Dalen's Logic and Structure.

The same rule is represented "in the context" of derivations $\mathcal D, \mathcal D'$.

For typographical reasons, we may represent it as follows:

$$\frac{\mathcal D ... \varphi \ \ \ \mathcal D' ... (\varphi \to \psi)}{\psi}.$$

And then we may use the derivability symbol "re-shape" it in sequent form:

If $(Γ \vdash \varphi)$ and $(Δ \vdash (\varphi → \psi))$ are both correct sequents, then the sequent $(Γ \cup \vdash \psi)$ is correct.

The final step is to put one premise on top of the other and we have Ebbinghaus's Modus Ponens.