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
))
Not-and implies or-not: (¬(
p
∧
q
) → (¬
p
∨ ¬
q
))
Not-or implies and-not: (¬(
p
∨
q
) → (¬
p
∧ ¬
q
))
And-not implies not-or: ((¬
p
∧ ¬
q
) → ¬(
p
∨
q
))
Or-not implies not-and: ((¬
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 Goedel-Gentzen 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 non-implications)
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.
D10-literal
Proponent may assert an atom only if Opponent has earlier asserted either that atom or its negation.
D11-most-recent
Defenses must be against the most recent attack (open or closed).
D11-queue
Defenses must be against the earliest open attack.
D11-Proponent
Proponent must defend against the most recent open attack.
D11-Opponent
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).
O-no-repeat
Opponent cannot repeat moves
P-no-repeat
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]