# Is there an recursively axiomatized system with infinitely many proofs for some propositions or a proposition [closed]

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"

-

## closed as not a real question by Andreas Blass, Andrés E. Caicedo, Andrej Bauer, Mark Sapir, Andy PutmanJun 25 '13 at 16:06

It's difficult to tell what is being asked here. This question is ambiguous, vague, incomplete, overly broad, or rhetorical and cannot be reasonably answered in its current form. For help clarifying this question so that it can be reopened, visit the help center.If this question can be reworded to fit the rules in the help center, please edit the question.

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$. – Qiaochu Yuan Jun 23 '13 at 0:33
@Qiaochu,Sorry,what I want to know is not such a trivial argument,please see the edited post and the following answer and comments. – XL _at_China Jun 23 '13 at 1:00
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 – XL _at_China Jun 23 '13 at 1:18

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!

-
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 :( – XL _at_China Jun 23 '13 at 2:26
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. – XL _at_China Jun 30 '13 at 23:44

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.

-
@Benjamin,yes,but i do not know how to define "genuinely different" proofs or " irrelevant padding or stupid detours ". – XL _at_China Jun 23 '13 at 0:48

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

-
Thank you,I will check – XL _at_China Jun 23 '13 at 4:13