Ling 726: Mathematical Linguistics, Lecture 7 Model Theory (expanded 2) V. Borschev and B. Partee, October 12-14, 2004 p. 1 Lecture 7. Model theory. Consistency, independence, completeness, categoricity of axiom systems. Expanded with algebraic view. CONTENTS 1. Syntactic provability and semantic entailment.......................................................................................................... 1 1.1. Semantic entailment and validity. ...................................................................................................................... 2 1.2. Soundness and completeness of a logic.............................................................................................................. 2 2. Consistency, completeness, independence, and other notions. ................................................................................ 3 2.1. Some syntactic concepts..................................................................................................................................... 3 2.2. Some semantic concepts..................................................................................................................................... 4 2.3. Soundness and completeness again.................................................................................................................... 4 2.4. Independence...................................................................................................................................................... 5 3. An algebraic view on provability and on the notions discussed above ..................................................................... 5 3.1. Closure systems.................................................................................................................................................. 5 Examples............................................................................................................................................................... 5 Closure operator.................................................................................................................................................... 6 Examples............................................................................................................................................................... 6 3.2. Galois connection............................................................................................................................................... 6 Examples............................................................................................................................................................... 7 4. Morphisms for models; categoricity........................................................................................................................ 7 Homework 8.................................................................................................................................................................. 8 Reading: Chapter 8: 8.1, 8.4, 8.5, of PtMW, pp. 179-189, 192-217. Good supplementary reading: Fred Landman (1991) Structures for Semantics. Chapter 1, Sections 1.1 and 1.3., which we draw on heavily here. Another nice resource (thanks to Luis for the suggestion) is Gary Hardegree’s online in-progress textbook Introduction to Metalogic : http://www-unix.oit.umass.edu/~gmhwww/513/text.htm . (Ch 5: semantics of first-order logic, with notions of consistency, etc.; Ch 14: models and interpretations.) This last reference is still new to us and we haven’t studied it. Anyone who has a chance to take Hardegree’s Mathematical Logic course would certainly get a thorough grounding in all the notions we are discussing here and more. 1. Syntactic provability and semantic entailment Proof theory: When we presented first order logic in earlier lectures, we specified only the syntax of well-formed formulas and their semantics. We did not give any proof theory. Let us add that now. Add to our first-order logic a set of axioms1 and Rules of Inference, such as those described in Chapters 7 and 8.6 of PtMW or Chapter 1 of Landman. (We are not going to specify these here.) Then we can specify the notion of a proof of a formula ϕ from premises ϕ1, ..., ϕn. A proof of a formula ϕ from premises ϕ1, ..., ϕn is a finite sequence of formulas <ψ1, ..., ψm > such that ψm = ϕ, and each ψi is either (a) an axiom, (b) a premise, or (c) inferred by means of one of the Rules of Inference from earlier formulas in the sequence. 1 Here we consider axioms for first order predicate logic itself (PtMW 8.6), which we should distinguish from axioms for theories describing axiomatic classes of models. The former are tautologies which are true in every model. The latter are contingencies which are true in some models and false in other.Ling 726: Mathematical Linguistics, Lecture 7 Model Theory (expanded 2) V. Borschev and B. Partee, October 12-14, 2004 p. 2 Call the resulting system of logic L0. An important aspect of the rules of inference is that they are strictly formal, i.e. “syntactic”: they apply when expressions are of the right form, with no need to know anything about their semantics. Corresponding notion of syntactic derivability or provability: (Landman p 8) Let ∆ be a set of formulas and φ a formula. We write ∆ ├ φ , meaning φ is provable from ∆, φ is derivable from ∆, iff there is an L0-proof of φ from premises δ1, ..., δn ∈ ∆. The symbol ├ is pronounced “turnstile”. (In Russian it is called “shtopr”, i.e. “corkscrew”.) We write ├ φ, φ is provable, φ is a tautology, for ∅ ├ φ, i.e. φ is provable from the axioms and inference rules of the logic without further assumptions. φ is a contradiction if ├ ¬ φ . It is common to use a special symbol ⊥ (“bottom”) to stand for an arbitrary contradiction. Note that here we use syntactic notion of tautologies and contradictions. Earlier in Lecture 6, and also below, we consider corresponding semantic notions. 1.1. Semantic entailment and validity. Instead of writing [[φ ]]M,g = 1, it is customary when discussing model theory to write M ╞ φ[g] , meaning φ is true in M relative to g. We write M ╞ φ (and say that φ is true in M) iff M ╞ φ[g] for all g. Note that if φ is a sentence (i.e., φ has no free variables), then for every model M we have φ is true in M or φ is false in