You'll need a modern, desktop browser with JavaScript enabled. Please keep in mind that this tool is essentially a compiler: it can tell you if you've written a program, but not whether you've written the right one. It can't tell you if you have the right answer.

All of the following are valid formulas (assuming you've selected the right preset):

• (T <-> F) and (T -> F)
• forall x. exists y. Loves(x, y)
• A x E y not x = y
• T iff F
• T <=> F
• ∃ x. ∀ y. (⊥ → ¬(x = y))
• \forall x \exists y (T \vee \neg (F \wedge T))
• exists x . (Add(x, x) = Add(x, Mult(x, x)))

You'll need to choose the preset corresponding to the problem you're working on. This will allow you to use the predicates and functions provided by that problem. For the "element of" symbol in 3.iii and 5.iv, ∈, you can write "in" or "∈".

Unfortunately, you can't write "∀ x ∈ S. (...)" for the time being. You'll have to leave off the "∈ S" part.

Tips:

• Click on an error to underline the relevant part of the expression, if it was able to render at all.
• Click on anything in the rendered expression to underline the innermost expression containing it. Essentially, you could generally add parentheses around underlined expressions without changing their meaning (though not around variables). For example, if you click on a ∀, it will underline everything that the ∀ applies to. This is especially helpful if you're unsure about operator precedence.
• The "parentheses depth" text which sometimes appears refers to the level of nesting that you're in at the end of what you have written. For example, "forall x. (T <-> (F or not F)" is at depth 1, meaning you need another end parenthesis to balance.
• This tool is not sufficiently sophisticated to handle expressions like "x+y". (It's harder than you'd think!) Instead, if you're checking one of the problems which involves those, you'll need to write "Add(x,y)" or "Mult(x,y)". To do "x+y+z", write "Add(x, y, z)", etc.
• Variables must be a single letter, lower or upper case, other than "A" or "E". Capitalization matters.
• In fact, capitalization matters everywhere. If you write "t iMpLiEs F", it's not going to work.
• If you're getting a SyntaxError and can't figure out why, ask on Piazza.