I'm studying Imre Lakatos' Proofs and Refutations for my master's thesis. Currently I address the concept of hidden lemmas, which I understand to mean unstated assumptions of a mathematical proof, which may turn out to be faulty, leading to counterexamples.
When contemplating hidden lemmas I postulated the following metamathematical statement: "It is impossible to explicitly list all hidden lemmas of a mathematical proof." or an alternate formulation of the statement as: "It is impossible to explicitly list all assumptions of a formal deduction."
- Are these two statements equal in the context of formal proofs?
For context, I'm primarily looking at mathematical formalism as it was in the beginning of the 20th century under the influence of David Hilbert and at Lakatos' criticism of it.
I am aware of Lakatos' interest in informal proofs, but for the sake of the argument I want to consider if a system where all assumptions are listable is possible. This leads to a follow-up question:
- Are there any logical systems where it is possible to list all assumptions of a formal deduction and to prove that such a list is complete?
My hunch is that even if such a list could be constructed, proving its completeness would be undecidable in the system itself. However, my own knowledge is not enough to prove this hunch, answer the first question or to give an example of or refute the statement implied in the second question.