1
$\begingroup$

Are axioms inference rules without assumptions, or not inference rules at all?

I heard that sequent calculus doesn't have axioms, is that true?

p69 in §6. Summary and Example in IV. A Sequent Calculus in Ebbinghaus' Mathematical Logic, summarize the inference rules in sequent calculus (is it called natural deduction outside the book?) for the first order language. Is there any axiom?

  • Is (Assm) an axiom? Is $\phi \in \Gamma$ considered an assumption of it?

  • Is ($\equiv$) an axiom?

enter image description here

$\endgroup$
  • 1
    $\begingroup$ Yes. See Gaisi Takeuti, Proof Theory (2nd ed 1987), page 11: "A sequent of the form $A \to A$ is called an initial sequent, or axiom." It is Natural Deduction that have no axioms. $\endgroup$ – Mauro ALLEGRANZA Sep 8 at 18:02
  • 1
    $\begingroup$ "I heard that ..." Please, provide the reference :-) $\endgroup$ – Mauro ALLEGRANZA Sep 8 at 18:04
  • 1
    $\begingroup$ The proof system used in Ebbinghaus' text is a variant of Natural Deduction; it is very similar to the "intermediate" system between ND and SC used by Gentzen (1936). $\endgroup$ – Mauro ALLEGRANZA Sep 8 at 18:50
  • 2
    $\begingroup$ If satisfied by the answer below, please accept it $\endgroup$ – Mauro ALLEGRANZA Sep 9 at 14:20
4
$\begingroup$

(Not too) Short answer. Yes, the rules $(Assm)$ and $(\equiv)$ are axioms. By axiom here (and in many textbooks such as Takeuti's Proof Theory cited by MauroALLEGRANZA) is intended an inference rule with no premises. In this sense, every proof system needs at least an axiom rule, otherwise there is no possibility to build a derivation: without any axiom, from what can we start a derivation on the top of the tree? Said differently, this is the only way to avoid infinite regress.

By the way, the rule $(Assm)$ means that if you assume $\varphi$ (the $\varphi \in \Gamma$) then $\varphi$ holds (the last $\varphi$ in the sequent). So, $(Assm)$ is a minimal commitment, if you don't have it, you can't say anything.

We need $(Assm)$ even in a purely logic language without the identity symbol $\equiv$. Of course, when you extend the language with other symbols, inevitably you need other axioms to deal with that symbol and to give it a meaning. For instance, the axiom $(\equiv)$ expresses the reflexivity of the identity.

When you hear that the sequent calculus does not have any axiom, it is intended that no axiom is needed other than the minimal one $(Assm)$, at least in a purely language without the identity symbol $\equiv$. This is the main difference with other proof calculi such as Hilbert system, where there are many axioms even for a purely logical language without the identity symbol.


First digression: What is a sequent calculus? The calculus defined in Ebbinghaus' Mathematical Logic is more an hybrid between sequent calculus and natural deduction, than a pure sequent calculus.

A "pure" sequent calculus is a proof system that manipulates sequents (i.e. finite sequences or multisets of formulas) or pairs of sequents and it is characterized by the fact that there are no elimination rules (a connective or quantifier cannot disappear moving from a premise to the conclusion of an inference rule) except the cut rule, which however is admissible, i.e. "superfluous" (everything derivable in the sequent calculus can be derived without using the cut rule). A standard presentation of the sequent calculus is given on Wikipedia page (see the system LK).

Why does Ebbinghaus' calculus not completely fit it this framework? Because of the rules $(PC)$ and $(Ctr)$, which are elimination rules (a formula in the premises disappears in the conclusion) and are not "superfluous": if you rule them out of the system, then you cannot prove all the valid formulas in classical logic.

Anyway, coming back to your main question, it does not change anything: the axiom $(Assm)$ is needed in both "pure" sequent calculus and Ebbinghaus' calculus.


Second digression: Are there axioms in natural deduction? Yes, $(Assm)$ is required also in natural deduction and, as in the sequent calculus, it is the only axiom required, at least in a pure logical language without the identity symbol. In this respect, my point of view is different from MauroALLEGRANZA's one. There are many different but equivalent presentations of natural deduction (the one manipulating formulas in tree-like derivations, the one manipulating sequents, Fitch-style system), in some of them the presence of $(Assm)$ is somewhat hidden, but it is still there.

In the presentation of natural deduction that manipulates formulas in tree-like derivations (see here for a gentle introduction), there is a special rule as the starting point for building proofs. It is called the assumption rule, and it looks like this, for any formula $\varphi$:

$$\tag{1}\varphi$$

What it means is that at any point we are free to simply assume any formula, $\varphi$. The single formula $\varphi$ constitutes a one-line proof, and the way to read this proof is as follows: assuming $\varphi$, we have proved $\varphi$.

This is exactly the same meaning as the rule $(Assm)$ in the sequent calculus. Indeed, the assumption rule $(1)$ in natural deduction can be seen as an axiom, in the sense of an inference rule without premises. This is evident in the sequent-like presentation of natural deduction (see here and here for an informal explanation of this presentation), where the assumption rule $(1)$ becomes exactly the rule $(Assm)$ (Ebbbinghaus' sequent $\Gamma \ \varphi$ is more commonly denoted by $\Gamma \vdash \varphi$).

As in the sequent calculus, you can hear that natural deduction does not have any axiom, but it should be intended that no axiom is needed other than the minimal one $(Assm)$, at least in a purely language without the identity symbol $\equiv$.

What is common in all the different presentations of natural deduction is that for every connective and quantifier there are introduction rules (that introduce a new connective or quantifier moving from their premises to their conclusion) and elimination rules (that discard a connective or quantifier moving from their premises to their conclusion).

Ebbinghaus' calculus is not a natural deduction system because there are not elimination rules for the connectives $\lor$ and the quantifier $\exists$, but the rules $(PC)$ and $(Ctr)$ can be considered as elimination rules, and there are not introduction rules for the connective $\lnot$.

| cite | improve this answer | |
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.