Formula
(enter a formula manually)
K formula: (p → (q → p))
S formula: ((p → (q → r)) → ((p → q) → (p → r)))
Conjunction introduction: (p → (q → (p ∧ q)))
Conjunction elimination (left): ((p ∧ q) → p)
Conjunction elimination (right): ((p ∧ q) → q)
Disjunction introduction (left): (p → (p ∨ q))
Disjunction introduction (right): (q → (p ∨ q))
Implicational disjunction introduction: ((p → r) → ((q → r) → ((p ∨ q) → r)))
Implicational contraposition: ((p → q) → ((p → ¬q) → ¬p))
Implicational ex falso quodlibet: (¬p → (p → q))
K formula: (p → (q → p))
B formula: ((p → q) → ((r → p) → (r → q)))
W formula: ((p → (p → q)) → (p → q))
C formula: ((p → (q → r)) → (q → (p → r)))
S formula: ((p → (q → r)) → ((p → q) → (p → r)))
I formula: (p → p)
Weak excuded middle: (¬p ∨ ¬¬p)
Dummett's formula: ((p → q) ∨ (q → p))
Conditional excluded middle: ((p → q) ∨ (p → ¬q))
Scott's formula: (((¬¬p → p) → (p ∨ ¬p)) → (¬p ∨ ¬¬p))
Smetanich's formula: ((¬q → p) → (((p → q) → p) → p))
Notand implies ornot: (¬(p ∧ q) → (¬p ∨ ¬q))
Notor implies andnot: (¬(p ∨ q) → (¬p ∧ ¬q))
Andnot implies notor: ((¬p ∧ ¬q) → ¬(p ∨ q))
Ornot implies notand: ((¬p ∨ ¬q) → ¬(p ∧ q))
Peirce's formula: (((p → q) → p) → p)
Excluded middle: (p ∨ ¬p)
Double negation elimination: (¬¬p → p)
Modus ponens: (((p → q) ∧ p) → q)
Modus tollens: (((p → q) ∧ ¬q) → ¬p)
Hypothetical syllogism: (((p → q) ∧ (q → r)) → (p → r))
Disjunctive syllogism: (((p ∨ q) ∧ ¬p) → q)
Constructive dilemma: (((p → q) ∧ (r → s)) → ((p ∨ r) → (q ∨ s)))
Destructive dilemma: (((p → q) ∧ (r → s)) → ((¬q ∨ ¬s) → (¬p ∨ ¬r)))
KP: ((¬p → (q ∨ r)) → ((¬p → q) ∨ (¬p → r)))
WKP: ((¬p → (¬q ∨ ¬r)) → ((¬p → ¬q) ∨ (¬p → ¬r)))
McColl's Connexive Axiom 1: ((p → q) → ((q → r) → (p → r)))
McColl's Connexive Axiom 2: (((p → p) → q) → q)
McColl's Connexive Axiom 3: ((p → q) → ((p ∧ r) → (q ∧ r)))
McColl's Connexive Axiom 4: ((q ∧ q) → (p → p))
McColl's Connexive Axiom 5: ((p ∧ (q ∧ r)) → (q ∧ (p ∧ r)))
McColl's Connexive Axiom 6: ((p ∧ p) → ((p → p) → (p ∧ p)))
McColl's Connexive Axiom 7: (p → (p ∧ (p ∧ p)))
McColl's Connexive Axiom 8: (((p → ¬q) ∧ q) → ¬p)
McColl's Connexive Axiom 9: ((p ∧ ¬(p ∧ ¬q)) → q)
McColl's Connexive Axiom 10: ¬(p ∧ ¬(p ∧ p))
McColl's Connexive Axiom 11: ((¬p ∨ ((p → p) → p)) ∨ (((p → p) ∨ (p → p)) → p))
McColl's Connexive Axiom 12: ((p → p) → ¬(p → ¬p))
(P → ¬P)  (¬P → P): ((p → ¬p) ∨ (¬p → p))
Translation
Identity function
The GoedelGentzen negative translation
Double negate the whole formula
Double negate all subformulas
Negate atomic subformulas
Double negate atomic subformulas
Replace all atomic subformulas p by (p ∧ p)
Replace all atomic subformulas p by (p ∨ p)
Take the contrapositive of all implications
Take the contrapositive of all implications (but do nothing inside the formula)
Replace all atomic subformulas p by (p ∨ ¬p)
Take the converse of an implication (but do nothing to nonimplications)
Ruleset
Skeletal: Minimal structural rules
D: D10, D11, D12, and D13
E: D rules plus rule E
CL: E rules minus D11 and D12
N: D10 and D13
Extras
Standard Structural Rules
Experimental Rules
Heuristic Rules
D10
Proponent cannot assert an atomic formula before Opponent has asserted it.
D11
A player must defend against the most recent open attack.
D12
Attacks may be answered at most once.
D13
Proponent's assertions may be attacked at most once.
E
Opponent must react to the most recent statement by Proponent.
D10literal
Proponent may assert an atom only if Opponent has earlier asserted either that atom or its negation.
D11mostrecent
Defenses must be against the most recent attack (open or closed).
D11queue
Defenses must be against the earliest open attack.
D11Proponent
Proponent must defend against the most recent open attack.
D11Opponent
Opponent must defend against the most recent open attack.
Symmetric D13
Assertions can be attacked at most once
D12 (2)
Attacks may be answered at most twice.
D13 (2)
Proponent's assertions may be attacked at most two times.
D13 (3)
Proponent's assertions may be attacked at most three times.
D14
Proponent's attacks may be defended at most once.
No repetitions
Neither player may repeat moves (same stance, same reference, same statement).
Onorepeat
Opponent cannot repeat moves
Pnorepeat
Proponent cannot repeat moves
Play Style
Play a game as both Proponent and Opponent
Play a game as Proponent (Opponent will choose its moves randomly)
Play a game as Opponent (Proponent will choose its moves randomly)
Search for a winning strategy for Proponent
Search for a winning strategy for Opponent
[About]

[Contact]