I've been reading the Stanford Encyclopedia of Philosophy article on classical logic, and I've been confused about Theorem 9, and the preceding statement. They mention how (*), the clause which states that any conclusion deducible from a set of premises is deduced by some nonempty set of the rules above, and state how this allows us to deduce that the number of steps is finite.

However, I'm confused as to how we derived such a conclusion from our deductive system. What problem does it pose for the deductive system the article posits if we have a deduction with infinite steps? I am intuitively skeptical of such a deduction, but I don't see a logical problem with the assertion. None, at least, which are derived from clause (*)

What am I missing?

Edit 1: While I am thankful for the responses from @Conifold and @Mauro ALLEGRANZA, I fear I have not been clear enough in what my confusion is. It makes sense that a valid derivation must be of finite length. My confusion is with the article linked, and how they derive this conclusion.

Edit 2: On request, the specific statement I'm having trouble with is the following: "By clause (*), all derivations are established in a finite number of steps". For reference, the clause posits that all derivations are performed by a combination of the introduction and elimination rules and the rule that you can deduce sentence s from any set of sentences L such that "s is an element of L."

  • The first problem is that in general it makes no sense: what would be the conclusion of an infinite chain of inferences? It is not like we have a notion of a limit for formulas. Even when one can make some sense of it (e.g. in infinitary logic) the resulting system does not behave very well, and it is certainly far from classical.
    – Conifold
    May 27, 2019 at 5:43
  • Can you edit your question to include the parts of the SEP article that you're having trouble with?
    – E...
    May 27, 2019 at 17:55
  • I tried to provide some reference in an edit, but I'm not sure precisely how to link a specific sentence in an article which is not directly under a section heading. While suboptimal, I thought the best thing I could do would be to post the exact quote which people could CTRL+F for. May 27, 2019 at 18:59
  • The clause (*) is a typical one in recursive definitions: one gives a set of recursive rules for generating X-s, and then stipulates that an X is that and only that generated by the rules provided. The process must terminate to produce a result, and, unless there is at least one infinitary rule (generating output from infinitely many inputs), by induction, the number of steps is finite. The clause ensures that any conclusion must be the result of such a terminating process.
    – Conifold
    May 27, 2019 at 21:04

2 Answers 2


The usual definition of derivation in a formal proof is a finite sequence of formulas.

Intuitively, a derivation is the formal counterpart of a human deductive inference : an infinite inferential process will never reach the conclusion.

In Mathematical Logic, we formalize the intuitive concept of deduction by way of the mathematical object : derivation.

We have to stress the fact that a derivation is a precisely defined mathematical object : either it is a finite sequence of formulas (see e.g. H.Enderton, A Mathematical Introduction to Logic (2001), page 111) or it is a tree-like structure (see e.g. Chiswell & Hodges, Mathematical Logic (2007), page 54).

The key-point of the definition is the possibility to perform induction on it.

Having said that, the definition of derivation used by the authors of the SEP's entry dedicated to Classical Logic is similar : a deduction (or derivation) is the formal counterpart of an

argument ⟨Γ,ϕ⟩, where Γ is a set of sentences, the premises, and ϕ is a single sentence, the conclusion,

and we say that conclusion is derivable (or deducible) from the premises :

(*) Γ ⊢ ϕ only if ϕ follows from members of Γ by the above rules.

We have a finite number of rules, and every rule has a finite number of premises (one or two); thus, also if the set Γ may be infinite, if we imagine a mechanincal process that writes down a derivation, we have only to write the premises (the members of Γ that we are using) and the conclusion.

Thus, at every stage of the process (and note that every application of a single rule produces a derivation) we have only written a finite number of formulas.

This is the reason of the statement :

By clause (*), all derivations are established in a finite number of steps.

The above fact is nor more true for Infinitary Logic, i.e.

a logic that allows infinitely long statements and/or infinitely long proofs.

Obviously, if a single rule allows for a countable infinite number of premises, a single inferential step will produce already a countable infinite list of formulas.

This is (one of) the reason why (see also comment above) infinitary logics are studied with "model theoretic" means.

  • 1
    How do infinitary logics allow for deductions of countable length? That makes no sense, unless one has some notion of "convergence". "Long" formulas in a derivation don't make the derivation infinite. Neither do infinitely many premises. You even said it yourself? May 26, 2019 at 17:32
  • @JishinNoben The word countable has a meaning that can include infinite sets: "A countable set is either a finite set or a countably infinite set." en.wikipedia.org/wiki/Countable_set
    – H Walters
    May 26, 2019 at 17:35
  • 1
    I know what countable means. If you read carefully, I am asking something different. It is formulated as a question, since I am assuming that @Mauro_Allegranza meant the last sentence not literally, but intended something else. May 26, 2019 at 17:37
  • I understand what you are expressing when you break down (*). However, I am confused as to how we can go from discussing the finitude of the rules of inference and the set we are deducing the conclusion from to discussing the steps. As I understand it, the steps would be the application of these rules. For instance, the proof of the law of excluded middle is 10 steps, since there are ten different applications of the rules established in the article. How can I gather that this must be finite from the fact that the rules and premises are finite (or can be placed in a finite number of sets)? May 28, 2019 at 18:26
  • @JishinNoben It depends on how narrowly one interprets "infinitely long." Perhaps "infinitely wide" would be a better way to phrase it: in both classical and infinitary (first-order) logics a proof is a well-founded tree of formulas with certain properties, but in the classical case that tree has to be finite while in the infinitary case it doesn't. The right notion of "length" for an infinitary proof is then the rank of that tree, which can indeed be infinite; the rank of a well-founded tree is defined recursively: the rank of a tree is the supremum of {the ranks of its child-trees +1}. Jun 3, 2019 at 5:53

Sorry if this is an improper way to make this statement, but I was able to figure it out. It was a misunderstanding regarding what was meant by "derivation." I thought that this referred to an entire argument, but it referred to the application of these rules. My apologies for the confusion, and thanks to everyone who offered their help!

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .