Name
Abstract | ||
|---|---|---|
This paper shows the equivalence for provability between two infinitary systems with the ω-rule. One system is the positive one-sided fragment of Peano arithmetic without Exchange rules. The other system is two-sided Heyting Arithmetic plus the law of Excluded Middle for Σ10 -formulas, and it includes Exchange. Thus, the logic underlying positive Arithmetic without Exchange, a substructural logic, is shown to be a logic intermediate between Intuitionism and Classical Logic, hence a subclassical logic. As a corollary, the authors derive the equivalence for positive formulas among provability in those two systems and validity in two apparently unrelated semantics: Limit Computable Mathematics, and Game Semantics with 1-backtracking. |
Year | DOI | Venue |
|---|---|---|
2007 | 10.1007/978-3-540-76637-7_18 | APLAS |
Keywords | Field | DocType |
infinitary system,positive one-sided fragment,subclassical logic,classical logic,positive arithmetic,limit computable mathematics,positive formula,substructural logic,game semantics,exchange rule,peano arithmetic | Provability logic,Intuitionistic logic,Second-order logic,Computer science,True arithmetic,Arithmetic,Substructural logic,Many-valued logic,Heyting arithmetic,Intermediate logic | Conference |
Volume | ISSN | ISBN |
4807 | 0302-9743 | 3-540-76636-7 |
Citations | PageRank | References |
4 | 0.65 | 9 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Stefano Berardi | 1 | 373 | 51.58 |
| Makoto Tatsuta | 2 | 111 | 22.36 |