...

КИВ:
Схемы аксиом (т.е. на место каждой переменной в схеме может быть поставлена любая формула КИВ, но одинаковые формулы на место одинаковых переменных)

Свойства "=>"
1. A => (B => A)
2. (A => B) => ((A => (B => C)) => (A => C)
Свойства "~"
3. ~~A => A
4. (A => B) => ((A => ~B) => ~A)
- эти 4 аксиомы (или из эквиваленты) обязательны для КИВ. Остальные аксиомы опциональны. Если мы вводим какую-то операцию (например, "&") то должны и добавить соответствующую группу аксиом:

Для "&":
(A & B) => A
(A & B) => B
A => (B => (A & B))

Для "v":
A => (A v B)
B => (A v B)
(A => C) => ((B => C) => ((A v B) => C))

Для "<=>":
(A <=> B) => (A => B)
(A <=> B) => (A <= B)
(A => B) => ((B => A) => (A <=> B))

Для "+" (XOR):
(A + B) => (~A => B)
(A + B) => (B => ~A)
(A => ~B) => ((~B => A) => (A + B))

Плюс правило вывода modus ponens:
A, A => B |- B

В интуиционизме делается одна замена. На место игрока номер 3:
3. ~~A => A
Приходит другой игрок номер 3:
3. ~A => (A => B)