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.
Pedicini, M., Piazza, M., Puite, Q.W.Q. (2021). On the number of provable formulas. In G.T. Luca Bellotti (a cura di), Fourth Pisa Colloquium in Logic, Language and Epistemology, Essays in Honour of Enrico Moriconi (pp. 145-166). Pisa : Edizioni ETS.
On the number of provable formulas
Marco Pedicini;
2021-01-01
Abstract
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.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
