International Workshop “Logic, Philosophy and Computation of Proofs” |
証明とカット消去の概念について議論することを目的として,「証明」の哲学と計算機科学についての国際ワークショップを開催いたします．
Saturday, November 28th
Sunday, November 29th
V. Michele Abrusci “Philosophical aspects of proof-nets”
Proof-nets are one of the most important innovations in mathematical logic which have been introduced by Jean-Yves in the framework of Linear Logic. My aim is to expose the aspects of proof-nets which are relevant from a philosophical point of view: some aspects are mathematical developments of old philosophical ideas concerning the concept of proof, other aspects open to new philosophical investigations on the concept of proof, other aspects may be presented as an original way to to deal with proofs in a kantian approach (i.e. to investigate the conditions of possibility of proofs).
Jean-Baptiste Joinet “Logic and Naturalness : from Gentzen to Girard”
J.-Y. Girard’s conception of logic originates in the critique of logical naturality made by G. Gentzen around 1930. Recently, Girard radicalized this critique and proposed a program for new foundations for logic, as a product of a general theory of interaction. In my talk, I will defend the thesis that this program tends to reunify the idea of natural logic and the idea of a logic of nature, via the notion of computation.
Paolo Pistone “Proofs, programs and the library of Babel”
Freely taking inspiration from a well-know novel by Borges, I will try to illustrate the opposition between two complementary (and irreducible, because of incompleteness) approaches in proof theory.
On the one hand, elementary techniques are used to capture the combinatorial and computational content of proofs ("le comment", Girard 2000). However, these techniques do not allow to trace the line between "meaningful proofs" and "meaningless codes", that is, between valid and invalid proofs.
On the other hand, non-elementary techniques are needed to prove foundational results, e.g. the Hauptsatz, which capture the validity and meaningfulness of proofs ("le pourquoi", Girard 2000); because of their infinitary character, however, these techniques run into a form of epistemological or "pragmatical" circularity.
Philip Scott “AF Inverse Monoids and the Coordinatization of MV-algebras”
MV-algebras (C.C. Chang, 1955) are the Lindenbaum-Tarski algebras associated to Lukasiewicz many-valued logics, analogous to the way that Boolean algebras are associated to classical
propositional logics. In the mid-1980’s, D. Mundici established an equivalence between the category of MV-algebras and the category of ℓ-groups (with archimedean order unit). This restricts to a
correspondence between countable MV-algebras and AF C*-algebras with lattice-ordered K0 group. We introduce a class of AF inverse Boolean monoids and prove a coordinatization theorem (in the spirit of von Neumann’s Continuous Geometry). This theorem states that every countable MV-algebra can be coordinatized (i.e. is isomorphic to the lattice of principal ideals of some AF Boolean inverse monoid).
Techniques involve use of Bratteli diagrams and colimits of semisimple inverse monoids. We shall illustrate this directly in the case of certain specific AF C*-algebras (e.g. the CAR algebra of a Fermi gas), using more specialized mathematical techniques. If time permits, we will mention related work, e.g. Effect Algebras (B. Jacobs) and a general coordinatization theorem in recent work of F. Wehrung.
[Joint work with Mark Lawson (Heriot-Watt)]
Masahiro Hamano “Geometry of Interaction for MALL via Hughes-van Glabbeek Proof-Nets”
We present a Geometry of Interaction (GoI) interpretation using Hughes-van Glabbeek (HvG) proof-nets for multiplicative additive linear logic (MALL). Our GoI captures dynamically HvG’s geometric correctness criterion–the toggling cycle condition–in terms of algebraic operators. Our new ingredient is a scalar extension of the *-algebra in Girard’s *-ring of partial isometries over a boolean polynomial ring with literals of eigenweights as indeterminates. In order to capture feedback arising from cuts, we construct a finer grained execution formula. The expansion of this execution formula is longer than that for collections of slices for multiplicative GoI, hence is harder to prove termination. Our GoI gives a dynamical, semantical account of boolean valuations (in particular, pruning sub-proofs), conversion of weights (in particular, alpha-conversion), and additive (co)contraction, peculiar to additive proof-theory. Termination of our execution formula is shown to correspond to HvG’s toggling criterion. The slice-wise restriction of our execution formula (by collapsing the boolean structure) yields the well known correspondence, explicit or implicit in previous works on multiplicative GoI, between the convergence of execution formulas and acyclicity of proof-nets. Feedback arising from the execution formula by restricting to the boolean structure yields definability of eigenweights among cuts from the rest of the eigenweights.
Kazushige Terui “Proof nets, boolean circuits and parsimonious modality’
As everyone notices, proof nets are similar to Boolean circuits. Indeed, an exact correspondence was established in (Terui 04). Furthermore, it was recently pointed out that constant depth proof nets correspond to *nonuniform* logspace predicates.
Then what about *uniform* logspace? The parsimonious lambda calculus of Damiano Mazza gives a good solution. The calculus is roughly multiplicative affine logic with a multi-functorial modality obeying Milner’s law: !A = A tensor !A.
Because of its limited power, each term in simply typed parsimonious calculus generates a constant-depth family of multiplicative proof nets. This leads to a tight correspondence among constant-depth proof nets, parsimonious terms and logspace. This talk is based on a joint work with Damiano Mazza.
Mitsuhiro Okada (Keio University, Chair)
Yutaro Sugimoto (Keio University)
Yuta Takahashi (Keio University)
主催：三田ロジックセミナー (科学研究費 新学術領域「予測・判断・意思決定の論理と計算」)
共催：慶應義塾大学 論理と感性のグローバルリサーチセンター
This document was translated from LATEX by HEVEA.