Treffer: Positive models and universal propositions

Suppose that we have a theory \(T\) that describes our knowledge. In case of incomplete knowledge, we can often write down the complete list of objects, but we are not sure which of these objects are identical (a typical situation in mystery novels, where we can have several suspects and a murderer, that can well be one of them). We may also be not sure whether some other property (not necessarily equality) is true or not. Based on this incomplete information, we can design several different models. A typical way to design a model is to add hypotheses, i.e., a finite set or a recursively enumerable set of additional facts and laws (universal statements). Then, we can say that an atomic statement \(P_ i(a_ 1,\dots)\) is true in the resulting model if it is deducible from the initial knowledge \(T\) with the new assumptions \(\Phi\) added. In some cases, it is reasonable to design a complete world model in the following sense: for each atomic statement \(A\), either \(A\) or \(\neg A\) are deducible from \(T+\Phi\). In this case, we have an evident algorithm that for each \(P_ i\) and each \(a_ 1,\dots\) decides whether the formula \(P_ i(a_ 1,\dots)\) is true or false in this model: we just try all possible proof trees; if one of them contains this atomic formula, then it is true, if it contains its negation, then \(P_ i(a_ 1,\dots)\) is false. Models for which such an algorithm exists are called constructive models. In many cases, we are not interested in designing a complete model, because we do not care what happens to the rest of the world. In this case, we also add some additional hypotheses \(\Phi\), and consider a statement \(P_ i(a_ 1,\dots)\) to be true if it is deducible from \(T+\Phi\) and false if its negation is deducible. As for the cases when neither an atomic statement nor its negation are deducible, we follow the idea of Closed World Assumption (widely used in logic programming and knowledge representation) and consider \(P_ i(a_ 1,\dots)\) to be false. For the resulting models, there is an algorithm that enumerates all sets \((a_ 1,\dots)\) for which \(P_ i\) is true. The models with such algorithmic property are called positive models. In some cases, after we discover some new facts and/or laws, we become able to prove new atomic statements that were previously undecidable. Thus these statements become true, and the set of all true atomic statements for a new theory is a superset for the set of all true atomic statements in an old model. Suppose now that we have a positive model. Since this model does not represent complete knowledge, it is natural to consider the case when we discover new objects in our universe, i.e., in mathematical terms, when we add additional constants to the constants from \(M\). This situation is again incomplete, but in principle we should be able to complete it (after we get some additional knowledge). Let us call a model completable if there exists a r.e. set of universal statements \(\Phi'\) and a model \(M'\) of the theory \(T+\Phi'\) (new constants added) with the property that no superset of the set of all atomic statements \(P(a_ 1,\dots,a_ k)\) and \(a_ i=a_ j\) makes a model of that enriched theory. The author proves that a model \(M\) has a completable extension \(M'\) if and only if it is constructive (to be more precise, iff it is constructivizable, i.e., it can be made constructive by an appropriate \(1-1\) mapping of its constants into the set \(N\) of all natural numbers). As a corollary, we can conclude that if a positive model \(M\) is not constructivizable, then for each extension \(M'\) of \(M\) to new constants, and for every r.e. set of universal statements that are true in \(M'\), all these statements are also true in some proper homomorphic image of \(M'\), i.e., they are still true when we add additional atomic statements to the list of those that are true in \(M'\). Similar results are true for the case (widely used in linear programming) when we allow only universal Horn statements in \(\Phi'\). If we allow existential statements there, then completability is possible for non- constructive models.