# Do minimal proofs exist?

The same way that we have minimal elements in sets, are there minimal proofs in the set of all proofs of a particular problem?

• You again ask a little weird question: define what is a minimal proof in the set of all proofs for a certain problem, please. – DonAntonio Apr 10 '17 at 13:54
• A proof where you can't remove anything. – Jordi Apr 10 '17 at 13:55
• @Jordi What do you mean by "remove" and what do you mean by "anything"? – 5xum Apr 10 '17 at 13:58
• One can define length of a proof by the number of bytes of the TeX file needed to write it up. As the length is a positive integer possible to define minimal proofs. The problem would be a proof assuming and quoting a result and hence shorter will it be considered as really shorter than a proof that assumes nothing. This enters the realm of subjectivity. – P Vanchinathan Apr 10 '17 at 13:58
• One way to define it would be to say that a proof is a Gentzen-style tree, and that its length is the number of nodes in the tree. Then if a formula is a theorem, it has a proof and therefore the set $\{n \mid$ there exists a proof of length $n$ of said formula$\}$ would be non empty, and thus have a minimal element. With such a minimal element comes a minimal proof. I don't see what's bothering you all. Obviously the choice of the deduction system (Gentzen type, or anything else) is subjective, but once you have (sensibly) defined what you call a proof, this becomes a mathematical problem. – Max Apr 10 '17 at 14:03