# Phobos: Proof Help

 There are four levels of proof available. (1) The definite level. This level only uses rules with `->` in them. To prove `x` at this level, type `+d x` (2) The plausible with ambiguity propagation (likely) level. This level uses all the rules and the priority (`>`) information. To prove x at this level type `+l x` (3) The plausible level without ambiguity propagation. This level uses all the rules and the priority (`>`) information. To prove x at this level type `+p x` (4) The supported level. This level uses all the rules and the priority (`>`) information. To prove x at this level type `+s x` This system can also prove that formulas cannot be proved. To prove that `+d x` cannot be proved, type `-d x` To prove that `+l x` cannot be proved, type `-l x` To prove that `+p x` cannot be proved, type `-p x` To prove that `+s x` cannot be proved, type `-s x` The positive (`+`) and negative (`-`) kinds of proof are related as follows. Let `a` be one of `d`, `l`, `p`, `s`. If `+a x` then not `-a x`. If `-a x` then not `+a x`. The levels of proof are related as follows. If `+d x` then `+l x`. If `+l x` then `+p x`. If `+p x` then `+s x`. If `-s x` then `-p x`. If `-d x` then `-l x`. If `-l x` then `-d x`.