The infix operators and stand for conjunction (And) and disjunction (Or), while is the prefix operator for negation (Not). The next two inputs are equivalent:

You can use symbols instead of True and False. BooleanConvert symbolically evaluates many logical expressions. We expect to be :

Use Resolve to find truth values of quantified logical statements:

You can also use the existential quantifier to check that :

Mathematica also recognizes the logical operator Implies; you can use it to show :

Use SatisfiableQ to check if and satisfy :