A completeness proof for an infinitary tense-logic

A completeness proof for an infinitary tense-logic by

GORAN SUNDHOLM (University of Uppsala)

I n his forthcoming examination of G. H. von Wright’s tense-logic [4],Krister Segerberg studies certain infinitary extensions of the original tense-logic created by von Wright. For one of these extensions the completeness problem turned out t o be harder than was expected a t first sight1 This paper is devoted t o a proof of a completeness theorem for the extension in question, called W1 by Segerberg. We use a countable language of ordinary propositional logic supplied with two modal operators: o (“tomorrow”) and I? (‘‘.Iways”). The relevant semantics for tense-logic based on this language uses the frame 3 = (N, 5 >, where the successorrelation is the accessibility-relation for o and < for I?, i.e., the formula o (A) is true a t the point n E N iff A is true a t n + 1, and the formula O A is true at n EN iff for all k 2 n A is true at k. We assume that the reader is familiar with ordinary Kripkesemantics for modal languages and, in particular, that he understands what it means that ’’% is a model on the frame %”. We shall use oI”(A)as a shorthand for I ,

-

o(o( . . . o ( A ) ...)). k times Professor Segerberg’s original proof idea turned out t o be incomplete in that it used the Lindenbaum lemma, as is usual in canonical model proofs. Because of the infinitary rules we do not have immediate access t o the Lindenbaum lemma, and I then undertook t o prove the lemma using the proof theoretic machinery hinted at the end of the paper. However, Professor Dag Prawitz pointed out an embarassing error in my argument for which I am very grateful. I also want t o express my gratitude t o Professor Segerberg for much encouragement.

48

G6RAN SUNDHOLM

Let 2 be a set of formulae from our language. 2 is said t o have a model on 5.R if there is a model on 5.R such that for some n EN it holds k n A, for every A in 2. The main part of Professor Segerberg’s paper is spent on a proof that if a finite 2 is consistent in von Wright’s tense logic, then it has a model on ‘3. Since the rules of von Wright’s logic are finitary, a set is consistent iff all its finite subsets are. As Segerberg observes, the set 8 = { - U p } U { on(p) : n EN} is consistent in von Wright’s logic, for every finite subset thereof has a model on ’3 and is thus consistent. e itself, however, has no model on 3. In order t o improve on this fact Segerberg introduces an infinitary extension WI of von Wright’s logic. WI is given by a Prawitz-type natural deduction system, and we assume some familiarity with, e g , [3]. For every n E N

a

on(B)

-,

on(o A )

nE(n)

-on(-B) A

o.’lccA)k=O,

on(-,B)

on(B)

-A

1, 2, ...

We will prove the following theorem, first stated by Segerberg in S 5 of [4].

A COMPLETENESS PROOF FOR AN INFINITARY

TENSE-LOGIC

49

THEOREM. I f Z is consistent in WI it has a model on 3, The proof is of the Henkin-type and is modelled on Feferman’s completeness-proof for L,,, in [l]. The crux of the proof is the fundamental LEMMA. If Z is a consistent set in WI, then so is Z U {o?,+k(A) + on(oA)}, for some k E N . Proof. Assume not. Then 2 U { o ~ + ” (+ A )on( uA)} is inconsistent for each lz. Hence, for each k E N , 2 t i ( o n + k ( A ) + on(uA)), Z t o~+K(A) A -on(oA), hence 2 t ~ n + k ( A ) and hence Z t -on(oA), and thus 2 t oa(oA) and Z t -o~(oA), by rule oI(n), which contradicts the consistency of Z.

Let Z be a consistent set in WI and (A,,, Al, . . .> an enumeration of our language. We define Zo= Z,

ZZnU {A,} if this is consistent, -An} otherwise, U ( o m + l i ( B ) +O ~ ( O B ) } ~ ~ A , = O ~ ( O B ) , 2’2n+l otherwise. In step 2 n + 2 , k should be chosen as small as possible while preserving consistency according to the Lemma. We observe that by construction each 2% is consistent in WI. Let A = U Zn. This set A has all the properties needed for a canonical model proof. (i) For all A, A E d or -.A E A , but not both. Proof. A = A,, for some n. In step 2n + 1 either A or -A is added. If both are in d then they are in some Z, but this contradicts consistency. (ii) 0nC-A) E d iff on(A)@ A . Proof. If 0nC-A) E il and o ~ ( AE)d then both are in some z,, which would then be inconsistent by two applications of rule -I(n). If O n ( A ) @d then - o ~ ( A )E A . Assume ofi(-A)@d. Then -on(-A)Ed. But then some Zk would be inconsistent by rule i E ( n ) . 4

- Theoria 1: 1977

50

GdRAN SUNDHOLM

(iii) o ~ ( BA C) E A iff o ~ ( B E) d and O n ( C ) E A . Proof. Assume on(B), on(C) and -on(B A C) all belong to d . The some Zkis inconsistent by rules /\I(.) and -E(O). The converse is similar. (iv) o n ( A V B ) E d iff o ~ ( AE) d or ofz(B) E d . Proof. Similar t o (iii). (v) o ~ ( A -+ B ) E d iff On(A) E 3 implies OQ) E d . Proof. There is no difficulty in showing the statement from left t o right. Assume for other way that the right hand is true but -.on(A -+ B) E d . Two cases: (a) o n ( B ) E A . Then -On(A -+ B ) , on@) both belong t o some Zk, which would be inconsistent by rules -+ I(.) and -E(O). (b) o ~ ( B ) @ A . Then on(A)@d and thus -on(A) E A . Hence -O.(A) and 1 0 n ( A -+ B ) belong t o some Zk. Then Zklon(A)t o ~ ( B by ) rule -E(O) and thus Zkt @(A -+ B), which contradicts the consistency. (vi) o ~ ( o AE) d iff o n + k ( A ) E A , all k E N . Proof. Left t o right is again easy. For the other way we use that by construction there is a formula ~ n + k ( A -+) o ~ ( u A )in d . If the right side is true and the left false, then by using the formula above some Zmwould be inconsistent. The model is now defined by

rn F~ p iff on(p) E A , for propositional letters p . Using (i)-(vi)

it requires no effort t o prove that

%R I nA iff on(A) E d , for all A. Hence by putting n = 0 we get the required model on %, not only for 2 but also for d . Note that the countability of the language is used essentially in the proof. It should be remarked here that by dropping V and from our language and adding absurdity I as a primitive with the rules

-

A COMPLETENESS PROOF FOR AN INFINITARY TENSE-LOGIC

51

then one will get a system that is easily seen t o be mutually interpretable with W2. For this system one proves without much effort a normalization theorem along the lines of [3] and [2]. The remarkable ease with which the natural deduction methods work for W l , and especially for the modified version hinted at above, should be credited to the great analogy between WI and Peano arithmetic with the omega-rule for which it is well-known that a smooth proof theory exists.

References [l] SOLOMONFEFERMAN. “Lectures on proof theory”. In Proceedings of the Summer School of Logic, Leeds, 1967, Lecture notes in mthematics, vol. 70, pp. 1-107 (Berlin: Springer, 1968) [2] PER MARTIN-L~P. “Infinite terms and a system o f natural deduction.” Compositio mathematica, vol. 24 (1972), pp. 93-103. [3] DAG PRAWITZ. Natural deduction: A proof-theoretical study. (Stockholm: Almqvist & Wiksell, 1965) [4] KRISTERSEGERBERG. “von Wright’s tense logic.” Forthcoming in The philosophy of G. H. uon Wright, t o be edited by P. A. Schilpp.

Received on January 30, 1976.