Tap the symbols in the bar under the editor and the letters on the keyboard or palette to build a formula, or just type on your keyboard. Press Enter to start a new line — useful for a multi-premise argument. Select text in the field and tap Negate to draw a line over it. The "Number lines" button automatically numbers each line (1), 2)…) and marks the last one as the conclusion (⊢).
What each button in the bar does. Select letters, symbols or spaces in the formula, then tap Negate: the line goes directly on the letters, or above a negation already in the selection — the editor works out which. Merge joins several separate negations (e.g. two individually negated letters) under one line. Remove negation takes off the top line (or, inside a negated group, removes the line from just the selected symbols). Two lines is the maximum, and a negation placed on part of an already-negated group always sits below the whole group's line.
A line drawn above a letter or group means "not" — the statement is false when the original is true.
One more line above letters or a group that are already negated — for example a second line over two already-negated letters. It isn't a double negation in the strict sense: it simply negates everything beneath it.
Takes off the top line over the selection. Inside a longer negated group, it removes the line from just the selected symbols. Greyed out until the selection has a line over it.
A→A→A
Joins several separate negations in the selection under one line over all of it. These are different formulas, so check it is what you mean. Greyed out until the selection contains at least two separately negated parts.
AB→AB
"If … then …" — reads left to right: the left side implies the right side.
"If and only if" — both sides are true together or false together.
"Or" — true when at least one side is true.
"And" — true only when both sides are true.
The turnstile — separates the premises on the left from the conclusion they entail on the right.
Three levels, from the inside out: parentheses ( ) group part of a formula, square brackets [ ] go around parentheses, braces { } go around square brackets: {[(A∧B)∨C]→D}.
The three icons at the left of the bar: Undo (up to 5 steps), Backspace (deletes the last character or block) and Clear (empties the whole formula).
The two arrows extend the selection one symbol at a time to the left or right (hold to repeat) — handy on a touch screen. The selection stays on a single line and its edges snap to whole symbols, and to the whole negated group if it reaches into one: that is what Negate acts on.
