Dialogues, strategies, and intuitionistic provability (Q1061740): Difference between revisions
From MaRDI portal
Set profile property. |
Set OpenAlex properties. |
||
| Property / full work available at URL | |||
| Property / full work available at URL: https://doi.org/10.1016/0168-0072(85)90016-8 / rank | |||
Normal rank | |||
| Property / OpenAlex ID | |||
| Property / OpenAlex ID: W2002823922 / rank | |||
Normal rank | |||
Revision as of 21:14, 19 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
