Arthur Paul Pedersen

A PROOF OF COMPLETENESS FOR CONTINUOUS FIRST-ORDER LOGIC ITA Ï BEN YAACOV AND

Continuous first-order logic has found interest among model theorists who wish to extend the classical analysis of "algebraic" structures (such as fields, group, and graphs) to various natural classes of complete metric structures (such as probability algebras, Hilbert spaces, and Banach spaces). With research in continuous first-order logic preoccupied with studying the model theory of this framework, we find a natural question calls for attention: Is there an interesting set of axioms yielding a completeness result?

The primary purpose of this article is to show that a certain, interesting set of axioms does indeed yield a completeness result for continuous first-order logic. In particular, we show that in continuous first-order logic a set of formulae is (completely) satisfiable if (and only if) it is consistent. From this result it follows that continuous first-order logic also satisfies an approximated form of strong completeness, whereby Σ ϕ (if and) only if Σ ⊢ ϕ -. 2 -n for all n < ω. This approximated form of strong completeness asserts that if Σ ϕ, then proofs from Σ, being finite, can provide arbitrary better approximations of the truth of ϕ.

Additionally, we consider a different kind of question traditionally arising in model theory -that of decidability: When is the set of all consequences of a theory (in a countable, recursive language) recursive? Say that a complete theory T is decidable if for every sentence ϕ, the value ϕ T is a recursive real, and moreover, uniformly computable from ϕ. If T is incomplete, we say it is decidable if for every sentence ϕ the real number ϕ • T is uniformly recursive from ϕ, where ϕ • T is the maximal value of ϕ consistent with T . As in classical first-order logic, it follows from the completeness theorem of continuous first-order logic that if a complete theory admits a recursive (or even recursively enumerable) axiomatization then it is decidable.

Introduction

Roughly speaking, model theory studies first-order theories and the corresponding classes of their models (i.e., elementary classes). Properties of the first-order theory of a structure can then give direct insight into the structure itself. Investigation thereof was

We wish to thank Jeremy Avigad for valuable comments. We also wish to thank Petr Hájek for offering useful remarks and for pointing us to important references. Finally, we wish to thank an anonymous referee for helpful suggestions.

First author supported by ANR chaire d'excellence junior THEMODMET (ANR-06-CEXC-007) and by Marie Curie research network ModNet.

Revision 856 of 16 March 2009.

classically restricted to so-called "algebraic" structures, such as fields, groups, and graphs.

Additionally, in modern model theory one often studies stable theories -theories whose models admit a "well-behaved" notion of independence (which, if it exists, is always unique). Continuous first-order logic was developed in [BU] as an extension of classical firstorder logic, permitting one to broaden the aforementioned classical analysis of algebraic structures to various natural classes of complete metric structures. (It should be pointed out that classes of complete metric structures cannot be elementary in the classical sense for several reasons. For example, completeness is an infinitary property and is therefore not expressible in classical first-order logic. See also [START_REF] Ben Yaacov | Model theory for metric structures, Model theory with Applications to Algebra and Analysis[END_REF] for a general survey of continuous logic and its applications for various kinds of metric structures arising in functional analysis and probability theory.) For example, the class (of unit balls) of Hilbert spaces and the class of probability algebras are elementary in this sense. (A probability algebra is the Boolean algebra of events of a probability space modulo the null measure ideal, with the metric d(A, B) = µ(A∆B).) Furthermore, the classical notion of stability can easily be extended to continuous first-order logic. Indeed, somewhat unsurprisingly, the classes of Hilbert spaces and probability algebras are stable, independence being orthogonality and probabilistic independence, respectively.

Historically, two groups of logics precede continuous first-order logic. On the one hand, continuous first-order logic has structural precursors. The structural precursors are those logics which make use of machinery similar to that of continuous first-order logic yet were never developed to study complete metric structures. Such structural precursors include Chang and Keisler's continuous logic [START_REF] Chang | Continuous model theory[END_REF], Lukasiewicz's many-valued logic [START_REF] Hájek | Metamathematics of fuzzy logic[END_REF], and Pavelka's many-valued logic [START_REF] Pavelka | On fuzzy logic I, II and III[END_REF]. Chang and Keisler's logic is much too general for the study of complete metric structures, while Lukasiewicz logic and Pavelka's logic were developed for different purposes. Nonetheless, continuous first-order logic is an improved variant of Chang and Keisler's logic. On the other hand, continuous first-order logic has purposive precursors. The purposive precursors are those logics which were developed to study complete metric structures yet do not make use of machinery similar to that of continuous first-order logic. The purposive precursors of continuous firstorder logic include Henson's logic for Banach structures [START_REF] Henson | Nonstandard hulls of Banach spaces[END_REF] and compact abstract theories ("cats") [Ben03a, [START_REF]Simplicity in compact abstract theories[END_REF][START_REF]Uncountable dense categoricity in cats[END_REF]. Continuous first-order logic does not suffer from several shortcomings of these logics. Importantly, continuous first-order logic is less technically involved than the previous logics and in many respects much closer to classical first-order logic. Still, continuous first-order logic is expressively equivalent to the logic of metric open Hausdorff cats. Continuous first-order logic also generalizes Henson's logic for Banach structures, and as such, is expressively equivalent to a natural variant of Henson's logic.

As an extension of classical first-order logic, continuous first-order logic satisfies suitably phrased forms of the compactness theorem, the Löwenheim-Skolem theorems, the diagram arguments, Craig's interpolation theorem, Beth's definability theorem, characterizations of quantifier elimination and model completeness, the existence of saturated and homogeneous models results, the omitting types theorem, fundamental results of stability theory, and nearly all other results of elementary model theory. Moreover, continuous first-order logic affords a tractable framework for ultraproduct constructions (and so hull constructions) in applications of model theory in analysis and geometry. In fact, expressing conditions from analysis and geometry feels quite natural in continuous first-order logic, furnishing model theorists and analysts with a common language.

Thus it is clear that continuous first-order logic is of interest to model theorists. Yet with research focused on the model theory of continuous first-order logic and thus semantic features of this framework, a natural question seems to lurk in the background: Is there an interesting set of axioms yielding a completeness result? The answer depends on how one formulates the notion of completeness. To be sure, there is an interesting set of axioms, and, as we will see, a set of formulae is (completely) satisfiable if (and only if) it is consistent. However, as for continuous propositional logic, only an approximated form of strong completeness is obtainable. By this we mean that Σ ϕ only if Σ ⊢ ϕ -. 2 -n for all n < ω, which amounts to the idea if Σ ϕ, then proofs from Σ, being finite, can provide arbitrarily better approximations of the truth of ϕ. (What this means will become clearer below.) This should hardly be surprising in light of the fact that continuous first-order logic has been developed for complete metric structures equipped with uniformly continuous functions with respect to which formulae take truth values anywhere in [0, 1].

Of course, a different kind of question traditionally arising in model theory is that of decidability: When is the set of all consequences of a theory (in a countable, recursive language) recursive? Again, such questions can be extended to continuous first-order logic. Say that a complete theory T is decidable if for every sentence ϕ, the value ϕ T is a recursive real, and moreover, uniformly computable from ϕ. If T is incomplete, we say it is decidable if for every sentence ϕ the real number ϕ • T is uniformly recursive from ϕ, where ϕ • T is the maximal value of ϕ consistent with T . (See Definition 9.7. If T is complete, then ϕ takes the same value in all models of T , so ϕ T coincides with ϕ • T and therefore ϕ • T is the unique value of ϕ consistent with T .) As in classical first-order logic, it follows from the completeness theorem that if a complete theory admits a recursive (or even recursively enumerable) axiomatization then it is decidable, whence the connection to the present paper.

Following an introduction to Lukasiewicz propositional logic and continuous propositional logic, we offer a definition of the language of continuous first-order logic and then supply a precise formulation of its semantics. Indeed, this paper can also be seen as an effort to precisely organize and unify the various presentations of continuous first-order logic found in the literature which are often intimated in a rough-and-ready form. Finally, we state and usually prove various results needed to reach the goal of this paper: to state and prove the completeness theorem for continuous first-order logic.

To follow our intuitions to this end, the structure of our approach is largely borrowed from the classical approach employed to prove the completeness theorem. In particular, we make use of a Henkin-like construction and a weakened version of the deduction theorem of classical first-order logic. Moreover, various definitions and results found in the classical approach are translated to play analogous roles in our development, while from [BU] we take some basic facts and definitions peculiar to continuous first-order logic. It will become apparent, however, that our approach differs from the classical one in many respects. Furthermore, the completeness theorem we offer is formulated with respect to the semantics employed by the model theorist who studies continuous firstorder logic. In particular, our work does not exploit an algebraic semantics. Finally, we should note that results of research on the interplay between logical and deductive entailment for both continuous propositional logic and Lukasiewicz propositional logic play a crucial role in getting our feet off the ground so that we may follow our intuitions in the first place [Ben]. (This work of the first author is partially based on the results of work done by Chang [START_REF] Chang | Proof of an axiom of Lukasiewicz[END_REF][START_REF]A new proof of the completeness of the Lukasiewicz axioms[END_REF] and Rose and Rosser [START_REF] Rose | Fragments of many-valued statement calculi[END_REF] on Lukasiewicz logic.) With this, we set out to the task at hand.

Lukasiewicz Logic and Continuous Logic

Definition 2.1. Let S 0 = {P i : i ∈ I} be a set of distinct symbols. Let S be freely generated from S 0 by the formal binary operation -. and the unary operation ¬. We call S a Lukasiewicz propositional logic. Definition 2.2. Let S be a Lukasiewicz propositional logic.

(i) If v 0 : S 0 → [0, 1] is a mapping, we can extend v 0 to a unique mapping v : S → [0, 1] by setting

• v(ϕ -. ψ) := max(v(ϕ) -v(ψ), 0). • v(¬ϕ) := 1 -v(ϕ).
We call v the truth assignment defined by v 0 . (ii) If Σ ⊆ S, we write v Σ if v(ϕ) = 0 for all ϕ ∈ Σ, and we call v a model of Σ.

We also write v ϕ if v {ϕ}. (iii) We say that Σ ⊆ S is satisfiable if it has a model. (iv) We write Σ ϕ if every model of Σ is also a model of ϕ.

We may write Σ L ϕ to indicate that we are dealing with a Lukasiewicz propositional logic.

Remark 2.3. Observe that 0 corresponds to truth and any r ∈ (0, 1] corresponds to a degree of truth or falsity, where 1 may be construed as absolute falsity. Also observe that '-. ' plays a role analogous to that of '→' in classical logic: We may interpret 'ψ -. ϕ' as 'ψ is implied by ϕ,' 'ϕ is at least as false as ψ', 'ψ is at most as true as ϕ,' or simply, 'ψ is less than or equal to ϕ.' We prefer the last interpretation.

Definition 2.4. Let S 0 = {P i : i ∈ I} be a set of distinct symbols. Let S be freely generated from S 0 by the formal binary operation -. and the unary operations ¬ and 1 2 . We call S a continuous propositional logic.

A truth assignment v is defined as in (i) of Definition 2.2 with the extra condition that v( 1 2 ϕ) := 1 2 v(ϕ). Models, satisfiability, and logical entailment are defined as in Definition 2.2. We may write Σ C L ϕ to indicate that we are dealing with a continuous propositional logic.

Axioms: Group 1

We now present six of our fourteen axiom schemata. The first four form an axiomatization for Lukasiewicz propositional logic [START_REF] Chang | Proof of an axiom of Lukasiewicz[END_REF][START_REF] Rose | Fragments of many-valued statement calculi[END_REF].

(A1) (ϕ -. ψ) -. ϕ (A2) ((χ -. ϕ) -. (χ -. ψ)) -. (ψ -. ϕ) (A3) (ϕ -. (ϕ -. ψ)) -. (ψ -. (ψ -. ϕ)) (A4) (ϕ -. ψ) -. (¬ψ -. ¬ϕ)
When the next two axiom schemata are added to the first four (in the appropriate language), we obtain an axiomatization for continuous propositional logic [Ben].

(A5) 1 2 ϕ -. (ϕ -. 1 2 ϕ) (A6) (ϕ -. 1 2 ϕ) -. 1 2 ϕ
Note that (A5) and (A6) say that 1 2 behaves as it ought to. Informally, under the intended interpretation, (A5) and (A6) taken together imply that 1 2 ϕ∔ 1 2 ϕ = ϕ. ('∔' may be defined by setting ϕ ∔ ψ := ¬(¬ϕ -. ψ); thus, according to the intended interpretation of '-. ', the interpretation of '∔' is given by x ∔ y = min(x + y, 1).)

Formal deductions and the relation ⊢ for both logics are defined in the natural way, the only rule of inference being modus ponens:

ϕ, ψ -. ϕ ψ
We can make this more precise as follows: a formal deduction from Σ is a finite sequence of formulae (ϕ i : i < n) such that for each i < n, either (i) ϕ i is an instance of an axiom schema, (ii) ϕ i ∈ Σ, or (iii) there are j, k < i such that ϕ k = ϕ i -. ϕ j . We accordingly say that ϕ is provable from (or deducible from, or a consequence of ) Σ and write Σ ⊢ ϕ if there is a formal deduction from Σ ending in ϕ. Observe that a formula ϕ is provable from Σ just in case it is provable from a finite subset of Σ. To avoid confusion, we may write Σ ⊢ L ϕ to indicate that ϕ is provable from Σ in Lukasiewicz propositional logic, and we may write Σ ⊢ C L ϕ to indicate that ϕ is provable from Σ in continuous propositional logic.

It should be fairly clear to the reader how the proof systems of continuous propositional logic and Lukasiewicz propositional logic are related. Both proof systems are of course sound, by which we mean that if Σ ⊢ L ϕ (respectively, Σ ⊢ C L ϕ), then Σ |= L ϕ (respectively, Σ |= C L ϕ). We leave this section with a definition, a few notational conventions, and a remark, each of which addresses some aspects of our presentation of continuous logic in this paper.

Definition 3.1. We say that a set of formulae Σ is inconsistent if Σ ⊢ ϕ for every formula ϕ and consistent otherwise. Notation 3.2. Define ψ -. nϕ by recursion on n < ω:

(i) ψ -. 0ϕ := ψ. (ii) ψ -. (n + 1)ϕ := (ψ -. nϕ) -. ϕ.
Notation 3.3. Let 1 be shorthand for ¬(ϕ -. ϕ), where ϕ is any formula, and let 2 -n be shorthand for

1 2 • • • 1 2 n-times
1. Also, let 0 be shorthand for ¬1.

Remark 3.4. Observe that on any truth assignment v the set D generated from 1 by applying the operations ¬, -. , and 1 2 is such that {v(d) : d ∈ D} = D, the set of dyadic numbers, i.e., numbers of the form k 2 n , where k, n < ω and k ≤ 2 n . For simplicity of notation, we do not distinguish between the syntactic set D thus generated and D.

Black Box Theorems

We now record several results which will be used in this paper. Fact 4.2. Let S be a Lukasiewicz propositional logic, and Σ ⊆ S. Then Σ is consistent if and only if it is satisfiable. Fact 4.3. Let S be a continuous propositional logic and Σ ⊆ S. Then Σ is consistent if and only if it is satisfiable.

An immediate corollary of the previous fact is the following approximated form of strong completeness.

if Σ ⊢ ϕ -. 2 -n for all n < ω.
In fact, this is the best we can hope for. To see why, consider Σ := {P -. 2 -n : n < ω}. Then Σ P , yet for no finite Σ 0 ⊆ Σ do we have Σ 0 P . However, we do have the following weaker result.

Fact 4.5 (Finite Strong Completeness for Continuous Logic). Let S be a continuous propositional logic, Σ ⊆ S be finite, and ϕ ∈ S. Then Σ ϕ if and only if Σ ⊢ ϕ.

In view of the above facts, observe that if S is a Lukasiewicz or continuous propositional logic and Σ ⊆ S,

• Σ is inconsistent if and only if Σ ⊢ L 1.

• Σ is inconsistent if and only if Σ ⊢ C L d for some d ∈ D\{0}. Fact 4.2 -Fact 4.5 have been established independently by the first author in [Ben]. Nonetheless, Fact 4.2 has been proved in [START_REF] Belluce | A weak completeness theorem for infinite valued first-order logic[END_REF] (indeed, for Lukasiewicz first-order logic; see also [START_REF] Hájek | Metamathematics of fuzzy logic[END_REF]) and Fact 4.4 has a counterpart in [START_REF] Hay | Axiomatization of the infinite-valued predicate calculus[END_REF] (again, see also [START_REF] Hájek | Metamathematics of fuzzy logic[END_REF]), while Fact 4.5 has been proved for rational Pavelka propositional logic [START_REF] Hájek | Metamathematics of fuzzy logic[END_REF] and for Lukasiewicz propositional logic [START_REF] Roberto | Algebraic foundations of many-valued reasoning[END_REF][START_REF] Hájek | Metamathematics of fuzzy logic[END_REF].

The Language and Semantics of Continuous First-Order Logic

Definition 5.1. The logical symbols of continuous first-order logic are

• Parentheses: ( , )

• Connectives: -. , ¬ , 1 2

• Quantifiers: sup (or inf)

• Variables: v 0 , v 1 , . . .

• An optional binary metric: d

The sup-quantifier plays the role of the ∀-quantifier from classical first-order logic, whereas the inf-quantifier plays the role of the ∃-quantifier from classical first-order logic. In fact, the sup-quantifier can be defined in terms of the inf-quantifier. Furthermore, instead of an optional binary congruence relation symbol ≈ as in classical first-order logic, continuous first-order logic has an optional binary metric symbol d.

We should now say something about the choice of connectives. In classical first-order logic, a set of connectives is complete if every mapping from {0, 1} n → {0, 1} can be written using the set of connectives. The set of connectives {¬, →} is complete in this sense. Similarly, in continuous first-order logic, a set of connectives is complete if every continuous mapping from [0, 1] n → [0, 1] can be written using the set of connectives. But this notion is much too demanding. Indeed, a complete set of connectives would require continuum many connectives. A more reasonable demand of a set of connectives is that every continuous function from [0, 1] n → [0, 1] can be written using the set of connectives up to arbitrarily better approximations. A set of connectives satisfying this requirement is said to be full (see [BU]; see also [START_REF] Roberto | Algebraic foundations of many-valued reasoning[END_REF]). The set of connectives {-. , ¬, 1 2 } is full in this sense, and {-. , 1 2 , 0, 1} is full as well -so is any set of connectives which includes -. , 1, and some dense set C ⊆ [0, 1], such as D or Q ∩ [0, 1]. Here we choose to canonize {-. , ¬, 1 2 } as the set connectives. As it is finite, this set of connectives is an economical choice, and it is the analogue of the popular choice of connectives {¬, →} of classical first-order logic.

Definition 5.2. A continuous signature is a quadruple L = (R, F , G, n) such that (i) R = ∅. (ii) R ∩ F = ∅. (iii) G has the form {δ s,i : (0, 1] → (0, 1] : s ∈ R ∪ F and i < n s }.
(iv) n : R ∪ F → ω. Members of R are called relation symbols, while members of F are called function symbols.

For each s ∈ R ∪ F , we write n s for the value of s under n and call n s the arity of s. We call a member of G a modulus of uniform continuity.

Remark 5.3. Observe that members of G are not syntactic objects. Rather, each member of G is a genuine operation on (0, 1]. The role of the moduli of uniform continuity will be clarified below.

Definition 5.4. A continuous signature with a metric is a continuous signature with a distinguished binary relation symbol d.

Terms, formulae, and notions of free and bound substitution are defined in the usual way (see §6 concerning these notions). We denote the set of variables by V and the set of formulae by For(L). In classical first-order logic, a metric symbol d would most naturally be thought of as a function symbol. In continuous first-order logic, however, d is a relation symbol, and as such, dt 0 t 1 is a formula rather than a term.

We write 'sup x ' (and 'inf x ') instead of 'sup x' (and 'inf x'). We define 'inf,' '∧,' '∨,' and '| |' by setting

inf x ϕ := ¬ sup x ¬ϕ. ϕ ∧ ψ := ϕ -. (ϕ -. ψ). ϕ ∨ ψ := ¬(¬ϕ ∧ ¬ψ). |ϕ -ψ| := (ϕ -. ψ) ∨ (ψ -. ϕ).
The reader should verify that the definition of 'inf' accords with the obvious intended interpretation when the semantics are given below. Observe that (A2) becomes '(ϕ ∧ ψ) -. (ψ ∧ ϕ).' Also, according to the intended interpretation of '-. ,' the interpretation of '∧' is given by x ∧ y = min(x, y). Thus, according to the interpretation of '∧,' the interpretation of '∨' is given by x ∨ y = max(x, y), whereby the interpretation of '| |' is one-dimensional Euclidean distance. As 0 corresponds to truth, it should be clear that the interpretation of '∧' is the continuous analogue of the classical 'or,' whereas the interpretation of '∨' is the continuous analogue of the classical 'and.' Definition 5.5.

(i) Let (M, d) and (M ′ , d ′ ) be metric spaces and f : M → M ′ be a function. We say that δ : (0, 1] → (0, 1] is a modulus of uniform continuity for f if for each ǫ ∈ (0, 1] and all

a, b ∈ M, d(a, b) < δ(ǫ) =⇒ d ′ (f (a), f (b)) ≤ ǫ. (ii)
We say that f is uniformly continuous if there is a modulus of uniform continuity for f . Definition 5.6. Let L be a continuous signature. A continuous L-pre-structure is an ordered pair M = (M, ρ), where M is a non-empty set and ρ is a function whose domain is R ∪ F , such that:

(i) To each f ∈ F , ρ assigns a mapping f M : M n f → M. (ii) To each P ∈ R, ρ assigns a mapping P M : M n P → [0, 1].
If L is also a continuous signature with a metric, then M is such that:

(iii) ρ assigns to d a pseudo-metric d M : M × M → [0, 1]. (iv) For each f ∈ F , i < n f , and ǫ ∈ (0, 1], δ f,i satisfies the following condition: ∀ā, b, c, e [d M (c, e) < δ f,i (ǫ) =⇒ d M (f M (ā, c, b), f M (ā, e, b)) ≤ ǫ],
where |ā| = i and |ā| + | b| + 1 = n f ; we thereby call δ f,i the uniform continuity modulus of f with respect to the ith argument. (v) For each P ∈ R, i < n P , and ǫ ∈ (0, 1], δ P,i satisfies the following condition:

∀ā, b, c, e [d M (c, e) < δ P,i (ǫ) =⇒ max(P M (ā, c, b) -P M (ā, e, b), 0) ≤ ǫ],
where |ā| = i and |ā| + | b| + 1 = n P ; we thereby call δ P,i the uniform continuity modulus of P with respect to the ith argument.

Here, as well as in the remainder of this paper, a tuple a 0 , . . . , a n-1 may be for convenience denoted by ā, whereby |ā| will denote the length of ā.

Convention 5.7. In this paper we make the convention that for an n-ary function f , the ith argument of the expression f (x 0 , . . . , x n-1 ) is x i . In particular, the 0 th argument of f is x 0 .

Remark 5.8. Conditions (iv) and (v) correspond to the congruence axioms of classical first-order logic. In classical first-order logic it is required that a distinguished binary relation symbol ≈ be such that for each classical structure A, the relation ≈ A is an equivalence relation satisfying the following congruence axioms: In classical first-order logic, one can thereby show that for each classical structure A, the relation ≈ A satisfies the following properties:

• For each function symbol f and i < n f , ∀ā, b, c, e (c ≈ A e =⇒ f A (ā, c, b) ≈ A f A (ā,
• For each function symbol f , ∀ā, b (( i<n f a i ≈ A b i ) =⇒ f A (ā) ≈ A f A ( b)), where |ā| = | b| = n f . • For each relation symbol P , ∀ā, b (( i<n P a i ≈ A b i ) =⇒ (P A (ā) ⇒ P A ( b))),
where |ā| = | b| = n P . Along a similar vein, in continuous first-order logic one can show that for each function symbol f and predicate symbol P , there are moduli of uniform continuity ∆ f and ∆ P which depend on their uniform continuity moduli (δ f,i : i < n f ) and (δ P,i : i < n P ), respectively. For example, ∆ f : (0, 1] → (0, 1] may be defined by setting ∆ f (ǫ) := min{δ f,0 (ǫ/n f ), . . . , δ f,n f -1 (ǫ/n f )}. Accordingly, in each continuous L-pre-structure M, the mapping ∆ f is a modulus of uniform continuity for f M with respect to the maximum metric

D M n f defined by D M n f (ā, b) := max i<n f (d M (a i , b i )) = i<n f d M (a i , b i ).
This may be expressed formally as follows:

• For each f ∈ F and ǫ ∈ (0, 1], ∆ f satisfies the following condition:

∀ā, b [( i<n f d M (a i , b i )) < ∆ f (ǫ) =⇒ d M (f M (ā), f M ( b)) ≤ ǫ],
where |ā| = | b| = n f . In light of the foregoing discussion, observe that for every continuous L-pre-structure M and s ∈ R ∪ F , s M is a uniformly continuous function. (ii) Every Cauchy sequence converges.

Definition 5.10. (i) If M is a continuous L-pre-structure, then an M-assignment is a mapping σ : V → M. (ii) If σ is an M-assignment, x ∈ V , and a ∈ M, we define an M-assignment σ a

x by setting for all y ∈ V ,

σ a x (y) := a if x = y σ(y) otherwise.
The interpretation of a term t in a continuous L-pre-structure M is defined as in classical first-order logic. We denote its interpretation by t M,σ . Definition 5.11. Let M be a continuous L-pre-structure. For a formula ϕ and an M-assignment σ, we define the value of ϕ in M under σ, M(ϕ, σ), by induction:

(i) M(P t 0 • • • t n P -1 , σ) := P M (t M,σ 0 , . . . , t M,σ n P -1 ). (ii) M(α -. β, σ) := max(M(α, σ) -M(β, σ), 0). (iii) M(¬α, σ) := 1 -M(α, σ). (iv) M( 1 2 α, σ) := 1 2 M(α, σ). (v) M(sup x α, σ) := sup{M(α, σ a
x ) : a ∈ M}. If one chooses to use 'inf' instead of 'sup,' one may replace (v) with M(inf x α, σ) := inf{M(α, σ a

x ) : a ∈ M}. Definition 5.12. Let M be a continuous L-pre-structure, let σ be an M-assignment, and let Γ ⊆ For(L).

(i) We say that (M, σ) models (or satisfies) Γ and that (M, σ) is a model of Γ, written

(M, σ) Q Γ, if M(ϕ, σ) = 0 for all ϕ ∈ Γ. We of course say that (M, σ) is a model of ϕ and write (M, σ) Q ϕ if (M, σ) Q {ϕ}. (ii)
We say that Γ is satisfiable if it has a model. Definition 5.13. Let Γ be a set of formulae and ϕ be a formula. We write Γ Q ϕ if every model of Γ is a model of ϕ. If ∅ Q ϕ, we say that ϕ is valid.

Definition 5.14. We write ϕ ≡ ψ if M(ϕ, σ) = M(ψ, σ) for every continuous L-prestructure and M-assignment σ.

With these definitions, many properties analogous to those of classical first-order logic can be derived (see [START_REF] Ebbinghaus | Mathematical logic[END_REF]).

Substitution and Metric Completions

Substitution. As in classical fist-order logic, free and bound substitution play an important role in connecting the syntax with the semantics. This brief subsection is intended to remind the reader of these two notions of substitution and to indicate to the reader what features of these notions are crucial for our purposes. Definition 6.1. Let t be a term, and let x be a variable. We define the free substitution of t for x inside a formula ϕ, ϕ[t/x], as the result of replacing x by t in ϕ if x occurs free in ϕ. We say that ϕ[t/x] is correct if no variable y in t is captured by a sup y (or inf y ) quantifier in ϕ[t/x].

The next lemma is the continuous analogue of the substitution lemma of classical first-order logic. Lemma 6.2 (Substitution Lemma). Let M be a continuous L-pre-structure, and let σ be an M-assignment. Let t be a term, x be a variable, and ϕ be a formula. Put a := t M,σ . Suppose ϕ[t/x] is correct. Then M(ϕ[t/x], σ) = M(ϕ, σ a x ). Definition 6.3. Let ϕ be a formula, and let x, y be variables. We define the bound substitution of y for x inside ϕ, ϕ{y/x}, as the result of replacing each subformula sup x α (or inf x α) of ϕ by sup y α[y/x] (or inf y α). We say that ϕ{y/x} is correct if y is not free in α and α[y/x] is correct in each such subformula sup x α (or inf x α).

The following lemma is an immediate result. The reader interested may consult [START_REF] Ebbinghaus | Mathematical logic[END_REF] for a classical first-order proof to see how a proof for continuous first-order logic may be constructed. Lemma 6.4 (Bound Substitution Lemma). Let ϕ be a formula, and let x 0 , . . . , x n-1 be a finite sequence of variables. Then by a sequence of bound substitutions there is a formula ϕ ′ in which x 0 , . . . , x n-1 are not bound and ϕ ≡ ϕ ′ . Metric Completions. We will presently see that each continuous L-pre-structure (for a continuous signature with a metric) is virtually indistinguishable from its metric completion (Theorem 6.9). To this end, we first offer a definition. Definition 6.5. Let M and N be continuous L-pre-structures, and let h : M → N. We call h an L-morphism of M into N if h satisfies the following two conditions:

(i) For each f ∈ F and all a 0 , . . . , a n f -1 ∈ M, h(f M (a 0 , . . . , a n f -1 )) = f N (h(a 0 ), . . . , h(a n f -1 )).

(ii) For each P ∈ R and all a 0 , . . . , a n P -1 ∈ M, P M (a 0 , . . . , a n P -1 ) = P N (h(a 0 ), . . . , h(a n P -1 )).

We call h an elementary L-morphism if h is an L-morphism and for every M-assignment σ and formula ϕ,

M(ϕ, σ) = N(ϕ, h • σ).
Observe that if L is a continuous signature with a metric d and h is an L-morphism of M into N, then for all a 0 , a 1 ∈ M, d M (a 0 , a 1 ) = d N (h(a 0 ), h(a 1 )).

In other words, h is an isometry.

An immediate consequence of our definitions is the following theorem.

Theorem 6.6. If M and N are continuous L-pre-structures and h : M → N is a surjective L-morphism, then h is an elementary L-morphism of M onto N.

Proof. Straightforward induction on formulae.

Definition 6.7. Let M be a continuous L-pre-structure. Let t be a term and ϕ be a formula such that all variables occurring in t and all free variables occurring in ϕ appear among n distinct variables x 0 , . . . , x n-1 . Define functions t M,x :

M n → M and ϕ M,x : M n → [0, 1] by setting for all ā ∈ M n , t M,ā := t M,σ ϕ M,x (ā) := M(ϕ, σ),
where σ is an M-assignment such that σ(x i ) = a i for each i < n.

We have all of the ingredients necessary to prove the following theorem. Theorem 6.8. Let M be a continuous L-pre-structure. Then for every term t and formula ϕ the mappings t M,x : M n → M and ϕ M,x : M n → [0, 1] are uniformly continuous.

Proof. By induction on terms and formulae, using the fact that moduli of uniform continuity can be built up from other moduli, as mentioned in Remark 5.8. Using Lemma 6.4, Theorem 6.6, and Theorem 6.8 , one can prove the following: Theorem 6.9 (Existence of Metric Completion). Let L be a continuous signature with a metric, and let M be a continuous L-pre-structure. Then there is a continuous Lstructure M and an elementary L-morphism of M into M.

Proof. The proof invokes elementary facts about metric spaces, pseudo-metrics, Cauchy sequences, and metric completions. Essential to this proof is the fact that for all metric spaces (M, d) and (M ′ , d ′ ) such that (M ′ , d ′ ) is complete and N ⊆ M, if f : N → M ′ is a mapping and δ is a modulus of uniform continuity for f , then f can be uniquely extended to a function f : N → M ′ such that δ is a modulus of uniform continuity for f (where N denotes the closure of N in M). This fact is important insofar as it implies that an underlying continuous signature with a metric will not have to be altered for a metric completion. Definition 6.10. Let L be a continuous signature with a metric, let Γ ⊆ For(L), and let ϕ be a formula.

(i) We write Γ QC ϕ if for every continuous L-structure M and M-assignment σ, if (M, σ) Q Γ, then (M, σ) Q ϕ. (ii) We say that Γ is completely satisfiable or that Γ has a complete model if there is a continuous L-structure M and M-assignment σ such that (M, σ) models Γ.

We therefore have the following corollary:

Corollary 6.11. Let L be a continuous signature with a metric, and let Γ ⊆ For(L).

Then for every formula ϕ, (i) Γ Q ϕ if and only if Γ QC ϕ.

(ii) Γ is satisfiable if and only if Γ is completely satisfiable.

We may thereby restrict the notion of logical entailment to continuous L-structures.

In classical first-order logic, if one were to require a distinguished binary relation symbol ≈ be interpreted only as a congruence relation in each classical structure rather than as strict equality, then one could show for each such structure that there is a surjective elementary L-morphism (in the obvious sense) onto its quotient structure. Accordingly, we would find that classical first-order logic does not distinguish between structures which require that ≈ be interpreted as a congruence relation and structures which require that ≈ be interpreted as strict equality.

In continuous first-order logic, we see a somewhat analogous result. We require that a distinguished binary relation symbol d be interpreted as a pseudo-metric that satisfies (A14) For each P ∈ R, ǫ ∈ (0, 1], and r, q ∈ D with r > ǫ and q < δ P,i (ǫ), the following is an axiom (where |x| = i and |x| + |ȳ| + 1 = n P ):

(q -. dzw) ∧ ((P xz ȳ -. P xwȳ) -. r)

Axiom schemata (A10) -(A12) assert that d is pseudo-metric. These axiom schemata correspond to the equivalence relation axiom schemata of classical first-order logic. Although less immediate, (A13) -(A14) define the uniform continuity moduli with respect to the ith argument.

Let us informally consider (A13). Suppose (A13) holds and that d(z, w) < δ f,i (ǫ). Then there is q ∈ D such that d(z, w) < q < δ f,i (ǫ), so q -. d(z, w) > 0, whence by (A13) it follows that d(f (x, z, ȳ), f (x, w, ȳ)) -. r = 0, i.e., d(f (x, z, ȳ), f (x, w, ȳ)) ≤ r for every r > ǫ. Thus, d(f (x, z, ȳ), f (x, w, ȳ)) ≤ ǫ, so δ f,i is a uniform continuity modulus of f with respect to the ith argument. Conversely, suppose δ f,i is a uniform continuity modulus of f with respect to the ith argument and that r, q ∈ D are such that r > ǫ and q < δ P,i (ǫ). On the one hand, if q -. d(z, w) > 0, then d(z, w) < q < δ f,i (ǫ) and so d(f

(x, z, ȳ), f (x, w, ȳ)) ≤ ǫ < r, whence d(f (x, z, ȳ), f (x, w, ȳ)) -. r = 0 and therefore (q -. d(z, w)) ∧ (d(f (x, z, ȳ), f (x, w, ȳ)) -. r) = 0. On the other hand, if q -. d(z, w) ≤ 0, again we have (q -. d(z, w)) ∧ (d(f (x, z, ȳ), f (x, w, ȳ)) -. r) = 0.
Remark 7.1. In view of Remark 5.8, the reader may have noticed that a continuous signature could equivalently be defined so that G may instead have the form {δ s : (0, 1] → (0, 1] : s ∈ R ∪ F }, whereby one could forgo talk of moduli of uniform continuity of each symbol s with respect to each of its arguments. In particuar, (A13) could be replaced by (A13 ′ ) For every ǫ ∈ (0, 1] and r, q ∈ D with r > ǫ and q < ∆ f (ǫ), the following is an axiom:

(q -. i<n f dx i y i ) ∧ (df x 0 • • • x n f -1 f y 0 • • • y n f -1 -. r) (
A14) could also be replaced by an analogous axiom. Situations might arise in which the uniform continuity moduli of a symbol with respect to each of its arguments are very different, and one might desire to keep track of this, thereby preferring one definition over the other.

We conclude this section with a soundness theorem.

Theorem 7.2 (Soundness). Let L be a continuous signature (with a metric), and let Γ ⊆ For(L). Then for every formula ϕ,

(i) If Γ ⊢ Q ϕ, then Γ Q ϕ (Γ QC ϕ). (ii) If Γ is (completely) satisfiable, then Γ is consistent.
Proof. It suffices to show that each axiom schema is valid. The facts recorded in §4 can be used to show that (A1) -(A6) are valid, while the results from §6 can be used to prove that (A7) -(A9) are valid. The discussion following (A14) explains why (A10) -(A14) are valid.

The Essentials

In this section, we rely heavily on facts recorded in §4 insofar as we exploit obvious relations amongst continuous first-order logic and continuous and Lukasiewicz propositional logics.

The Deduction Theorem, Generalization Theorem, and a Lemma about Bound Substitution. Observe

{(P -. Q) -. Q, Q} ⊢ L P, but {(P -. Q) -. Q} L P -. Q.
Thus the reader should be unsurprised to find that continuous first-order logic only satisfies a weak version of the classical Deduction Theorem.

Theorem 8.1 (Deduction Theorem). Let Γ ⊆ For(L), and let ϕ, ψ be formulae.

Then Γ ∪ {ψ} ⊢ Q ϕ if and only if Γ ⊢ Q ϕ -. nψ for some n < ω.
Proof. Right to left is clear. For the implication from left to right, observe that for all α, β, γ and n, m < ω,

⊢ L ((β -. (n + m)α) -. ((β -. γ) -. nα)) -. (γ -. mα).
This can be shown using the semantics of Lukasiewicz propositional logic. The proof then proceeds by induction on the set of consequences of Γ ∪ {ψ}.

Lemma 8.2 (Generalization Theorem). Let Γ ⊆ For(L), and let ϕ be a formula. If Γ ⊢ ϕ and x is not a free variable in Γ, then Γ ⊢ sup x ϕ.

Proof. This is similar to the proof of the Generalization Theorem for classical first-order logic (see [START_REF] Herbert | A mathematical introduction to logic[END_REF]).

To illustrate how we rely on facts recorded in §4 , we provide a proof of the next lemma.

Lemma 8.3. Let ϕ be a formula, and let y be a variable which does not occur in ϕ. Then

(a) ⊢ Q ϕ -. ϕ{y/x}. (b) ⊢ Q ϕ{y/x} -. ϕ.
Proof. This is proved by induction on ϕ for y which does not occur in ϕ. ϕ = P t 0 • • • t n P -1 : Then by definition ϕ{y/x} = ϕ; since ⊢ Q ϕ -. ϕ, we are done. ϕ = 1 2 ψ: Then by definition ϕ{y/x} = 1 2 ψ{y/x} and this bound substitution is correct. So by the induction hypothesis, we have ⊢ Q ψ -. ψ{y/x} and ⊢ Q ψ{y/x} -. ψ. Now observe

⊢ C L 1 2 α -. α, and
⊢ C L ( 1 2 β -. 1 2 α) -. 1 2 (β -. α).
Thus by a few applications of modus ponens, we arrive at

⊢ Q α -. α{y/x}, ⊢ Q α{y/x} -. α, and
⊢ Q β -. β{y/x}, ⊢ Q β{y/x} -. β. Moreover, observe ⊢ L (((β ′ -. α ′ ) -. (β -. α)) -. (β ′ -. β)) -. (α -. α ′ ).
Hence, by repeated applications of modus ponens and the induction hypothesis, we obtain (a) and (b). ϕ = sup x ψ: Then ϕ{y/x} = sup x ψ[y/x] and this substitution is correct (y is not free in ψ). Hence,

⊢ Q ψ[y/x] -. sup x ψ (A8) ⊢ Q sup y (ψ[y/x] -. sup x ψ) (Generalization Theorem) ⊢ Q (sup y ψ[y/x] -. sup y sup x ψ) -. sup y (ψ[y/x] -. sup x ψ) (A7) ⊢ Q sup y ψ[y/x] -. sup y sup x ψ (modus ponens) ⊢ Q ((sup y ψ[y/x] -. sup x ψ) -. (sup y ψ[y/x] -. sup y sup x ψ)) -. (sup y sup x ψ -. sup x ψ) (A2) ⊢ Q sup y sup x ψ -. sup x ψ (A9) (y is not free in sup x ψ),
from which it follows by applying modus ponens several times that ⊢ Q ϕ{y/x}-. ϕ. A similar argument can be used to establish (a). ϕ = sup z ψ and z = x: Then ϕ{y/x} = sup z ψ{y/x} and this bound substitution is correct. Apply the induction hypothesis, the Generalization Theorem, (A7), and modus ponens to obtain (a) and (b).

If c is an 0-ary function symbol (what we of course call a constant symbol ) and x is a variable, we may define ϕ[x/c] in the expected way. However, we omit a formal definition and state a lemma without proof.

Lemma 8.4. Let Γ ⊆ For(L), and let ϕ be a formula. If Γ ⊢ Q ϕ, c is a constant symbol that does not occur in Γ, and x does not occur in ϕ, then

Γ ⊢ Q sup x ϕ[x/c].
Maximal Consistent Sets of Formulae. In classical first-order logic, we say that a set ∆ of formulae is maximal consistent if ∆ is consistent and for every formula ϕ, ϕ ∈ ∆ or ¬ϕ ∈ ∆. In continuous first-order, however, this definition will not do. For we certainly should like to exclude both 1 2 and ¬ 1 2 from every consistent set. In this subsection, we show what one should mean by calling a set of formulae maximal consistent in continuous first-order logic.

Lemma 8.5. Let Γ ⊆ For(L) be consistent. Then for all formulae ϕ, ψ,

(i) If Γ ⊢ Q ϕ -. 2 -n for all n < ω then Γ ∪ {ϕ} is consistent. (ii) Either Γ ∪ {ϕ -. ψ} or Γ ∪ {ψ -. ϕ} is consistent.
Proof.

(i) Suppose Γ ⊢ Q ϕ -. 2 -n for all n < ω. For reductio ad absurdum, assume Γ ∪ {ϕ} is inconsistent. Then by the Deduction Theorem, Γ ⊢ 1 -. mϕ for some m < ω. Observe

⊢ L (((β -. α σ(0) ) -. α σ(1) ) -. • • • -. α σ(k-1) ) -. (((β -. α 0 ) -. α 1 ) -. • • • -. α k-1 )
for any k < ω and permutation σ on k. By repeated uses of this fact, axiom (A2), and our supposition, we find that Γ ⊢

Q ((1 -. 2 -1 ) -. 2 -2 ) -. • • • -. 2 -m
, so Γ is inconsistent, yielding a contradiction. (ii) Suppose Γ ∪ {ϕ -. ψ} is inconsistent. Then by the Deduction Theorem, there is n < ω such that Γ ⊢ Q 1 -. n(ϕ -. ψ). Observe that for all m < ω, ⊢ L (β -. α) -.

(1 -. m(α -. β)), whereby it follows that ⊢ Q (ϕ -. ψ) -. (1 -. n(ϕ -. ψ)). Hence, by modus ponens we have Γ ⊢ Q ψ -. ϕ, so Γ ∪ {ψ -. ϕ} is consistent.

Lemma 8.6. Let Γ ⊆ For(L) be consistent, and let E(Γ) := {Γ ′ : Γ ⊆ Γ ′ ⊆ For(L) and Γ ′ is consistent} Then ∆ is a maximal member of E(Γ) if and only if for all formulae ϕ, ψ, (i) Γ ⊆ ∆ and ∆ is consistent.

(ii) If ∆ ⊢ Q ϕ -. 2 -n for all n < ω then ϕ ∈ ∆. (iii) ϕ -. ψ ∈ ∆ or ψ -. ϕ ∈ ∆.
Proof.

(⇒) If ∆ is a maximal member of E(Γ), then (i) is immediate, while (ii) and (iii) follow from Lemma 8.5. (⇐) Suppose (i), (ii), and (iii) hold. Let Γ ′ ∈ E(Γ) be such that ∆ ⊆ Γ ′ . Assume ϕ ∈ Γ ′ . Then for every n < ω, 2 -n -. ϕ / ∈ Γ ′ and so ϕ -. 2 -n ∈ ∆. It follows that ϕ ∈ ∆, as desired.

Remark 8.7. In continuous propositional logic, conditions (ii) and (iii) are independent. To see this, let S be a continuous propositional logic. First we show that (ii) does not imply (iii). Let ∆ := {ϕ ∈ S : ⊢ C L ϕ}. Observe that by completeness of continuous Lemma 8.12. Let Γ ⊆ For(L) be consistent, let ∆ be a maximal consistent set of formulae containing Γ, and let ϕ be a formula. Then sup{p ∈ D : p -. ϕ ∈ ∆} = inf{q ∈ D : ϕ -. q ∈ ∆}.

Proof. Straightforward, by Lemma 8.6.

Completeness Theorem

In classical first-order logic, we say that a set Γ of formulae is Henkin complete if for every formula ϕ and variable x, there is a constant c such that ¬∀xϕ → ¬ϕ[c/x] ∈ Γ. The intuition to define a Henkin complete set in continuous first-order logic as the syntactic translation of this definition will not work. Indeed, if Γ is maximal consistent and ¬ sup x ¬ϕ ∈ Γ, i.e., inf x ϕ ∈ Γ, we would be better off to not require that there is a constant c such that ϕ[c/x] ∈ Γ. For example, a perfectly consistent situation could arise in which inf x ϕ ∈ Γ, there is a sequence of formulae (ϕ[

t i /x] : i < ω) such that Γ ⊢ Q ϕ[t n /x] -. 2 -n for each n < ω, yet each term t has a non-zero p t ∈ D such that Γ ⊢ Q p t -. ϕ[t/
x], whereby we should certainly not require that there is a term t such that ϕ[t/x] ∈ Γ. Rather than attempt to prevent this sort of situation from ever occurring, we wish to accommodate this sort of situation in our definition of a Henkin complete set. Definition 9.1. Let Γ be a set of formulae. We say that Γ is Henkin complete if for every formula ϕ, variable x, and p, q ∈ D with p < q, there is a constant symbol c such that (sup x ϕ -. q) ∧ (p -. ϕ[c/x]) ∈ Γ.

The next proposition guarantees we can construct a consistent Henkin complete set.

Proposition 9.2. Let L be a continuous signature. There exists a continuous signature L c with L ⊆ L c and a set Γ c ⊆ F or(L c ) such that for every Γ ⊆ For(L),

(i) Γ ∪ Γ c is Henkin complete. (ii) If Γ is consistent, then Γ ∪ Γ c is consistent.
Proof. Permitting some abuse of notation, we define an increasing sequence of signatures inductively:

L 0 := L L n+1 := L n ∪ {c (ϕ,x,p,q) : ϕ ∈ F or(L n ),
x ∈ V, and p, q ∈ D with p < q} where each c (ϕ,x,p,q) is a new constant symbol. We then put L c := n<ω L n ψ (ϕ,x,p,q) := (sup x ϕ -. q) ∧ (p -. ϕ[c (ϕ,x,p,q) /x]) and Γ c := {ψ (ϕ,x,p,q) : ϕ ∈ F or(L c ), x ∈ V, and p, q ∈ D with p < q}.

(i) is obviously true, so we proceed to establish (ii). Suppose Γ is consistent. For reductio ad absurdum, assume Γ ∪Γ c is inconsistent. Then there is a minimal finite non-empty Γ c 0 ⊆ Γ c such that Γ ∪ Γ c 0 is inconsistent. We may write Γ c 0 = {ψ (ϕ i ,x i ,p i ,q i ) : i < n}, where the (ϕ i , x i , p i , q i ) are pairwise distinct. For each i < n, there is a minimal m i such that ϕ i ∈ F or(L m i ). Let m i 0 be the maximal such m i . For simplicity of notation, put ϕ := ϕ i 0 , x := x i 0 , p := p i 0 , q := q i 0 , and m := m i 0 . Now observe that for each i < n, ϕ i ∈ F or(L m ), while c (ϕ,x,p,q) ∈ L m+1 \L m . Put Γ c 1 := Γ c 0 \{ψ (ϕ,x,p,q) } and Γ 1 := Γ ∪ Γ c consistent and Henkin complete set ∆ ⊆ F or(L c ) with ∆ ⊇ Γ, a continuous L c -prestructure M, and an M-assignment σ such that (M, σ) Q ∆.

Proof. Suppose Γ is consistent. By the previous proposition, there is Γ c ⊆ F or(L c ) such that Γ ∪ Γ c is consistent and Henkin complete, so by Theorem 8.10 there is a maximal

consistent ∆ ⊆ F or(L c ) such that ∆ ⊇ Γ ∪ Γ c . Define a continuous L c -pre-structure M such that M is the set of all L c -terms. (i) For each f ∈ F , define f M : M n f → M by setting f M (t 0 , . . . , t n f -1 ) := f t 0 • • • t n f -1 for all t 0 , . . . , t n f -1 ∈ M. (ii)
For each P ∈ R, define P M : M n P → [0, 1] by setting P M (t 0 , . . . , t n P -1 ) := sup{p ∈ D : p -. P t 0 • • • t n P -1 ∈ ∆} for all t 0 , . . . , t n P -1 ∈ M. Define an M-assignment σ by setting σ(x) := x for all x ∈ V . It is a simple matter to check that t M,σ = t for all terms t.

It suffices to prove by induction on the number of quantifiers and connectives in ϕ, i.e., the rank of ϕ, that M(ϕ, σ) = sup{p ∈ D : p -. ϕ ∈ ∆} for all ϕ ∈ F or(L c ). For the sake of brevity, here we only consider the subcases ϕ = 1 2 ψ and ϕ = sup x ψ. Although the case for rank(ϕ) = 0 is trivial, we encourage the reader to work out the subcases of ¬ and -. for rank(ϕ) > 0. (a) Suppose sup{M(ψ, σ t x ) : t ∈ M} < sup{p ∈ D : p -. sup x ψ ∈ ∆}. Then for some p, q ∈ D, sup{M(ψ, σ t x ) : t ∈ M} < p < q < sup{p ∈ D : p -. sup x ψ ∈ ∆}. Since Γ c ⊆ ∆ and p < q, there is a constant c such that (sup x ψ -. q) ∧ (p -. ψ[c/x]) ∈ ∆. Furthermore, there is r ∈ D such that q < r and r -. sup x ψ ∈ ∆. As ∆ is maximal consistent, by x ) : t ∈ M}. On the one hand, since ∆ is maximal consistent, for all p ∈ D such that p > sup{p ∈ D : p -. sup x ψ ∈ ∆}, sup x ψ -. p ∈ ∆. On the other hand, there must be t ∈ M such that M(ψ, σ t

x ) > sup{p ∈ D : p -. sup x ψ ∈ ∆}, so there is p ∈ D such that M(ψ, σ t x ) > p > sup{p ∈ D : p -. sup x ψ ∈ ∆}. Thus sup x ψ -. p ∈ ∆, whence by Lemma 8.11, there is ψ ′ ≡ ψ such that ψ ′ [t/x] -. p ∈ ∆. Thus inf{p : ψ ′ [t/x] -. p ∈ ∆} ≤ p. By Lemma 8.12, inf{p : ψ ′ [t/x] -. p ∈ ∆} = sup{p ∈ D : p -. ψ ′ [t/x] ∈ ∆}, and because rank(ψ ′ [t/x]) < rank(ϕ), our induction hypothesis tells us that M(ψ ′ [t/x], σ) = sup{p ∈ D : p -. ψ ′ [t/x] ∈ ∆}. Moreover, since ψ ′ [t/x] is correct, M(ψ ′ [t/x], σ) = M(ψ ′ , σ t x ) by Lemma 6.2. Finally, since ψ ′ ≡ ψ, we have M(ψ ′ , σ t

x ) = M(ψ, σ t x ). It follows that M(ψ, σ t x ) ≤ p, yielding another contradiction. Now if ϕ ∈ ∆, then by (A1), ϕ -. 0 ∈ ∆, so M(ϕ, σ) = sup{p ∈ D : p -. ϕ ∈ ∆} = inf{q ∈ D : ϕ -. q ∈ ∆} = 0 (Lemma 8.12). This shows that (M, σ) Q ∆, proving our theorem.

We may now state and prove the long-awaited completeness theorem. Theorem 9.5 (Completeness for Continuous First-Order Logic). Let L be a continuous signature, and let Γ ⊆ For(L). Then Γ is consistent only if Γ is satisfiable. Furthermore, if L is a continuous signature with a metric, then Γ is consistent only if Γ is completely satisfiable. Proof. By Theorem 9.4, there is a continuous signature L c ⊇ L, a maximal consistent set ∆ ⊆ F or(L c ) with ∆ ⊇ Γ, an L c -pre-structure M, and an M-assignment σ such that (M, σ) Q ∆. If L does not have a metric, we are done; we observe (M, σ) models Γ and simply restrict M to our original signature. But if L has a metric d, we can only guarantee that d M is a pseudo-metric relative to this restriction. We wish to find a continuous L-structure M and an M-assignment σ such that ( M, σ) Q Γ. By Theorem 6.9, there is a continuous L-structure M and an L-morphism h : M → M such that for every formula ϕ, M(ϕ, σ) = M(ϕ, h • σ). Therefore, putting σ := h • σ, since (M, σ) models Γ, ( M, σ) models Γ.

We conclude with several corollaries. The following result has a counterpart in [START_REF] Hay | Axiomatization of the infinite-valued predicate calculus[END_REF] (see also [START_REF] Hájek | Metamathematics of fuzzy logic[END_REF]).

(ii) We call a theory T complete if there is a continuous L-structure M (and an Massignment σ) such that T = {ϕ : (M, σ) QC ϕ}. Otherwise, we call T an incomplete theory.

Definition 9.10. Let T be a theory. (i) If T is complete, we say T is decidable if for every sentence ϕ, the value ϕ • T is a recursive real and uniformly computable from ϕ. (ii) If T is incomplete, we say T is decidable if for every sentence ϕ the real number ϕ • T is uniformly recursive from ϕ. Corollary 9.11. Every complete theory with a recursive or recursively enumerable axiomatization is decidable.

As with classical first-order logic, the following corollary could be obtained more directly by way of an ultraproduct construction (see [BU]). We nevertheless include it for the sake of completeness. Corollary 9.12 (Compactness). Let L be a continuous signature, and let Γ ⊆ For(L). If every finite subset Γ 0 of Γ is (completely) satisfiable, then Γ is (completely) satisfiable.

Fact 4. 1 (

 1 Weak Completeness for Lukasiewicz Logic[START_REF]A new proof of the completeness of the Lukasiewicz axioms[END_REF][START_REF] Rose | Fragments of many-valued statement calculi[END_REF]). Let S be a Lukasiewicz propositional logic and ϕ ∈ S. Then ϕ if and only if ⊢ ϕ.

Fact 4. 4 (

 4 Approximated Strong Completeness for Continuous Logic). Let S be a continuous propositional logic, Σ ⊆ S, and ϕ ∈ S. Then Σ ϕ if and only

  e, b)), where |ā| = i and |ā| + | b| + 1 = n f . • For each relation symbol P and i < n P , ∀ā, b, c, e (c ≈ A e =⇒ (P A (ā, c, b) ⇒ P A (ā, e, b))), where |ā| = i and |ā| + | b| + 1 = n P .

Definition 5. 9 .

 9 A continuous L-structure is a continuous L-pre-structure M = (M, ρ) such that ρ assigns to d a complete metric: (i) ∀a, b (d M (a, b) = 0 =⇒ a = b).

  (a) and (b). ϕ = ¬ψ: Then again by definition ϕ{y/x} = ¬ψ{y/x} and this bound substitution is correct. Observe ⊢ L (¬α -. ¬β) -. (β -. α). Using the induction hypothesis and modus ponens we obtain (a) and (b). ϕ = (β -. α): Then ϕ{y/x} = (β{y/x} -. α{y/x}) and β{y/x} and α{y/x} are correct. Our induction hypothesis supplies us

  We wish to show that M( 1 2 ψ, σ) = sup{p ∈ D : p -. 1 2 ψ ∈ ∆}. By definition, M( 1 2 ψ, σ) = 1 2 sup{p ∈ D : p -. ψ ∈ ∆}, and by induction hypothesis, M(ψ, σ) = sup{p ∈ D : p -. ψ ∈ ∆}. We must therefore show 1 2 sup{p ∈ D : p -. ψ ∈ ∆} = sup{p ∈ D : p -. 1 2 ψ ∈ ∆}. We consider two cases. (a) By Fact 4.5, since ∆ is maximal consistent, for every p ∈ D, p -. 1 2 ψ ∈ ∆ only if ¬(¬p -. p) -. ψ ∈ ∆. Hence, for every p ∈ D such that p -. 1 2ψ ∈ ∆, p ≤ 1 2 ¬(¬p -. p) ≤ 1 2 sup{p ∈ D : p -. ψ ∈ ∆}. It follows that sup{p ∈ D : p -. 1 2 ψ ∈ ∆} ≤ 1 2 sup{p ∈ D : p -. ψ ∈ ∆}. (b) By Fact 4.5, since ∆ is maximal consistent, for every p ∈ D, p -. ψ ∈ ∆ only if 1 2 p-. 1 2 ψ ∈ ∆ (cf.proof of Lemma 8.3). Hence, for every p ∈ D such that p-. ψ ∈ ∆,1 2 p ≤ sup{p ∈ D : p -. 1 2 ψ ∈ ∆} and therefore p ≤ 2 sup{p ∈ D : p -. 1 2 ψ ∈ ∆}. It follows that sup{p ∈ D : p -. ψ ∈ ∆} ≤ 2 sup{p ∈ D : p -. 1 2 ψ ∈ ∆}, whence 1 2 sup{p ∈ D : p -. ψ ∈ ∆} ≤ sup{p ∈ D : p -. 1 2 ψ ∈ ∆}, as desired. ϕ = sup x ψ:We wish to show that M(sup x ψ, σ) = sup{p ∈ D : p-. sup x ψ ∈ ∆}. Observe that by definition M(sup x ψ, σ) = sup{M(ψ, σ t x ) : t ∈ M}. So it suffices to show that sup{M(ψ, σ t x ) : t ∈ M} = sup{p ∈ D : p -. sup x ψ ∈ ∆}. For reductio ad absurdum, assume this equality fails to hold. We of course consider two cases.

  Fact 4.5 it follows that p -. ψ[c/x] ∈ ∆. Since rank(ψ[c/x]) < rank(ϕ), our induction hypothesis tells us that M(ψ[c/x], σ) = sup{p ∈ D : p-. ψ[c/x] ∈ ∆}. Also, since ψ[c/x] is correct, by Lemma 6.2 it follows that M(ψ[c/x], σ) = M(ψ, σ c x ). Thus p ≤ M(ψ, σ c x ) ≤ sup{M(ψ, σ t x ) : t ∈ M}, yielding a contradiction. (b) Suppose sup{p ∈ D : p -. sup x ψ ∈ ∆} < sup{M(ψ, σ t

. Note that c (ϕ,x,p,q) does not occur in Γ 1 and that Γ 1 must be consistent (by the minimality of Γc 0 ). Nonetheless, Γ ∪ Γ c 0 = Γ 1 ∪ {(sup x ϕ -. q) ∧ (p -. ϕ[c (ϕ,x,p,q) /x])} is inconsistent. Observe that ⊢ L (α ∧ β) -. α and ⊢ L (α ∧ β) -. β.Thus, by modus ponens,Γ 1 ∪ {(sup x ϕ -. q)} ⊢ Q (sup x ϕ -. q) ∧ (p -. ϕ[c (ϕ,x,p,q) /x]), and Γ 1 ∪ {(p -. ϕ[c (ϕ,x,p,q) /x])} ⊢ Q (sup x ϕ -. q) ∧ (p -. ϕ[c (ϕ,x,p,q) /x]).Since Γ ∪ Γ c 0 is inconsistent, by the Deduction Theorem there is n < ω such that Γ 1 ⊢ Q 1 -. n((sup x ϕ -. q) ∧ (p -. ϕ[c (ϕ,x,p,q) /x])). Therefore, by modus ponens, we find thatΓ 1 ∪ {(sup x ϕ -. q)} and Γ 1 ∪ {(p -. ϕ[c (ϕ,x,p,q) /x])} are both inconsistent. It follows that Γ 1 ⊢ Q (q -. sup x ϕ) and Γ 1 ⊢ Q (ϕ[c (ϕ,x,p,q) /x] -. p) (cf. proof of Lemma 8.5).Now let y be a variable not occurring in ϕ. On the one hand, by Lemma 8.3 we have

Definition 9.7. Let L be a continuous signature (possibly with a metric), let Γ ⊆ For(L), and let ϕ be a formula.(i) We define the degree of truth of ϕ with respect to Γ, ϕ • Γ , by setting ϕ • Γ := sup{M(ϕ, σ) : (M, σ) Γ}. (ii) We define the degree of provability of ϕ with respect to Γ, ϕ ⊚ Γ , by setting ϕ ⊚ Γ := inf{p ∈ D : Γ ⊢ ϕ -. p}. We then have the following result, commonly called Pavelka-style completeness.Corollary 9.8. Let L be a continuous signature, and let Γ ⊆ For(L). Then for every formula ϕ, the degree of truth of ϕ with respect to Γ equals the degree of provability of ϕ with respect to Γ. In other words,ϕ • Γ = ϕ ⊚ Γ .Proof. We consider two cases:(i) We first show ϕ • Γ ≤ ϕ ⊚ Γ . This follows from soundness (Theorem 7.2). To see this, observe that for every p ∈ D such that Γ ⊢ ϕ -. p, by soundness Γ ϕ -. p, so for any continuous L(-pre)-structure M and M-assignment σ such that (M, σ) Γ, M(ϕ, σ) ≤ p; thus, ϕ• Γ ≤ p. It follows that ϕ • Γ ≤ ϕ ⊚ Γ . (ii) We now show ϕ • Γ ≥ ϕ ⊚ Γ .It suffices to show that for each p ∈ D such that p < ϕ ⊚ Γ , there is a continuous L(-pre)-structure M and M-assignment σ such that

congruence properties, akin to those of classical first-order logic (cf. Definition 5.6, parts (iii) and (iv)). One can show that for each L-pre-structure, there is a surjective elementary L-morphism onto its quotient structure (which essentially transforms d into a genuine metric). Yet one can go one step further: For any L-pre-structure with a genuine metric, there is an injective elementary L-morphism (and a fortiori an isometry) into its completion, a continuous L-structure. Therefore, continuous first-order logic does not distinguish between continuous L-pre-structures and continuous L-structures. Theorem 6.9 can be seen as encoding this fact. As you would expect, most of our work does not rely on this fact, but it nevertheless indicates what matters.

Axioms: Group 2

Before we present the second group of axioms, let us define a notion familiar from classical first-order logic. We say that a formula ϕ is a generalization of a formula ψ if for some n < ω there are variables x 1 , . . . , x n such that ϕ = sup x 1 • • • sup xn ψ (see [START_REF] Herbert | A mathematical introduction to logic[END_REF]). Observe that every formula is a generalization of itself.

When all generalizations of the following eight axiom schemata are added to all generalizations of (A1) -(A6) (in the appropriate language of course), we obtain an axiomatization for continuous first-order logic. In this article we show that this axiomatization is complete. Formal deductions and provability are defined as in §3, the only rule of inference again being modus ponens. We write Γ ⊢ Q ϕ to indicate that ϕ is provable from Γ in continuous first-order logic. Recall that a formula ϕ is provable from Γ just in case it is provable from a finite subset of Γ.

The first three schemata are analogues of axiom schemata of classical first-order logic (see [START_REF] Herbert | A mathematical introduction to logic[END_REF]).

, where substitution is correct (A9) sup x ϕ -. ϕ, where x is not free in ϕ If we are dealing with a continuous signature with a metric, we add:

1], and r, q ∈ D with r > ǫ and q < δ f,i (ǫ), the following is an axiom (where |x| = i and |x|

propositional logic (Fact 4.5), ∆ is consistent, and if ∆ ⊢ C L ϕ -. 2 -n for all n < ω, then ϕ ∈ ∆. However, since C L P -. 1 2 and C L 1 2 -. P , neither P -. 1 2 nor 1 2 -. P is in ∆. We now show that (iii) does not imply (ii). Let Γ := {P -. 2 -n : n < ω}. Then Γ is consistent, and so by (ii) of Lemma 8.5 we can construct a consistent set ∆ ⊇ Γ such that for every ϕ, ψ ∈ S, either ϕ -. ψ ∈ ∆ or ψ -. ϕ ∈ ∆. Nonetheless, ∆ ⊢ C L P -. 2 -n for all n < ω, yet P / ∈ ∆.

Lemma 8.6 justifies the following the definition.

Definition 8.8. Let ∆ ⊆ For(L). We say that ∆ is maximal consistent if ∆ is consistent and for all formulae ϕ, ψ,

Condition (i) says that if ∆ can furnish a series of proofs which altogether indicate that ϕ is a consequence of ∆, then ∆ must be granted ϕ. Condition (ii) says that ∆ can compare any two formulae.

Remark 8.9. Observe that if ∆ a maximal consistent set of formulae, then ϕ ∈ ∆ if and only if ∆ ⊢ Q ϕ. It can be shown that in the above definition condition (i) can be replaced by condition (i ′ ): If {ϕ -. 2 -n : n < ω} ⊆ ∆, then ϕ ∈ ∆. Indeed, condition (i ′ ) is also independent of (ii) in continuous propositional logic.

We thereby obtain the following result.

Theorem 8.10. If Γ ⊆ For(L) is consistent, then there exists a maximal consistent set of formulae ∆ ⊇ Γ.

Proof. By Zorn's Lemma and Lemma 8.6.

Lemma 8.11. Let Γ ⊆ For(L), let ∆ be a maximal consistent set of formulae containing Γ, let t be a term, and let p ∈ D. Then if sup x ϕ -. p ∈ ∆, there is a formula ϕ ′ such that ϕ ≡ ϕ ′ and ϕ ′ [t/x] -. p ∈ ∆.

Proof. By Lemma 6.4, there is a formula ϕ ′ such that no variable of t is bound in ϕ ′ and ϕ ≡ ϕ ′ , so by repeated applications of Lemma 8.3 and (A2), we have

Then by the Generalization Theorem, ⊢ Q sup x (ϕ ′ -. ϕ), whence by (A7) it follows that

is correct, again by (A2) and by (A8) we have ∆ ⊢ Q ϕ ′ [t/x] -. sup x ϕ, so once more by (A2) it follows that ∆ ⊢ Q ϕ ′ [t/x] -. p. Therefore, since ∆ is maximal consistent, we conclude that ϕ ′ [t/x] -. p ∈ ∆, as desired.

We will use the following lemma to define a continuous pre-structure and to help us in parts of our proof of completeness. Γ 1 ⊢ Q (q -. sup x ϕ){y/x} -. (q -. sup x ϕ), so by modus ponens,

= (q -. sup y ϕ[y/x]).

On the other hand, because c (ϕ,x,p,q) does not occur in Γ 1 , by Lemma 8.4 we have Γ 1 ⊢ Q sup y (ϕ[c (ϕ,x,p,q) /x] -. p)[y/c (ϕ,x,p,q) ] = sup y (ϕ[c (ϕ,x,p,q) /x][y/c (ϕ,x,p,q) ] -. p[y/c (ϕ,x,p,q) ]) = sup y (ϕ[y/x] -. p).

Then by (A7) and modus ponens, Γ 1 ⊢ Q sup y ϕ[y/x] -. sup y p. Since y is not free in p, (A9) yields Γ 1 ⊢ Q sup y p -. p. Thus by (A2) and modus ponens, Γ 1 ⊢ Q sup y ϕ[y/x] -. p. It remains to observe that since Γ 1 ⊢ Q (q -. sup y ϕ[y/x]) and Γ 1 ⊢ Q sup y ϕ[y/x] -. p, by (A2) we have Γ 1 ⊢ Q q -. p, so Γ 1 is inconsistent, which is impossible (q -. p ∈ D and q -. p > 0 by construction). Definition 9.3. We define the rank of ϕ, rank(ϕ), by recursion:

Theorem 9.4. Let L be a continuous signature (possibly with a metric), and let Γ ⊆ For(L). Assume Γ is consistent. Then there is a continuous signature L c ⊇ L, a maximal (M, σ) Γ and p ≤ M(ϕ, σ). Let p ∈ D, and suppose p < ϕ ⊚ Γ . Then Γ ϕ -. p, so Γ ∪ {p -. ϕ} is consistent (cf. proof of Lemma 8.5), whence by Theorem 9.5, Γ ∪ {p -. ϕ} is (completely) satisfiable. Hence, there is a continuous L(-pre)structure M and M-assignment σ such that (M, σ) Γ and M(p -. ϕ, σ) = 0, so p ≤ M(ϕ, σ). Definition 9.9. Let L be a continuous signature with a metric.

(i) We call T a theory if T is a set of formulae in L without free variables, i.e., a set of sentences.