Relation between Semantics of Logical System and its Syntactic Properties

点击翻译按钮获取中文摘要

We have investigated how the cut elimination operations of the modal substructural logic can be regarded as computation rules, by proving the cut elimination theorem and assigning terms. We can give an integrated viewpoint to the similar researches on the computational meaning of the intuitionistic linear logic and the intuitionistic modal logic, because the modal substructural logic contains the intuitionistic linear logic and the intuitionistic modal logic as special cases. Many such researches done so far are based on natural deduction, but we have assigned terms to the modal substructural logic given in the sequent calculus style. Since the cut rule corresponds to the explicit substitution in this case, we were able to apply the results about the explicit substitution to obtain a term assignment to the intuitionistic modal logic and cut elimination operations as computation rules. We have proved the cut-free provability theorem in general case, but we need to continue the research on the concrete cut elimination operations and its properties.We have also studied about the extension of the typed λ-calculus with explicit substitution and proposed the system with first-class contexts. A context is a λ-term with holes and it is introduced to implement the meta-level operation within the system. In the system, we cannot use the traditional substitution operation that uses α-conversion, so gave a new method of defining substitution where we rename free variables. We have shown that the system has good properties such as confluence and strong normalizability and elaborated the conservativity theorem over the simply typed λ-calculus by taking account of α-conversions.