Occasionally I come across a definition based on what will happen in all models, for example, that a contradiction is a statement that is false in all models, that a tautology is a statement that is true in all models, that sentence A implies sentence B if in all models in which A is true, B is also true, and similar for "and" and "or". But these definitions cannot be formalized as is, because they quantify over "all models", an impossibility. How does one get around this? Does one quantify over all models of first-order theories inside a second-order theory?

  • $\begingroup$ We can quantify over "all models" in first-order set theory, and we can formalize these definitions within that set theory. So they can be formalized as-is. $\endgroup$ – Carl Mummert Jul 23 '16 at 15:02
  • $\begingroup$ There is no more need to formalize than in any other branch of mathematics, $\endgroup$ – André Nicolas Jul 23 '16 at 15:22
  • $\begingroup$ @CarlMummet Interesting, I assumed that one could not quantify over all models in first-order set theory, because the modal quantifiers for necessity or possibility are essentially quantifying over all models in the frame, and they are classified as second-order. Could you give me an indication as to how such quantification can be done in order to keep it first order? $\endgroup$ – nomadreid Jul 24 '16 at 14:45
  • $\begingroup$ @nomadreid: in first-order set theory, the quantifiers quantify over all sets. Because models are sets, this means that they quantify over all models. $\endgroup$ – Carl Mummert Jul 25 '16 at 2:07
  • $\begingroup$ I am puzzled by the following description from Wikipedia:"First-order logic quantifies only variables that range over individuals; second-order logic, in addition, also quantifies over sets; third-order logic also quantifies over sets of sets, and so on." In a set theory, it makes sense that individuals are sets, so that I am not clear on the difference between "quantify over individuals" and "quantify over sets" in this description (taken from en.wikipedia.org/wiki/Higher-order_logic) $\endgroup$ – nomadreid Jul 26 '16 at 4:05

You would need to specify your meta-system, before you can formalize a meta-theoretic statement. Conventionally logicians use some conservative extension of ZFC as their meta-system. Within ZFC one can consider any first-order language and collection of sentences (encoded in some way) over it, and ask whether there is a model, which is defined as a tuple consisting of a set for the domain and interpretations for each predicate or function or constant symbol of the language.

However, this definition does not give a set of all models, because no such set can exist (unless you love contradictions). But "$M$ is a model of $X$" can be expressed by a first-order sentence over ZFC. So what you can do is to define a new abbreviation $IsModelOf$, namely a binary predicate symbol such that, for every (sets) $M,X$, we have $IsModelOf(M,X)$ iff $M$ is a model of $X$.

Quantifying over all models is then possible, since restricted quantification over elements satisfying a predicate can be easily expressed using unrestricted quantification. What cannot be done is to use the collection of all models as a single object in the set-theoretic universe. You are right that if you use second order ZFC you can natively have the collection of all (set) models of a set of sentences. One commonly used essentially second-order set theory is MK (Morse-Kelley), which has two sorts, one for sets and one for collections of sets called classes.

| cite | improve this answer | |

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.