0
$\begingroup$

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

$\endgroup$
  • 1
    $\begingroup$ You again ask a little weird question: define what is a minimal proof in the set of all proofs for a certain problem, please. $\endgroup$ – DonAntonio Apr 10 '17 at 13:54
  • $\begingroup$ A proof where you can't remove anything. $\endgroup$ – Jordi Apr 10 '17 at 13:55
  • 2
    $\begingroup$ @Jordi What do you mean by "remove" and what do you mean by "anything"? $\endgroup$ – 5xum Apr 10 '17 at 13:58
  • 1
    $\begingroup$ 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. $\endgroup$ – P Vanchinathan Apr 10 '17 at 13:58
  • 1
    $\begingroup$ 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. $\endgroup$ – Max Apr 10 '17 at 14:03
1
$\begingroup$

Yes. This was studied by Chaitin in his seminal paper Information-Theoretic Limitations of Formal Systems.

$\endgroup$
  • $\begingroup$ I'm guessing, though, that minimality is uncomputable at best... $\endgroup$ – W. Cadegan-Schlieper Apr 10 '17 at 18:38

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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