Source author record

Michele Basaldella

Michele Basaldella appears in the imported research catalog. Authorship, coauthor and topic links are available while profile ownership is still unclaimed.

ResearcherUnclaimed source record

Logic in Computer Science

Catalog footprint

What is connected

3works

1topics

2close collaborators

Actions

Connect this record

Open graph Browse works

Inspect adjacent papers, topics, institutions and collaborators without losing the researcher page.

Building this map preview

BZPEER is loading the nearby papers, people, topics and institutions for this page.

preprint2014arXiv

Infinitary Classical Logic: Recursive Equations and Interactive Semantics

In this paper, we present an interactive semantics for derivations in an infinitary extension of classical logic. The formulas of our language are possibly infinitary trees labeled by propositional variables and logical connectives. We show that in our setting every recursive formula equation has a unique solution. As for derivations, we use an infinitary variant of Tait-calculus to derive sequents. The interactive semantics for derivations that we introduce in this article is presented as a debate (interaction tree) between a test << T >> (derivation candidate, Proponent) and an environment << not S >> (negation of a sequent, Opponent). We show a completeness theorem for derivations that we call interactive completeness theorem: the interaction between << T >> (test) and << not S >> (environment) does not produce errors (i.e., Proponent wins) just in case << T >> comes from a syntactical derivation of << S >>.

preprint2011arXiv

Ludics with repetitions (Exponentials, Interactive types and Completeness)

Ludics is peculiar in the panorama of game semantics: we first have the definition of interaction-composition and then we have semantical types, as a set of strategies which "behave well" and react in the same way to a set of tests. The semantical types which are interpretations of logical formulas enjoy a fundamental property, called internal completeness, which characterizes ludics and sets it apart also from realizability. Internal completeness entails standard full completeness as a consequence. A growing body of work start to explore the potential of this specific interactive approach. However, ludics has some limitations, which are consequence of the fact that in the original formulation, strategies are abstractions of MALL proofs. On one side, no repetitions are allowed. On the other side, the proofs tend to rely on the very specific properties of the MALL proof-like strategies, making it difficult to transfer the approach to semantical types into different settings. In this paper, we provide an extension of ludics which allows repetitions and show that one can still have interactive types and internal completeness. From this, we obtain full completeness w.r.t. a polarized version of MELL. In our extension, we use less properties than in the original formulation, which we believe is of independent interest. We hope this may open the way to applications of ludics approach to larger domains and different settings.

preprint2010arXiv

On the meaning of logical completeness

Goedel's completeness theorem is concerned with provability, while Girard's theorem in ludics (as well as full completeness theorems in game semantics) are concerned with proofs. Our purpose is to look for a connection between these two disciplines. Following a previous work [3], we consider an extension of the original ludics with contraction and universal nondeterminism, which play dual roles, in order to capture a polarized fragment of linear logic and thus a constructive variant of classical propositional logic. We then prove a completeness theorem for proofs in this extended setting: for any behaviour (formula) A and any design (proof attempt) P, either P is a proof of A or there is a model M of the orthogonal of A which defeats P. Compared with proofs of full completeness in game semantics, ours exhibits a striking similarity with proofs of Goedel's completeness, in that it explicitly constructs a countermodel essentially using Koenig's lemma, proceeds by induction on formulas, and implies an analogue of Loewenheim-Skolem theorem.