Relation between Semantics of Type Theory and its Syntactic Properties

1998年，我们获得了关于二阶λ-微积分句法性质的模型理论证明的一些结果。在通常的二阶λ微积分范畴论模型构造中，函数空间和二阶量化是用伴随性来定义的。但是我们考虑了用半伴随性代替通常结构中使用的伴随性所得到的结构，发现它具有强规范化证明和β-正规形式唯一性证明中常见的结构特征。当我们申请这个项目时，我们在1999年计划做的是将上述结果发展为CC和PTS。事实上，我们发现双范畴更适合描述证明CC强规格化所必需的结构，但是，为了表明我们关于句法性质的模型理论证明的总体计划可以应用于更广泛的领域，我们推迟了对发展的详细调查，并研究了子结构逻辑的性质。我们证明了在使用fl代数或so- monooid构造的语义结构中可以证明无切可证明性。通过这种构造，我们澄清了某些子结构逻辑的无切割可证性不成立的原因。在此基础上，我们构造了Kripke语义，并对其与直觉模态逻辑的Kripke语义的关系进行了观察。但是我们发现很难将直觉模态逻辑的Kripke语义推广到子结构逻辑的Kripke语义，因为直觉模态逻辑的Kripke语义是使用直觉模态逻辑特有的属性来构建的。我们还研究了具有显式环境的简单型λ微积分，证明了它具有合流性和强归一化性等基本性质。强规范化证明的思想来自语义，但目前完整的证明是纯语法的。

In 1998, we have obtained some results about model theoretic proof of syntactic properties of 2nd order λ-calculus. In the usual category theoretic model construction of 2nd order λ-calculus, function space and 2nd order quantification are defined using adjointness. But we considered the structure obtained by replacing adjointness used in the usual structure by sem-adjointness and found that it characterizes the structure common in the proof of strong normalization and that of uniqueness of β-normal form.When we applied for this project, what we planned to do in 1999 was to develop the above results to CC and PTS. In fact, we found that bicategory is more appropriate to describe the structure necessary to prove the strong normalization of CC. But, to show that our general plan about the model theoretic proof of syntactic properties can be applied to wider area, we postponed the detailed investigation of the development and studied the properties of substructural logics. We have shown that cut-free provability can be proved in the semantic structure that is constructed using FL-algebra or so-monoid. By this construction, we have clarified the reason why the cut-free provability does not hold for some of the substructural logics. Furthermore, we have constructed the Kripke semantics using this structure and made observations on the relationship with the Kripke semantics of intuitionistic modal logics. But we found that it is hard to generalize the Kripke semantics of intuitionistic modal logics to that of substructure logics, because the Kripke semantics of intuitionistic modal logics is constructed using the properties specific to intuitionistic modal logics.We have also studied the simply-typed λ-calculus with explicit environment and shown that fundamental properties such as confluence and strong normalizability hold. The idea of the proof of strong normalizability came from the semantics, but the completed proof is purely syntactical for now.