Proof Theory for Positive Logic with Weak Negation
| Autor: | Almudena Colacito, Marta Bílková |
|---|---|
| Rok vydání: | 2019 |
| Předmět: |
Logic
Computer science 010102 general mathematics Sequent calculus Craig interpolation Mathematics - Logic 06 humanities and the arts Intuitionistic logic 0603 philosophy ethics and religion 16. Peace & justice 01 natural sciences Decidability TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES History and Philosophy of Science Fragment (logic) Negation Proof theory TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Computer Science::Logic in Computer Science 060302 philosophy FOS: Mathematics Calculus Sequent 0101 mathematics Logic (math.LO) |
| Zdroj: | Studia Logica. 108:649-686 |
| ISSN: | 1572-8730 0039-3215 |
| DOI: | 10.1007/s11225-019-09869-y |
| Popis: | Proof-theoretic methods are developed for subsystems of Johansson's logic obtained by extending the positive fragment of intuitionistic logic with weak negations. These methods are exploited to establish properties of the logical systems. In particular, cut-free complete sequent calculi are introduced and used to provide a proof of the fact that the systems satisfy the Craig interpolation property. Alternative versions of the calculi are later obtained by means of an appropriate loop-checking history mechanism. Termination of the new calculi is proved, and used to conclude that the considered logical systems are PSPACE-complete. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Full text from SpringerLink