Glossary of Logic Symbols in Axiom Room

Capital letters are used as symbols for statements. Their meaning is not fixed. In one level, P may be the starting point, while another symbol becomes the statement to derive.

Example P → Q

Shows an implication. If the statement on the left is available, the statement on the right can be derived.

Example P → Q

Marks the negation of a statement. ¬P means that P does not hold.

Example ¬Q

A double negation returns the statement to its positive form.

Example ¬¬P becomes P

Shows a conjunction, which joins two statements into one.

Example P ∧ Q

Shows a disjunction. If one branch is eliminated, the other branch can remain.

Example P ∨ Q

If an implication is available and its left-side condition is also available, the right-side result can be derived.

Example P → Q and P produce Q

If the result of an implication is denied, the condition that would lead to it is denied too.

Example P → Q and ¬Q produce ¬P

Two implications can be joined when their middle statement matches.

Example P → Q and Q → R produce P → R

Two available statements can be joined into one conjunction.

Example P and Q produce P ∧ Q

From one joined statement, one of its parts can be taken out.

Example P ∧ Q produces P

If one branch of a disjunction is denied, the other branch can remain.

Example P ∨ Q and ¬P produce Q

A statement with two negations can be read again as a positive statement.

Example ¬¬P produces P

An implication can be rewritten by reversing its direction and negating both sides.

Example P → Q becomes ¬Q → ¬P

Marks a valid inference. In the Proof Log, the left side is the input, and the right side is the derived result.

Example P, P → Q ⊢ Q

Marks a block combination that does not match any inference rule in the current level.

Example P → Q and R do not automatically produce Q

Marks a target that has not yet been derived.

Example ? ⊢ Q

Marks the end of a proof. It appears when the level target has been derived.

Example ■ Q.E.D.

ASCII forms for logic symbols: -> means →, ~ means ¬, & means ∧, and v means ∨.

Example P -> Q is the same as P → Q

A symbolic block available from the start of a level. Premises are the starting material for deriving the target.

Example P → Q and P in Level 1

The statement that must be derived to complete a level.

Example target V in Level 18

A selectable button containing a logic statement. A block may be an initial premise or a derived result.

Example P ∧ Q, Q → R, ¬P

A new block created from a valid inference. It can be used in later steps.

Example from P → Q and P, derive Q

One step of drawing a conclusion from selected inputs.

Example selecting P → Q and P to produce Q

A sequence of connected inferences. The result of one step becomes input for the next.

Example P becomes Q, then Q becomes R

A panel that records newly derived results. An inference whose output already exists does not add a new entry.

Example P → Q, P ⊢ Q

The statistics for the level currently being played, including successful steps, invalid attempts, and hints used.

Example 2 successful steps, 0 invalid attempts, 1 hint used

The best level record saved in the browser. Records compare hints, invalid attempts, then successful steps.

Example a no-hint record is better than a record with one hint

A level completed with no invalid attempts and no hints. In the level selector, this status is marked with a star badge.

Example 0 invalid attempts and 0 hints used

A valid inference that creates a new block. An output that already exists is not counted as a new successful step.

Example P ∧ Q produces P

An attempt to select blocks that do not form a valid inference.

Example selecting two blocks that do not match the level rule

A logically valid step that does not help reach the target.

Example in Level 10, Q ∧ T acts as a decoy for target R

A direction that can be taken from one symbol or disjunction. Some branches lead to the target, while others only create side results.

Example from P, both P → Q and P → R are valid branches

A valid conclusion that is not the level target.

Example U in Level 17 is valid, but the target is V

The name of Level 11. It does not mean a valid consequence that does not help with the target.

Example P → Q produces Q, but the target is R

The name of Level 12. Among several valid steps, only one chain really leads to the target.

Example P → Q → T is needed, while P → R → S is only a detour

The name of Level 13. The target sits at the end of a longer chain, even though shorter valid branches exist.

Example P → Q → R → U

The name of Level 14. A disjunction must be narrowed before the path to the target opens.

Example P ∨ Q and ¬P leave Q

The name of Level 15. Several implications are combined into a shorter route before the final step.

Example P → Q and Q → R become P → R

The name of Level 16. Two simple statements must be joined before they match the condition of an implication.

Example P and Q become P ∧ Q

The name of Level 17. More than one block can be opened, but only one path leads to the target.

Example P ∧ R helps reach V, while Q ∧ S leads to a side result

The name of Level 18. It closes the logic wing with double negation, side branches, contraposition, and a compressed route.

Example Q → R and R → S are compressed before reaching V

The part of Axiom Room that contains symbolic inference levels. Players build steps from premises toward a target using available logic rules.

Example The logic wing closes with a longer proof.