Journal
JOURNAL OF LOGIC AND COMPUTATION
Volume 31, Issue 7, Pages 1608-1639Publisher
OXFORD UNIV PRESS
DOI: 10.1093/logcom/exab040
Keywords
Proof theory; neighbourhood semantics; intuitionistic logic; infinitary logic
Categories
Funding
- Academy of Finland [1308664]
Ask authors/readers for more resources
Neighbourhood semantics for intuitionistic logic extended with countable conjunctions and disjunctions is introduced and shown equivalent to topological semantics, with an indirect completeness proof as payoff. The new semantics is used to obtain a labelled sequent calculus with good structural properties, demonstrating admissibility of weakening and contraction, invertibility with preservation of height for each rule, and cut elimination. Finally, a direct Tait-Schutte-Takeuti style form of completeness via the extraction of a countermodel from a failed proof search is proved.
Neighbourhood semantics for intuitionistic logic extended with countable conjunctions and disjunctions is introduced and shown equivalent to topological semantics, with an indirect completeness proof as payoff. The new semantics is used to obtain a labelled sequent calculus with good structural properties. In particular, admissibility of weakening and contraction, invertibility with preservation of height for each rule and cut elimination are shown. Finally, a direct Tait-Schutte-Takeuti style form of completeness via the extraction of a countermodel from a failed proof search is proved.
Authors
I am an author on this paper
Click your name to claim this paper and add it to your profile.
Reviews
Recommended
No Data Available