Semantics and Model Theory
At first, I thought teaching students an informal semantics for predicate logic was only a compromise we had to choose because the real thing, formal model theory, is just too difficult for beginners. But now I'm inclined to believe that the informal semantics is itself the real thing. Maybe for those of us who have no quarrals with set theory, the difference is only superficial since both accounts assign the same truth conditions to all sentences, and truth conditions are all that matters. But that's not quite true. For example, when we talk about all sets (or all classes, or all things whatsoever), standard model theory is in trouble. I think it's silly to conclude that we can't really talk about all sets or classes or things. We obviously can do so in English, and we can also do so in (interpreted) first-order logic.
Even if the truth conditions always matched, I would still claim that the informal semantics has conceptual priority. For it's the informal account that decides which of the indefinitely many possible model theories are acceptable. That is more obvious for non-elementary logics like the Gödel-Löb provability logic: It has two model theories, one in terms of possible worlds, the other in terms of arithmetical provability. The first one, though it is the standard account for modal logics, is (to me) rather unintelligible (mainly because of its weird accessibility relation). It's just a mathematical framework that happens to give the same result as the second model theory, the real thing. It doesn't tell you anything at all about provability in arithmetic even though that's what sentences in GL are meant to talk about.
If formal model theory is presented as the real semantics for predicate logic, it gets difficult to explain why soundness and completeness of deductive systems are valuable: Why should we care whether the deductive consequence relation exactly matches that set theoretical relation? If on the other hand formal model theory is regarded as a regimentation of informal semantics, then an explanation is easier to find: Corresponding to the informal semantics there is an informal account of logical consequence and logical truth, something roughly like truth-in-virtue-of-the-logical-constants, or truth-no-matter-what-the-non-logical-words-mean. This is what the formal account tries to capture, and it is what we want our deductive system to tell.
I am studying Model checking and came through this term "interpreted" first order logic. I know first order logic as predicates and quantifiers, what are "interpreted" first order logic (IFOL) and how are they different from FOL?