Gianluigi Bellin

The goal of [3] is to sketch the construction of a syntactic categorical model of the bi-intuitionistic logic of assertions and hypotheses AH, axiomatized in a sequent calculus AH-G1, and to show that such a model has a chirality-like structure inspired by the notion of dialogue chirality by P-A. Melliès [8]. A chirality consists of a pair of adjoint functors L ⊣ R, with L: A → B, R: B → A, and of a functor (.)* : A → Bop(0,1) satisfying certain conditions. The definition of the logic AH in [3] needs to be modified so that our categories A and B are actually dual. With this modification, a more complex structure emerges.

We reconsider the pragmatic interpretation of intuitionistic logic [21] regarded as a logic of assertions and their justi cations and its relations with classical logic. We recall an extension of this approach to a logic dealing with assertions and obligations, related by a notion of causal implication [14, 45]. We focus on the extension to co-intuitionistic logic, seen as a logic of hypotheses [8, 9, 13] and on polarized bi-intuitionistic logic as a logic of assertions and conjectures: looking at the S4 modal translation, we give a de nition of a system AHL of bi-intuitionistic logic that correctly represents the duality between intuitionistic and co-intuitionistic logic, correcting a mistake in previous work [7, 10]. A computational interpretation of cointuitionism as a distributed calculus of coroutines is then used to give an operational interpretation of subtraction.Work on linear co-intuitionism is then recalled, a linear calculus of co-intuitionistic coroutines is de ned and a probabilistic interpretation of linear co-intuitionism is given as in [9]. Also we remark that by extending the language of intuitionistic logic we can express the notion of expectation, an assertion that in all situations the truth of p is possible and that in a logic of expectations the law of double negation holds. Similarly, extending co-intuitionistic logic, we can express the notion of conjecture that p, de ned as a hypothesis that in some situation the truth of p is epistemically necessary.

We consider a “polarized” version of bi-intuitionistic logic [5, 2, 6, 4] as a logic of assertions and hypotheses and show that it supports a “rich proof theory” and an interesting categorical interpretation, unlike the standard approach of C. Rauszer’s Heyting-Brouwer logic [28, 29], whose categorical models are all partial orders by Crolard’s theorem [8]. We show that P.A. Melliès notion of chirality [21, 22] appears as the right mathematical representation of the mirror symmetry between the intuitionistic and co-intuitionistc sides of polarized bi-intuitionism. Philosophically, we extend Dalla Pozza and Garola’s pragmatic interpretation of intuitionism as a logic of assertions [10] to bi-intuitionism as a logic of assertions and hypotheses. We focus on the logical role of illocutionary forces and justification conditions in order to provide “intended interpretations” of logical systems that classify inferential uses in natural language and remain acceptable from an intuitionistic point of view. Although Dalla Pozza and Garola originally provide a constructive interpretation of intuitionism in a classical setting, we claim that some conceptual refinements suffice to make their “pragmatic interpretation” a bona fide representation of intuitionism. We sketch a meaning-asuse interpretation of co-intuitionism that seems to fulfil the requirements of Dummett and Prawitz’s justificationist approach. We extend the Brouwer-Heyting-Kolmogorov interpretation to bi-intuitionism by regarding co-intuitionistic formulas as types of the evidence for them: if conclusive evidence is needed to justify assertions, only a scintilla of evidence suffices to justify hypotheses.

"We detail Abramsky's 'proofs-as-processes" paradigm for interpreting classical linear logic (CCL) [11] into a 'synchronous' version of the [pi]-calculus recently proposed by Milner [24]. The translation is given at the abstract level of proof structures. We give a detailed treatment of information flow in proof-nets and show how to mirror various evaluation strategies for proof normalization. We also give Soundness and Completeness results for the process-calculus translations of various fragments of CLL. The paper also gives a self-contained introduction to some of the deeper proof-theory of CLL, and its process interpretation."

Few systems for mechanical proof-checking have been used so far to transform formal proofs rather than to formalize informal arguments and to verify correctness. The unwinding of proofs, namely, the process of applying lemmata and extracting explicit values for the parameters within a proof, is an obvious candidate for mechanization. It corresponds to the procedures of Cut-elimination and functional interpretation in proof-theory and allows the extraction of the constructive content of a proof, sometimes yielding information useful in mathematics and in computing. ;Resource-aware logics restrict the number of times an assumption may be used in a proof and are of interest for proof-checking not only in relation to their decidability or computational complexity, but also because they efficiently solve the practical problem of representing the structure of relevance in a derivation. In particular, in Direct Logic only one subformula-occurrence of the input is allowed, and the connections established during a successful proof-verification can be represented on the input without altering it. In addition, the values for the parameters obtained from unwinding are read off directly. ;In Linear Logic, where classical logic is regarded as the limit of a resource-aware logic, long-standing issues in proof-theory have been successfully attacked. We are particularly interested in the system of proof-nets as a a multiple-conclusion Natural Deduction system for Linear Logic. ;In Part I of this thesis we present a new set of tools that provide a systematic and uniform approach to different resource-aware logics. In particular, we obtain uniqueness of the normal form for Multiplicative and Additive Linear Logic and an extension of Direct Logic of interest for nonmonotonic reasoning. In Part II we study Herbrand's Theorem in Linear Logic and the No Counterexample Interpretation in a fragment of Peano Arithmetic. As an application to Ramsey Theory we give a parametric form of the Ramsey Theorem, that generalizes the Infinite, the Finite and the Ramsey-Paris-Harrington Theorems for a fixed exponent.