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 | |
| Biconditional | <> | |||
| Existential Quantifier | E | |||
| Universal Quantifier | A | |||
| Identity Relation | = | |||
| Absurdity/Falsum | # |
Here are some examples of well-formed formulas the program will accept:
- Fa > ~Raa
- ExRxa
- ExAy(Rxy <> Ryx)
- Ax(Fx > EyRxy) & EzRaz
- AxEyx=y
- AxAy(x=y > (Fx > Fy))
- Ex(P > Fx) > (P > ExFx)
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:
- φ := ~φ | (φ & φ) | (φ v φ) | (φ > φ) | (φ <> φ) | Eνφ | Aνφ |
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.)