| The Completeness Theorem
Dpt of Philosophy |
 |
|
|||||
|
1 The Completeness Theorem To reconcile the syntactic and semantic presentations of consequence is at the core of any logic (be it pure or applied, classical or non classical). This aim can also be seen as the goal to compare (and relate), side by side, the expressive capacity of a formal language, with the computational power of a particular presentation (calculus). Together, the soundness and completeness theorems, establish the equiva- lence between the syntactic (associated to a given calculi) and semantic (asso- ciated to a given class of models) notions of consequence, for a given language. Intuitively, the semantic notion of ?truth?helps us select the set of all the sen- tences of a given language that are always true in all structures or models ? this set of formulas are usually called ?logically valid,?VAL ? . On the other hand, we can also describe a set of formulas using a purely syntactic de?nition in the form of a deductive calculus. Such calculus would de?ne when a formula ?logically follows?from others. In particular, the set of formulas which ?logically follows?from the empty set is call the set of logical theorems, THEO. Are these two sets the same? That is the exact question addressed by the soundness and completeness theorems. 2 Relevance of the Completeness Theorem Theoretical Relevance We can say that we don?t know a logic till we haven?t identi?ed its set of valid formulas. Intuitively, we can say that the logi- cality of a given formal language resides in the set VAL of valid sentences. Each model A for a given signature select from the set of all sentences those which are true under this particular interpretation. This set of formulas is usually called the theory of the structure, Th(A), and it characterizes the structure A. But all such theories share a common nucleus which is the set VAL. Does this set characterize something? The answer is yes, VAL characterizes the logic in question itself. It repre- sents what the logic ?has to say?about any arbitrary structure. If we are able to ?generate?this set easily, we would have ?nally capture the essence of a logic, its perfume. Practical Relevance As we just discussed, the semantic notion of truth is at the core of a given logic. But because of its generality, it is very di˘ cult to manipulate. For example, the semantic notion of consequence perfectly de?nes when a formula ' follows from a given set of formulas ?? (it is ?enough?to verify that ' is true in all models where ?? is true); but it does not provide for an ?algorithm?that helps us verify this relation. This is when the set THEO of theorems, and the notion of completeness, come to our help. In particular, we can establish a chain of inference from the premises in ?? to the conclusion '. Actually, this operational de?nition of consequence seems even more adequate and closer to the intuitive notion of inference, given that it re?ects the discursive character of the process. 3 The Completeness of the First-order Calculus Completeness theorem is proved in its strong sense, �� j= ' implies �� ` ' — for any ��, ' such that �� [ f'g Sent(L)— . One prove completeness and its corollaries following the path: Lindenbaum’s lemma + Henkin’s lemma 9= ;! Henkin’s theorem #S trong completeness #Weak completeness % Compactness & Löwenheim-Skolem These theorems are understood as follows: Lindenbaum lemma: If �� Sent(L) is consistent, there exists �� such that �� �� Sent(L), �� is maximally consistent and contains witnesses. Henkin’s lemma: If �� is a maximally consistent set of sentences and contains witnesses, then �� has a countable model. Henkin’s theorem: If �� Sent(L) is consistent, then �� has a model whose domain is countable. Strong completeness: If �� j= ' then �� ` ' — for any �� [ f'g Sent(L). Weak completeness: If j= ' then ` ' — any ' 2 Sent(L). Compactness theorem: �� has a model i¤ every …nite subset of it has a model — any �� Sent(L). Löwenheim-Skolem: If �� has a model, then it has a countable model — any �� Sent(L).
|
|||||||
|
4 Completeness Notions In logical writings we ?nd the term ?completeness?applied either to theories, to deductive calculuses, or just to logics. In all three cases we wish to express some kind of su˘ ciency of the rules (or completeness of the ?nal product) but, as we shall see, these concepts di¤er in some aspects having to do with the resources and methods needed to establish them. In [14] we focus on the evolution of the notion of completeness in contem- porary logic. We discuss the di¤erences between the notions of completeness of a theory, the completeness of a calculus, and the completeness of a logic in the light of Gödel?s and Tarski?s crucial contributions. As far as ?rst-order logic is concerned, our thesis is that the contemporary understanding of completeness of a calculus was born as a generalization of the concept of completeness of a theory. There are three main lines that I want to consider in the tutorial: 1. Origin: When and how is the necessity of a completeness proof born? When does it separate itself from a theorem concerning the decidability of satis?ability for a given logic? For example, the ?rst completeness proofs for Propositional Logics are intimately related to decidability and representation in terms of ?nite algebras. The original publications of Post, Stone, Quine, Tarski, and Gödel are relevant for this line. 2. It seems natural to think that Henkin?s completeness theorem for ?rst- order logic was proved before the completeness for type theory. Surpris- ingly, in his 1996 paper he stated that he obtained the proof of complete- ness of ?rst-order logic by readapting the argument found for the theory of types, not the other way around. 3. Evolution of Henkin Completeness Proof: The original proof of complete- ness for classical logic resulted extremely versatile, and its fundamental idea of using witnesses during the model construction can be used for many other logics. In [1] we use a similar idea. It is specially interest- ing to establish the relation between Henkin proof and the use of rigid designators in hybrid logics [2]. Bibliography:
|
|||||||