Understanding natural deduction and derivable rules

Question

I've been learning about natural deduction recently and I'm having some trouble understanding it's meaning.

My main reference is the book "A Concise Introduction to Mathematical Logic" by Wolfgang Rautenberg. In this book they use the following notation $$\frac{X \vdash \alpha}{X \vdash \beta}$$ where $X$ is a set of formulas and $\alpha, \beta$ are formulas. Unfortunately, in the book there is no rigorous definition of this "fraction-notation", so I'm just left with an intuitive understanding. Could someone explain what exactly this "fraction" stands for and how the above statement is different from writing $${X \vdash \alpha} \implies {X \vdash \beta}?$$

A specific example that I'm struggling with:

My intuitive understanding leads me to believe that the statement $\frac{X \vdash \alpha}{X \vdash \beta}$ is "equivalent" to the statement $\frac{X \vdash \lnot \beta}{X \vdash \lnot \alpha}$. But how does one go about proving something like this, and in what sense are they "equivalent"?

I am very confused by these notions and would appreciate any help!

Answer 1

See page 22 (3rd ed ) :

We will now define a derivability relation $\vdash$ by means of a calculus operating solely with some structural rules. [...] If $\vdash$ applies to the pair $(X, \alpha$) [called : sequent] then we write $X \vdash \alpha$ and say that $\alpha$ is derivable or provable from $X$.

And page 23 :

$X \vdash \alpha$ (read "from $X$ is provable or derivable $\alpha$”) is to mean that the sequent $(X, \alpha)$ can be obtained after a stepwise application of the basic rules. We can make this idea of “stepwise application” of the basic rules rigorous and formally precise (intelligible to a computer, so to speak) in the following way: a derivation is to mean a finite sequence $(S_0, \ldots, S_n)$ of sequents such that [...].

Thus, an inference rule is a "basic" allowable step in the calculus of the derivability relation : $\vdash$.

Having e.g. a derivation $X \vdash \alpha, \beta$, the application of the rule $\land_1$ licences us to attach to this derivation (a finite list of sequents) the new sequent : $X \vdash \alpha \land \beta$.

See again page 22 :

[the derivability relation] $\vdash$ turns out to be identical to the consequence relation $\vDash$ [see page 18 for the definition].

This result is [page 28] :

Theorem 4.6 (Completeness theorem). $X \vdash \alpha$ ⇔ $X \vDash \alpha$, for all formula sets $X$ and formulas $\alpha$.

---

You have to note that $\Rightarrow$ and $\Leftrightarrow$ are meta-linguistic symbols, abbreviating "if ___, then ___" and "___ if and only if ___" respectively, and not part of the calculus [see page xxi].

---

Derivable rules [see page 23] are "patterns of inference" not included into the initial list of rules but that can be proved to be valid on the basis of the initial rules.

---

Regarding you example of a derived rule, it is not correct; contraposition must be written (in Rautenberg's system) as :

$$\frac{X , \alpha \vdash \beta}{X , \lnot \beta \vdash \lnot \alpha}.$$

We can derive it as follows :

1) $X, \alpha \vdash \beta$ --- supposition

2) $X, \lnot \beta, \alpha \vdash \beta$ --- (MR) on 1

3) $X, \lnot \beta, \alpha \vdash \lnot \beta$ --- (IS), (MR)

4) $X, \lnot \beta, \alpha \vdash \lnot \alpha$ --- ($\lnot$-1) on 2 and 3

5) $X, \lnot \beta, \lnot \alpha \vdash \lnot \alpha$ --- (IS), (MR)

6) $X, \lnot \beta \vdash \lnot \alpha$ --- ($\lnot$-2) on 4 and 5.

Answer 2

A statement of the form $$\frac{X \vdash \alpha}{X \vdash \beta}$$ is called an inference rule. The part above the line is called the premise of the rule, and the part below the line is called the conclusion of the rule. Basically, what such a rule says is that given the premises, we can infer the conclusion. So in a sense, you should think if this as "if the premises are true, then the conclusion is true", which is similar to $$X \vdash \alpha \implies X \vdash \beta$$ as you wrote. Note, however, as Mauro Allegranza explained, that the inference rules form the actual deduction system, whereas the symbol $\implies$ is external to this system, and in this sense they are not similar.

So what is the point of writing inference rules in this way? Well, there are other proof systems, such as Hilbert-style axiomatizations, which do not state its rules in this way. However, natural deduction allows you to nicely represent derivations as (upside-down) trees, which makes it nice to work with in terms of algorithms, and gives you a neat visual representation of the derivation. In a sense, this may feel more natural (hence the name), but this is of course highly subjective.