Natural Deduction

The most basic construct in natural logic is a predicate.

A predicate takes entities in the domain of discourse and evaluates to either true, false or undefined.

You can bind a predicate (denoted by a name, e.g. Socrates) and a tuple of entities (denoted by a list of arguments, e.g. u) by making statements (denoted by a full-stop punctuation mark):

You can evaluate the mapping between predicates and entities with questions:

By default, if a proposition is left unstated, it is assumed to be undefined.

Composite propositions are formed with the help of operators.

You can state the refutation of a proposition with the not operator:

You can state the exclusive disjunction of propostions using the either-or operator:

You can state the conjunction of a series of propositions with the space operator:

You can state pressupositions using the if statement:

You can apply statements over all entities of the domain of discourse using the for operator:

You can ask questions with free variables that bind to entities in the domain of discourse:

Predicates can take an arbitrary number of arguments:

You can also ask questions about ifs and fors: