On the number of provable formulas

This work is a tribute to the combinatorial nature of logical objects (formulas, sequents, proofs). In particular, we investigate the combinatorics of proof nets, that is pure geometrical objects, issued from the study of linear logic, intended to capture essential aspects of proofs in sequent calculus; in fact, proof nets can be obtained from proof structures (pure combinatorial nets of rules (or links)) by adding a constraint known as correctness criterion. In trying to establish the exact ratio between proof structures and proof nets in the multiplicative fragment of linear logic, we obtain an upper bound and a lower bound.