Turning cycles into spirals Original Research Article

In [13] Parikh proved the first mathematical result about concrete consistency of contradictory theories. In [6] it is shown that the bounds of concrete consistency given by Parikh are optimal. This was proved by noting that very large numbers can be actually constructed through very short proofs. A more refined analysis of these short proofs reveals the presence of cyclic paths in their logical graphs. Indeed, in [6] it is shown that cycles need to exist for the proofs to be short. Here, we present a new sequent calculus for classical logic which is close to linear logic in spirit, enjoys cut-elimination, is acyclic and its proofs are just elementary larger than proofs in LK. The proofs in the new calculus can be obtained by a small perturbation of proofs in LK and they represent a geometrical alternative for studying structural properties of LK-proofs. They satisfy the constructive disjunction property and most important, simpler geometrical properties of their logical graphs. The geometrical counterpart to a cycle in LK is represented in the new setting by a spiral which is passing through sets of formulas logically grouped together by the nesting of their quantifiers.