Computer Science Logic. 9th Workshop, csl'95. Paderborn. Selected Papers (Springer, Berlin, 1996) 1–15 Incompleteness of a First-order Gödel Logic and some Temporal Logics of Programs Matthias Baaza,?, Alexander Leitschb, Richard Zachb a Institut für Algebra und Diskrete Mathematik E118.2, Technische Universität Wien, A–1040 Vienna, Austria b Institut für Computersprachen E185.2, Technische Universität Wien, A–1040 Vienna, Austria Abstract. It is shown that the infinite-valued first-order Gödel logic G0 based on the set of truth values {1/k : k ∈ ω \ {0}} ∪ {0} is not r.e. The logic G0 is the same as that obtained from the Kripke semantics for first-order intuitionistic logic with constant domains and where the order structure of the model is linear. From this, the unaxiomatizability of Kröger's temporal logic of programs (even of the fragment without the nexttime operator ©) and of the authors' temporal logic of linear discrete time with gaps follows. Keywords: temporal logic, intermediate logic, many-valued logic MR Classification: 03B45, 03B50, 03B55 1 Introduction In [4], Kurt Gödel introduced a sequence of finite-valued logics Gn in order to show that there are infinitely many propositional systems intermediate in strength between classical and intuitionistic propositional logic. In [3], Dummett considers the natural infinite-valued analogue LC of Gödel's systems and shows that it is axiomatized using the intuitionistic propositional calculus plus the axiom schema (A ⊃ B) ∨ (B ⊃ A). Little is known about first-order versions of Dummett's LC and related systems and about infinite-valued first-order logics in general. The most famous result (Scarpellini [8]) in this area is that the infinitevalued first-order Lukasiewicz logic is not recursively axiomatizable. We arrive at a first-order Gödel logic by taking the truth functions for the propositional connectives and defining truth functions for universal and existential quantifiers as infimum and supremum over the truth values, respectively. It is worth pointing out right away that which logic we get depends crucially on the order type of the set of truth values. In Section 2 we define these logics and describe their differences. The main result of this paper is that a particular Gödel logic G0, namely that based on the set of truth values V 0 = { 1/k : k ∈ ω\{0} } ∪{0}, is not recursively axiomatizable. Indeed, already the ∃-free fragment is not r.e. We give the proof in Section 3. ? Corresponding author. Email addresses: {baaz, leitsch, zach}@logic.tuwien.ac.at. This work is supported by FWF grant P–10282 MAT. 1 The main interest of Dummett's LC is that it axiomatizes linear intuitionistic Kripke semantics: LC is the set of all propositional formulas valid in all Kripke trees consisting of just one branch. We see that there is a strong connection between infinite-valued Gödel logic and logics based on linearly ordered models. In the first-order case it turns out that the logic defined by linearly ordered Kripke structures and constant domains ILC is exactly the same as G0. The logic we get by dropping the requirement that the domains are constant, IL, is arguably the more natural analogue to LC in the first-order case. We obtain the result that the set of validities of IL is not r.e. as a corollary to the result for G0 (which is equal to ILC). Other logics based on linearly ordered Kripke structures are, e.g., variants of Kröger's [5] Temporal logic of programs TL. TL is based on the temporal operators 2 (henceforth) and © (nexttime) and is characterized by temporal structures order isomorphic to ω. It is known [9, 6, 7] that first-order TL is not axiomatizable. The logic arising from temporal structures that have the form of trees of segments each of which is order-isomorphic to ω is axiomatizable [2]. It has been an open question whether the logic based on chains of segments orderisomorphic to ω is axiomatizable or not. In Section 4 we use the incompleteness result to give a negative answer to this question. We also strengthen the result of [6]: Already first-order TL without © is not axiomatizable. 2 First-order Temporal, Intuitionistic and Gödel Logics We shall work in a usual language L of predicate logic containing countably many variables (x, y, z, . . . ), function symbols (s, h, . . . ), predicate symbols (P , Q, R, . . . ), connectives (∧, ∨, ⊃, ¬) and the universal (∀) and existential (∃) quantifiers. The language L extended by the temporal operators 2 (henceforth always) and © (next time) is denoted Lt. The set of (closed) formulas of L resp. Lt is denoted Frm(L) resp. Frm(Lt). For a given interpretation K we will also consider extended languages LK where the elements of a given domain are added as constant symbols the interpretation of which is fixed. We proceed to define Kripke semantics for first-order temporal logics. These logics are all based on discrete time; this reflects their use in theoretical computer science where "time" is taken to be the discrete states of program executions (see [5]). Definition 21. Let T be a denumerable partially ordered set. T belongs to the class L of linear discrete orders iff it is order isomorphic to ω; it belongs to the class T of trees if it is order isomorphic to a rooted tree; it belongs to the class G of linear discrete orders with gaps if it is order isomorphic to an ω-chain of ω-segments (i.e., to ω *ω); it belongs to the class B of linear discrete orders with branching gaps iff it is order isomorphic to a rooted tree of ω-segments. Definition 22. Let W be L, G, or B, and let Frm(Lt) be the set of formulas over some first-order temporal language. A temporal structure K for Lt is a tuple 〈T, {Di}i∈T , {si}i∈T , s〉, where T ∈ W, Di is a set called the domain at state i, 2 Di ⊆ Dj if i ≤ j, si is a function mapping n-ary predicate symbols to functions from Dni to {>,⊥}, and s is a function mapping n-ary function symbols to functions from ⋃ Di → ⋃ Di s.t. s(f)(d1, . . . , dn) ∈ Di for di ∈ Di, in particular for d ∈ Di, s(d) = d. The valuation function s can be extended in the obvious way to a function on all terms. We define the valuation functions Ki from Frm(LK) to {>,⊥} as follows. Suppose A ∈ Frm(LK). (1) A ≡ P (t1, . . . , tn): Ki(A) = si(P ) ( s(t1), . . . , s(tn) ) (2) A ≡ ¬B: Ki(A) = > if Ki(B) = ⊥, and = ⊥ otherwise. (3) A ≡ B ∧ C: Ki(A) = > if Ki(B) = Ki(C) = >, and = ⊥ otherwise. (4) A ≡ B ∨ C: Ki(A) = > if Ki(B) = > or Ki(C) = >, and = ⊥ otherwise. (5) A ≡ B ⊃ C: Ki(A) = > if Ki(B) = ⊥ or Ki(C) = >, and = ⊥ otherwise. (6) A ≡ (∀x)B(x): Ki(A) = > if Ki[d/x](A(d)) = > for every d ∈ Di, and = ⊥ otherwise (7) A ≡ (∃x)B(x): Ki(A) = > if Ki[d/x](A(d)) = > for some d ∈ Di and = ⊥ otherwise (8) A ≡ 2B: Ki(A) = > if Kj(B) = > for every j ≥ i, and = ⊥ otherwise. (9) A ≡ ©B: Ki(A) = > if Ki+1(B) = >, and = ⊥ otherwise A is satisfied in a temporal structure K, K |=t A, iff K0(A) = >. Definition 23. We define the following logics: Linear discrete temporal logic TL is the set of all A ∈ Frm(Lt) s.t. K = 〈T, {Di}i∈T , {si}i∈T , s〉 with T ∈ L satisfies A. Linear discrete temporal logic with constant domains TLC is the set of all A ∈ Frm(Lt)every K = 〈T, {Di}i∈T , {si}i∈T , s〉 with T ∈ L and Di = Dj for all i, j ∈ T satisfies A. Linear discrete temporal logic with gaps TG is the set of all A ∈ Frm(Lt) s.t. K = 〈T, {Di}i∈T , {si}i∈T , s〉 with T ∈ G satisfies A. Linear discrete temporal logic with gaps and constant domains TGC is the set of all A ∈ Frm(Lt)every K = 〈T, {Di}i∈T , {si}i∈T , s〉 with T ∈ G and Di = Dj for all i, j ∈ T satisfies A. Linear discrete temporal logic with branching gaps TB is the set of all A ∈ Frm(Lt) s.t. K = 〈T, {Di}i∈T , {si}i∈T , s〉 with T ∈ B satisfies A. As indicated in the introduction, the logic TL is not axiomatizable. This was shown for the original formulation of Kröger by Szalas [9] and Kröger [6] (two binary function symbols have to be present for the results to hold). If the operator until is also present, or if local variables (i.e., variables whose interpretation may me different for each state) are allowed, then the empty signature suffices, as was shown by Szalas and Holenderski [10] and Kröger [6], respectively. These results were strengthened and extended in various ways by Merz [7]. In fact, to be precise, Kröger's original formulation TLV differs from TL as defined here in several respects: it has (1) constant domains, (2) rigid predicate symbols (i.e., the interpretation of the predicate symbols is the same for each state) and (3) 3 local variables. Merz [7, Lemma 1] shows that the validity problem for TLC can be reduced to to the validity problem for TLV. Hence, our results extend also to Kröger's original formulation. On the other hand, TB is axiomatizable by a sequent calculus presented in [2]. Next we give Kripke semantics for various fragments of first-order intuitionistic logic. We use the term "intuitionistic logic" par abus de langage: "Real" intuitionistic logic is defined not via Kripkeor any other semantics but by Heyting's calculi which he extracted from the writings of Brouwer. It is a more recent discovery that one can give Kripke semantics for these logics which are complete for the calculi. This completeness result, however, is of doubtful value from the intuitionistic point of view. Definition 24. Let Frm(L) be the set of formulas over some first-order language, and let T bei in T or L. An intuitionistic Kripke-structure K for L is a tuple 〈T, {Di}i∈T , {si}i∈T , s〉, where Di is a set called the domain at state i, Di ⊆ Dj if i ≤ j, si is a function mapping n-ary predicate symbols to functions from Dni to {>,⊥}, and s is a function mapping n-ary function symbols to functions from ⋃ Di → ⋃ Di s.t. s(f)(d1, . . . , dn) ∈ Di for di ∈ Di, in particular for d ∈ Di, s(d) = d. The valuation si has to satisfy a monotonicity requirement: if si(P (d)) = > then sj(P (d)) = > for all j ≥ i. The valuation function s can be extended in the obvious way to a function on all terms. We define the valuation functions Ki from Frm(LK) to {>,⊥} as follows. Suppose A ∈ Frm(LK). (1) A ≡ P (t1, . . . , tn): Ki(A) = si(P ) ( s(t1), . . . , s(tn) ) . (2) A ≡ ¬B: Ki(A) = > iff Kj(B) = ⊥ for all j ≥ i, and = ⊥ otherwise. (3) A ≡ B ∧ C: Ki(A) = > iff Ki(B) = Ki(C) = >, and = ⊥ otherwise. (4) A ≡ B ∨ C: Ki(A) = > iff Ki(B) = > or Ki(C) = >, and = ⊥ otherwise. (5) A ≡ B ⊃ C: Ki(A) = > iff for all j ≥ i, Kj(B) = ⊥ or Kj(C) = >, and = ⊥ otherwise. (6) A ≡ (∀x)B(x): Ki(A) = > if Kj [d/x](A(d)) = > for every j ≥ i and every d ∈ Dj , and = ⊥ otherwise. (7) A ≡ (∃x)B(x): Ki(A) = > if Ki[d/x](A(d)) = > for some d ∈ Di and = ⊥ otherwise. A is satisfied in an intuitionistic Kripke structure K, K |=i A, iff K0(A) = >. Definition 25. We define the following logics: Intuitionistic logic I is the set of all A ∈ Frm(L) s.t. every K = 〈T, {Di}i∈T , {si}i∈T , s〉 with T ∈ T satisifies A. Linear intuitionistic logic IL is the set of all A ∈ Frm(L) s.t. every K = 〈T, {Di}i∈T , {si}i∈T , s〉 with T ∈ L satisfies A. Linear intuitionistic logic with constant domains ILC is the set of all A ∈ Frm(A) s.t. every K = 〈T, {Di}i∈T , {si}i∈T , s〉 with T ∈ L and Di = Dj for all i, j ∈ T satisfies A. 4 As usual, if L is some logic, we write L |= A for A ∈ L. First-order Gödel logics are given by a first-order language, truth functions for the connectives and quantifiers, and a set of truth values. The sets of truth values for the systems we consider are subsets of [0, 1]; the designated truth value is 1. The propositional versions of these logics were originally introduced by Gödel [4], and have spawned a sizeable area of logical research subsumed under the title "intermediate logics" (intermediate between classical and intuitionistic logic). Interpretations are defined as usual: Definition 26. Let V ⊆ [0, 1] be some set of truth values which contains 0 and 1 and is closed under supremum and infimum. A many-valued interpretation I = 〈D, s〉 based on V is given by the domain D and the valuation function s where s maps atomic formulas in Frm(LI) into V and n-ary function symbols to functions from Dn to D. s can be extended in the obvious way to a function on all terms. The valuation for formulas is defined as follows: (1) A ≡ P (t1, . . . , tn) is atomic: I(A) = s(P )(s(t1), . . . , s(tn)). (2) A ≡ ¬B: I(A) = { 0 if I(B) 6= 0 1 otherwise. (3) A ≡ B ∧ C: I(A) = min(I(B), I(C)). (4) A ≡ B ∨ C: I(A) = max(I(A), I(B)). (5) A ≡ B ⊃ C: I(A) = { I(C) if I(B) > I(C) 1 if I(B) ≤ I(C). The set {I(A(d)) : d ∈ D} is called the distribution of A(x), we denote it by DistrI(A(x)). The quantifiers are, as usual, defined by infimum and supremum of their distributions. (6) A ≡ (∀x)B(x): I(A) = inf DistrI(B(x)). (7) A ≡ (∃x)B(x): I(A) = sup DistrI(B(x)). I satisfies a formula A, I |=m A, if I(A) = 1. In considering first-order infinite valued logics, care must be taken in choosing the set of truth values. In order to define the semantics of the quantifier we must restrict the set of truth values to those which are closed under infima and suprema. Note that in propositional infinite valued logics this restriction is not required. For instance, the rational interval [0, 1]∩Q will not give a satisfactory set of truth values. The following, however, do: VR = [0, 1] V 0 = { 1/k : k ∈ ω \ {0} } ∪ {0} V 1 = { 1− 1/k : k ∈ ω \ {0} } ∪ {1} The corresponding infinite-valued Gödel logics are GR, G0, and G1. 5 Definition 27. GR is the set of all A ∈ Frm(L) s.t. for every I based on VR, I |=m A. G0 is the set of all A ∈ Frm(L) s.t. for every I based on V 0, I |=m A. G1 is the set of all A ∈ Frm(L) s.t. for every I based on V 1, I |=m A. Note that V 0 is order isomorphic to the set of truth values for LC (ω + 1, with 0 designated and reverse order); hence G0 is the natural generalization of LC to first-order. The corresponding propositional systems all have the same sets of tautologies, as can easily be seen. In other words, propositional infinitevalued logic is independent of the cardinality or order type of the set of truth values. The finite-valued versions are all distinct, however, and in fact LC is the intersection of all finite-valued Gödel logics. The first-order infinite-valued systems are not equivalent, however. Proposition 28. Let C = (∃x)(A(x) ⊃ (∀y)A(y)) and C ′ = (∃x)((∃y)A(y) ⊃ A(x)) Then (1) I(C) = 1 if DistrI(A(x)) has a minimum (w.r.t. I) and = I((∀y)A(y)) otherwise. (2) I(C ′) = 1 if DistrI(A(x)) has a maximum and = I((∃y)A(y)) otherwise. Proof. (1) Let us assume that DistrI(A(x)) has the minimum d. I(A(d)) = I((∀y)A(y)) and therefore I(A(d) ⊃ (∀y)A(y)) = 1 and I(C) = 1. If DistrI(A(x)) does not have a minimum then I(A(d)) > I((∀y)A(y)) for all d ∈ D(I) and, by definition of the semantics of ⊃, I(A(d) ⊃ (∀y)A(y)) = I((∀y)A(y)) for all d ∈ D(I); thus also the supremum I(C) gets this value. (2) If DistrI(A(x)) has the maximum d then, similarly, I(A(d)) = I((∃y)A(y)) and I(C ′) = 1. If DistrI(A(x)) does not have a maximum then we always have I((∃y)A(y)) > I(A(d)) and I((∃y)A(y) ⊃ A(d)) = I(A(d)), whence I(C ′) = sup DistrI(A(x)) = I((∃y)A(y)).  Corollary 29. Let C and C ′ be defined as in Proposition 28. Then C ′ is valid in both G0 and G1. C is valid in G1 but not in G0. Neither C nor C ′ are valid in GR. Proof. C ′ is valid in G0 because every supremum is a maximum; it is also valid in G1 because the only supremum which is not a maximum is 1. C is not valid in G0 because there exists a sequence of truth values converging to 0, having no minimum and I((∀y)A(y)) = 0. In G1 every infimum is also a minimum and thus C is valid in G1. C and C ′ are both nonvalid in GR because – at arbitrary places in the open interval (0, 1) there are infinite (increasing and decreasing) sequences without maximum and minimum.  6 Note that both C and C ′ are valid in classical logic and not valid in intuitionistic logic. Dummett's formula (A ⊃ B) ∨ (B ⊃ A) is also not valid intuitionistically, but-of course-it is true in all three infinite-valued Gödel logics: Whatever A and B evaluate to, one of them is certainly less than or equal to the other. Proposition 210. For any first-order formula A, G0 |= A iff ILC |= A. Proof. Only if: Let K = 〈ω,D, {si}i∈ω, s〉 be an ILC interpretation. Define the maps φK: Frm(LK) → {>,⊥}ω and φK: Frm(LK) → V 0 as follows: φK(A) = 〈Ki(A)〉i∈ω φK(A) = { 1/(min{i : Ki(A) = >}+ 1) if Ki(A) = > for some i 0 otherwise Note that the monotonicity proviso in the definition of ILC-interpretations implies that φ(A) is of the form {⊥}n_{>}ω for some n ∈ ω, or equals {⊥}ω. We can now associate to each ILC-interpretation K a many-valued interpretation IK = 〈D, sK〉 by setting sK(A) = φK(A) for A atomic in LK. It is then easily proved, by induction on the complexity of a formula A, that IK(A) = φK(A). The only nontrivial induction step is that concerning implication. Suppose IK(A) = φK(A), IK(B) = φK(B). (IH) (1) K0(A ⊃ B) = >: By definition of the ILC-semantics we get Ki(A) = ⊥ or Ki(B) = > for all i ∈ ω. Moreover, by definition of φK, we have φK(A ⊃ B) = 1. (a) K0(A) = >: By definition of the ILC-semantics, Ki(A) = > for all i ∈ ω. From K0(A ⊃ B) = > we thus get Ki(B) = > for all i ∈ ω. By definition of φK, φK(A) = φK(B) = 1 and, by (IH), IK(A) = IK(B) = 1. So the G0-semantics yields IK(A ⊃ B) = 1. (b) K0(A) = ⊥: Let mA = min{j : Kj(A) = >}, mB = min{j : Kj(B) = >}. mA and mB may be undefined. But by K0(A ⊃ B) = > and the ILC-semantics mB can only be undefined ifmA is too. If both are defined then mB ≤ mA. By definition of φK this gives us φK(A) ≤ φK(B). (IH) yields IK(A) ≤ IK(B) and the semantics of G0 that IK(A ⊃ B) = 1. (2) K0(A ⊃ B) = ⊥: By definition of the ILC-semantics there exists a j ∈ ω s.t. Kj(A) = > and Kj(B) = ⊥. Let m be the least such. By the ILCsemantics Kj(A) = > for all j ≥ m and m < min{j : Kj(B) = >} giving φK(B) < φK(A). From (IH) we thus derive IK(B) < IK(A) and, by the semantics of G0, IK(A ⊃ B) = IK(B). If Kj(B) = ⊥ for all j ∈ ω then, by definition of φK, φK(A ⊃ B) = φK(B) = 0. From IK(B) = φK(B) = 0 we get φK(A ⊃ B) = IK(A ⊃ B). If, on the other hand, Kj(B) = > for some j ∈ ω then φK(B) = φK(A ⊃ B). By (IH) we get φK(B) = IK(B) and finally φK(A ⊃ B) = IK(A ⊃ B). This concludes the induction step. It immediately follows that if ILC 6|= A then G0 6|= A. 7 If: Conversely, let I = 〈D, s〉 be a G0-interpretation. Let KI = 〈ω,D, {si}i∈ω, s′〉 be given by: si(A) = { > if I(A) ≥ 1i+1 ⊥ otherwise. for atomic A, and s′ according to the interpretation of the function symbols in s. Again by induction on the complexity of formulas we have I(A) = φKI(A), in particular, KI 6|=i A if I 6|=m A.  3 Incompleteness of G0, ILC and IL We proceed to prove that the valid formulas of G0are not recursively enumerable. In contrast to this result, all finite-valued Gödel logics are r.e. [1] as well as GR [11] (GR there appears as intuitionistic fuzzy logic). Proposition 31. Let I be a G0interpretation, A a formula and v = I((∀x)¬[A(x) ⊃ (∀y)A(y)]) Then v = 0 if DistrI(A(x)) has a minimum and v = 1 otherwise. Proof. Just as in Proposition 28: Suppose DistrI(A(x)) has a minimum v, let d ∈ D be s.t. I(A(d)) = v. Then I(A(d)) = I((∀y)A(y)), so I(¬[A(d) ⊃ (∀y)A(y)]) = 0. Conversely, if DistrI(A(x)) has no minimum, then I((∀y)A(y)) = 0 and I(A(d)) > 0 for all d ∈ D. Hence I(A(d) ⊃ (∀y)A(y)) = 0, and I(¬[A(d) ⊃ (∀y)A(y)]) = 1 for all d ∈ D.  In order to prove the main theorem of this chapter we need some tools from recursion theory. Definition 32. Let ψ be an effective recursive enumeration of the set PR11 of all primitive recursive functions from ω to ω. We define a two place function φ (which enumerates a subclass of PR11): φk(x) = 0 if x = 00 if ψk(y) = 0 for 1 ≤ y ≤ x1 otherwise The index set Oφ is defined as {k : (∀y)φk(y) = 0}. Proposition 33. The index set Oφ is not recursively enumerable. Proof. By definition of φ, {k : (∀y)φk(y) = 0} = {k : (∀y)ψk(y) = 0}. But for every g ∈ PR11 the index set {k : (∀y)ψk = g} is Π1-complete. Therefore Oφ is Π1-complete and thus not recursively enumerable.  The essence of the incompleteness proof is represented by a sequence of formulas (Ak)k∈ω constructed via φ s.t. G0 |= Ak ⇐⇒ k ∈ Oφ i.e. Oφ is m-reducible to the validity problem of G0. 8 Definition 34. Let P be a one-place predicate symbol, s be the function symbol for the successor function and 0 be the constant symbol representing 0 (in particular, we choose a signature containing this symbol and all symbols from Robinson's arithmetic Q). Let A1 be a conjunction of axioms strong enough to represent every recursive function (e.g. the axioms of Q) and a defining axiom for the function φ s.t. every atomic formula is negated or doubly negated. We define the formulas A2, A k 3 , A k 4 , A k 5 for k ∈ ω; for formulas representing the equality φk(x) = 0 we write [φk(x) = 0]. A2 ≡ (∀x)¬¬P (x) Ak3 ≡ (∀x, y)(¬[φk(x) = 0] ∧ ¬¬x ≤ y ⊃ ¬[φk(y) = 0]) Ak4 ≡ (∀x)(¬[φk(x) = 0] ⊃ (P (0) ⊃ P (x)) Ak5 ≡ (∀x){¬¬[φk(s(x)) = 0] ⊃ ⊃ [(P (x) ⊃ P (s(x))) ⊃ P (s(x))] ∧ [P (s(x)) ⊃ P (0)]} Finally we set Bk ≡ A1 ∧A2 ∧Ak3 ∧Ak4 ∧Ak5 and Ak ≡ Bk ⊃ ((∀x)¬[P (x) ⊃ (∀y)P (y)] ∨ P (0)). The double negations in Definition 34 serves the purpose of giving classical truth values to the formulas; note that, for a G0-interpretation I, I(B) > 0 implies I(¬¬B) = 1 (clearly I(B) = 0 implies I(¬¬B) = 0). Therefore the formulas in A1, A2 and Ak3 may only the receive the truth values 0 and 1 and thus have a classical meaning. Intuitively A2 expresses that P is always true, A3k states that φk(x) = 0 implies that φk(y) = 0 for all y greater than x. Ak4 and A k 5 are not classical in the sense that they may assume truth values between 0 and 1. I(Ak4) = 1 means (according to the ⊃-semantics of G 0) that for all x with φk(x) 6= 0, I(P (0)) is less or equal to I(P (x)). Lemma 35. If I is a G0-interpretation s.t. I(Bk) < 1, then I(Ak) = 1. Proof. (1) I(A1∧A2∧Ak3∧Ak4) < 1: If I(A1∧A2∧Ak3) < 1 then the value is actually 0 and thus I(Bk) = 0; I(Ak) = 1 is a trivial consequence. If I(A1∧A2∧Ak3) = 1 and I(Ak4) < 1 then there must be some d s.t. I(¬[φk(d) = 0]) = 1 and I(P (0) ⊃ P (d)) < 1. But then, by the semantics of G0, I(P (d)) ≤ (P (0)). Therefore I(Ak4) ≤ I(P (0)) and also I(Bk) ≤ I(P (0)). But P (0) occurs disjunctively in Ak and so I(Ak) = 1. (2) I(A1 ∧ A2 ∧ Ak3 ∧ Ak4) = 1: If I(P (0)) = 1 then clearly I(Ak) = 1. Thus let us assume that I(P (0)) < 1. As I(Bk) < 1 we must have I(Ak5) < 1. That means there exists some d s.t. I(¬¬[φk(s(d)) = 0]) = 1 and I(((P (d) ⊃ P (s(d))) ⊃ P (s(d))) ∧ (P (s(d)) ⊃ P (0))) < 1. (∗) 9 For such a d we either have (I(P (d)) ≤ I(P (s(d))) and I(P (s(d))) < 1) or I(P (0)) < I(P (s(d))). In the latter case we get I(P (s(d)) ⊃ P (0)) = I(P (0)). Thus in any case (∗) gets a value ≤ I(P (0)) and I(Bk) ≤ I(P (0)). Again we obtain I(Ak) = 1.  Theorem 36. The ∃-free fragment of G0is not recursively enumerable. Proof. We show that G0 |= Ak iff k ∈ Oφ (i.e. iff for all x, φk(x) = 0). The sequence (Ak)k∈ω is ∃-free and (trivially) r.e. Thus a recursive enumeration of all Ak with G0 |= Ak would give a recursive enumeration of the set Oφ which, by Proposition 33, does not exist. Now let us assume that G0 |= Ak. We define a specific G0-interpretation Nk: The domain of Nk is the set of natural numbers ω and the evaluation function s for the atoms is defined by: s(P (sn(0))) = { 1 n+2 if φk(n) = 0 1 if φk(n) > 0 For all other atoms A we set s(A) = 1 if N |= A and s(A) = 0 otherwise (N |= A means that A is true in the standard model N). Note that P (0) receives the value 12 . By definition of Nk all conjuncts of Bk are verified and so Nk(Bk) = 1. By G0 |= Ak we must have Nk |=m Ak and therefore Nk |=m (∀x)¬[P (x) ⊃ (∀y)P (y)] ∨ P (0). From Nk(P (0)) = 12 we infer Nk |=m (∀x)¬[P (x) ⊃ (∀y)P (y)]. By Proposition 31 the last property only holds if DistrNk(P (x)) does not have a minimum. We show now that φk must be the constant function 0. We assume that there exists a number r s.t. φk(r) 6= 0 and derive a contradiction: By definition of s we obtain s(P (sr(0))) = 1. But Nk |=m Ak3 what implies that for all number terms (i.e. successor terms) sp(0) with p ≥ r the formula ¬[φk(sp(0)) = 0] evaluates to 1. As A1 represents φ we obtain φk(p) 6= 0 for all p ≥ r and, by definition of φk, φk(p) = 1 for all p ≥ r. By definition of s we thus obtain s(P (sp(0))) = 1 for all p ≥ r But Nk(P (0)) = 12 and, consequently, for almost all p Nk(P (s p(0))) > 12 . Therefore DistrNk(P (x)) has a minimum; a contradiction. Note that by the choice of the standard model N we only have standard elements in our domain (i.e. elements which are represented by successor terms). So there cannot be another sequence in the set DistrNk(P (x)) which converges to 0. We infer that φk must be identical to 0, and so k ∈ Oφ. 10 For the other direction let us assume that k ∈ Oφ, i.e. φk(n) = 0 for all n. As A1 represents φ the formula [φk(s`(0)) = 0] is provable for all ` ∈ ω. Now let I be an arbitrary G0-interpretation of Ak. If I(Bk) < 1 then, by Lemma 35, I(Ak) = 1. Thus it remains to investigate the case I(Bk) = 1. By definition ofBk, I(Bk) = 1 implies I(Ak5) = 1. We substitute all ground terms s n(0) into the matrix of Ak5 . These instances are true in I either if all P (sn(0)) evaluate to 1 (in which case Ak is true because also P (0) is true) or the sequence I(P (sn(0))n∈ω is strictly decreasing. In the last case the sequence must converge to 0. By the axiom A2 no element of this sequence is actually = 0; this property also holds for all (potential) nonstandard elements, which may be present as the domain is arbitrary. As a consequence DistrI(P (x)) does not have a minimum. Proposition 31 then implies that I |=m (∀x)¬[P (x) ⊃ (∀y)P (y)]. But the last formula occurs disjunctively in the consequent of Ak and thus I |=m Ak. Putting things together we see that Ak evaluates to 1 under all G0interpretations, i.e., G0 |= Ak.  Corollary 37. (1) ILC is not recursively enumerable. (2) IL is not recursively enumerable. Proof. (1) Immediate by Proposition 210. (2) We show: IL |= Ak iff φk(n) = 0 for all n. If φk(n) 6= 0 for some n, then G0 6|= Ak by Theorem 36. Since G0 = ILC, there is some ILC-interpretation K s.t. K 6|=i Ak; but K is also an IL-interpretation, so IL 6|= Ak. So suppose that φk(n) = 0 for all n ∈ ω. Let K = 〈ω, (Di)i∈ω, {si}i∈ω, s〉 be an IL–interpretation. Then, by definition of the formulas Ak and Bk, K0(Bk) = ⊥ implies K0(Ak) = >. It remains to investigate the case K0(Bk) = >. All domains Di of K must contain the interpretation of the number terms sn(0). Therefore either K0(P (0)) = >, in which case K0(Ak) = 1 by definition of Ak, or (by the proof of Theorem 36) the sequence φK(P (sn(0)))n∈ω is strictly decreasing. Note that we may define φK and φK exactly like in Proposition 210 (although K need not be an ILC–interpretation). So let us assume that φK(P (sn(0)))n∈ω is strictly decreasing. We will show that φK((∀x)P (x)) = {⊥}ω. Suppose, by way of contradiction, that φK((∀x)P (x)) 6= {⊥}ω, i.e. there exists an i ∈ ω s.t. Ki((∀x)P (x)) 6= ⊥. As (∀x)P (x) does not contain function symbols, Ki((∀x)P (x)) cannot be undefined and so Ki((∀x)P (x)) = >. By definition of the IL-semantics this implies that for all j ≥ i and d ∈ Dj , Kj(P (d/x)) = >. In particular, we get for all d ∈ Di : Ki(P (d/x)) = >. As Di contains the interpretation of all number terms we also obtain Ki(P (sn(0))) = > for all n ∈ ω. Consequently min{j : Kj(P (sn(0))) = >} ≤ i for all n ∈ ω. By definition of φK we thus obtain φK(P (sn(0))) ≥ 1 i+ 1 for all n ∈ ω 11 and φK(P (sn(0))) = 1 kn + 1 for kn ∈ ω, kn ≤ i, n ∈ ω. This however contradicts our assumption that the sequence φK(P (sn(0)))n∈ω is strictly decreasing. So we obtain φK((∀x)P (x)) = {⊥}ω. However, there are no i and d ∈ Di s.t. Ki(P (d/x)) = ⊥, since K0((∀x)¬¬P (x)) = > by A2 in Bk. Therefore Ki(P (d/x) ⊃ (∀y)P (y)) = ⊥ for all i ∈ ω and d ∈ Di. By the semantics of IL this implies K0((∀x)¬[P (x) ⊃ (∀y)P (y)]) = >. But then K0(Ak) = > and the reduction of Oφ to IL is completed.  4 Incompleteness of temporal logics We now proceed to show that (a) ©-free TL and TLC and (b) TG and TGC are also not recursively axiomatizable. This strengthens the incompleteness result for TL of Szalas and Kröger [6] and answers a question left open in [2]. In contrast to TG, however, TB is r.e. [2]. An axiomatization is given by adding to first-order S4 the axioms: ©(A ⊃ B) ⊃ (©A ⊃ ©B) ¬©A↔ ©¬A ©2A ∧A↔ 2A and the rule A/©A. Definition 41. We define the operator Ψ as follows: Ψ(A) = 2A A atomic Ψ(A ∨B) = Ψ(A) ∨ Ψ(B) Ψ(A ∧B) = Ψ(A) ∧ Ψ(B) Ψ(A ⊃ B) = 2[Ψ(A) ⊃ Ψ(B)] Ψ(¬A) = 2(¬Ψ(A)) Ψ((∀x)A(x)) = 2(∀x)Ψ(A(x)) Proposition 42. Let A be an ∃-free first-order formula. Then (1) TL |= Ψ(A) iff IL |= A and (2) TLC |= Ψ(A) iff ILC |= A. Proof. Suppose IL 6|= A, let K = 〈ω,Di, {si}, s〉 be a countermodel. We can interpret K as a TL-interpretation Kt. By induction on the complexity of a formula A and using the monotonicity property of K we have Kti(Ψ(A)) = Ki(A). Hence, Kt 6|=t Ψ(A). 12 Conversely, let Kt = 〈ω,Di, {sti}, s〉 be a TL-interpretation s.t. Kt 6|=t Ψ(A). Then define K = 〈ω,Di, {si}, s〉 by si(A) = Kti(2(A)). Again, by an easy induction on the complexity of A we have Kti(Ψ(A)) = Ki(A). Thus, K 6|=i A. Similarly, for TLC and ILC.  Corollary 43. The ∃and ©-free fragments of TL are not r.e. Proof. By Corollary 37 and Proposition 42.  The reader will note the similarity between the above embedding of IL in TL with Gödel's, and McKinsey and Tarski's embeddings of intuitionistic predicate logic into S4. In contrast to first order TL, propositional TL is axiomatizable (even with ©). In [5] it is shown that we get TLprop by adding to TBprop the rule A ⊃ B A ⊃ ©B A ⊃ 2B Definition 44. The set S∗(A) of strict subformulas of a formula A is defined as follows: S∗(A) = {A} ∪ S ∗(B) if A ≡ ¬B S∗(B) ∪ S∗(C) if A ≡ B ∧ C, B ∨ C, or B ⊃ C S∗(B(x)) if A ≡ (∀x)B(x) or (∃x)B(x) Let P1, . . . , Pm be the predicate symbols with occurring in A with arities r1, . . . , rm and xr1 , . . . , xrm corresponding variable vectors. Then we define S(A) = S∗(A) ∪ {Pi(xri) : i = 1, . . . ,m} Definition 45. Let A be a first-order formula without ∃. Define CA ≡ 2 ∧ B(x)∈S(A) (∀x) ( B(x) ↔ ©B(x) ) Let TG∗ be the logic based on TG-interpretations where the domains within an ω-sequence are equal, i.e., for all i, j we have Di*ω+j = Di*ω. Proposition 46. Suppose A is ©and ∃-free. Then TG |= CA ⊃ A iff TG∗ |= CA ⊃ A. Proof. Only if: Immediate. If: Let K be a TG-interpretation s.t. K 6|=t CA ⊃ A. Let K∗ = 〈D∗i , s∗i 〉 be defined by D∗i*ω+j = Di*ω and s∗i = si |\ D∗i . We prove by induction on the complexity of A(c) (for c ∈ D∗i*ω) that Ki*ω+j(A) = K∗i*ω+j(A). This is immediately seen for A atomic or with outermost logical symbol a propositional connective. If A ≡ (∀x)B(x) we argue as follows: Let (i, j) denote i * ω + j. If Ki,j(A) = > then Ki,j(B(d)) = > for all d ∈ Di,j ⊇ Di,0. By induction hypothesis, K∗i,j(B(d)) = > for all d ∈ D∗i,j , so K∗i,j(A) = >. 13 If Ki,j(A) = ⊥ then for some d ∈ Di,j , Ki,j(B(d)) = ⊥. Suppose for all d ∈ Di,0, Ki,j(B(d)) = >. Then we have Ki,0((∀x)© j B(x)∧¬©j(∀x)B(x)) = >. Since we have Ki,0 |= (∀x)(B(x) ↔ ©B(x)) and Ki,0 |= (∀x)B(x) ↔ ©(∀x)B(x)) this gives Ki,0 |= (∀x)B(x)∧¬(∀x)B(x), a contradiction. Hence actually there is d ∈ Di,0 s.t. Ki,j(B(d)) = ⊥. By induction hypothesis, K∗i,j(B(d)) = ⊥ = K∗i,j(A).  Let TG∗∗ (TGC∗∗) be the logic based on TG(TGC)-interpretations where the worlds within an ω-sequence are equal, i.e., for all i, j we have Di,j = Di,0 and si,j = si,0. Proposition 47. Let A be a © and ∃-free formula. (1) TGC∗ |= CA ⊃ A iff TGC∗∗ |= CA ⊃ A. (2) TG∗ |= CA ⊃ A iff TG∗∗ |= CA ⊃ A. Proof. Obvious, since A does not contain ©.  Proposition 48. Let A be an ©and ∃-free formula. (1) TGC∗∗ |= CA ⊃ A iff TLC |= A. (2) TG∗∗ |= CA ⊃ A iff TL |= A. Proof. (1) Only if: Suppose TLC 6|= A, let K = 〈ω,D, {si}, s〉 be a countermodel. Define Kg = 〈ω *ω,D, {sgi }i∈ω*ω, s〉 by s g j,k = sj where i, j, k ∈ ω. Clearly, Kg 6|=t CA ⊃ A. If: Suppose TGC∗∗ 6|= CA ⊃ A, let K = 〈ω *ω,D, {si}, s〉 be a countermodel. Since K |= CA and the domains are constant, Kj,k(A) = Kj,`(A) for A, and in particular sj,k = sj,`. Define K` = 〈ω,D, {s`i}, s〉 by s`j = sjω for j ∈ ω. Again by induction on the complexity of A it is easily shown that K`j(A) = K ` j,k(A). So K` 6|=t A. (2) Similarly.  Corollary 49. The ∃-free fragments of TG and TGC are not r.e. Proof. By Corollary 43 and Propositions 46, 47 and 48.  For an axiomatization of the propositional logic TGprop it is convenient to introduce a new connective 4 defined by Ki,j(4A) = 1 iff Ki+1,0(A) = 1. Then TGprop is axiomatized by S4 plus ©(A ⊃ B) ⊃ (©A ⊃ ©B) 4(A ⊃ B) ⊃ (4A ⊃ 4B) ©¬A↔ ¬©A 4¬A↔ ¬4A ©4A↔4A ©2A ∧42A ∧A↔ 2A and the rules A ©A A 4A A ⊃ B A ⊃ ©A A ⊃ 4A A ⊃ 2B 14 5 Conclusion We used the main result of this paper, the incompleteness of the infinitely valued first-order Gödel logic based on the domain of truth values V0 : {1/k : k ≥ 1}∪{0}, to demonstrate the incompleteness of first-order discrete linear temporal logics with/without time gaps and with/without constant domains. The firstorder discrete branching time logic with time gaps, however, is complete, but it is an open question whether the same applies for the same logic with constant domains. The infinitely valued first-order Gödel logics define another field of future research; we conjecture that the logic based on V1 = {1−1/k : k ≥ 1}∪{1} and the ∃-fragment of the Gödel logic based on V0 are recursively axiomatizable. References 1. M. Baaz, C. G. Fermüller, and R. Zach. Elimination of cuts in first-order finitevalued logics. J. Inform. Process. Cybernet. EIK, 29(6), 333–355, 1994. 2. M. Baaz, A. Leitsch, and R. Zach. Completeness of a first-order temporal logic with time-gaps. Theoret. Comput. Sci., 1996 to appear. 3. M. Dummett. A propositional calculus with denumerable matrix. J. Symbolic Logic, 24, 97–106, 1959. 4. K. Gödel. Zum intuitionistischen Aussagenkalkül. Anz. Akad. Wiss. Wien, 69, 65–66, 1932. 5. F. Kröger. Temporal Logic of Programs. eatcs Monographs in Computer Science 8. (Springer, Berlin, 1987). 6. F. Kröger. On the interpretability of arithmetic in temporal logic. Theoret. Comput. Sci., 73, 47–60, 1990. 7. S. Merz. Decidability and incompleteness results for first-order temporal logics of linear time. J. Applied Non-Classical Logics, 2(2), 139–156, 1992. 8. B. Scarpellini. Die Nichtaxiomatisierbarkeit des unendlichwertigen Prädikatenkalküls von Lukasiewicz. J. Symbolic Logic, 27, 159–170, 1962. 9. A. Szalas. Concerning the semantic consequence relation in first-order temporal logic. Theoret. Comput. Sci., 47, 329–334, 1986. 10. A. Szalas and L. Holenderski. Incompleteness of first-order temporal logic with until. Theoret. Comput. Sci., 57, 317–325, 1988. 11. G. Takeuti and T. Titani. Intuitionistic fuzzy logic and instuitionistic fuzzy set theory. J. Symbolic Logic, 49, 851–866, 1984.