An interpretation is an assignment of meaning to all the symbols of a formal language. [Wikipedia]
An interpretation often (but not always) provides a way to determine the truth values of formulae in a language.
If a given interpretation assigns the value true to a formula, the interpretation is called a model of that formula.
There are other (than determining truth values) ways models can be useful.
The information required to record a derivation is, minimally, the domain of the interpretation, and the mapping of symbols applied to domain elements, to domain elements (constatnts and funtions) or truth values (predicates). Other useful information that might be recorded includes: the role of each interpretation formula; properties of the domain elements; the worlds of Kripke interpretations; the accessibility relation between works of Kripke interpretations.
Now:
Read the Quick Guide for writing interpretations.
Read on ...
Consider the following FOF problem. It is CounterSatisfiable, i.e., there is a model for the axioms and negated conjecture.
Here is a model in the new format, in a single annotated formula with the role interpretation. Note how the use of "distinct object"s makes the domain elements distinct.
The verification proof problem FOF_Finite_Coarse.s.p can be proved by Vampire.
The parts of a single interpretation formula can be separated out at varying levels of granularity, using subroles. At a medium grained level (which seems to be the best) the domain and mappings can be separated:
At a fine grained level the domain and mappings can be separated by symbol:
The new format for interpretations can also be used for saturations that induce a set of Herbrand interpretations, by giving the saturation formulae the role interpretation-herbrand. (the -herbrand is optional but useful). This saturation was created by E.
The consistency of the interpretation formulae can be confirmed by Vampire.
The verification proof problem FOF_Saturation.s.p can be proved by E.
The new format for interpretations can also be used for formulae that induce a set of Herbrand interpretations, by giving the formulae the role interpretation-herbrand (the -herbrand is optional but useful). This set of formulae is a modified version of the Herbrand-formulae created by iProver.
The consistency of the interpretation formulae can be confirmed by Vampire.
The verification proof problem FOF_Formulae.s.p can be proved by Vampire.
The example of a finite FOF interpretation clearly points to the need for types. Here's a problem with types:
A finite interpretation - a countermodel for the conjecture - is .shown here. Note how using separate types makes it necessary to add type promotion bijections to raise domain elements from domain types to term types, so that it's possible to reuse the problem's functions and predicates and keep things well typed.
The consistency of the interpretation formula can be confirmed by Vampire.
The verification proof problem TFF_Finite.s.p can be proved by Vampire.
The domain and mappings parts of an interpretation can be combined:
The parts of an interpretation formula can be separated out using subroles. The types of the symbols and the types of the domain must be given.
The use of separate domain types makes the use of quantification clearly possible.
When the domain elements are complex, or of a defined type like $int, then the use of type promotions functions is necessary. In simple cases it is possible to use even the problem types for domains elements, if you don't get confused between the domain elements and the constants of the language. Here's an example.
The consistency of the interpretation formula can be confirmed by Vampire.
The verification proof problem TFF_Finite.s.p can be proved by Vampire.
That representation blurs the distinction between terms and domain elements. A clearer alternative is to use typed "distinct objects", but they are not yet formally part of the TFF language. Progress is being made with developers to allow them. Here's an example of how they will be used.
The following TH0 problem is CounterSatisfiable, i.e., there is a model for the axioms and negated conjecture.
Here's a finite model.
The verification proof problem THF_Finite.s.p can be proved by Vampire.
Consider the following TFF example that requires an integer size domain.
Here's a model using closed terms representing Peano numbers as the domain elements.
The consistency of the interpretation formula cannot be confirmed by any ATP system I have.
The verification proof problem TFF_Peano.s.p can be proved by Vampire.
Here's a model using the integers for the domain elements.
The consistency of the interpretation formula cannot be confirmed by any ATP system I have.
TFF_Integer.s.p is the proof problem to verify the countermodel.
The consistency of the proof problem's axioms cannot be confirmed by any ATP system I have.
The verification proof problem can be proved by Vampire.
Finite and infinite domains can be mixed. Here's a problem that can be proven by Vampire. With the conjecture modified as below, it has a countermodel with integer domains for the X and Y positions (mimicing the logic), and a finite domain for the Z level.
Here's the countermodel.
The consistency of the interpretation formula can be confirmed by Z3 (and not by Vampire).
The verification proof problem TFF_Mixed.s.p can be proved by Vampire.
This can be done in only a typed logic.
Kripke interpretations are defined in interpretation formulae. Four new defined symbols are used:
The defined type $world for worlds. Different constants of type $world are known to be unequal.
The defined predicate $accessible_world of type ($world * $world) > $o to specify accessibility between worlds.
The defined constant $local_world of type $world that identifies the world in which the conjecture is proved.
The defined predicate $in_world of type ($world * formula) > $o to provide worldly scope for the formula that defines the Tarskian interpretation in the specified world.
The logic specification of the problem is included as a comment, because the interpretation formulae under-specify the logic, e.g., it's usually not possible to see whether an interpretation was meant to exemplify a S5 logic specification or a K logic specification - in both cases the concrete model could interpret the accessibility relation as equivalence relation (this is required for S5 but it is also OK for K).
Here's a non-theorem. Note that there are only global axioms and a local conjecture, which is the TPTP standard for non-classical logic problems.
Here's the countermodel.
The consistency of the interpretation formula can be confirmed by Vampire.
The NXF verification proof problem NXF_Finite-Finite-Global.s.p can be proved by Leo-III.
Here's an interpretation for that signature with a varying-flexible logic, using various possible techniques in an interpretation representation. Note that the types are distinguished using the interpretation subrole, which is necessary for processing interpretations with flexible designation.
Here's a problem that can be proven by Leo-III. Note that it has both global and local axioms (contrary to the standard case for proving, where all the axioms are global). With the conjecture modified as below, it has a countermodel with a finite number of worlds each of which has a finite domain.
After using NTF2THF to embed the problem into TH0, Nitpick finds a countermodel that I converted by hand into TPTP format.
The consistency of the interpretation formula can be confirmed by Vampire.
Here's a problem that can be proven by Leo-III. With the conjecture modified as below, it has a countermodel that requires (I think, at least it uses) only two worlds, and they have infinite domains because sequences of tosses are infinite and different sequences are unequal.
After using NTF2THF to embed the problem into TH0, Nitpick cannot find a countermodel ... as expected ... Nitpick can find only finite models. So I hand-rolled a countermodel. In the countermodel sequences of tosses are represented by integers, with the null sequence represented by 1. The encoding is easy to see in binary, reading the tosses left-to-right and the bits right-to-left. If the last bit is 0 a head was tossed, if 1 a tail was tossed: null = 1 = 0001, head = 2 = 0010, tail = 3 = 0011, head-head = 4 = 0100, head-tail = 5 = 0101, tail-head = 6 = 0110, tail-tail = 7 = 0111, head-head-head = 8 = 1000, head-head-tail = 9 = 1001, head-tail-head = 10 = 1010, head-tail-tail = 11 = 1011, tail-head-head = 12 = 1100, etc, etc. The local world tosses a sequence of heads, interpreted as integer domain elements that are powers of 2. The other world first tosses a tail, represented by 3, and then tosses all heads, interpreted as integer domain elements that are powers of 2 multiplied by 3. There is no definition of sequences interpreted as integer domain elements less or equal to 0, but they are not "all_heads".
The consistency of the interpretation formula cannot be confirmed by any ATP system I have.
This example requires (I think) an infinite number of worlds. The interpretation in the local world will have an infinite domain, but all the other worlds' domains need only a single element (one of the domain elements from the local world). All the domain elements of the local world need to have a corresponding world with that domain element.
Here's a model with an integer number of worlds.
The consistency of the interpretation formula cannot be confirmed by any ATP system I have.
Here's a problem that I think should be provable, but none of the ATP systems I know can (after conversion to TH0, Leo-III does not have the arithmetic power, E, Vampire, and Zipperposition don't do arithmetic (at least in THF), cvc5 gives parse error). With the conjecture commented out as below, the axioms have a an Infinite-Infinite model (I think).
Here's a model in which there are an infinite number of worlds - one for each integer numbered year, an infinite number of ages as integers, and just one person in each world.
The consistency of the interpretation formula cannot be confirmed by any ATP system I have.