1,721,006 research outputs found
A geometrical procedure for computing relaxation
No full textPermutative logic is a non-commutative conservative extension of linear logic suggested
by some investigations on the topology of linear proofs. In order to syntactically reflect
the fundamental topological structure of orientable surfaces with boundary, permutative
sequents turn out to be shaped like q-permutations. Relaxation is the relation induced on
q-permutations by the two structural rules divide and merge; a decision procedure for
relaxation has been already provided by stressing some standard achievements in theory
of permutations. In these pages, we provide a parallel procedure in which the problem at
issue is approached from the point of view afforded by geometry of 2-manifolds and solved
by making specific surfaces interact
Permutative Additives and Exponentials
No full textPermutative logic (PL) is a noncommutative variant of multiplicative
linear logic (MLL) arising from recent investigations concerning
the topology of linear proofs. Permutative sequents are structured as
oriented surfaces with boundary whose topological complexity is able to
encode some information about the exchange in sequential proofs. In this
paper we provide a complete permutative sequent calculus by extending
that one of PL with rules for additives and exponentials. This extended
system, here called permutative linear logic (PLL), is shown to be a
conservative extension of linear logic and able to enjoy cut-elimination.
Moreover, some basic isomorphisms are pointed out
Uniqueness of axiomatic extensions of cut-free classical propositional logic
Full text linkIn this paper, we prove that, for any cluster of extra-logical assumptions, there exists exactly one axiomatic (i.e., minimal) extension of classical propositional logic that admits cut elimination. As a corollary, it follows that classically equivalent formulas share the same axiomatization. The moral is that cut elimination “flattens” the specific information encoded by the logical structure of proper axioms
Rewriting systems for the surface classification theorem
No full textThe work reported in this paper refers to Massey’s proof of the surface classification theorem
based on the standard word-rewriting treatment of surfaces. We arrange this approach into
a formal rewriting system R and provide a new version of Massey’s argument. Moreover, we
study the computational properties of two subsystems of R: Ror for dealing with words
denoting orientable surfaces and Rnor for dealing with words denoting non-orientable
surfaces. We show how such properties induce an alternative proof for the surface
classification in which the basic homeomorphism between the connected sum of three
projective planes and the connected sum of a torus with a projective plane is not required
Unifying logics via context-sensitiveness
Full text linkThe goal of this article is to design a uniform proof-theoretical framework encompassing classical, non-monotonic and
paraconsistent logic. This framework is obtained by the control sets logical device, a syntactical apparatus for controlling
derivations.Abasic feature of control sets is that of leaving the underlying syntax of a proof system unchanged, while affecting
the very combinatorial structure of sequents and proofs. We prove the cut-elimination theorem for a version of controlled
propositional classical logic, i.e. the sequent calculus for classical propositional logic to which a suitable system of control
sets is applied. Finally, we outline the skeleton of a new (positive) account of non-monotonicity and paraconsistency in terms
of concurrent processes
A Deflationary Account of the Truth of the Gödel Sentence G
No full textWe give a negative answer to the question of whether our conviction about the truth of the G ̈odel sentence G involves a theory of truth beyond the deflationary theories. After discussing and dismissing Neil Tennant’s de- flationary account of incompleteness, we show how a new deflationary construal of the incompletability of formal systems can be framed in the setting of Peano Arithmetic augmented to include a constructive version of the ω-rule based on Herbrand’s notion of prototype proof
Computing Surfaces via pq-Permutations
No full textIn algebraic topology, compact two-dimensional manifolds
are usually dealt through a well-defined class of words denoting
polygonal presentations. In this article, we show how to eliminate the
useless bureaucracy intrinsic to word-based presentations by considering
very simple combinatorial structures called pq-permutations.
Thanks to their specific effectiveness, pq-permutations induce a
rewriting system P able to compute, in a very easy and intuitive way,
the quotient surface associated with any given polygonal presentation.
The system P is shown to enjoy both the fundamental computational
properties of strong normalization and strict strong confluence
- …
