Logic and Semantics

While (classical) model theory is using a logical language $\cal{S}$ in combination with an inference relation $\vdash$ to discuss the relationship with a satisfaction relation, this close relationship between a logical inference and the satisfaction relation is not necessary. Formal semantics as such does not depend on such a logical inference concept. Because the truth conditions of the language expressions are part of the meaning of the language, logic is strictly speaking not necessary.

Why then logic? In the most general sense has logic to be understood as a system of inference rules defining how one can deduce a subset Th of expressions of a formal language S given a subset P of expressions of S. The expressions of S as well those of Th are assumed to be 'true'. In the general case one use an inference predicate $\vdash$ as ' $P \vdash Th$' meaning 'The set of expressions Th of S can be inferred from the the set of expressions P of S if all elements of P are 'true' and one applies only inference operations according to $\vdash$ from the logic L. Then all elements of the set Th are also true. The elements of Th are called theorems of the logic L.

Since the beginning of modern formal logic with Bool (1815 - 1864 ), Frege (1848 - 1925), Peano (1858 -1932)), Whitehead (1861 - 1947), Hilbert (1862 -1943) , Russel (1872 - 1970), Ackermann (1896 - 1962), -to mention only a few of the main founders- many hundreds of different instances of concrete logical systems have been introduced and used since. 'Traditional style logics' are using e.g. two-valued logic with the truth values 'true' and 'false' ('1' and '0'); newer ones introduced three-valued logics or even n-valued logic. Other distinctions resulted from the kind of formal language used. 'Simple' types of logic are using only one kind of variable (e.g. for propositions), others are using more than one type of variable (e.g. individuals, predicates, and functions). Furthermore there is a distinction between descriptive signs and logical signs. 'Simple' languages in use for logic are e.g. using only propositional logical signs; others are using additional logical signs like quantifiers or modal signs. Thus as different the language can be which is used within logic, as different can be the inference rules used.

This great variety shows that a systematic account of the many hundreds of modern logical systems is difficult. And, although there is no necessity to use formal logic for formal semantics and vice versa, there can nevertheless be some interesting 'interaction' between formal logic and formal semantics possible, as illustrated by the case of classical model theory.

This interaction can emerge from the fact that one uses the same formal language S for the formal semantics as well as for the formal logic. In such a special case one can ask whether the semantical satisfaction relation $\models$ can somehow be related to the inference relation $\vdash$? Turn it otherwise: Given a certain formal domain model $M$, a formal language $S$, a formal interpretation $I : S \longleftrightarrow M$ with the satisfaction relation $\models$, a formal logic $L$ with the formal inference relation $\vdash$: Is it possible to construct $\models$ as well as $\vdash$ in a way that $M, m \models f \Longleftrightarrow P \vdash f$? Clearly such a question can only be answered if there exists a mapping from $P$ into $M$ which is sufficient. Because $P \subseteq S$ and $I : S \longleftrightarrow M$ we can say that we have $I : P \longleftrightarrow M$. Therefore we have a control about every $P$ related to $M$ and then we can ask again: If $I(P) = M'$ , $M' \subseteq M$, is it true that $M' \models f \longleftrightarrow P \vdash f$? If this equivalence can be proven than one can use either formal semantics with model checking to check some properties of a formal domain model $M$ or one can use formal logic to deduce certain properties. The final decision then will depend only from the 'costs' of the procedure; which one is 'cheaper' to realize?