1
$\begingroup$

Is there any recursively axiomized system with infinitely many proofs for some propositions or a proposition? So we will have at least one proposition which is deduced from the recursively axiomatic system in infinite ways.Could any one give an example or proof?

EDIT:We define a proof or a reduced proof as one which could not omit any proposition in the arguments,otherwise would be invalid. Or we can view it as question of formal language,that is :is there a formal language with at least one word which can be parsed in infinitely many ways?Of course there have to be no rewriting like "irrelevent padding or stupid detours"

Improve this question
$\endgroup$
3
  • $\begingroup$ Yes, but for trivial reasons. At any point in a proof you can insert, say, $p \to p \text{ and } q$ and then insert $p \text{ and} q \to p$. $\endgroup$
    – Qiaochu Yuan
    Jun 23, 2013 at 0:33
  • $\begingroup$ @Qiaochu,Sorry,what I want to know is not such a trivial argument,please see the edited post and the following answer and comments. $\endgroup$
    – XL _At_Here_There
    Jun 23, 2013 at 1:00
  • $\begingroup$ Actually,I do not like the reduced proof being defined in such way,but it is very easy to define it in such a way $\endgroup$
    – XL _At_Here_There
    Jun 23, 2013 at 1:18

3 Answers 3

Reset to default
7
$\begingroup$

How about the theorem "There exists at least one prime number?" There are infinitely many distinct proofs of this result, none of which includes another as a subproof. Certainly this example is trivial in some sense, but I think it is not obvious how to pin down why this shouldn't be counted.

Perhaps a better example is "There is at least one Turing machine which halts." Now - in a precise sense - any possible logical deduction is paralleled by a proof that some specific machine halts, so if there are infinitely many "distinct" deductions at all, then there are infinitely many "distinct" proofs of this proposition.

EDIT: This is entirely tangential, but I think you may find it interesting. There is a strong and fruitful tradition in mathematical logic - especially on the constructive side - of drawing analogies between (or equating) proofs and algorithms; so an at-least-vaguely related question is, "How do we tell if two algorithms are the same?" This paper (http://research.microsoft.com/en-us/um/people/gurevich/Opera/192.pdf) by Andreas Blass, Nachum Dershowitz, and Yuri Gurevich argues that there is no entirely satisfactory answer to this question. I think at least one thing to take away from this is that one should not be cavalier about the notion of "distinct proof": finding a satisfactory such notion would be a huge advancement in logic!

Improve this answer
$\endgroup$
2
  • $\begingroup$ Thank you, Noah,actually it is motivated by ambiguity (whether there is a language with at least word having infinite ambiguities ).I will check if your post have solved my question about formal language.Yes,I tried to find one of such notion,but now it just shows such effort seems to be cavalier :( $\endgroup$
    – XL _At_Here_There
    Jun 23, 2013 at 2:26
  • $\begingroup$ Andreas,Nachum,and Yuri's article was published at Bellitin of symbolic logic or JSL,I had browsed it several years ago,but have gotten it and occasionally have found it today. $\endgroup$
    – XL _At_Here_There
    Jun 30, 2013 at 23:44
6
$\begingroup$

In any of the usual axiomatic systems (ZF set theory, Peano arithmetic, etc.), any proposition that has a proof at all will have infinitely many. The reason is that you can add irrelevant padding or stupid detours to any argument. To make a real question along these lines, you'd have to specify some notion of "genuinely different" proofs that prohibits such trivial variations.

Improve this answer
$\endgroup$
1
  • $\begingroup$ @Benjamin,yes,but i do not know how to define "genuinely different" proofs or " irrelevant padding or stupid detours ". $\endgroup$
    – XL _At_Here_There
    Jun 23, 2013 at 0:48
3
$\begingroup$

The question of whether two proofs are essentially the same is sometimes called "proof identity". It is an active topic in proof theory and there is an old MO thread with some references:

When are two proofs of the same theorem really different proofs

Improve this answer
$\endgroup$
0

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