The substitution interpretation and the expressive power of intensional logics.
James W. Garson · Notre Dame Journal of Formal Logic · 1979
The substitution interpretation may be employed in place of the objectual interpretation in giving the semantics for first-order logic, without affecting the class of formulas defined as valid.If the usual definition of satisfaction is given, namely that a set is satisfiable just in case its members are all true on some model, and the substitution interpretation is used, the notion of satisfaction is no longer compact.So notions of semantic entailment and satisfaction differ from those generated by the standard account.However, with a simple adjustment to the definition of satisfaction, compactness is restored, and notions of satisfiability and semantic entailment match exactly those of the standard account, at least as far as their extensions go.An adjusted definition of satisfaction suitable for the substitution interpretation looks something like this: a set of formulas is satisfiable just in case there is a syntax for first-order logic which has those formulas among its well-formed formulas, and a model for that syntax such that every formula of the set is ruled true.In a sense to be made somewhat clearer below, (semantics for) first-order logic has substitution interpretation invariance (sii), at least when the definition of satisfaction is adjusted correctly.The same is not true of intensional logics.The results of Garson [2] show that a semantics for topological logic is not sii, and one of the results of this paper will be that Thomason's Q2 is not sii either [4].We need to present some of the details of these two systems.We give here a definition of w-semantics for topological logic.A w-model is a triple (C, F, ύ) where C is a non-empty set (of possible worlds, contexts, etc.), F is the set of all transformations on C, and u is an interpretation function which assigns intensions to the terms and predicates as we would expect: u(n) e F, for each term n u(pi)e{f:f:C -*P(C 1 )}, for each j-ary predicate P 7 where ( P' indicates power set.