ONT Re: Model Theory
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
Note 25
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
| 1. Introduction
|
| 1.3. Languages, Models, and Satisfaction (cont.)
|
| We now come to an extremely important
| convention of notation. To make sure
| that the reader does not miss it, we
| enclose it in a box:
|
| o-----------------------------------------------------o
| | |
| | We use t(v_0 ... v_n) to denote a term t whose |
| | |
| | variables form a subset of {v_0, ..., v_n}. |
| | |
| | Similarly, |
| | |
| | we use p(v_0 ... v_n) to denote a formula p whose |
| | |
| | free variables form a subset of {v_0, ..., v_n}. |
| | |
| o-----------------------------------------------------o
|
| Notice that we do not require that all of the variables v_0, ..., v_n be free
| variables of p(v_0 ... v_n). In fact, p(v_0 ... v_n) could even have no free
| variables. Also, we make no restriction on the bound variables. For example,
| each of the following formulas is of the form p(v_0 v_1 v_2):
|
| (`A`v_1)(`E`v_3) R(v_0 v_1 v_3),
|
| R(v_0 v_1 v_2),
|
| S(v_0 v_2),
|
| (`A`v_4) S(v_4 v_4).
|
| A 'sentence' is a formula with no free variables.
|
| Notice that even if $L$ has no symbols, there are still formulas of $L$.
| These formulas are built up entirely from the identity symbol '=' and the
| other logical symbols listed. Such formulas are called 'identity formulas'
| and 'they occur in every language'. The following proposition is simple
| but important.
|
| 1.3.4. Proposition. The cardinal of the set of all formulas of $L$ is ||$L$||.
|
| To make all the above syntactical notions into a 'formal system' we
| need 'logical axioms' and 'rules of inference'. The logical axioms
| for $L$ are divided into three groups:
|
| 1.3.5. Sentential Axioms.
|
| Every formula p of $L$ which can be obtained
| from a tautology q of $S$ by (simultaneously
| and uniformly) substituting formulas of $L$
| for the sentence symbols of q is a logical
| axiom for $L$. From now on we shall call
| such a formula p a 'tautology' of $L$.
|
| 1.3.6. Quantifier Axioms.
|
| 1. If p and q are formulas of $L$ and v is a variable not free in p,
| then the formula:
|
| (`A`v)(p => q) => (p => (`A`v)q)
|
| is a logical axiom.
|
| 2. If p and q are formulas and q is obtained from p by freely
| substituting each free occurrence of v in p by the term t
| (that is, no variable x in t shall occur bound in q at
| the place where it is introduced), then the formula:
|
| (`A`v)p => q
|
| is a logical axiom.
|
| 1.3.7. Identity Axioms.
|
| Suppose x, y are variables, t(v_0 ... v_n) is a term, and
| p(v_0 ... v_n) is an atomic formula. Then the formulas:
|
| x = x
|
| x = y => t(v_0 ... v_(i-1) x v_(i+1) ... v_n) =
| t(v_0 ... v_(i-1) y v_(i+1) ... v_n)
|
| x = y => p(v_0 ... v_(i-1) x v_(i+1) ... v_n) =
| p(v_0 ... v_(i-1) y v_(i+1) ... v_n)
|
| are logical axioms.
|
| There are two rules of inference:
|
| 1.3.8. Rule of Detachment (or Modus Ponens).
|
| From p and p => q, infer q.
|
| 1.3.9. Rule of Generalization.
|
| From p, infer (`A`x)p.
|
| Given the axioms and the rules of inference, we assume that the
| resulting notions of 'proof', 'length of proof', 'theorem' are
| already familiar to the reader. As we are dealing with the
| usual first-order logic with identity, we shall assume as
| known and make free use of all of the basic theorems and
| metatheorems of such formal systems.
|
| Chang & Keisler, 'Model Theory', pages 23-25.
|
| C.C. Chang and H.J. Keisler, 'Model Theory',
| North-Holland, Amsterdam, Netherlands, 1973.
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤