The FOL Evaluator is a semantic calculator which will evaluate a wellformed formula of firstorder logic on a userspecified 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 wellformed 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  NonLogical 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 2Place Predicates  A, B, C, ... Z  
Biconditional  <>  
Existential Quantifier  E  
Universal Quantifier  A  
Identity Relation  =  
Absurdity/Falsum  # 
Here are some examples of wellformed 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 nonlogical constant the formula contains.
Notice that only binary connectives introduce parentheses, whereas quantifiers don't, so e.g. 'ExRxa' and 'Ex(Rxa & Fx)' are wellformed 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 1place predicate or a 2place predicate. Internally it therefore adds two versions of the predicate to the model, a 1place version and a 2place version, each with an empty extension. (Extensions for sentences and individual constants can't be empty, and neither can domains.)