7 found
Order:
  1.  7
    Softness of MALL Proof-Structures and a Correctness Criterion with Mix.Masahiro Hamano - 2004 - Archive for Mathematical Logic 43 (6):751-794.
    We show that every MALL proof-structure [9] satisfies the property of softness, originally a categorical notion introduced by Joyal. Furthermore, we show that the notion of hereditary softness precisely captures Girard’s algebraic restriction of the technical condition on proof-structures. Relying on this characterization, we prove a MALL+Mix sequentialization theorem by a proof-theoretical method, using Girard’s notion of jump. Our MALL+Mix correctness criterion subsumes the Danos/Fleury-Retoré criterion [6] for MLL+Mix.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   4 citations  
  2.  15
    A Categorical Semantics for Polarized MALL.Masahiro Hamano & Philip Scott - 2007 - Annals of Pure and Applied Logic 145 (3):276-313.
    In this paper, we present a categorical model for Multiplicative Additive Polarized Linear Logic , which is the linear fragment of Olivier Laurent’s Polarized Linear Logic. Our model is based on an adjunction between reflective/coreflective full subcategories / of an ambient *-autonomous category . Similar structures were first introduced by M. Barr in the late 1970’s in abstract duality theory and more recently in work on game semantics for linear logic. The paper has two goals: to discuss concrete models and (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  3.  30
    A Direct Independence Proof of Buchholz's Hydra Game on Finite Labeled Trees.Masahiro Hamano & Mitsuhiro Okada - 1998 - Archive for Mathematical Logic 37 (2):67-89.
    We shall give a direct proof of the independence result of a Buchholz style-Hydra Game on labeled finite trees. We shall show that Takeuti-Arai's cut-elimination procedure of $(\Pi^{1}_{1}-CA) + BI$ and of the iterated inductive definition systems can be directly expressed by the reduction rules of Buchholz's Hydra Game. As a direct corollary the independence result of the Hydra Game follows.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  4.  5
    Z-Modules and Full Completeness of Multiplicative Linear Logic.Masahiro Hamano - 2001 - Annals of Pure and Applied Logic 107 (1-3):165-191.
    We prove that the full completeness theorem for MLL+Mix holds by the simple interpretation via formulas as objects and proofs as Z-invariant morphisms in the *-autonomous category of topologized vector spaces. We do this by generalizing the recent work of Blute and Scott 101–142) where they used the semantical framework of dinatural transformation introduced by Girard–Scedrov–Scott , Logic from Computer Science, vol. 21, Springer, Berlin, 1992, pp. 217–241). By omitting the use of dinatural transformation, our semantics evidently allows the interpretation (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  5.  12
    A Relationship Among Gentzen's Proof‐Reduction, Kirby‐Paris' Hydra Game and Buchholz's Hydra Game.Masahiro Hamano & Mitsuhiro Okada - 1997 - Mathematical Logic Quarterly 43 (1):103-120.
    We first note that Gentzen's proof-reduction for his consistency proof of PA can be directly interpreted as moves of Kirby-Paris' Hydra Game, which implies a direct independence proof of the game . Buchholz's Hydra Game for labeled hydras is known to be much stronger than PA. However, we show that the one-dimensional version of Buchholz's Game can be exactly identified to Kirby-Paris' Game , by a simple and natural interpretation . Jervell proposed another type of a combinatorial game, by abstracting (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  6.  4
    A Direct Independence Proof of Buchholz's Hydra Game on Finite Labeled Trees.Masahiro Hamano & Mitsuhiro Okada - 2001 - Bulletin of Symbolic Logic 7 (4):534-535.
    Direct download  
     
    Export citation  
     
    Bookmark  
  7.  6
    A Phase Semantics for Polarized Linear Logic and Second Order Conservativity.Masahiro Hamano & Ryo Takemura - 2010 - Journal of Symbolic Logic 75 (1):77-102.
    This paper presents a polarized phase semantics, with respect to which the linear fragment of second order polarized linear logic of Laurent [15] is complete. This is done by adding a topological structure to Girard's phase semantics [9]. The topological structure results naturally from the categorical construction developed by Hamano—Scott [12]. The polarity shifting operator ↓ (resp. ↑) is interpreted as an interior (resp. closure) operator in such a manner that positive (resp. negative) formulas correspond to open (resp. closed) facts. (...)
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark