A fashionable Partial and Heterogeneous mirror for Modality

María Manzano and Antonia Huertas March 30, 1999

Contents

1 Introduction 2 2 Predicate Modal Logic (ML) as a Prelogic. 2 3 The Logic PHL for ML. 5 4 Building PHL for any prelogic XL. 10 5 Translating XL into PHL 11 6 Translating the prelogic ML into PHL 13 7 Building the improved PML. 16 8 Building the logic PXL. 18 9 Concluding Remarks. 19

1 Introduction

The aim of this paper is twofold: In the first place we present a partial and heterogeneous mirror for modality which serves to build a modal predicate partial logic; in the second place, we propose a general method to redesign a logic.

In both cases the starting point is a logic non totally developed or accepted, which we call here a prelogic. From a complete analysis of this prelogic, we build a possibly partial and heterogeneous logic which serves as the underlying logic of the whole construction to be carried out afterwards. For the predicate modal logic ML (as presented in [2]), the logic we build is PHL, a fashionable mirror where ML is reflected^{1}. In this logic the implicit partiallity of ML is made explicit, with a complete set of partial connectives and suitable quantifiers. Moreover, modality is washed out, heterogeneous quantification used for the purpose. We also provide some broad guidelines to build the appropriate PHL for any prelogic XL.

Once we have our partial and heterogeneous logic, PHL, we should define a translation of formulas of the original logic into PHL and a conversion of structures of the original logic into the partial and heterogeneous structures ^{2}. As a result of this process, we obtain a theory in PHL representing the original logic. In the case of predicate modal logic this is the theory Δ, while for the general case we provide some goals in the form of theorems we will need in further stages.

Provided we have a representation theorem, we easily obtain the enumerability theorem for the logic being studied and the possibility of using the deductive machinery of the underlying logic. In case you can represent in PHL not only validity, but also consequence, compactness and Löwenheim theorems can be dragged out from PHL to the original logic.

In correspondence theory, where the logics we study are well equipped, with a proper semantics, this is the end of the story. But in our case we use the mirror image to build an improved logic in the real world. This has been done for predicate modal logic, obtaining PML; i.e., a modal logic where partiality is proper. In the general case, some goals are provided to guide the construction.

2 Predicate Modal Logic (ML) as a Prelogic.

A prelogic is a non totally defined or accepted logic. There are many reasons for regarding predicate modal logic as a prelogic. First of all, although the semantics of propositional modal logic has been known and accepted since Kripke, the suitable semantics for the predicate case is still an open problem. The number of papers written on predicate modal logic is small, if we compare it to the enormous quantity of work on propositional modal logic. In fact, in many cases predicate modal logic appears as a single chapter or an appendix in books on propositional modal logic. Modal predicate logic is usually given syntactically and no fixed semantics is often discussed.

1The results are in Antonia’s thesis[4].

2This plan coincides basically with the one followed in Chapter VII of Maria’s [5]

We refer to three of the most important works on predicate modal logic: chapters VIII and X of [2], chapter IX of [3] and chapter XII of [6]. In all these papers, and in most of the papers written on the subject, predicate modal logic is obtained by adding the monadic operator □ (or L), with the usual modal interpretation of necessity, to the standard language of predicate logic, i.e. exactly in the same way that it is added to the standard language of propositional logic in order to obtain the propositional modal logic. Terms and formulas are defined as expected.

Modal predicate logic usually given syntactically. Modal predicate logic is usually given by axiomatization, i.e. adding modal axioms and the modal rule of necessitation to the classical first order axioms and the classical rules.

On the other hand, including the equality symbol in a predicate modal language brings about enormous difficulties and it is often left out.

Modal predicate logic without a fixed semantics. All the historically proposed semantics have problems and, as we mentioned before, equality is a big problem when defining predicate modal semantics. The main reason is that terms can be interpreted either as objects (a fixed individual for all possible worlds) or concepts (possible different individuals for different worlds). In the first case problems appear when the objects do not persist when accessing to a new world. In the second case the usual Tarski semantics is no longer applicable. Hughes and Cresswell imposed the nested domain’s condition as the minimal acceptable prize to be paid in the objectual option. A more complete study of the development of predicate modal logic and the related problems can be found in [4].

The history of predicate modal logic tells us that no satisfactory system can be found. But, it also tells us that, eliminating up the identity issue, the most acceptable and successful choice for a general predicate modal logic is Hughes and Cresswell truth-value gaps system. In this context the modal formulas whose interpretation involves objects that don‘t exist in the domain of the given world lack classical truth-value true or false. They have truth-value gaps. In what follows we call ML to that predicate modal logic.

The two problems of this system (ML) are the impossibility of defining identity and the existence of so many formulas outside the bounds of semantics (the formulas which have no truth-value assigned). Hughes & Cresswell explained well the problems with identity (in “Identity and Description” in [2]) and it was clear that no satisfactory solution could be found. But, with regard to the other problem, there is still an avenue that they did not try: to avoid the semantic deficiency of the ‘undefined formulas’ or truth-value gaps by accepting that the absence of truth-value should be a truth-value in itself (a third non-classical one). Thus, why not investigate this partial nature of Hughes & Cresswell’s predicate modal logic [2]?

ML deals with two kinds of objects: individuals and worlds, and then we have two different universes, a universe of individuals and a universe of possible worlds. In what follows we start off with this particular presentation of predicate modal logic (ML).

Variables are interpreted as individuals, and if a variable x is assigned to the individual h′ in the domain A_{m} of individuals of the world m′ but not in the domain A_{m} of the world m, we can’t associate a truth value T (true) or F (false) to a formula φ(x) in the world m. Thus φ(x) has a truth-value gap in this world. Implicitly, we have three different truth-values, T, F and gap. For the time being, ML is not using the gap as a third truth value in a proper sense, but we will transform ML into a partial logic in a explicit way.

VARIABLES .........................x.......

H ↓

...

A_{m}

\begin{matrix}•h′ \\ A_{m′} \end{matrix}

...

UNIVERSE OF INDIVIDUALS

Q ↑

..., m , ......., m′, ....

POSSIBLE WORLDS

φ(x) \underrightarrow{interpretation} I(φ)(h′)

Note that a variable assignment H is a universal (global) concept in ML, that is, it does not depend on the worlds. Hughes and Cresswell also investigated the possibility of taking assignments as local concepts, but they ended up in predicate S5 (with a unique universe of individuals). A variable x is assigned to an individual of the universe A, and then, whether H(x) belongs to a particular world’s universe of individuals A_{m′} ( m′ a world) or not, depends only on the assignment of domains, Q. It is similar to the classical first order assignment concept. We will define the modal structures A and interpretations I = ⟨A, H⟩ based on Hughes & Cresswell’s truth-value gaps’ semantics [2].

Definition: A = ⟨A, W,R,Q, {f^{A}}_{f∈OP ER.SY M}⟩ , where W ≠ ∅ is the set of worlds, R ⊆ W ×W is the accessibility relation between worlds, Q: W ⟶ 𝔓A is a function assigning a domain of individuals to each world, and f^{A} is the interpretation of the symbol f in A (for function symbols, f^{A} : A^{k} → A , for predicate symbols, r^{A} ⊆ A^{k} × W ).

We define I_{m} as ⟨A, H, m⟩ and we also define (I_{m})_{x}^{a} as ⟨A, H_{x}^{a}, m⟩ where H_{x}^{a} = (H − ⟨x, H(x)⟩) ∪ {⟨x, a⟩} with m ∈ W.

Getting to know the qualities of ML. We need to know the specific properties and qualities of ML. By using the available literature on ML we have elaborated a questionnaire that will allow us to classify the different components of ML.

Some general questions that can be useful in the understanding of any prelogic are the following:

(a) How many kinds of objects does ML have?

(b) How many truth values?

(c) Is there any kind of quantification? If so, is it classical?

(d) Are the semantics concepts defined?

(e) Is there a concept of identity?

(f) Are there semantical restrictions?

(g) How much ‘classicality’ do we have or want in ML?

The answers of ML, as presented in Hughes & Cresswell to the questionnaire above are:

(a) ML has two kinds of objects; i.e. individuals and worlds.

(b) ML has T and F as the linguistic truth-values and ‘gaps of truth−value’ (null) as an extralinguistic truth-value, i.e. while T and F are semantic values, the gaps are not properly considered as such.

(c) There is a classical quantification for individuals, that is, a universal quantified formula ∀xφ is true when the formula φ is true for all possible values of the quantified variable x and it is false when the formula φ is false for at least one value. There occurs, however, a quantification over worlds at the metalanguage level when interpreting modal formulas such as □φ.

(d) Validity is defined but logical consequence is not.

(e) It doesn’t include identity.

(f) There is the semantical restriction of nested domains.

(g) Language and deductive rules must be as fully classical as possible.

3 The Logic PHL for ML.

In order to build the suitable Partial and Heterogeneous Logic for ML (namely, PHL), which we will use as the underlying logic (i.e. as mirror), we need to make clear what the corresponding partial and heterogeneous components of ML are. The construction will proceed on the following seven steps.

After presenting these seven steps for ML, in the next section, we will see that they can suggest the equivalent seven steps to build the suitable PHL in a general case, for any prelogic XL.

Step 1. Defining the set of genera and of truth-values. We define the set of genera GEN (dealing with the different kinds of objects: individuals and worlds) and the set of truth-values TV.

The set of genera is GEN={1,2}, 1 for individuals and 2 for worlds.

As we pointed out above, gap can be a new third value. The truth-values set is TV = {T, F, N} , where T and F are values truth and false of the classical two-valued logic and N is value null corresponding to the truth-value gaps.

We build PHL as a fruitful tool to construct a counterpart of ML; i.e. its image in the PHL mirror. This image is the PHL-theory PHLM, which will be used at the end of the process to build PML as an improved modal logic. PML is placed at this side of the mirror, it is a predicate modal logic and incorporates partiality in a explicit way.

Step 2. Finding a complete set of connectives. As we have a third truth-value, we will need to extend the system of primitives connectives (the classical negation and disjunction for example) to a functional complete system of connectives for the three valued system.

It is known that the suitable extension of negation and disjunction connectives for the truth-value gaps semantics of predicate modal logic are Bočvar‘s (see [1]). They preserve the classical connectives and they generate null from null. We refer to them as ¬_{B} and ∨_{B}, respectively:

\begin{matrix}α & ¬_{B}α \\ T F N & F T N \end{matrix} (α ∨_{B} β) / (α\β T F N)

T F N  T T N T F N N N N

But they are not a functionally complete set of connectives, that is, we can not express any other three-value connective as a composition of ¬_{B} and ∨_{B}. What we want is a set of connectives containing the Bočvar connectives ¬_{B}, ∨_{B} being functionally complete for Bočvar‘s system. This issue is solved in [4]

Definition: C is a functionally complete set of connectives for TV iff for any n-ary function F :TV^{n} →TV (n ≥ 0) there is G :TV^{n} →TV (n ≥ 0) such that G is obtained by composition of connectives of C , and F (x̄) = G(x̄) for all x̄ ∈ TV^{n} .

The solution is to consider C = {¬_{B}, ∨_{B}, V, ξ}

\begin{matrix}α & V α & ξα \\ \begin{matrix}T \\ F \\ N \end{matrix} & \begin{matrix}T \\ F \\ F \end{matrix} & \begin{matrix}T \\ N \\ T \end{matrix} \end{matrix}

Where V is called verification and ξ is called defalsification.

What is proved in [4] is Theorem 1:

Theorem 1. C is a functionally complete set of connectives for TV. (Where C = {¬_{B}, ∨_{B}, V, ξ})

We say that the connectives in C are significant in the sense that they have some semantic relevance or distinctive character; meaning that they show up at the semantic or syntactical theorems of the logic.

Step 3. Defining the language. We build the terms and formulas of PHL for ML by using the primitive connectives ¬_{B}, ∨_{B}, V, ξ, and ∀, ∃ as heterogeneous quantifiers (quantification over variables of different kinds), as we usually do in heterogeneous logic.

Step 4. Defining the interpretation of quantifiers. There are two possibilities for the PHL quantification.

(a) ∀ as an infinite Bočvar conjunction and ∃ as an infinite Bočvar disjunction (if we follow the usual construction in predicate logic). We will call them Bočvar quantifiers [B]

I(∀x_{i}φ) = \{ \begin{matrix}T ⇔ \{a ∈ A_{i} / I_{x_{i}}^{a}(φ) = T \} = A_{i} \\ F ⇔ \{ \begin{matrix}\{a ∈ A_{i} / I_{x_{i}}^{a}(φ) = N\} = ∅ and \\ \{a ∈ A_{i}/ I_{x_{i}}^{a}(φ) = F \} ≠ ∅ \end{matrix} \\ N ⇔ \{a ∈ A_{i} / I_{x_{i}}^{a}(φ) = N\} ≠ ∅ \end{matrix}

and I(∃x_{i}φ) = I(¬∀x_{i}¬φ). where I is an interpretation, I_{x_{i}}^{a} = ⟨A, H_{x_{i}}^{a}⟩, H_{x_{i}}^{a} = (H−⟨x_{i}, H(x_{i})⟩)∪{⟨x_{i}, a⟩}, a and x_{i} are of the same genera, i ∈ {1, 2} .

(b) ∀ and ∃ as classical quantifiers. They are the ones Hughes & Cresswell [2] defined when x_{i} is assigned to an individual. Remember that we also have the genera corresponding to worlds.

I(∀x_{i}φ) = \{ \begin{matrix}T ⇔ \{a ∈ A_{i} / I_{x_{i}}^{a}(φ) = T \} = A_{i} \\ F ⇔ \{a ∈ A_{i} / I_{x_{i}}^{a}(φ) = F \} ≠ ∅ \\ N ⇔ \{ \begin{matrix}\{a ∈ A_{i} / I_{x_{i}}^{a}(φ) = N\} ≠ ∅ and \\ \{a ∈ A_{i} / I_{x_{i}}^{a}(φ) = F \} = ∅ \end{matrix} \end{matrix}

I(∃x_{i}φ) = I(¬∀x_{i}¬φ)

As in PHLM we want to model ML, we have chosen option (b). There are other reasons for doing it, mainly the difficulty to extend the classical predicate calculus to a calculus with a quantification of the (a) kind.

Step 5. Defining semantics: interpretation, validity and logical consequence. The assignments of variables are heterogeneous, i.e., they assign an element of the universe of genus 1 or 2 to a variable of genus 1 or 2, respectively. An interpretation is a pair I = ⟨A, H⟩ where H is a heterogeneous assignment of variables and A is a heterogeneous structure.

A = ⟨A_{1}, A_{2}, {f^{A}}_{f∈OP ER.SY M}⟩, where A_{1} and A_{2} are the universes of genus 1 or 2, respectively, and {V^{A}, ξ^{A}} ⊆ {f^{A}}_{f∈OP ER.SY M} .

1. I(x_{i}) = H(x_{i})

2. I(fϵ_{1}...ϵ_{m}) = f^{A}(I(ϵ_{1}), ..., I(ϵ_{m}))

3. I(¬φ) = ¬^{A}(I(φ))

4. I(φ ∨ ψ) = ∨^{A}(I(φ), I(ψ))

5. I(V φ) = V^{A}(I(φ))

6. I(ξφ) = ξ^{A}(I(φ))

7. I(∀x_{i}φ) = \{ \begin{matrix}T ⇔ \{a ∈ A_{i} / I_{x_{i}}^{a}(φ) = T \} = A_{i} \\ F ⇔ \{a ∈ A_{i} / I_{x_{i}}^{a}(φ) = F \} ≠ ∅ \\ N ⇔ \{ \begin{matrix}\{a ∈ A_{i} / I_{x_{i}}^{a}(φ) = N\} ≠ ∅ and \\ \{a ∈ A_{i} / I_{x_{i}}^{a}(φ) = F \} = ∅ \end{matrix} \end{matrix}

where I_{x_{i}}^{a} = ⟨A, H_{x_{i}}^{a}⟩ and H_{x_{i}}^{a} = (H − ⟨x_{i}, H(x_{i})⟩) ∪ {⟨x_{i}, a_{i}⟩}, a and x_{i} are of genera i.

Now we need the validity and logical consequence concepts for defining the core of the semantics of PHL for ML.

As we have three truth-values and thus false is different from not true we will have more than one possibility for validity. We also have more than one possibility for logical consequence, because we have more than one kind of validity. Validity: We have two possibilities.

(a) strong. I is a model of φ ( I ⊧_{s} φ ) iff I(φ) = T (φ is true in I).

(b) weak. I is a model of φ ( I ⊧_{w} φ ) iff I(φ) ≠ F (φ is not false in I). We also have strong and weak satisfiability: for any set Γ of formulas, I ⊧_{s} Γ

iff I(γ) = T for all γ ∈ Γ and, I ⊧_{w} Γ iff I(γ) ≠ F for all γ ∈ Γ.

Logical consequence: we have four possible consequences (ss, sw, ws, ww).

(a) strong-strong. Γ ⊧_{ss} φ iff for every model I , if I ⊧_{s} Γ then I ⊧_{s} φ.

(b) weak-weak. Γ ⊧_{ww} φ iff for every model I , if I ⊧_{w} Γ then I ⊧_{w} φ.

(c) strong-weak. Γ ⊧_{sw} φ iff for every model I , if I ⊧_{s} Γ then I ⊧_{w} φ.

(d) weak-strong. Γ ⊧_{ws} φ iff for every model I , if I ⊧_{w} Γ then I ⊧_{s} φ.

The semantics of ML was not fixed and therefore we have to check the different possibilities to choose the best option, so, we prove some theorems of comparison between different validities and different logical consequences of PHL:

Theorem 2:.

Γ ⊧_{sw} φ iff Γ ∪ {¬φ} is NOT s-satisfiable.

Γ ⊧_{ws} φ iff Γ ∪ {¬φ} is NOT w-satisfiable.
Γ ⊧_{ss} φ iff Γ ∪ {ξ(¬φ)} is NOT s-satisfiable.
Γ ⊧_{ww} φ iff Γ ∪ {V (¬φ)} is NOT w-satisfiable.

Theorem 3:.

(1) Γ ⊧_{ws} φ ⟹ \{ \begin{matrix}Γ ⊧_{ss} φ \\ Γ ⊧_{ww} φ \end{matrix} \} ⟹ Γ ⊧_{sw} φ .

(But Γ ⊧_{ss} φ and Γ ⊧_{ww} φ are not comparable).

(2) Γ ⊧_{ws} φ ⟹ V Γ ⊧_{ws} ξφ ⟺ \begin{matrix}Γ ⊧_{ss} φ \\ ⇓ \end{matrix} ; \{ \begin{matrix}Γ ⊧_{ss} ξφ \\ V Γ ⊧_{ww} φ \end{matrix} \} ; \begin{matrix}⇑ \\ Γ ⊧_{ww} φ \end{matrix} ⟺ Γ ⊧_{sw} φ.

The logical consequence finally chosen for PHL will be the one giving us the equivalence with the best syntactical deduction for PHL. In theorem 4 bellow we will see how each one of the four logical concepts of consequence corresponds to some well known syntactical rules of inference. These important rules are Modus Ponens (MP), Generalization Rule (GEN), Deduction Rule (DED) and Cut Rule (CUT).

Theorem 4.

⊧_{ss} verifies mp, cut, gen.

⊧_{sw} verifies mp, ded, gen.

⊧_{ww} verifies ded, cut, gen.

⊧_{ws} verifies cut.

Now that we have these results, we can provide an accurate discussion about the four logical consequences. Thus, ⊧_{sw} is the only one having a good condition of satisfiability and verifying Modus Ponens, GEN and the Deduction rule, it is also the weakest one. The only objection is that it does not verify the Cut rule, and so there is no hope of having a Hilbert-style complete calculus for ⊧_{sw}. But it is known that in this case a Gentzen-style calculus is possible (see[4] for a complete calculus for PHL).

For all these reasons our choice for PHL semantics must be the strong-weak logical consequence (⊧_{sw}) and the strong validity (s-satisfiability). Note that from now on we will write ⊧ instead of ⊧_{sw} and ⊧ instead of ⊧_{s}.

Step 6. Checking semantic theorems. Once validity and logical consequence are fixed, we can adjust and check the semantic properties of PHL: compactness, enumerability and Löwenheim-Skolem theorems, etc.

These properties can be proved either directly, or as corollaries of the completeness theorem. When we plan to have a complete calculus, these properties are easier proved in the next step.

PHL for ML has the semantical properties of compactness and Löwenheim-Skolem. In our case we prove them after the completeness of PHL.

Step 7. Finding a complete calculus. To complete PHL for ML a further construction is required. We can try to find a calculus for PHL to make it a sound and complete logic; this is always a difficult thing but it is worth trying. Although it is not fundamental for our partial and heterogeneous tools, it will surely make PHL a more desirable logic. In [4] a complete and sound sequent calculus for PHL for ML and ⊧_{sw} is presented. The common corollaries of completeness are also proved.

4 Building PHL for any prelogic XL.

Taking the process to build PHL for ML as modelwe can define the corresponding seven steps to build PHL for XL.

Step 1. Defining the set of genera and truth-values. We define the set of genera GEN (dealing with the different kinds of objects) and the set of truth-values TV (truth, false and some new partial values ).

We build the mirror PHL as a useful tool to construct a counterpart of XL, so the image of XL in the mirror (the theory PHLX, ) has to be semantically equivalent to PXL (the improved XL, to be built at the end of the whole process).

Step 2. Finding a complete set of connectives. We need to fix a functionally complete set of connectives for the set TV. We also desire that the connectives in C are significant in the sense that they have some semantical relevance or distinctive character. We have two possibilities: either to look for it in the logic stock or to construct them ourselves. We know that the set is the suitable one if we obtain the following result:

GOAL-1 Theorem I.

For any n-ary function F :TV^{n} →TV (n ≥ 0) there is G :TV^{n} →TV (n ≥ 0) such that G is obtained by composition of connectives of C , and F (x̄) = G(x̄) for all x̄ ∈TV^{n}. (i.e. C is a complete set of connectives for TV.)

Step 3. Defining the language. The alphabet of PHL includes: the partial connectives, different sorts of variables for every genera, quantifiers (if XL is a quantified logic) and function and relation symbols. Terms and formulas are defined as they usually are in heterogeneous logic.

Step 4. Defining the interpretation of quantifiers. If XL were a quantified logic, we would need PHL quantifiers. As in partial logic we have nonclassical connectives, we have a variety of options. Following the case of ML we can choose the PHL quantification among the following possibilities.

(a) ∀ as an infinite partial conjunction and ∃ as an infinite partial disjunction.

(b) ∀ and ∃ as classical quantifiers: ∀xφ is true iff for every a ∈ A, I_{x}^{a}(φ) is true and ∀xφ is false iff there is a ∈ A such that I_{x}^{a}(φ) is false, independently of the remaining truth-values. Also ∃xφ = ¬∀x¬φ holds.

(c) Other quantifiers, depending of the nature of partiality and other aspects of XL.

Step 5. Defining validity and logical consequence. At this stage we need to define the concepts of validity and logical consequence to define the semantic core of PHL.

As we have more than two classical truth values and thus false is different from not true we will have more than one possibility for validity:

(a) I is a model of φ iff φ is true in I.

(b) I is a model of φ iff φ is not false in I.

(c) Others (depending on the remaining truth-values).

We also have more than one possibility for logical consequence, because we have more than one kind of validity.

If the semantics of XL were fixed enough, we would take those definitions from XL. But if the semantics of XL were not fixed, we would need to check the different possibilities to choose the best for PHL. Then, the goal is the following:

GOAL-2

(a) To find the theorems of comparison for the variety of validity and logical consequence concepts of PHL.

(b) We also have to study the degree of compatibility between these concepts and some desirable deductive rules for PHL.

Step 6. Checking semantic theorems. We can now look for the semantical properties of PHL: compactness, enumerability and Löwenheim-Skolem theorems, etc. These properties can be proved either directly or as corollaries of the completeness theorem. If we plan to have a complete calculus, these properties will be proved in the next step.

Step 7. Finding a complete calculus. We can try to find a calculus for PHL to make it a sound and complete logic. Although it is not fundamental for our purpose, it will surely make PHL a more desirable logic.

Since we have the Henkin style of completeness proof in mind, we start by fixing the required theorems of consistency and maximal consistency. They depend on the connectives, quantifiers and other semantic concepts for PHL. We can also aim at having some desirable rules in PHL, as for example some classical rules (Modus Ponens, Deduction, etc.).

5 Translating XL into PHL

In the general case we have constructed already the partial and heterogeneous logic PHL which will serve as the underlying logic. What we need to do now is to obtain a theory, PHLX (Δ, for short) as a counterpart of XL. Δ is a theory in PHL representing XL in a sense to be clarified below.

The general plan is as follows^{3}: the signature of the logic XL is transformed into a partial and heterogeneous signature, the expressions of the logic XL are translated into PHL and the structures of the original logic are converted into partial and heterogeneous structures. And then, we should try to find the T RANS and CONV_{1} functions which will allow us to obtain semantic equivalence theorems.

3This plan coincides basically with the one followed in Chapter VII of Extensions of First Order Logic [5].

Step1. Toward a representation theorem. So we need to find the definitions of:

T RANS : EXP R(XL) → EXP R(P HL)

and

CONV_{1} : ST (XL) → ST (P HL)

(Where EXP R and ST stand for ‘expressions of’ and ‘structures of’ respectively).

Let us call S∗ to the class of converted structures; i.e.

S^{∗} = CONV_{1}(ST (XL))

When defining the direct conversion of structures what we want is to obtain the equivalence between validity in the original structures for XL and validity of the translated formulas in the class S^{∗}.

The goal must be to produce the following theorems:

GOAL-3

Theorem 5. For every A ∈ ST (XL) there is CONV_{1}(A) ∈ ST (P HL) such that for every φ ∈ SENT (XL) , A is a ‘model’ of φ iff CONV_{1}(A) is a model of T RANS(φ).

Using Theorem 5 we easily obtain the desired semantic equivalence; namely, Theorem 6.

Theorem 6. Let S^{∗} ⊆ ST (P HL) . φ ‘is valid in XL’ iff T RANS(φ) is valid in PHL with respect to the structures in the class S^{∗}.

Remember that the semantics in XL might be not fixed, and in fact this is usually the situation. In this case, those goal-theorems must be understood as a tool to improve XL, adding the necessary elements to obtain such theorems. Since the concepts of model and validity in XL required definition (and still had), we use quoted expressions to denote that they should be defined later so that the goal-theorems are fulfilled.

What we want is S^{∗} to be close to

MOD(T RANS(V AL(XL)))

Possibly, we also want every expression ε of XL to define in its own structures “almost” the same object that T RANS(ε) defines in CONV_{1}(A).

And then the important question is if S^{∗} can be axiomatized in PHL. In fact, we look forward to a representation theorem and so we are satisfied with an axiomatizable class containing S^{∗} such that Theorem 7 can be proved.

Theorem 7. There is a recursive Δ , Δ ⊆ SENT (P HL) , with CONV_{1}(ST (XL)) ⊆ MOD(Δ) such that ‘⊧ φ in XL’ iff Δ ⊧ T RANS(φ) in PHL, for every φ in XL.

Once we have a representation theorem, we easily obtain the enumerability theorem for XL provided we have plugged in the missing semantic components.

So we have learned that a calculus for the logic XL is a natural demand, but we have also learned that in PHL we can simulate such a calculus. If available, we can use the PHL theorem prover, and we can certainly use the PHL calculus.

Step 2. Further semantic equivalences. Is the representation theorem our ultimate goal? When the logic XL admits a concept of logical consequence, we can try to prove Theorem 9 ; that is, the equivalence of consequence in the original XL with the logical consequence in PHL, module the theory Δ. From Theorem 9, compactness and Löwenheim-Skolem can be dragged from PHL to XL. To prove Theorem 9 a reverse conversion of structures should be defined; our goal is to prove first the Theorem 8.

If Δ exists we will define the reverse conversion:

CONV_{2} : MOD(Δ) → ST (XL), where MOD(Δ) ⊆ ST (P HL)

Now the goal is to obtain the following theorems:

GOAL-4 Theorem 8: There is a recursive Δ ⊆ SENT (P HL) such that for every B ∈ MOD(Δ), CONV_{2}(B) is ‘a model’ of φ iff B is a model of T RANS(φ). Now, by using theorems 5 and 8, we easily prove theorem 9 bellow. Theorem 9: There is a recursive Δ ⊆ SENT (P HL) with CONV_{1}(ST (XL)) ⊆ MOD(Δ) such that

‘Γ ⊧ φ in XL’ ⇔ T RANS(Γ) ∪ Δ ⊧ T RANS(φ) in PHL. Using Theorem 9 we obtain compactness and Löwenheim-Skolem for free.

6 Translating the prelogic ML into PHL

We have constructed already the partial and heterogeneous logic PHL which will serve as the underlying logic. What we need to do now is to obtain the theory PHLM (Δ, for short) as a counterpart of the prelogic ML.

Step1. Toward a representation theorem. So we need to define T RANS and CONV_{1}:

T RANS : EXP R(ML) → EXP R(P HL for ML)

CONV_{1} : ST (ML) → ST (P HL for ML)

In this case the partial and heterogeneous language of PHL contains two genera and three truth-values, the connectives ¬, ∨, V, ξ , the quantifiers and the operation symbols in ML. In addition, PHL contains two special binary relation symbols: R and Q .

Notation: Let us assume that we have an enumeration of the set of variable of genus 2, V_{2}. T RANS(φ)[u] means that u is the free variable of genus 2 in T RANS(φ), although we simple write T RANS(φ) if the variable u is not relevant. T RANS(φ)[u/v] means that u was the free variable in T RANS(φ) and all the occurrences of u were replaced by the first variable v in the enumeration of V_{2} different from u. In the translation to be defined below we need a new connective, the restricted implication ↪ , which is defined by the following table:

α ↪ β
α\β T F N
\begin{matrix}T \\ F \\ N \end{matrix}  \begin{matrix}T & F & N \\ T & T & T \\ N & N & N \end{matrix}

Definition of the translation of expressions: We define T RANS : EXP R(ML) → EXP R(P HL) inductively:

1. T RANS(rϵ_{1}...ϵ_{n}) = ξ(Quϵ_{1} ∧ ... ∧ Quϵ_{n}) ∧ rϵ_{1}...ϵ_{n}u , where u ∈ V_{2} is the first variable in the enumeration of V_{2} , r is a relation symbol, and Q is one of the added PHL-relation symbol.

2. T RANS(¬φ) = ¬T RANS(φ) and T RANS(α ∨ β) = T RANS(α)[v/u] ∨ T RANS(β)[w/u]

3. T RANS(∀xφ) = ∀x(Qux ↪ T RANS(φ)[u])

4. T RANS(□φ) = ∀v(Ruv ↪ T RANS(φ)[u/v]) , where R is a PHLrelation symbol.

The intuition behind these translations is:

1. Quε is always T or F, because it says whether or not the term ε is in the domain of the world u. When it is F, then Quϵ_{1} ∧ ... ∧ Quϵ_{n} is F , and ξ(Quϵ_{1} ∧ ... ∧ Quϵ_{n}) is N. Thus T RANS(rϵ_{1}...ϵ_{n}) is N, as desired. This guarantees the truth-value gaps.

2. The translation respects booleans.

3. The translation of ∀xφ acts as a restricted quantification over the universe of individuals corresponding to the given world; it only takes into account the value of the formula T RANS(φ)[u] for variables such that Qux.

4. The translation of □φ acts as a restricted quantification over the accessible worlds from u.

Definition of the conversion of structures: We define CONV_{1} : ST (ML) → ST (P HL) as follows: If

A = ⟨W, R, Q, {f^{A}}_{f∈OP ER.SY M}⟩ ∈ ST (ML)

then

CONV_{1}(A) = A^{∗} = ⟨A_{1}, A_{2}, {f^{A∗}}_{f∈OP ER.SY M^{∗}}⟩ ∈ ST (P HL)

(where OP ER.SY M^{∗} − OP ER.SY M = {R, Q})

f^{A∗} = f^{A} if f ∈ OP ER.SY M, and

R^{A∗} =R, Q^{A∗} =Q. A^{∗} consists of the PHL-structure resulting by replacing in A the classical interpretation of the connectives by the partial one.

Let us call S^{∗} to the class of converted structures; i.e. S^{∗} = CONV_{1}(ST (ML)) The conversion of a modal assignment is its extension obtained by adding

the values for the variables of genus 2.

The conversion of an interpretation is the PHL interpretation obtained by the translation of its structure and its assignment. We will only consider the global modal interpretations here, that is, the ones not depending on the world.

Now that we have defined the translation from the prelogic ML into PHL we can obtain the following semantic equivalence theorems^{4}.

Theorem 5. For every A ∈ ST (ML) there is CONV_{1}(A) ∈ ST (P HL) such that for every φ ∈ SENT (ML), A ⊧_{s} φ iff CONV_{1}(A) ⊧_{s} T RANS(φ).

Using Theorem 5 we easily obtain the desired semantic equivalence; namely, Theorem 6.

Theorem 6. Let S^{∗} ⊆ ST (P HL). φ ‘is valid in prelogic ML’ iff T RANS(φ) is valid in PHL with respect to the structures in the class S^{∗}.

Remember that the semantics in ML is no fixed. Since the concepts of model and validity in the improved ML still require definition, we use quoted expressions to denote that they should be defined later so that these goaltheorems are fulfilled. We want S^{∗} to be close to MOD(T RANS(V AL(ML))). In fact, we look forward to a representation theorem and so we are satisfied with an axiomatizable class containing S^{∗} such that Theorem 7 can be proved.

Definition: Δ = {σ_{1}, σ_{2}, σ_{3}, σ_{4}} ∪ {σ_{r} / r ∈ OP ER.SY M} ⊆ SENT (P HL) where: σ_{1} ≡ ∀u∃xQux σ_{2} ≡ ∀u∃vRuv σ_{3} ≡ ∀u∀x((V Qux) ∨ (V ¬Qux)) σ_{4} ≡ ∀u∀v((V Ruv) ∨ (V ¬Ruv)) σ_{r} ≡ ∀((V rϵ_{1}...ϵ_{k}) ∨ (V ¬rϵ_{1}...ϵ_{k})) , for every relation symbol r of a modal

4The proofs of these theorems are in [4].

language L.

The quantifier in σ_{r} means that we quantify over all the variables appearing in ϵ_{1}, ..., ϵ_{k}.

Theorem 7. There is a recursive Δ , Δ ⊆ SENT (P HL) , with CONV_{1}(ST (ML)) ⊆ MOD(Δ) such that

‘φ is valid in XL’ iff Δ ⊧_{sw} T RANS(φ) in PHL, for every φ in XL.

Step 2. Further semantic equivalences. ML admits a concept of logical consequence, an so we can try to prove Theorem 9 ; that is, the equivalence of consequence in the improved ML with the logical consequence in PHL module the theory Δ. From Theorem 9, compactness and Löwenheim-Skolem can be dragged from PHL to ML. To prove Theorem 9 we will prove first Theorem 8 and a reverse conversion of structures should be defined:

Taking Δ as above, the reverse conversion:

CONV_{2} : MOD(Δ) → ST (ML), where MOD(Δ) ⊆ ST (P HL)

can be defined in a trivial way. Now the goal is to obtain the following theorems: Theorem 8: CONV_{2}(B) is ‘a ML-model’ of φ iff B ⊧_{s} T RANS(φ).

Now, by using theorems 5 and 8, we easily prove theorem 9 below.

Theorem 9: ‘φ is logical consequence of Γ in ML’ iff T RANS(Γ) ∪ Δ ⊧_{sw} T RANS(φ) in PHL. Using Theorem 9 we obtain compactness and Löwenheim-Skolem for free.

7 Building the improved PML.

Since PHL has been built and we have defined a translation from ML into PHL, we are ready to define an improved ML, which we call PML.

The construction of PML is reached in two steps corresponding with two different levels of completion. The first one concerns the definition of the semantics for PML. The best semantics for PML is the one allowing the semantic equivalence theorems between PML and PHLM (Δ).

In the second step we define a sound and complete calculus for PML. This calculus is based on the calculus of PHL and uses the fact that derivability in PML is implied by derivability of the translation in PHL.

Step 1. Defining the partial modal logic PML. We can redefine ML as a partial logic PML providing a semantics in which the above mentioned Theorem 5 to Theorem 9 hold for PML. The function T RANS will be extended to include the formulas with the new partial connectives.

We redefine predicate modal logic ML as a partial logic in such a way that we can obtain the equivalence theorem, extending the function T RANS. We call it the partial modal logic PML, whose definition is:

(1) Language for PML is defined as a language for ML by adding the set {V, ξ} to the alphabet.

(2) Structures for PML are defined as ML-structures by eliminating the restriction of the nested-domains and adding the condition that the accessibility relation is serial.

(3) Semantics of PML. The set of truth-values, assignment of variables and interpretation over a structure are defined as in ML, but replacing the classical interpretation of the connectives by the partial ones and adding the interpretation for the new partial connectives. Denotation of an expression of the language with an interpretation I_{m} in PML is defined as in ML, by adding the following conditions:

(i) \begin{matrix}I_{m}(V φ) = T iff I_{m}(φ) = T \\ I_{m}(V φ) = F iff I_{m}(φ) = F or I_{m}(φ) = N \\ I_{m}(V φ) ≠ N for all φ ∈ F ORM \end{matrix}

(ii) \begin{matrix}I_{m}(ξφ) = T iff I_{m}(φ) = T or I_{m}(φ) = N \\ I_{m}(ξφ) ≠ F for all φ ∈ F ORM \\ I_{m}(ξφ) = N iff I_{m}(φ) = F \end{matrix}

Validity in PML must be the strong one: a modal interpretation I is a (strong) model of a formula φ iff I(φ) = T. In such a situation we write I ⊧ φ

The concept of Logical consequence in PML must be the strong-weak one: φ is (global) consequence for models of Γ iff for all interpretation I, if I ⊧ Γ then I(φ) ≠ F.

Now we can prove the semantical equivalence theorems between PML and PHL.

Theorem 5 (bis). For every A ∈ ST (P ML) there is CONV_{1}(A) ∈ ST (P HL) such that for every φ ∈ SENT (P ML), sentence of PML,

A ⊧ φ iff CONV_{1}(A) ⊧_{s} T RANS(φ).

Theorem 6 (bis). φ is valid in PML iff T RANS(φ) is valid in PHL in the class S^{∗}.

Theorem 7 (bis). ⊧ φ in PML iff Δ ⊧_{sw} T RANS(φ) in PHL, for every φ in PML.

Theorem 8 (bis). for every B ∈ MOD(Δ), CONV_{2}(B) ⊧ φ iff B ⊧_{s} T RANS(φ).

Theorem 9 (bis). Γ ⊧ φ in PML iff T RANS(Γ) ∪ Δ ⊧_{sw} T RANS(φ) in PHL.

Step 2. Defining a calculus. The common calculi for ML extends a predicate calculus by adding the necessitation rule and, occasionally, the Barcan Formula. This calculus is usually given just to generate the set of validities as in Hughes and Cresswell. As we also have defined the concept of consequence, we would like our calculus to be able to derive in the whole set of semantical consequences of a given set of sentences. In this situation we can try to find a complete and sound calculus for PXL in such a way that Theorems 10 and 11 holds.

Theorem 10: If Δ ⊢ T RANS(φ) in PHL then ‘⊢ φ’ in PML.

Theorem 11: If T RANS(Γ) ∪ Δ ⊢ T RANS(φ) in PHL then ‘Γ ⊢ φ’ in PML.

We can define a calculus for PML by adding to the calculus of our underlying logic PHL some modal rules. The calculus will be accepted, provided that Theorem 10 and Theorem 11 hold^{5}.

Finally, we can borrow from PHL soundness, completeness, compactness and Löwenheim-Skolem.

8 Building the logic PXL.

As in previous sections we can now write the generalization to the case to any prelogic XL, with the characteristics expressed above.

The construction of PXL is reached in two steps:

Step 1. Defining the partial logic PXL. We redefine XL as a partial logic, PXL, providing a semantics in which the above mentioned Theorem 5 to Theorem 9 hold for PXL. The function T RANS will be extended to include the formulas with the new partial connectives.

Theorem 5 (bis). For every A ∈ ST (P XL) there is CONV_{1}(A) ∈ ST (P HL) such that for every φ ∈ SENT (P XL), sentence of PXL, A is a ’model’ of φ iff CONV_{1}(A) is a model of T RANS(φ).

Theorem 6 (bis). Let S^{∗} ⊆ ST (P HL). φ is valid in PXL iff T RANS(φ) is valid in PHL with respect to the structures in the class S^{∗}.

Theorem 7 (bis). There is a recursive Δ , Δ ⊆ SENT (P HL), with CONV_{1}(ST (P XL)) ⊆ MOD(Δ) such that

⊧ φ in PXL iff Δ ⊧ T RANS(φ) in PHL, for every φ in PXL.

Theorem 8 (bis). There is a recursive Δ ⊆ SENT (P HL) such that for every B ∈ MOD(Δ), CONV_{2}(B) is a model of φ iff B is a model of T RANS(φ).

Theorem 9 (bis). There is a recursive Δ ⊆ SENT (P HL) with CONV_{1}(ST (P XL)) ⊆ MOD(Δ) such that

Γ ⊧ φ in PXL iff T RANS(Γ) ∪ Δ ⊧ T RANS(φ) in PHL.

5See [4].

Step 2. Defining a calculus. There are two possible cases:

Case (a): XL had a calculus already. Frequently a prelogic is given as a set of formulas produced within a deductive calculus. In that case the translation into PHL can be used to test that calculus. The test is section (a) of Theorem 11. below.

Case (b): XL had no calculus. In this situation we can try to find a complete and sound calculus for PXL in such a way that section (b) of Theorem 11 holds.

In both cases the translation could allow us to borrow soundness and completeness from PHL. The goal now is:

GOAL-5 Theorem 10:

(a) (a) If ’⊢ φ’ in XL then Δ ⊢ T RANS(φ) in PHL.

(b) If Δ ⊢ T RANS(φ) in PHL then ’⊢ φ’ in PXL.

Theorem 11:

(a) If ‘Γ ⊢ φ’ in XL then T RANS(Γ) ∪ Δ ⊢ T RANS(φ) in PHL

(b) If T RANS(Γ) ∪ Δ ⊢ T RANS(φ) in PHL, then ‘Γ ⊢ φ’ in PXL.

We will look for a calculus for PXL satisfying the condition posed by Theorem 11 (b). The idea is to build up a proof of φ from Γ in PXL, given that we have a proof of T RANS(φ) from Δ∪ T RANS(Γ).

As discussed above, there are several choices for the semantical definition of logical consequence and these choices are linked with certain deduction rules. We may use the semantical decisions for PXL and we should add these rules.

9 Concluding Remarks.

We have presented a general method for building new logics using the existent semantics and/or syntactic components of a logic. This procedure is an extension of the method used by ourselves when representing non-classical logics in a flexible setting such as heterogenous logic. There are several important differences from the previous method that we would like to point out:

(1) The underlying logic; i.e. the Partial and Heterogeneous logic has to be modelled in the process using the existent first order heterogeneous logic but adding the partiality to it. As a consequence, we need to find a complete set of connectives and also to design the semantics and syntax of the partial and heterogeneous logic emerging from the connectives and quantifiers. Soundness and completeness results are also a common demand.

(2) Since the logic we depart from could be very limited, the translation of this logic into the partial and heterogeneous logic is not the end of the process. Our aim can’t be the representation of a logic in a better known and studied logic (since there is little to be represented). The emphasis now is placed in modelling a new logic. This new logic is obtained with the help of the partial and heterogeneous logic already developed. In fact, properties of the original logic can now be established clearly and even proved in the deductive calculus of the underlying logic.

The translation of the original logic into the logic acting as a framework will guide the whole process of building a better equipped logic; i.e. with a good defined semantics and/or calculus. It is mainly in this sense that we can consider the partial and heterogeneous logic as a tool for building the new, redesigned logic.

References

[1] S. Haak. Deviant logic. CUP. Cambridge, 1974.

[2] G.E. Hughes and M.J. Cresswell. An introduction to modal logic. Methuen, London, 1968.

[3] G.E. Hughes and M.J. Cresswell. A companion to modal logic. Methuen, London, 1984.

[4] A. Huertas. Modal Logic (of predicates) and (partial and heterogeneous) Non-Classical Logic. PhD thesis, Universidad de Barcelona, 1994.

[5] M. Manzano. Extensions of first order logic. CUP. Cambridge 1996.

[6] J. van Benthem. Modal logic and classical logic. Bibliópolis, Napoli, 1983.