[Back]

J. Bydzovsky:
"The Number of Axioms";
Talk: Celebrating 90 Years of Gödel´s Incompleteness Theorems, Nürtingen, Deutschland (invited); 2021-07-05 - 2021-07-09.

Following Goedel's incompleteness theorem no recursive notion of a proof can be efficient enough to ensure that every provable first-order formula A is also provable by a proof its length is recursively bounded in the number of symbols in A. However, this does not directly give much inside into the structure of long proofs when a particular proof system is fixed. I will comment on a new result together with Juan P. Aguilera and Matthias Baaz that for cut-free sequent calculus one of the sources of hardness to prove a formula is the number of (instances) of the axioms one needs to use. I will also comment on what the situation is for sequent proofs with cuts and sequent proofs from theories like Robinson arithmetic, PA or ZFC.