Consider the question.

Given the nature of a sentence $S$, it there any way to tell how many different ways you can prove this sentence?

Proofs are not distinct if we have a situation such as: $P \implies Q$ and we want to prove that $A\implies B$ and say we have $A\implies P$ and $Q\implies B$ then $A\implies P\implies Q\implies B$ is the same proof as $A \implies P \implies B$. So the methods of proving such statements must be as "concise" as possible. However this logically means that given a set of axioms, they can directly imply the result. This is an example of conditions.

So my real question(s) is/are:

What conditions are necessary to distinguish between proof (proofs being a set of logical sentences determining the desired result as true) such that the amount of proofs can be counted?

Is it easily determined which conditions imply the cardinality of the set of proofs?

eg. if I say conditions $X$ for proofs I may be able to get countibly amount infinite proofs. (Which wouldn't be useful). Or as the above condition, which implies proofs are just applications of the axioms. (Also not very useful).

  • $\begingroup$ I don't see how A⟹P⟹Q⟹B is the same proof as A⟹P⟹B. I'm not even sure what A⟹P⟹Q⟹B means (⟹ doesn't associate). $\endgroup$ Aug 7, 2014 at 16:21
  • 2
    $\begingroup$ Given the context, I assume it means "$A \implies P, \quad P \implies Q$ and $Q \implies B$"... $\endgroup$ Aug 7, 2014 at 16:36

1 Answer 1


A proof consists of a sequence of statements. When are two sequences distinct? Well, if two sequences have a different length, then they qualify as distinct. Now consider any proof that you have which say proves A as an intermediate step before you prove the conclusion C. Well, since A is true, it follows that (B$\rightarrow$A) holds as true also (where $\rightarrow$ indicates the conditional of two-valued logic or any logical system where $\vdash$(A$\rightarrow$(B$\rightarrow$A)) or |=(A$\rightarrow$(B$\rightarrow$A))). But "B" indicates an arbitrary variable. And thus you can insert a subsequence




to any proof that you already have, including the proof that you will obtain when doing this. Consequently, the cardinality of all proofs comes as at least countably infinite.

That said, there may exist an infinite number of proofs of a given length, where the length of the proof comes as the number of steps and a "step" in a proof consists of a the result of an application of a rule. There may also exist a finite number of proofs of a given length.

  • $\begingroup$ Ahem.. "probably does exist"??? By your definition it is often infinite, because we have infinitely many variable symbols and any quantification can use any of them. However, by my definition the length of a proof is the actual length of the string of symbols, and the alphabet is finite (we just need a prefix-free code so that we have infinitely many variable names), in which case surely there are finitely many proofs of any specific length. $\endgroup$
    – user21820
    Apr 30, 2016 at 6:10
  • $\begingroup$ @user21820 Suppose that you want to find the shortest proofs in axiomatic propositional calculi under condensed detachment. To find the shortest proof of a given theorem, we don't need infinitely many variables. We only need twice the number of variables of the formula with the most variables in the shortest proof sequence. E. G. Our axiom set is {CpCqp, CCpCqrCCpqCpr}. The theorem is CCpqCCrpCrq. 8 variables suffice to find the shortest proof [CpCqp CpCCqCrsCCqrCqs CCpCqCrsCpCCqrCqs CCpqCCrpCrq] which has length 48. $\endgroup$ May 2, 2016 at 18:01
  • $\begingroup$ My point is that under any reasonable definition, either there surely exists finitely many proofs or there surely exists infinitely many proofs. Also, "probably" is not well-defined. $\endgroup$
    – user21820
    May 3, 2016 at 1:00
  • $\begingroup$ @user21820 Surely there exists finitely many proofs or there exists infinitely many proofs of a given length once there exists enough information about the system. The original question didn't provide any information about the system in question. Thus, neither 'there exists finitely many proofs' nor 'there exists infinitely proofs' holds. You spoke correctly about me using the word 'probably' poorly. $\endgroup$ May 3, 2016 at 13:10

You must log in to answer this question.

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