# model definitions for tautology, contradiction, and connectives quantify too much, no?

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?

• 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. – Carl Mummert Jul 23 '16 at 15:02
• There is no more need to formalize than in any other branch of mathematics, – André Nicolas Jul 23 '16 at 15:22
• @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? – nomadreid Jul 24 '16 at 14:45
• @nomadreid: in first-order set theory, the quantifiers quantify over all sets. Because models are sets, this means that they quantify over all models. – Carl Mummert Jul 25 '16 at 2:07
• 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) – nomadreid Jul 26 '16 at 4:05

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$.