Dialogical Logic

Origin. Lorenzen, Lorenz (1960s). Erlangen school. Game semantics. Dialogue games. Foundation of constructive semantics.

Models. Logic as dialogue game. Proponent defends thesis. Opponent attacks. Winning strategy = validity. Constructive and classical variants.

Formalism.

Players: P (Proponent): defends thesis. O (Opponent): attacks thesis. Alternating moves. Dialogue.

Particle rules (attacks/defenses): A ∧ B: O chooses, P defends chosen conjunct. A ∨ B: P chooses, defends chosen disjunct. A → B: O asserts A, P must defend B. ¬A: O asserts A, P must show contradiction. ∀x.A: O chooses term, P defends instance. ∃x.A: P chooses term, defends instance.

Structural rules: Turn-taking. When P can use O's assertions. Winning conditions. Different rule sets → different logics.

Intuitionistic vs classical: Intuitionistic: P may use only last O statement. Classical: P may use any O statement. Structural rule difference. Game semantics.

Winning: P wins if dialogue ends with O unable to respond. O wins if P unable to respond. Validity = P has winning strategy. Regardless of O's moves.

Formal vs material: Formal dialogue: only logical structure. Material dialogue: non-logical content. Formal: P wins by form alone. Logic proper.

Extensions: Modal dialogues. Relevance dialogues. Linear logic dialogues. Flexible framework.

Symbols.

Symbol	Unicode	Name	Meaning
∧	U+2227	Conjunction	O chooses the conjunct P must defend
∨	U+2228	Disjunction	P chooses the disjunct to defend
→	U+2192	Conditional	O grants the antecedent, P must defend the consequent
¬	U+00AC	Negation	O asserts the negatum; P has no defence, only counterattack
∀	U+2200	Universal quantifier	O chooses the instance
∃	U+2203	Existential quantifier	P chooses the witness
P	—	Proponent	The player defending the thesis
O	—	Opponent	The player attacking it
!	—	Assertion	A move putting forward a formula
?	—	Attack	A move challenging a formula
A, B	—	Formula variables	The contents of moves
x	—	Individual variable	Bound by the quantifier rules

Metatheory. The framework separates two kinds of rule. Particle rules fix how each connective is attacked and defended and are meant to constitute its meaning; structural rules govern the shape of the dialogue — who moves when, which earlier assertions may be reused, and how often a formula may be attacked. Felscher (Annals of Pure and Applied Logic 28, 1985) proved the central result: a formula is intuitionistically valid exactly when the Proponent has a winning strategy in the dialogue game under the intuitionistic structural rules, and his proof goes through a translation between winning strategies and cut-free derivations in Gentzen's sequent calculus. Classical validity is obtained by one change to the structural rules, allowing the Proponent to defend against any earlier attack rather than only the most recent, with the particle rules untouched. Rahman and Rückert extended the method to modal and relevance logics by further structural variation.

Applies to. Proof theory. Game semantics. Constructive logic. Argumentation.

Limitations. The logic obtained is fixed by the structural rules, not by the particle rules that are supposed to give the connectives their meaning: intuitionistic and classical dialogues share every particle rule and differ only in which earlier assertions the Proponent may answer. That undercuts the framework's philosophical claim, since the meaning-constitutive component leaves the logic undetermined. The rule sets are also fragile — repetition ranks and other bookkeeping conditions must be imposed to keep dialogues finite, and small variations validate formulas that are not valid in any recognized system, so the correct rules are identified by checking that they yield the intended logic. Strategies are not proofs: the correspondence with sequent derivations holds only after quotienting away move orderings the game distinguishes and proof theory does not.