Intuitionistic Games: Determinacy, Completeness, and Normalization
| Autor: | Paweł Urzyczyn |
|---|---|
| Rok vydání: | 2016 |
| Předmět: |
Discrete mathematics
Determinacy Sequential game Logic 010102 general mathematics Principal (computer security) ComputingMilieux_PERSONALCOMPUTING 0102 computer and information sciences Intuitionistic logic Mathematical proof 01 natural sciences TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES History and Philosophy of Science 010201 computation theory & mathematics Simple (abstract algebra) TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Completeness (order theory) 0101 mathematics Computational linguistics Mathematical economics Mathematics |
| Zdroj: | Studia Logica. 104:957-1001 |
| ISSN: | 1572-8730 0039-3215 |
| DOI: | 10.1007/s11225-016-9661-4 |
| Popis: | We investigate a simple game paradigm for intuitionistic logic, inspired by Wajsberg's implicit inhabitation algorithm and Beth tableaux. The principal idea is that one player, źros, is trying to construct a proof in normal form (positions in the game represent his progress in proof construction) while his opponent, źphrodite, attempts to build a counter-model (positions or plays can be seen as states in a Kripke model). The determinacy of the game (a proof-construction and a model-construction game in one) implies therefore both completeness and semantic cut-elimination. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Full text from SpringerLink