We analyse the structure of propositional proofs in the sequent calculus focusing on the well-known procedures of Interpolation and Cut Elimination. We are motivated in part by the desire to understand why a tautology might be ‘hard to prove’. Given a proof we associate to it a logical graph tracing the flow of formulas in it . We show some general facts about logical graphs such as acyclicity of cut-free proofs and acyclicity of contraction-free proofs , and we give a (...) proof of a strengthened version of the Craig Interpolation Theorem based on flows of formulas. We show that tautologies having minimal interpolants of non-linear size must have proofs with certain precise structural properties. We then show that given a proof Π and a cut-free form Π′ associated to it , certain subgraphs of Π′ which are logical graphs correspond to subgraphs of Π which are logical graphs for the same sequent. This locality property of cut elimination leads to new results on the complexity of interpolants, which cannot follow from the known constructions proving the Craig Interpolation Theorem. (shrink)

Succinct representation and fast access to large amounts of data are challenges of our time. This unique book suggests general approaches of 'complexity of descriptions'. It deals with a variety of concrete topics and bridges between them, while opening new perspectives and providing promising avenues for the 'complexity puzzle'.

Ce livre propose une interprétation inédite de la biologie d'Aristote. Il montre que, dans la démarche aristotélicienne, à côté de la pensée discursive, oeuvre une pensée visuelle qui élabore une représentation de l'organisation spatiale du corps vivant, apportant ainsi une contribution décisive à la définition des deux tâches majeures de l'enquête scientifique aristotélicienne: l'explication causale et la détermination des genres.

We develop a combinatorial model to study the evolution of graphs underlying proofs during the process of cut elimination. Proofs are two-dimensional objects and differences in the behavior of their cut elimination can often be accounted for by differences in their two-dimensional structure. Our purpose is to determine geometrical conditions on the graphs of proofs to explain the expansion of the size of proofs after cut elimination. We will be concerned with exponential expansion and we give upper and lower bounds (...) which depend on the geometry of the graphs. The lower bound is computed passing through the notion of universal covering for directed graphs. In this paper we present ground material for the study of cut elimination and structure of proofs in purely combinatorial terms. We develop a theory of duplication for directed graphs and derive results on graphs of proofs as corollaries. (shrink)

Journal Name: Apeiron Issue: Ahead of print.

Any arbitrarily complicated non-oriented graph, that is a graph of arbitrarily large genus, can be encoded in a cut-free proof. This unpublished result of Statman was shown in the early seventies. We provide a proof of it, and of a number of other related facts.

Aristotle’s biology is based on his method of division of animal kinds by multiple differentiae. This results in complex clusters of non-subordinate terms, between which Aristotle seeks to establish universal correlations. The form of these, however, does not correspond to that prescribed by his theory of syllogism. Mereological relations between terms are not linear and quantification is far more complex than the distinction between universal and particular propositions. Thus the axiomatisation of Aristotle’s biology requires a tool designed for analysing such (...) complex universal correlations into valid syllogistic premises. Prosleptic-like premises turn out to be the solution outlined by Aristotle. They make it possible to handle both the logic of consequence which translates from and into mereological relations between term clusters, and the complex quantification required by division based on multiple differentiæ, through the instantiation of a variable ideally consisting of indivisible groups of animals. (shrink)

Two of Aristotle’s major legacies, namely, the theory of scientific syllogism and teleology seem to conflict on several planes. Indeed, an array of formal limitations prevents him from formalizing teleological explanations into scientific syllogisms, which are entirely absent from his works. To achieve this, Aristotle resorts to a different tool, the logic of ‘consequence’. This governs both the teleological relation between an end and a means that underlies necessity ‘from a hypothesis’—which is the necessity proper to living things—and a different (...) form of syllogisms, namely, syllogisms ‘from a hypothesis’. His guidelines in the first chapter of his Parts of Animals on the proper form of demonstration to be adopted in biology should be read as laying out the rules of inference for translating teleological explanations into syllogisms ‘from a hypothesis’. (shrink)

Many times in mathematics there is a natural dichotomy betweendescribing some object from the inside and from the outside. Imaginealgebraic varieties for instance; they can be described from theoutside as solution sets of polynomial equations, but one can also tryto understand how it is for actual points to move around inside them,perhaps to parameterize them in some way. The concept of formalproofs has the interesting feature that it provides opportunities forboth perspectives. The inner perspective has been largely overlooked,but in fact (...) lengths of proofs lead to new ways to measure informationcontent of mathematical objects. The disparity between minimallengths of proofs with and without ``lemmas'' provides an indicationof internal symmetry of mathematical objects and their descriptions.A principal observation of this paper is that mathematicalstructures can be embedded into spaces of logical formulae and inheritadditional structure from proofs. We shall look at finitely-generatedgroups, rational numbers and SL(2,Z), and examples fromtopology and analysis. (shrink)

Les cours sur la Logique transcendantale sont l'un des lieux de la production fichtéenne dans lequel le philosophe de Rammenau réfléchit sur le langage et en particulier sur la capacité performative de la parole. A travers la déconstruction du discours de la logique commune, déjà durement frappée dans les leçons de Zurich de 1794, articulée en trois moments principaux (identifiés comme processus ironique, inventio et ruse du langage), la Doctrine de la Science révèle le lien entre le mot, le concept (...) et l'intuition intellectuelle et exprime le besoin de subsumer le premier au concept correctement compris, de sorte qu'il puisse révéler la présence d'une pensée synthétique, dont le mot lui-même est l'image. (shrink)

The study investigates how the territorial community can influence the individual and social well-being of lesbian, gay, bisexual youth and especially the recognition of their feelings and the construction of their own identity as well as their needs to be socially recognized. This research focuses on the experiences of 30 LGB individuals, with a mean age of 25.07 years, living in urban and rural areas of Southern Italy. Focalized open interviews were conducted, and the Grounded Theory Methodology, supported by the (...) Atlas.ti 8.0 software, was used for data analysis. The textual material was first coded, and then codes were grouped into five macro-categories: Freedom of identity expression in the urban and rural context, identity construction and acceptance process, need of aggregation and identification with the LGB community, role of the interpersonal relationship in the process of identity acceptance, socio-cultural context, and LGB psychological well-being. The results showed a condition common to the two contexts that we can define as “ghettoization.” The young LGB is alone in the rural area due to a lack of places and people to identify with and greater social isolation. On the contrary, although there are more opportunities in the urban area, young people feel stigmatized and ghettoized because “their places” are frequented exclusively by the lesbian, gay, bisexual, transexual, queer community. The work will extensively discuss the limitations of the research, future proposals, and the practical implications of the results. (shrink)

We establish a connection between the geometric methods developed in the combinatorial theory of small cancellation and the propositional resolution calculus. We define a precise correspondence between resolution proofs in logic and diagrams in small cancellation theory, and as a consequence, we derive that a resolution proof is a 2-dimensional process. The isoperimetric function defined on diagrams corresponds to the length of resolution proofs.

There is an exponential speed-up in the number of lines of the quantified propositional sequent calculus over Substitution Frege Systems, if one considers proofs as trees. Whether this is true also for the number of symbols, is still an open problem.

The logical flow graphs of sequent calculus proofs might contain oriented cycles. For the predicate calculus the elimination of cycles might be non-elementary and this was shown in [Car96]. For the propositional calculus, we prove that if a proof of k lines contains n cycles then there exists an acyclic proof with O(k n+l ) lines. In particular, there is a polynomial time algorithm which eliminates cycles from a proof. These results are motivated by the search for general methods on (...) proving lower bounds on proof size and by the design of more efficient heuristic algorithms for proof search. (shrink)