Schurz - Carnap Modal Logic

Titel / Title: Rudolf Carnap’s Modal Logic

Autor / Author: Gerhard Schurz

PE PREPRINTS Annual 2000

No. 2

Edited by Dietmar von der Pfordten und Gerhard Schurz

Philosophische Vorveröffentlichungsreihe an der Universität Erfurt Philosophical Prepublication Series at the University of Erfurt

1

Rudolf Carnap's Modal Logic Gerhard Schurz, Universität Salzburg

1. Introduction Rudolf Carnap was the first who has developed a formal modal logic based on the famous semantic idea which goes back to Leibniz. According to this idea, a statement is necessary iff it is true in all possible worlds. Carnap represents possible worlds by state descriptions, while we will represent them by possible interpretations of the formal language - but this does not make a big difference for our purpose. Carnap developed his modal logic in his JSL-paper of 1946 and in his book Meaning and Necessity of 1947. His modal logic, which we call here C, is usually presented as a version of the Lewis system S5 - indeed Carnap himself has sometimes presented it in that way. But in fact, his system C is much stronger than S5 and it has very unusual logical properties. However, this fact is not wellknown to the broad philosophical audience - probably because Carnap himself was unclear about it. Only a few authors have recognized the deep difference between S5 and Carnap's C - among them D. Makinson (1966), S. K. Thomason (1973), Cochiarella (1975), Hendry and Pokriefka (1985), and recently Georg Gottlob (1999) who works in Artificial Intelligence Research. In this paper I will argue for three points: 1. If one identifies necessity with logical necessity, then C is the only complete modal logic. 2. C is connected with an interesting nonmonotonic inference relation. 3. C supplies motivation to revise the traditional understanding of logics in the following three respects. Traditionally one is used to think that: A) Logical truth and validity are a matter of form or structure. Hence logics and inference relations have to be closed under substitution (i.e., under uniform replacement of arbitrary statements for the atomic statements).

2

B) There is a general distinction between the metalogical properties of effective axiomatizability (recursive enumerability, semi-decidability) and decidability. And likewise, between semantical correctness and semantical completeness. C) Logical inference relations must be monotonic (in the sense that inference is preserved under enrichment of premises). In the following I will show that Carnap's modal logic satisfies neither of these three traditional claims A) - C). I will argue that: • A) is mistaken: formality does not require closure under (arbitrary) substitution but a weaker property. • The distinctions mentioned in B) break down for certain logics - and C-type logics are among them. • Likewise, C) does not hold for certain interesting inference relations - and certain Cbased inference relations are among them. 2. Carnap's Modal Logic C

We restrict ourselves mainly to the language of propositional modal logic, which consists of a denumerable set P of so-called propositional variables p, q, .…, and the standard connectives and operators ∧, ∨, ¬, → (material implication), ↔, T (Verum), ⊥ (Falsum),

and ◊. We assume standard interpretations (truth valuations) I: P→{0,1} and a

classical semantics for nonmodal formulas. We identify interpretations with possible worlds; W is the set of possible worlds (interpretations) I: P →{0,1}. A sentences is called logically true iff it is true in all possible worlds (vide Carnap 1947, p. 10, 2-2). Note that it follows from this standard semantical setting that propositional variables figure as variables for primitive, i.e. atomic statements, since W contains every possible assignment of truthvalues to the elements of P. Although this point seems to be trivial, it will play an important role below.

3

Carnap introduces the following general semantical rule for the truth value of modal sentences (1946, convention C1-1; 1947, p. 174f., 39-1 - 39-3): (C1) A is true (in any given world I) iff A is true in all possible worlds iff A is logically true. The brackets "(…)" are not explicitly contained in Carnap's text, but it is clear that with "truth simpliciter" Carnap means "truth in an arbitrary given world". Obviously, the truth of A according to (C1) is logically determined. So if

A is true or false, it is so in all

interpretations, and hence it is logically true or false, respectively. Thus Carnap's modal logic implies the following semantical rules, which are also explicit in Carnap (in what follows, "||" always stands for C-validity): (C2) if ||A, then || A

if ||- /- A, then || ¬ A

(= ◊¬A).

(C2) follows from (C1) and the logical determinateness (LD) of then ||

A as follows: If ||A,

A by (C1) and (LD). And if ||-/ - A, then ||-/- A by (C1), whence || ¬ A by

(LD). This semantics characterizes logical necessity and possibility in a complete way. It implies immediately the validity of all well-known theorems and rules of S5, such as T: A→ A, 4: A→

A, 5: ◊A→ ◊A, etc. But it implies much more. For example,

(C3) All completely modalized sentences are logically determined in C. This follows from the facts that sentences of the form

A are C-logically determined, and

every truthfunctional combination of logically determined sentences is itself logically determined. More striking is the following: (C4) For every propositional variable p ∈ P, ◊p is a theorem of C, and the same is true for

4

every C-consistent sentence A. This has the following immediate consequence: (C5) C is not closed under substitution. For example, ||◊p, since p can be made true by at least one I ∈ W. Obviously, ◊(p∧¬p) is a substitution instance of ◊p (by substituting p∧¬p for p). But not ||◊(p∧¬p), since every I ∈ W makes p∧¬p false. 3. Closure under Substitution and the Relation between C and S5

The fact that C is not closed under substitution has led to two historical peculiarities. The first is this. In his 1946-paper, Carnap first introduces the above semantical rules. He then develops a modal propositional logic and a modal predicate logic. He develops the modal predicate logic according to his semantical rules. But in his modal propositional logic he deviates from his ideas by the following ad hoc step: he restricts the logical truths of modal propositional logic to a certain subclass of those statements which are valid under his semantics: namely those statements which are in addition closed under substitution (1946, p. 40, D4-1). By doing this, he throws away all non-trivial possibility-theorems of C. He shows then that the system so defined is equivalent to Lewis' famous system S5. Maybe Carnap was so happy about this result that he forgot about the other part of C. The second historical peculiarity was pointed out by Hendry and Pokriefka (1985, p. 111) and concerns Feys' reconstruction of Carnap's propositional modal logic in the Schilpp volume of 1965. Feys reconstructs this logic as the system C, not as S5, but Feys presents this system as if it were S5 (Feys 1965, p. 286). Moreover, in his reply Carnap states that Feys had correctly reconstructed his system S5. These peculiarities may explain why the mistaken view that Carnap's modal logic is S5 is still widely held under philosophical logicians. What Carnap in fact had proved in 1946 was a certain relation between C and S5 -

5

namely that S5 contains exactly those C-logical truths which are substitutionally closed. This relation was independently proved in 1973 by S. K. Thomason and is stated in our theorem 1. Let Lprop denote our formal language of propositional modal logic, and let s vary over substitution functions of the form s: P → Lprop. Then theorem 1 runs as follows: Theorem 1: S5 = {A ∈ C : ∀s(sA ∈ C)}. The relation between C and S5 stated in theorem 1 is a syntactical one. What is the semantical relation between C and S5? Let us see how Kripke (1959) succeeded in establishing a possible world semantics which leads to a modal logic which is indeed closed under substitution - namely S5. In Carnap, the space of possible world is a fixed space W it contains all possible interpretations of the language. This has the unavoidable consequence that for all satisfiable sentences A, ◊A comes out as a logical theorem, for A is true in at least some interpretation I which is in W. And it are these non-trivial possibilitytheorems which are not closed under substitution. Kripke, however, assumes the set of possible worlds W to be a variable subspace of W. His modal logics contains only those sentences as theorems which are valid with respect to every subspace W ⊆ W. And these are exactly the S5-theorems. Hence Kripke relates necessity to all subspaces of possible worlds in W. If, on the other hand, necessity is related to a specific (proper) subspace of possible worlds W ⊆W, this means philosophically that one has in mind a concept of necessity which is stronger than logical necessity - for example, physical necessity (i.e., necessity w.r.t. laws of nature). Given such a subspace W (e.g., the set of physically possible worlds), then one can consider the modal statements which are semantically valid w.r.t. W (i.e., A is valid in W iff A is true in all I∈W, etc.). Call this system of statements SW. SW contains more necessity statements than C, but less possibility statements. So SW is neither stronger nor weaker than C. If W is smaller than W, then SW is, so to speak, a material modal system. If W = W, then SW coincides with C. Now, Hendry and Pokriefka (1985) have proved the following semantical connection between S5 and these SW-systems with C-type semantics: S5 is the

6

intersection of all modal systems w.r.t. to arbitrary possible world spaces W ⊆W. This is stated in our second theorem: Theorem 2: S5 = ∩ {SW: W ⊆W} where C = SW It is a well-known consequence of this conception of S5 that it can prove no non-trivial possibility-theorems. If A is nonmodal, this insufficiency of proving non-trivial possibility theorems can even be proved for every normal modal logic. These two facts are stated in the next two theorems. Theorem 3: If ◊A ∈ S5, then A ∈ S5. Proof: Assume A ∉ S5. Then A is invalid w.r.t. some W ⊆W. So there exists I∈W such that I falsifies A. Let W* be the one-element subspace W* = {I} containing this I. Then ◊A is invalid w.r.t. W* = {I}. Hence ◊A ∉ S5. Q.E.D. Theorem 4: For every nonmodal formula A∈Lprop and normal modal propositional logic L: if ◊A ∈ L, then: A ∈ L, and A is a truthfunctional tautology provided L is consistent. Proof: If L is the inconsistent logic, the claim is obvious. Assume L is consistent. It is a well-known fact of frame-semantics (i.e. semantics with possible world sets plus accessibility relation) that every consistent normal modal logic is either valid on the reflexive singleton frame <{w}, <{w,w}>>, or on the irreflexive singleton frame <{w},

> (cf.

Makinson 1971, Schurz 1997, p. 64; note that in frame-semantics we have to distinguish between worlds and interpretations in the well-known way). So ◊A ∈ L implies that ◊A is valid on one of these singleton frames (hence true for every interpretation associated with the world w). Since A is nonmodal, this implies that A is verified by every interpretation. Hence A must be a truthfunctional tautology, whence A ∈ L. Q.E.D.

7

The first author who to my knowledge has explicitly reflected the fact that C is not closed under substitution was David Makinson 1966. His arguments at that time are characteristic for the traditional views outlined in section 1. He assumes three conditions which he presents to be more or less equivalent: a) Logics have to be a matter of form; their theorems are characterizable by structural conditions alone - they do not depend on particular interpretations of nonlogical symbols. b) Logics have to be closed under substitution (i.e., if A ∈ L, then sA ∈ L for every logic L and substitution function s). c) Logics must be axiomatizable by schematic axioms and rules (i.e.., by axioms and rules which are closed under substitution in the following sense: if A is an instance of an axiom, then for every s, sA is also an instance of that axiom, and if A1,…,An/B is an instance of a rule, then for every s, sA1,…,sAn/sB is also an instance of that rule). On these reasons Makinson (1966) concludes that C presents a naive view of modal logic and should not be regarded as a proper logic - he argues that only S5 is a proper logic. I wish to show now that: • a), b) and c) are pairwise nonequivalent, and • only a) is a correct condition for logics. I agree with a) because first, I think that proper logics should be independent from the particular interpretations of nonlogical symbols, and second, I think that the distinction between logical and non-logical symbols is well-founded (cf. Schurz 1999). That a) does not imply b) becomes obvious if one distinguishes between syntactically isomorphic versus merely homomorphic substitutions. The former ones replace primitives, i.e. atomic statements (propositional variables) by other primitives in a unique way. They perform merely a relettering of primitives. Syntactically isomorphic sentences are indeed indistinguishable by their syntactic form. However, syntactically homomorphic substitutions may

8

replace a primitive statements p by a complex statement such as p∧¬p. A homomorphic substitute of a sentence is distinguishable from the original sentence by syntactic means, by its richer syntactic complexity. In semantic respect, a homomorphic substitution may restrict the semantical degrees of freedom - it may restrict the possible variations of interpretation. In our example, p can be true or false, but its substitute p∧¬p can only be false. I think there is no apriori reason why one should assume that logical concepts such as logical truth should always be invariant under operations like homomorphic substitution which change their syntactic structure (increase syntactical complexity) and which restrict their semantical degrees of freedom. That this invariance holds for traditional logics has a special reason which I will discuss immediately. But also in these traditional logics there are other logical concepts which are not closed under homomorphic substitution: for example, logical consistency is not closed under homomorphic substitution, but only under the inverse operation of substitutive generalization (A is a substitutive generalization of B iff there exists an s such that B = sA). So I arrive at my first thesis: Thesis 1: Proper logics have to be closed under syntactically isomorphic substitutions, but not necessarily under syntactically homomorphic substitutions. We may generalize this thesis in a semantical way. Homomorphic substitutions don't preserve validity because they may restrict the semantical freedom of interpretations, and the truth of possibility formulas is not preserved under restrictions of possible interpretations. Let us call a substitution function s semantically isomorphic iff it preserves the semantical freedom of interpretations. More precisely, this means that Ws =def {Is : I ∈ W} = W, where Is is the interpretation function which assigns to p what I assigns to sp. In informal worlds, the logical space of all possible interpretations of the substituted statements sp preserves the total space of interpretations - the sentences sp which are substituted for the primitives p∈P are pairwise logically independent from each other. Note that syntactically isomorphic substitution functions are a proper subclass of semantically isomorphic substitution functions. For example, the substitution function which assigns to each p∈P the

9

formula ¬p is semantically but not syntactically isomorphic. Assuming an enumeration of all p∈P, then another example of a semantically but not syntactically isomorphic substitution function would be, for example: spi = pi for i even, and spi = (p i ↔ pi-1) for i odd. My second thesis is this: Thesis 2: Logics have to be closed under semantically isomorphic substitutions. This is the strongest reasonable requirement

concerning closure under substitutions.

Theorem 5 tells us that C satisfies both requirements. Theorem 5: C is closed under all syntactically isomorphic and under all semantically isomorphic substitutions. Proof: Assume s is semantically isomorphic. We prove, by induction on the complexity of A ∈ Lprop, the following lemma: For all I∈W: Is |==A iff I |==sA. The induction steps for atoms and propositional connectives are trivial. For boxed formulas: Is |== A iff ∀Is∈Ws, Is |==A, iff ∀Is∈Ws, I |==A (by induction hypothesis), iff ∀I ∈W, I |==A (since Ws = W by semantic isomorphy of s), iff I |== A. - From the lemma and Ws = W we obtain ||sA iff ||A, hence sA ∈C whenever A ∈ C. This proves closure under semantically isomorphic substitutions, and thus also under syntactically isomorphic substitutions, because the latter are a subclass of the former. Q.E.D. So there is no reason not to regard C as a proper logic. In the contrary, C it is the only complete proper logic of logical necessity and possibility, since it is the only proper modal logic which contains ◊A for every satisfiable sentence A. We finally mention a further interesting application of semantically isomorphic substitution functions which shall be worked out in a separate paper. Each semantically isomorphic substitution function corresponds to a semantical intertranslation between two languages in the sense of Kanger (1968) and Schurz (1990). The important fact is here that

10

we have a bijection between the set of interpretations W and Ws, and hence also a bijection between their power sets. Since each formula of the two intertranslatable (propositional) languages L1 and L2 corresponds to an element of Ws or W, respectively, this bijection gives a bijective intertranslation function between formulas. It is the fundamental property of such intertranslations that they do not affect logical relationships: Γ | A iff t(Γ) | t(A), where Γ ⊆L1, A∈L1, and t:L1→L2 is the bijective translation function. This fact underscores the reasonableness of the requirement of logics to be closed under semantically isomorphic substitutions. 4. Axiomatization of C and (Non)Monotony of Rules

What is the reason why homomorphic substitutions never destroy the validity of logical theorems of classical propositional logic, predicate logic or Kripkean modal logic, although they destroy the validity of certain logical theorems of Carnapian modal logic? The reason has to do with the question of monotonic versus nonmonotonic rules, to which I turn now. This point will also explain why Makinson's conditions (b) and (c) are not equivalent. Keep in mind the distinction between a logic L abstractly defined as a set of semantically valid statements, and an axiomatization of L in the usual sense of a set of axioms, rules, and a definition of "proof". One usually assumes that the axiomatization is effective, which means that the question whether a statement is an instance of an axiom, or whether a sequence of statements is an instance of a rule, is decidable. Often, axioms and rules are formulated with help of schematic letters. Whenever this is the case, they are schematic in the sense explained in section 3, i.e., their instances are closed under substitution. First a clarification about the word "nonmonotonic". Given an inference relation |, the corresponding consequence operation C| is an operation on sets of formulas, C|:Pow(L)→Pow(L). C|is called monotonic iff Γ ⊆∆ implies C|(Γ) ⊆C|(∆). This corresponds to the use of this word in analysis, where a function f:Re→Re is called monotonic wr.t. an ordering relation < over Re iff x < y implies f(x) < f(y). Hence an inference relation is called monotonic iff the so-called law of weakening holds: Γ ⊆∆, Γ |

11

A implies ∆ | A. Otherwise, an inference relation (and its corresponding consequence operation) is called nonmonotonic. A rule is usually conceived as a pair, consisting of a finite set of preconditions and a conclusion. In traditional (monotonic) logics, the premises claim that certain (schematic) formulas are derivable, and the conclusion claims that another (schematic) formula is derivable. We call these formulas also the premise formulas and the conclusion formulas of the rule, respectively - but note that the proper premises and conclusion of rules are not merely object language formulas, but derivability claims associated with these formulas. For nonmonotonic logics, we need a broader conception of rules - we allow that the premises and the conclusion of a rule may also consist of non-derivability claims, saying that a certain formula is not derivable. Within this broader concept of rule, we call a rule monotonic, if the derivability of a conclusion formula depends solely on derivability of premise formulas (or likewise, if the non-derivability of the conclusion formula depends solely on non-derivability claims of premise formulas). A rule is called nonmonotonic, if the derivability of conclusion formulas may also depend on the non-derivability of premise formulas (or likewise, if the non-derivability of conclusion formulas may also depend on the derivability of premise formulas). This terminology is justified, because if R is a rule, and R(Γ) denotes the closure of formula set Γ under the rule R, then the operation R on formula sets will be monotonic in the previous sense (i.e., in the sense that Γ ⊆ ∆ implies R(Γ) ⊆R(∆)) iff the rule R is monotonic in the latter sense. Consider the two modal rules of C: (R ) | A / |

A

(R◊) ||-/- A / | ◊¬A

Both rules are schematic, i.e., the set of their instances are closed under homomorphic substitution. But while the left rule is monotonic, the right rule is nonmonotonic. A logic is called monotonically axiomatizable iff it has an axiomatization which consists only of monotonic rules containing only derivability claims. All of the mentioned traditional logics are monotonically axiomatizable in this sense. The relation to closure under substitution is

12

expressed in theorem 6. Theorem 6: If a logic is schematically and monotonically axiomatizable, then its theorems are closed under (homomorphic) substitutions. Proof: By simple induction on the length of proofs in the object language. The proof breaks down if the axiomatization contains nonmonotonic rules. For then, the induction hypothesis that derivable formulas are closed under substitution does not apply to the non-derivability assertion of one the premises of the non-monotonic rule. Q.E.D. Theorem 6 tells us that every axiomatization of a logic which is not closed under homomorphic substitutions must deviate from traditional axiomatizations in at least one of the following two respects. First, if this axiomatization keeps all axioms and rules schematic, then it must introduce nonmonotonic rules. Second: if it keeps the rules monotonic, then it must introduce some non-schematic axioms. The second strategy to axiomatize C exists already in the literature. The trick here is to isolate that part of C which is not closed under substitution and represent this part solely by axioms. Then monotonic rules will be sufficient for C. Such an axiomatization of C was first suggested by Cocchiarella (1975), who calls C the system S13, and in a more refined form by Hendry and Pokriefka (1985). Roughly speaking, Hendry and Pokriefka assume an S5-system and add an infinite list of possibility axioms to it which are not closed under substitution. I think that this second technique is not especially natural. The nonmonotonic rule (R◊) reflects the meaning of ◊ in C much more directly. Therefore, I think a schematic axiomatization of C which uses nonmonotonic rules is more natural. In what follows I present an axiomatization of an inference relation in C, |C, which is simply defined by strict truth preservation in all possible worlds: Γ |C A iff ∀I∈W: if I |== Γ , then I |== A. The inference relation |C is has mainly technical importance for axiomatizing the logic C: C = {A∈Lprop: ∅|C A}. This inference relation is monotonic, simply because all in-

13

ference relations defined via strict truth preservation in a fixed class W of interpretations are monotonic (for, if Γ1 ⊆ Γ2, then W(Γ2) ⊆ W(Γ1), where W(Γ) = {I∈W: I |==Γ}). How is this possible in spite of the nonmonotonic ◊-rule? Because this inference relation is irrelevant with respect to modal premises or modal conclusions, since modal formulas are always logically determined. Hence, modal premises or modal conclusions can be related to their conclusion partners, or premise partners, respectively, only via Verum ex Quodlibet or Ex Falsum Quodlibet: Γ |C A iff |C A or Γ |C ⊥ Γ, A |C B iff Γ |C B or A |C ⊥

likewise for ◊ likewise for ◊

It follows that the relevant inferential part of |C is restricted to the nonmodal part of C which is axiomatized by monotonic rules only. One axiomatization technique with help of nonmonotonic rules which is also applied in a family of nonmonotonic logics, the so-called defeasible logics, is to give a simultaneous axiomatization of the theorems as well as the non-theorems of the logic. I speak here of a simultaneous axiomatization. Let | A+ mean that A is derivable as a theorem, and | Amean A is derivable as a non-theorem. Then, a simultaneous axiomatization should satisfy the requirement of negation-adequateness, which consists of the conjunction of the following two requirements (cf. Schurz 1996): Negation-correctness:

| A- ⇒ |-/- A+

Negation-completeness:

|-/- A+ ⇒ | A-

A simultaneous axiomatization of C in propositional logic is possible by using natural deduction rules which hold in both directions and reduce complexity in one direction (i.e., are recursive). We state the rules as if-and-only-if-conditions - for use in the calculus, read them from right to left. For simplicity, I assume only ¬ and ∧ as connectives. Li stands for a literal, i.e. an unnegated or negated propositional variable.

14

Rules of Derivability (rule-direction ⇐): L1,…,Ln |C L L1,…,Ln |C ⊥

iff iff

L ∈ {L1,…,Ln} or L1,…,Ln |C ⊥ ∃L',L''∈ {L1,…,Ln} : L' = ¬L''

(Literal-Conc) (Literal-Prem)

Γ |C ¬¬A iff Γ |CA

(Negation-Conc)

Γ, ¬¬A |C B iff

(Negation-Prem)

Γ, A |CB

Γ|C A∧B iff Γ |C A and Γ |C B

(Conjunction-Conc)

Γ, A∧B |C C iff Γ, A, B |C C

(Conjunction-Prem)

Γ |C ¬(A∧B) iff Γ, A |C ¬B Γ, ¬(A∧B) |C C iff Γ, ¬A |C C or Γ, ¬B |C C

(NegConjunction-Conc)

Γ |C A iff |C A or Γ |C ⊥ Γ, A |C B iff Γ |C B or |-/-C A

(Necessity-Conc) (Necessity-Prem)

Γ |C ¬ A iff

(NegNecessity-Conc)

|-/-C A or Γ |C ⊥

Γ, ¬ A|C B iff Γ |C B or |C A

(NegConjunction-Prem)

(NegNecessity-Prem)

If we negate these equivalences and transform them by De Morgan rules, we obtain the corresponding dual axiomatization of the non-theorems by rules of non-derivability: Rules of Non-derivability (Rule direction

⇐ ):

L1,…,Ln |-/-C ⊥ iff ¬∃L',L''∈ {L1,…,Ln} : L' = ¬L'' L1,…,Ln |-/-C L iff L ∉ {L1,…,Ln} and L1,…,Ln |-/-C ⊥ Γ |-/-C ¬¬A iff Γ |-/-C A Γ, ¬¬A |-/-C B iff Γ, A |-/-C B

15

Γ |-/-C A∧B iff Γ |-/-C A or Γ |-/-C B Γ, A∧B |-/-C C iff Γ, A, B |-/-C C Γ |-/-C ¬(A∧B) iff Γ, A |-/-C ¬B Γ, ¬(A∧B)

|-/-C C iff Γ, ¬A |-/-C C and Γ, ¬B |-/-C C

Γ |-/-C A iff

|-/-C A and Γ |-/-C ⊥

Γ, A |-/-C B iff

Γ |-/-C B and |-/-C A

Γ |-/-C ¬ A iff

|C A and Γ |-/-C ⊥ Γ, ¬ A |-/-C B iff Γ |-/-C B and |-/-C A.

Theorem 8: The above axiomatization is schematic, correct, complete and decidable. Proof: Schematicity follows from the very formulation of the rules. Decidability holds, because the rules are recursive (reduce complexity) in the right-to-left direction. So for each sequent (i.e., for each derivability or nonderivability claim) which figures as proof-goal, the search for a proof will stop after finitely many steps at a sequent containing only literals, which can be decided by the Start rules. Correctness is shown by simple semantical means. Completeness follows from the fact that the rules are semantically valid in both directions. So, if a sequent is not derivable, its terminating sequent which contains only literals is not an instance of a Start-rule and hence not valid, whence (by induction on the length of the failed proof-attempt), also the original sequent can't be valid (this procedure is used in tableaux methods). Q.E.D. As we shall see in the next section, such a simultaneous axiomatization can only be effective iff the underlying logic is decidable.

16

5. Axiomatizability, Decidability, Correctness and Completeness It is well known that the theorems of an effectively axiomatizable logic are recursively enumerable - one calls this property also semi-decidability. Semi-decidability does not imply decidability. But in the logic of the kind discussed here, this distinction breaks down. First of all, every logical system L with an interpretational semantics - e.g. propositional logic, monadic or relational predicate logic, and even Kripkean modal logic - may be expanded into a Carnapian modal logic by adding the two Carnapian modal operators the two semantical interpretation clauses for

and ◊, and

and ◊. We call this logic the C-modal

expansion CL of L. Let L range over logic defined by an interpretational semantics. Then: Theorem 9: For any logic of kind CL: CL is (correctly, completely and effectively) axiomatizable if and only if CL is decidable. Proof: The direction from right to left is obvious. The direction from left to right follows from the well known fact that if both the theorems and the non-theorems of a logic are recursively enumerable, then the logic is decidable. But every logic CL has the property that ||-/- A iff ||◊¬A. Thus, if CL were effectively axiomatized, then we could construct a recursive enumeration of CL's non-theorems out of the given recursive enumeration of CL's theorems, since for every nontheorem A of CL, ◊¬A will eventually appear in the enumeration of theorems. Q.E.D. It follows that the Carnapian first order modal logic cannot be effectively axiomatized because if it were, it would be decidable, and hence first order logic, which is part of it, would be decidable. In other words, the undecidability of nonmodal first order logic implies the non-axiomatizability of first order C. That first order logic is undecidable has been disproved in 1936 by Church. It is interesting that in 1946, Carnap regarded the axiomatizability of first order C as an open question (p. 63). Since we can assume that Carnap was aware of Church' results at that time, we may conjecture that he was not aware of this

17

connection. Also the distinction between semantical correctness and completeness breaks down for axiomatizations of Carnapian modal logics, if we assume that their axiomatization is consistent and that the two schematic modal rules are admissible in them. Theorem 10: For every consistent axiomatization of a logic of kind CL in which the rules (R ) and (R◊) are admissible, the following holds: CL is semantically correct if and only if it is semantically complete. Proof: Assume CL correct and ||A. Then ||-/- ◊¬A. Correctness implies |-/- ◊¬A. Hence | A by (R◊), so CL is complete. Assume CL complete and | A. Then | A by (R ), hence |-/- ¬ A by consistency. So ||-/- ¬ A = ◊¬A by completeness. Hence ||A, so CL is correct. Q.E.D. It is easily proved that these results are generalizable to all simultaneously axiomatizable logics which posses the property of negation adequateness. Theorem 11: In every simultaneously axiomatizable logics with negation adequateness, effectivity of axiomatization coincides with decidability, and semantical correctness coincides with semantical completeness. Proof: See Schurz (1996), p. 226f, observations 5.2-4. This result is not only of interest for the mentioned defeasible nonmonotonic logics, but also for the programming language PROLOG, since the negation by failure operator of PROLOG has the negation adequacy property. 6. A nonmonotonic inference relation based on C

18

In 1999 and in a several previous papers, Georg Gottlob has investigated further properties of the logic C. In particular, Gottlob suggests to define a nonmonotonic C-inference relation, |∼∼C, in the following way: the C-conclusions of a nonmodal premise set T, intuitively a theory, should be those nonmodal and modal sentences which are valid in the space of all worlds which verify T. Let W(T) ={I : I |==T} and SW(T) be the system of formulas defined in the sense of Hendry and Pokriefka (cf. section 3) - more precisely, SW(T) = {A∈L: ∀I∈W(T), I |==A}, where the truth-clause for

-formulas is relativized to

the set W(T): I |== A iff ∀I∈W(T): I |==A. Then: Definition of ||∼∼C:

T ||∼∼C A iff A ∈ SW(T).

A first important application of this consequence relation which Gottlob does not discuss is a theory-relativized conception of nonlogical (e.g. physical) necessity and possibility: A is necessary iff it follows from the given theory T, and A is possible iff its negation is consistent with T. This leads to the following philosophical interpretations. Let T be an 'ideally complete' physical theory implying all laws of nature. Then: T ||∼∼C

A:

A is true by laws of nature

T ||∼∼C ◊A and A true: A is contingently true (e.g., an initial or boundary condition) T ||∼∼C ◊A:

A is possible by laws of nature

T ||∼∼C ◊A and A false: A was not prescribed by laws of nature . The nonmonotonicity of ||∼∼C is explained by the fact that if T gets stronger, not only new necessity statements are inferable, but also old possibility statements are no longer inferable. For example: Assumption:

T |-/- p. Then:

Hence:

T ||∼∼ C ◊¬p

(since T ||∼/∼C p)

But:

T, p ||∼/∼C ◊¬p

(since T, p ||∼∼C

p)

19

In the enriched theory T* = T ∪ {p}, ◊¬p is no longer derivable. A second application of the nonmonotonic inference relation ||∼∼C is autoepistemic nonmonotonic logic. For this application we refer the reader to the work of Gottlob (1999), where this application is extensively discussed; for an overview on autoepistemic logic cf. Konolige (1994).

References Carnap, R. (1946): "Modality and Quantification", Journal of Symbolic Logic 11, 33 - 64. Carnap, R. (1947): Meaning and Necessity, University of Chicago Press, Chicago. Cocchiarella, N. B. (1975): "Logical Atomism, Nominalism, and Modal Logic", Synthese 31, 23 67. Feys, R. (1963): "Carnap on Modalitis", in: P. A. Schilpp (ed.), The Philosophy of Rudolf Carnap, LaSalle, Open Court, 283 - 297. Gottlob, G. (1999): "Remarks on a Carnapian Extension of S5", in: J. Wolenski, E. Köhler (eds.), Alfred Tarski and the Vienna Circle, Kluwer, Dordrecht, 243 - 259. Hendry, H. E., Pokriefka, M. L. (1985): "Carnapian Extensions of S5", Journal of Philosophical Logic 14, 111 - 128. Kanger, S. (1968): "Equivalent Theories", Theoria 34, 1 - 16. Konolige, K. (1994): "Autoepistemic Logic", in: Gabbay, D. M. et al. (eds.), Handbook of Logic in Artificial Intelligence and Logic Programming, Vol. 3: Nonmonotonic Reasoning and Uncertain Reasoning, Clarendon Press, Oxford. Kripke, S. (1959): "A Completeness Theorem in Modal Logic", Journal of Symbolic Logic 24/1, 1 14. Makinson, D. (1966): "How Meaningful are Modal Operators", Australasian Journal of Philosophy 44, 331 - 337. Makinson, D. (1971): "Some Embedding Theorems for Modal Logic", Notre Dame Journal of Formal Logic 12, 252 - 254. Schurz, G. (1990): "Sprachabhängigkeit der Erkenntnis. Eine logische Analyse", in: R.Wohlgenannt et al. (Hg.), Reflexion und Wirklichkeit, VWGÖ, Vienna, 309 - 327. Schurz, G. (1996): "The Role of Negation in Nonmonotonic Logic and Defeasible Reasoning", in: H. Wansing (ed.), Negation. A Notion in Focus, W. de Gruyter, Berlin, 197-231. Schurz, G. (1997): The Is-Ought Problem. An Investigation in Philosophical Logic, Kluwer (Studia

20

Logica Library), Dordrecht. Schurz, G. (1999): "Tarski and Carnap on Logical Truth - or: What is Genuine Logic?", in: J. Wolenski, E. Köhler (eds.), Alfred Tarski and the Vienna Circle, Kluwer, Dordrecht, 77 - 94. Thomason, S. K. (1973): "A New Representation of S5", Notre Dame Journal of Formal Logic 14/2, 281 - 284.