Dialogues, strategies, and intuitionistic provability (Q1061740)
From MaRDI portal
scientific article
| Language | Label | Description | Also known as |
|---|---|---|---|
| English | Dialogues, strategies, and intuitionistic provability |
scientific article |
Statements
Dialogues, strategies, and intuitionistic provability (English)
0 references
1985
0 references
This paper presents an equivalent theorem proof, namely that for every winning strategy in certain Lorenzen-style dialogue games there is a proof in LJ, the Gentzen consecution calculus for intuitionistic logic, and vice versa. There is an algorithm for transforming either into the other. In addition, for propositional languages, every LJ proof can be transformed into an irreducible normal form.
0 references
natural deduction
0 references
winning strategy
0 references
dialogue games
0 references
Gentzen consecution calculus
0 references
intuitionistic logic
0 references
irreducible normal form
0 references
