Craig interpolation in displayable logics
File(s)
Published version
Author(s)
Brotherston, James
Gore, Rajeev
Type
Report
Abstract
We give a general proof-theoretic method for establishing
Craig interpolation for displayable logics, based upon an analysis of the
individual proof rules of their display calculi. Using this uniform method,
we establish interpolation for a spectrum of display calculi differing in
their structural rules, including those for multiplicative linear logic, mul-
tiplicative additive linear logic and ordinary classical logic.
Our analysis at the level of proof rules also provides new insights into the
reasons why interpolation fails, or seems likely to fail, in many substruc-
tural logics. Specifically, we identify contraction as being particularly
problematic for interpolation except in special circumstances.
Craig interpolation for displayable logics, based upon an analysis of the
individual proof rules of their display calculi. Using this uniform method,
we establish interpolation for a spectrum of display calculi differing in
their structural rules, including those for multiplicative linear logic, mul-
tiplicative additive linear logic and ordinary classical logic.
Our analysis at the level of proof rules also provides new insights into the
reasons why interpolation fails, or seems likely to fail, in many substruc-
tural logics. Specifically, we identify contraction as being particularly
problematic for interpolation except in special circumstances.
Date Issued
2011-01-01
Citation
Departmental Technical Report: 11/1, 2011, pp.1-30
Publisher
Department of Computing, Imperial College London
Start Page
1
End Page
30
Journal / Book Title
Departmental Technical Report: 11/1
Copyright Statement
© 2011 The Author(s). This report is available open access under a CC-BY-NC-ND (https://creativecommons.org/licenses/by-nc-nd/4.0/)
Publication Status
Published
Article Number
11/1