Dialogues, strategies, and intuitionistic provability (Q1061740): Difference between revisions
From MaRDI portal
Added link to MaRDI item. |
Set profile property. |
||
| Property / MaRDI profile type | |||
| Property / MaRDI profile type: MaRDI publication profile / rank | |||
Normal rank | |||
Revision as of 03:04, 5 March 2024
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
