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.
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 Symbols||Non-Logical Symbols|
|Negation||~||Individual Constants||a, b, c ... z (except v)|
|Conjunction||&||Variables||a, b, c ... z (except v)|
|Disjunction||v||Propositional Constants||A, B, C, ... Z|
|Conditional||>||1- and 2-Place Predicates||A, B, C, ... Z|
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.)