Axiom Room uses a small set of logical symbols to turn reasoning into playable blocks. This page is a compact glossary for the symbols that appear in the first twelve levels.
The symbols are not meant to make logic look distant or decorative. They are small machines. Each one changes how a statement can move, split, combine, or fail inside the room.
Core symbols
P
Q
R
S
TRead as: propositions
Basic statement blocks. They stand for simple claims without saying what the claims are about.
Example
P
→Read as: if... then...
Implication. The statement on the left leads to the statement on the right.
Example
P → Q
¬Read as: not
Negation. It denies a statement or marks that the statement is false.
Example
¬Q
¬¬Read as: not not
Double negation. In the game, it can be unwrapped back into the original statement.
Example
¬¬P becomes P
∧Read as: and
Conjunction. Both statements are joined into one block.
Example
P ∧ Q
∨Read as: or
Disjunction. At least one branch is available. If one branch is ruled out, the other branch can remain.
Example
P ∨ Q
⊢Read as: therefore / derives
The selected blocks produce a valid result.
Example
P, P → Q ⊢ Q
⊬Read as: does not derive
The selected blocks do not produce a valid inference in the current level.
Example
P → Q, Q ⊬ P
■ Q.E.D.Read as: proof complete
The target has been reached. The room accepts the proof.
Example
■ Q.E.D.
Rules used in the first twelve levels
Modus PonensAppears in: Levels 1, 4, 6, 8, 9, 10, 11, 12
If P leads to Q, and P is available, then Q follows.
Pattern
P → Q, P ⟶ Q
Modus TollensAppears in: Levels 2, 4
If P would lead to Q, but Q is false, then P cannot be accepted.
Pattern
P → Q, ¬Q ⟶ ¬P
Hypothetical SyllogismAppears in: Level 3
Two implications can be connected into a longer chain.
Pattern
P → Q, Q → R ⟶ P → R
Conjunction IntroductionAppears in: Level 5
If two statements are both available, they can be joined.
Pattern
P, Q ⟶ P ∧ Q
SimplificationAppears in: Level 6
A conjunction can release one of its parts.
Pattern
P ∧ Q ⟶ P
Disjunctive SyllogismAppears in: Level 7
If one branch of an or-statement is denied, the other branch remains.
Pattern
P ∨ Q, ¬P ⟶ Q
Double NegationAppears in: Level 8
A statement denied twice returns to the original statement.
Pattern
¬¬P ⟶ P
ContrapositionAppears in: Level 9
An implication can be rewritten by reversing and negating both sides.
Pattern
P → Q ⟶ ¬Q → ¬P
Reading a proof block
A proof in Axiom Room is built by selecting compatible symbolic blocks. When the selection is valid, the game produces a new block. When the selection reaches the target, the level is complete.
For example:
P → Q
PRule: Modus Ponens
From an available implication and its starting statement, the game yields the valid consequence.
Result
Q
P → Q
¬QRule: Modus Tollens
If the consequence fails, the original statement must also be rejected.
Result
¬P
P ∧ QRule: Simplification
A conjunction can be opened to retrieve one of its parts when the proof needs it.
Result
P
In Axiom Room, a valid move is not always the winning move. Some levels include correct detours, decoys, or statements that lead away from the target.
Small note
The first twelve levels are intentionally narrow. They focus on a few basic moves in propositional logic: following implications, denying consequences, joining statements, splitting conjunctions, eliminating branches, and recognizing proof status.
The goal is not to memorize symbols like museum labels. The goal is to feel how a proof moves.