Selector proofs and the provability of consistency

Mathematical theories, such as formal arithmetic PA, have infinite sets of axioms, but a proof of a formula is compact, i.e., it involves only a finite number of axioms. Gödel's Second Incompleteness Theorem, which states that the consistency represented as a single formula is unprovable in PA, in fact rules out only compact proofs of consistency in PA, i.e., proofs of PA-consistency in finite fragments of PA. In mathematical practice, however, some proofs are not compact. For example, standard proofs of commonly known versions of Induction in arithmetic are not compact, since they require unbounded access to the axioms of PA. 

Building on Hilbert's efforts, we introduce  "selector proofs" that capture non-compact reasoning in a finite form. Selector proofs of universal statements "for all natural numbers n, F(n)" are finite constructive objects; they are checkable and formalizable in PA, and they secure the conventional provability of each F(n). Selector proofs do not extend PA, but rather reveal the hidden capability of PA to prove combinatorial properties, e.g., Induction, Consistency, etc., without their preliminary formalization as a single formula.

We offer a selector proof of consistency for PA, which can be formalized in PA itself. This refutes the famous unprovability of consistency thesis and removes the principal roadblock of the provability of consistency studies initiated by Hilbert in the 1920s.