Home > &c > FOL Evaluator
FOL Evaluator

The FOL Evaluator is a semantic calculator which will evaluate a well-formed formula of first-order logic on a user-specified model. In its output, the program provides a description of the entire evaluation process used to determine the formula's truth value. For a list of the symbols the program recognizes and some examples of well-formed formulas involving those symbols, see below. Click the "Sample Model" button for an example of the syntax to use when you specify your own model.


Enter a Model:
Enter a Formula:
  

Here is a list of the symbols the program recognizes (note that since the letter 'v' is used for disjunction, it cannot be used as a variable or individual constant):

Logical SymbolsNon-Logical Symbols
Negation~Individual Constantsa, b, c ... z (except v)
Conjunction&Variablesa, b, c ... z (except v)
DisjunctionvPropositional ConstantsA, B, C, ... Z
Conditional>1- and 2-Place PredicatesA, B, C, ... Z
Biconditional$
Existential QuantifierE
Universal QuantifierA
Identity Relation=
Absurdity/Falsum#

Here are some examples of well-formed formulas the program will accept:

If you load the "sample model" above, these formulas will all successfully evaluate in that model. In general, in order for a formula to be evaluable in a model, the model needs to assign an extension to every non-logical constant the formula contains.

Notice that only binary connectives introduce parentheses, whereas quantifiers don't, so e.g. 'ExRxa' and 'Ex(Rxa & Fx)' are well-formed but 'Ex(Rxa)' is not. In the above examples, I've left off the outermost parentheses on formulas that have a binary connective as their main connective (which the program allows). In general, the formal grammar that the program implements for complex wffs is:

One final point: if you load a model that assigns an empty extension to a predicate, the program has no way of anticipating whether you intend to use that predicate as a 1-place predicate or a 2-place predicate. Internally it therefore adds two versions of the predicate to the model, a 1-place version and a 2-place version, each with an empty extension. (Extensions for sentences and individual constants can't be empty, and neither can domains.)