First-order models and evaluation

Change a model’s interpretations and calculate what terms denote, whether formulas are true, and which assignments satisfy an open formula.

Scope. Finite models over the supplied object palette and signature: constants LittleJimmy, MrSir, and Socrates; the unary function fatherOf; unary predicates Human and Mortal; binary predicates BiggerThan and Sibling. Each canvas has its own model. Truth is evaluated in that model.

Edit a model

Enable JavaScript to use the model canvas. The definitions and worked examples remain available.

Evaluate a term

Enable JavaScript to use the model canvas. The definitions and worked examples remain available.

Evaluate a formula

Enable JavaScript to use the model canvas. The definitions and worked examples remain available.

Find satisfying assignments

Enable JavaScript to use the model canvas. The definitions and worked examples remain available.

Using it

Modify opens the domain and interpretation controls. Choose a symbol, then select objects in argument order; a function takes one further selection for its value. View switches between facts, tables, graph, and sets.

Each canvas starts with an empty domain. Use Modify to add objects and assign interpretations. Enter your term or formula, then Check or Query. Open formulas have assignment choices. The step arrows show how the result follows from the interpretation. Changing the model clears the previous result; supply any missing interpretations before checking again.

In the book