\underline{\underline{\underline{5}}} A persistent notion of truth in dynamic semantics

Abstract. For a certain interpretation of first-order formulas A as binary (input/output) relations [[A]] on a set S of states (specifying state transitions induced by A), a notion |A| ⊆ S of truth for A is investigated, arising from a so-called double (intuitionistic) negation translation of the domain of [[A]] (or of, equivalently, as it turns out, the fixed points of [[A]]). A global, Boolean-valued analysis is presented alongside a local, three-valued non-compositional approximation of it. Complications with existence and identity are exposed, and suitable generic models constructed. The analysis is carried over to a determinization of transitions between “disjunctive” sets of output states.

1. Introduction

The essential idea behind “dynamic semantics” (e.g., [14]) is that the semantic content of a formula (or statement) lies not so much in its truth relative to a state (or context) but in the change in state that it induces (that change being the reason the statement is used). That is, over a given set S of states, a formula A is interpreted as a binary relation [[A]] ⊆ S × S describing transitions between states s and s′

s[[A]]s′ iff on input s, A can output s′ .

By contrast, let us understand the truth value |A| of a formula A to be the subset {s ∈ S : A is true at s} of S, given some definition of

(∗) A is true at s .

The problem addressed by the present work is to define a notion (∗) of truth, given a relational interpretation [[A]] of formulas A.

1.1. Related work. Two obvious candidates for (∗) mentioned in [4] amount essentially to what are called acceptance and acceptability in [19]

(i) A is accepted at s if s[[A]]s (i.e., s ∈ fix([[A]]))

(ii) A is acceptable at s if there is some state s′ for which s[[A]]s′ (i.e.,

s ∈ dom([[A]])). Neither definition mentions any notion of partiality on states, measuring say information content — a feature that is particularly prominent in [19], where a state is formed from a set of worlds. If the partiality of a state s is understood to refer to the possibility of a formula A as well as its negation being (separately) acceptable in s, then adopting (ii) for (∗) yields an incoherent notion of truth. Option (i) would, on the other hand, mean that asserting a truth can have no effect on the initial state, thereby building a certain logical omniscience into states, as well as trivializing the informational significance of truths.

Proceeding more concretely, consider, for example, Dynamic Predicate Logic (DPL, [7]), where a state is a function from a set of variables to the universe of some first-order model. It is easy to see (under definitions reviewed in §2.1 below) that over a first-order model M where the unary relation symbol R has a non-empty denotation R^{M}, and a function f that fails to map the variable x to an element of R^{M},

R(x) is neither accepted nor acceptable at f ,
∃x R(x) is not accepted but is acceptable at f ,

and

(∃x R(x)) & R(x) is not accepted but is acceptable at f .

Hence, if the formula ∃xR(x) ought to be true at f, then stipulating that A is true at s precisely when A is accepted at s is too strong to account for the dynamic effects of quantification. As for identifying truth with acceptability, it is slightly embarrassing to assert that the conjunction of a true formula with an untrue formula is true. It is only slightly embarrassing in view of the somewhat novel “dynamic” interpretation of conjunction as relational composition. Even so, however, when breaking new ground, there is every reason to pause before throwing out hard-won fruits of past labor, among which one might count a Boolean-valued notion of truth.

Bringing into the picture a pre-order ⊑ on the set S of states (comparing information content), a natural intuition is that if s ⊑ s′ then every formula true at s is also true at s′. That is, the truth set |A| of a formula A ought to be persistent, where a set U ⊆ S of states is understood to be persistent if for all s ∈ U, s′ ⊒ s implies s′ ∈ U. As there is no reason to expect that fix([[A]]) or dom([[A]]) should be persistent relative to natural measures ⊑ of information content (a point confirmed in section 4 below), a bit more work needs to be put into the definition of truth. And also, as it turns out, into the relational interpretation [[A]] of formulas A, which will be defined below to be more faithful to [14], extended with witness constructs ϵx: A for explicit quantification ∃x A.

1.2. Summary of present work. Building on the idea that a state s ∈ S is encompassed by a set U ⊆ S of states if

(∀s′ ⊒ s) (∃s′′ ⊒ s′) s′′ ∈ U ,

a formula A is defined to be true at s if s is encompassed by fix([[A]]) — i.e.,

(∀s′ ⊒ s) (∃s′′ ⊒ s′) s′′[[A]]s′′ .

Then the truth set |A| = {s ∈ S : A is true at s} is manifestly persistent, and is, in fact, a persistent negation applied twice. That is, |A| is the image j(fix([[A]])) of fix([[A]]) under the the so-called double negation translation^{1} j that maps subsets U of S into persistent subsets of S according to

j(U) = {s ∈ S : s is encompassed by U} .

A certain interpretation [[A]] of first-order formulas A as binary relations on finite functions from a set Var of variables to the universe |M| of a first-order model M is defined supporting the following facts.

(i) Although acceptance is, as it stands, an inappropriate notion of truth for the dynamic effects introduced to handle anaphora, j makes acceptance acceptable in the sense that

j(fix([[A]])) = j(dom([[A]])) .

(ii) |A| is compositional (relative to the logical connectives), and is moreover

Boolean-valued (e.g., |A&B| = |A| ∧ |B|). (iii) The truth of A at s is determined by the behavior of A at completions

of s, or more precisely, the “generic models” of s

A is true at s iff every generic model of s satisfies A .

(iv) |A| supports truth gaps implicated in presupposition failure.

(v) Under a passage to a richer notion of (“information”) state (compatible with [19]), j is well-behaved.

The relational interpretation [[A]] is essentially the part of [14] that was meant to be reformulated by DPL, plus certain constructs introduced to handle complications with existence and identity. These constructs are reminiscent of Hilbert’s epsilon terms as well as restricted parameters in situation theory.

2. Preliminaries

The linguistic motivation for the present work can be traced back to Discourse Representation Theory (DRT, [14]). Although DRT covers a good deal of ground (see, for example, [13]), only a small part of it need concern us here. That part is henceforth referred to as DRT/DPL, having been analyzed in DPL, modulo certain simplifications that unfortunately constitute significant differences from DRT. Nonetheless, it is instructive to reverse the

s ||−\overline{A} iff not (∃s′ ≥ s) s′ ||−A .
s ||−^{w}A iff s ||−\overline{\overline{A}}
iff (∀s′ ≥ s)(∃s′′ ≥ s′) s′′ ||−A

1“Negation” here refers to Kripke’s semantic interpretation of the intuitionistic negation \overline{A} of a formula A under a forcing relation ||− between states s partially ordered by ≤ and formulas The double negation translation \overline{\overline{A}} of a formula A then yields a so-called weak forcing relation ||−^{w} (e.g., [15])

typically subject to Boolean logic. In the present context, the terms “weak acceptance”

and “weak acceptability” are somewhat inappropriate because neither acceptance nor acceptability is persistent, as pointed out in section 4, and thus neither implies truth.

historical order, and present DPL (in its simplicity) before DRT/DPL. Towards that end, fix a signature L with equality, and a countable set Var of variables.

2.1. Dynamic Predicate Logic. At the heart of DPL is a translation ·^{DP L} of first-order L-formulas with variables from Var into programs from (quantified) dynamic logic (see, for instance, [9]) according to

A^{DP L} = A?  for atomic formulas A
(¬A)^{DP L} = ¬(A^{DP L})
(A&B)^{DP L} = A^{DP L} ; B^{DP L}
(∃x A)^{DP L} = x :=? ; A^{DP L} ,

where the programs p (in the right hand side) are interpreted relative to an L-model M as binary relations ρ(p) on functions (f, g, h, …) from Var to the universe |M| of M as follows

f ρ(A?) g iff f = g and M ⊧ A[f]
f ρ(x :=?) g iff (∀x′ ≠ x) f(x′) = g(x′)
f ρ(p; q) g iff (∃h) f ρ(p) h and h ρ(q) g
f ρ(¬p) g iff f = g and f ∉ dom(ρ(p)) .

The reader familiar with dynamic logic may code ¬p up as the test ([p]⊥)?, where [p] is the universal (box) modality labelled by the program p, and ⊥ is some contradictory formula. As in classical logic, disjunction, implication and universal quantification can be defined in DPL from negation, conjunction and existential quantification

A ∨ B ≡ ¬(¬A & ¬B)
A ⊃ B ≡ ¬(A & ¬B)
∀x A ≡ ¬∃x ¬A ,

where A ≡ B means ρ(A^{DP L}) = ρ(B^{DP L}).

2.2. DRT/DPL. A consequence of the use of total functions as inputs and outputs in dynamic logic is that the value of a variable can be destroyed by a program interpreting quantification. One can argue, however, that there is no compelling reason for such destruction of information, and that, indeed, the use of total functions in dynamic logic obscures the expansive growth of information implicit in the introduction of discourse markers in DRT. Without getting into the details of DRT, let us switch from total functions to finite functions, and call a function from a finite subset of Var to |M| an (M- )substitution. (We will often say “substitution” without mentioning M, with the understanding that M is fixed in the background.) The interpretations ρ(p) are characterized as before (i.e., A? as a test for A, sequential composition p; q as relational composition ρ(p) ∘ ρ(q), and negation ¬p as a test for the complement of the domain of ρ(p)), except that the relation ρ(x :=?) is no longer symmetric:

f ρ(x :=?) g iff dom(g) = dom(f) ∪ {x} and
(∀x′ ∈ dom(f) − {x}) f(x′) = g(x′)

for all substitutions f and g. Now, to protect a pre-existent binding on a variable x ∈ Var, let us define a guarded assignment x := ∗ to behave exactly like x :=? on input substitutions where x is uninitialized, and to do nothing elsewhere. That is, let x := ∗ abbreviate

x = x? + ¬(x = x?) ; x :=? ,

where + is non-deterministic choice, and interpreted as union:

f ρ(p + q) g iff f ρ(p) g or f ρ(q) g

for all substitutions f and g. Observe that ¬¬ reduces + to DPL disjunction

ρ(¬¬(p + q)) = ρ(¬(¬p; ¬q)) ,

or, put in another way, + provides a “dynamic” alternative to DPL disjunction. Note also that because a substitution need not be defined on a variable occurring in a formula A, the program A? + \overline{A}? (or ¬(¬A?; ¬\overline{A}?)), where \overline{A} is interpreted as the complement of A, may fail to return an output. That is, bivalence may break down because of variables undefined at the input state.

The precise relationship between the modification of DPL above and DRT is described in [6]. As detailed there, guarded assignments provide an implicit treatment of existential quantification, in the sense that the fragment of DRT covered by DPL is given by the following translation ·^{•} of quantifier-free firstorder formulas

(R(\overline{t}))^{•} = \overline{x} := ∗ ; R(\overline{t})? for all relation

symbols R including =

(A&B)^{•} = A^{•}; B^{•}
(¬A)^{•} = ¬(A^{•})

where the list \overline{x} = x_{1}, …, x_{n} in the first line for ·^{•} above consists of all variables occurring in \overline{t}, and \overline{x} := ∗ is x_{1} := ∗; …; x_{n} := ∗. An explicit treatment of quantification will be presented in the next section that extends this translation conservatively.

3. An interpretation of formulas as programs

To overcome complications with identity and existence, it is useful to introduce terms that witness existential formulas ∃x A. Such terms can be viewed as “labelled variables” y_{A,x} or as epsilon terms ϵx:A, similar to those of Hilbert mentioned in [12] (except that here such terms will not always be defined, thus blocking the treatment of universal quantification intended by Hilbert). (These terms can also be viewed situation-theoretically as restricted parameters; see [5].) We will use the notation y_{A,x} and ϵx:A interchangably.

3.1. A language. To avoid pesky variable clashes, let us be careful to partition the set Var of variables into two disjoint sets X and Y, where X is a countable set of “unlabelled variables” given at the outset (along with a fixed signature L) and the set Y of fresh “labelled” variables is defined simultaneously with the set L(Var) of formulas as follows.

(i) If R is an n-ary relation symbol of L (including =), and \overline{t} is a list of n L-terms with variables from X ∪ Y, then R(\overline{t}) belongs to L(Var).

(ii) If x ∈ X, and A and B belong to L(Var), then A&B, A ∨ B, ¬A, and

∃x A belong to L(Var). (iii) If x ∈ X and A ∈ L(Var), then the fresh variable y_{A,x} (= epsilon term

ϵx:A) belongs to Y.

Observe that L(Var) is not closed under ⊃ or ∀. The expressions A ⊃ B and ∀xA can, if the reader insists, be understood as abbreviations of ¬(A&¬B) and ¬∃x¬A, respectively.

3.2. A translation. Next, modifying the DRT/DPL translation slightly, define a translation ·^{u} from formulas A ∈ L(Var) into programs by

(1)  (R(\overline{t}))^{u} = \overline{x} := ∗ ; R(\overline{t})?
(A&B)^{u} = A^{u}; B^{u}
(A ∨ B)^{u} = A^{u} + B^{u}
(¬A)^{u} = ¬(A^{u})
(∃x A)^{u} = y_{A,x} := ∗ ; A[y_{A,x}/x]^{u} ;

always(A[y_{A,x}/x]) , (2)

where the list \overline{x} in (1) consists of all variables in X occurring in \overline{t}, the witness variable y_{A,x} in (2) belongs to Y, and the program always(A[y_{A,x}/x]) will be described shortly. Observe that variables in X occuring freely in a formula A are automatically initialized in A^{u} (in accordance with (1)), whereas other variables (in Y) are initialized only when they are bound (according to (2)). That is, the choice between using unlabelled and labelled variables (to represent discourse markers) in a formula depends on how much one wishes to fuss over variable initializations.^{2}

                 If a farmer owns a donkey then he beats it

farmer(x) & own(x, x′) & donkey(x′) ⊃ beat(x, x′)
(∃x)(∃x′)(farmer(x) & own(x, x′) & donkey(x′)) ⊃
beat(ϵx:∃x′A, ϵx′:A′) ,

2For example, the donkey sentence can be translated as (because of effects on initializing unlabelled variables reminiscent of [17]), or (among other possibilities) as

To insure that a labelled variable y_{A,x} is initialized only if it will always witness the formula, a program always(A[y_{A,x}/x]) is appended^{3} to the translation of ∃xA. (For example, if A were v = v ⊃ R(x) — i.e., ¬(v = v&¬R(x)) —, where v ∈ Y, then any object would witness ∃xA at a state f where v ∉ dom(f).) Note that a witness to A can be spoiled only if variables mentioned in A^{u} are given new values. Fortunately, there are only finitely many such variables. This allows us to construct always(A) as

always(A) = ¬ (in(A) ; ¬(A^{u})) ,

where the program in(A) is the non-deterministic choice

∑ In(A)

of the set In(A) of all “legal” initializations that have some bearing on A^{u}. Just what the set In(A) is, we turn to next. The reader is warned that the description of In(A) is annoyingly technical, and is perhaps best skipped on a first reading. (Afterall, once all free variables in A which can be initialized are initialized, the test always(A[y_{A,x}/x]) added to (2) can be ignored.) With this in mind, the definition of In(A) is indented below to mark it from the rest of the text.

For v ∈ Y, let us write W_{v} for the formula that v should witness

W_{v} = C[v/x]  where v is y_{C,x} .

Then, given an A ∈ L(Var), define the sets Y_{A} ⊂ Y and Fmla_{A} ⊂ L(Var) inductively by

if v ∈ Y occurs in A or in some B ∈ Fmla_{A} then v belongs to Y_{A} and W_{v} belongs to Fmla_{A}.

Proposition. For every A ∈ L(Var), A ∉ Fmla_{A} and the sets Fmla_{A} and Y_{A} are finite. Moreover, for every B ∈ Fmla_{A}, Fmla_{B} ⊂ Fmla_{A} and Y_{B} ⊆ Y_{A}.

Proof. That A ∉ Fmla_{A} follows from the inductive construction of Var and L(Var). The inclusions Fmla_{B} ⊂ Fmla_{A} and Y_{B} ⊆ Y_{A} for B ∈ Fmla_{A} are easy consequences of the definitions of Fmla_{(·)} and Y_{(·)}. An application of König’s Lemma to the derivation trees of Fmla_{A} and Y_{A} yields the finiteness of the sets Fmla_{A} and Y_{A}. ⊣

(∃xA) & B ≡ ∃x(A & B)
(∃xA) ⊃ B ≡ ∀x(A ⊃ B)
(∃x A)^{u} = init(A) ; y_{A,x} := ∗ ; A[y_{A,x}/x]^{u}

where A is farmer(x) & own(x, x′) & donkey(x′), A′ is A[(ϵx : ∃x′A)/x], and B ⊃ C is understood as an abbreviation of ¬(B&¬C). Observe that we lose the DPL equivalences because of variable labelling, although ∃x still introduces a variable available for reference outside ∃’s usual scope.

3An alternative might be to initialize all variables in A that can be initialized before choosing a witness for ∃xA (for some suitable program init(A)) but this possibility will not be pursued here.

Next, let X_{A} be

{x ∈ X : x occurs freely in A
or in some B ∈ Fmla_{A}} ,

and finally let In(A) be the (finite) set of programs of the form

x_{1} := ∗ ; x_{2} := ∗ ; ⋯; x_{m} := ∗ ;
v_{1} := ∗ ; v_{2} := ∗ ; ⋯; v_{n} := ∗ ;
(W_{v_{1}})^{u} ; (W_{v_{2}})^{u} ; ⋯; (W_{v_{n}})^{u}

where x_{1}, …, x_{m} is some list of elements from X_{A} (that does not necessarily include every x ∈ X_{A}), and (similarly) v_{1}, …, v_{n} is some list of elements from Y_{A}. (The sequence (W_{v_{1}})^{u} ; (W_{v_{2}})^{u} ; ⋯; (W_{v_{n}})^{u} is appended to verify that the initializations of labelled variables are “legal”.) The astute reader concerned about the inductive character of our definition of ·^{u} may draw from the previous proposition the

Corollary. The binary relation ≻ on L(Var) given by

A ≻ B iff B ∈ Fmla_{A}

is well-founded (and transitive), and for every A ∈ L(Var), the set {B : A ≻ B} is finite.

Having defined the translation ·^{u}, let us isolate the set S of states that will interest us

S = {f : for some A ∈ L(Var), ∅ ρ(A^{u}) f} .

For every A ∈ L(Var), define

[[A]] = ρ(A^{u}) restricted to S .

Notice that for every A ∈ L(Var), the program A^{u} is guarded in that all occurrences of random assignments in it are within guarded assignments.

Proposition 1 (Monotonicity). For every guarded program p, and for all substitutions f and g, if f ρ(p) g then f ⊆ g. In particular, for all A ∈ L(Var), f[[A]]g implies f ⊆ g.

By contrast, under DPL, the output state of [[∃xA]] may destroy a variable binding in the input state.

4. Truth of formulas qua programs

Let ⊑ be the restriction of ⊆ to S. A natural property to require of a definition of “A is true at f” is that truth persist through ⊑-larger states g. Neither acceptance nor acceptability is persistent; indeed

f[[A]]f and f ⊑ g need not imply g ∈ dom([[A]]) ,

since a variable may be assigned a value at g that precludes the acceptability of A. (For example, take A to be ¬x = x.) To secure persistence, let us recall the double negation translation j mentioned in the introduction.

Definition. A formula A of L(Var) is true at a state f ∈ S if f ∈ j(fix([[A]]))

— i.e.,

(∀g ⊒ f) (∃h ⊒ g) h[[A]]h .

Proposition 2 (Persistence). If A is true at f and f ⊑ g then A is true at g.

Proposition 2 is immediate from the transitivity of ⊒. The next lemma may seem rather technical, but will nevertheless prove important, particularly as fix([[A]]) is not necessarily persistent.

Lemma 3 (Eventual stability). Given an A ∈ L(Var) and a g ∈ S, there is a ĝ ⊒ g such that

(∃h ⊒ ĝ) h ∈ dom([[A]]) implies (∀h ⊒ ĝ) h[[A]]h .

Proof. The idea is to choose ĝ such that g[[A′]]ĝ, where A′ is some tautology that translates (under ·^{u}) to a program initializing all variables in A^{u} which can be initialized (given input g). Towards this end, recall the definitions of Fmla_{A}, Y_{A} and X_{A} from §3.2, and choose (by the inductive construction of L(Var) along with Var) an enumeration B_{0}, …, B_{n} of Fmla_{A} such that for all i and j with 0 ≤ i < j ≤ n,

if B_{j} is W_{v} then v does not occur in B_{i}.

Take A′ to be

⋀_{0≤j≤m} x_{j} = x_{j} & ⋀_{0≤i≤n} (B_{i} ∨ ¬B_{i}) ,

where x_{0}, …, x_{m} is an (any) enumeration of the set X_{A} of all variables in X occurring freely in A or in some B ∈ Fmla_{A}.^{4} Let Var_{A} = Y_{A} ∪ X_{A} and F be the set of substitutions in S with domain contained in Var_{A}

F = {f ∈ S : dom(f) ⊆ Var_{A}} .

Observe that for every ĝ such that g[[A′]]ĝ, the restriction of ĝ to Var_{A} is ⊑-maximal among all substitutions in F, yielding the desired property. ⊣

We can now provide three alternatives U to fix([[A]]) satisfying j(U) = j(fix([[A]]).

Theorem 4. Given an A ∈ L(Var) and an f ∈ S, the following are equivalent. (i) A is true at f. (ii) f ∈ j(dom([[A]])). (iii) f ∈ j({h ∈ S : (∀f′ ⊒ h) f′[[A]]f′}). (iv) f ∈ j({h ∈ S : (∀f′ ⊒ h) f′ ∈ dom([[A]])}).

4This proof exploits the ”dynamic” interpretation of disjunction as union, [[A ∨ B]] = [[A]] ∪ [[B]]. If disjunction A ∨ B is instead reduced “statically” to ¬(¬A&¬B), then the formula A′ in the proof above will have to be replaced by one of the 2^{n+1} combinations of negated or unnegated B_{i}’s that is satisfiable (i.e., returns an output).

Proof. Clearly, (i) implies (ii), and (iii) implies (i). To see that (ii) implies (iii), assume (ii) and suppose g ⊒ f. Appealing to Lemma 3, pick a ĝ ⊒ g such that (by (ii)) (∀f′ ⊒ ĝ) f′[[A]]f′, thus validating (iii). Finally, note that (iii) implies (iv), while (iv) implies (ii). ⊣

As dom([[A]]) = dom([[¬¬A]]), Theorem 4 yields

Corollary 5 (Static projection). For every formula A and state f, A is true at f iff for some B such that [[B]] = [[¬¬A]], B is true at f.

As ¬¬p never returns an output state different from the input, Corollary 5 raises the question as to whether or not the truth of a formula at a state f can be predicted from information about the truth of its (proper) parts at f. As the double negation translation j involves the totality of all states, it is hardly surprisingly that the answer, as the next subsection shows, is negative. Nevertheless, this exercise will prove useful warm-up for the global analysis that then follows.

4.1. A local three-valued analysis of truth. The present subsection is concerned with the question of predicting the truth of a formula A at a state f from information about the truth at the same state f of (proper) subformulas of A. Complementing the notion of truth, a notion of falsehood will be considered that builds on certain harmless assumptions, yielding a negation map ∼. Let L be a signature such that a bijective map ˆ· on the relation symbols in L can be defined assigning to every R its “complement” R̂ (also in L) with the same arity, such that ˆ ˆ· is the identity on the relation symbols of L. (A simple doubling of L will suffice.) An L-model M is understood always to satisfy

(†) R^{M} ⊆ |M|^{n} − R̂^{M}

for every n-ary relation symbol R in L, which is easy enough to express in the first-order language of L. Next, let ∼ be the map on L(Var) defined recursively by

∼R(\overline{t}) = R̂(\overline{t})
∼(A&B) = ∼A ∨ ∼B
∼(A ∨ B) = ∼A & ∼B
∼¬A = A
∼(∃x A) = ¬∃x A

(e.g., [16], except that the clause for ∃ is modified, based on an identification of ∀xA with ¬∃x¬A, as L(Var) is not closed under ∀). Because of (†) above,

Lemma 6. If f[[A]]f then not f[[∼A]]f.

We can now assign a truth value |A|_{f} to a formula A ∈ L(Var) at a state f from the 3-element set {t, f, u}. Define

|A|_{f} = t if A is true at f,

A is false at f, |A|_{f} = f, if |∼A| = t,

and

A is undetermined at f, |A|_{f} = u, otherwise. That is, |A|_{f} = u iff

(∃g ⊒ f)(∀h ⊒ g) not h[[A]]h and
(∃g ⊒ f)(∀h ⊒ g) not h[[∼A]]h .

A formula may be neither true nor false at a state not only because a variable may be uninitialized at that state, but also because the inclusion ⊆ in (†) may be proper. Moreover, from the preceding lemma,

Corollary 7 (3-valuedness). A cannot be both true and false at the same state.

Although the truth values t and f persist, u need not. Holding a state f fixed, however, the definitions above yield the following truth tables, where A ⊃ B is taken as an abbreviation of ¬(A&¬B).

A B & ∼ ∨ ⊃
t t t f t t
t f f  t f
t u u  t u
f t f t t t
f f f  f t
f u f  u t
u t u u t t
u f f  u ≠ f
u u ≠ t  ≠ f ≠ f

The truth tables are strong Kleene except on certain entries where one of the subformulas has an undetermined truth value and no truth value can be predicted for the formula as a whole. For instance, if |A|_{f} = |B|_{f} = u, then |A ⊃ B|_{f} can be t, as with

|x = 1 ⊃ x = 1|_{∅} ,

or u, as with

|x = 1 ⊃ x = 0|_{∅} .

Observe that |A ⊃ B|_{f} can never be f, or else ∼(A ⊃ B) would be true at f; i.e., |A &¬B|_{f} = t, which is absurd since |A|_{f} = u.

4.2. A global Boolean-valued analysis. The non-compositionality in §4.1 can be repaired through an analysis of truth that is global in that the relativization of the truth value |A|_{f} to a state f is dropped.^{5} Instead, we define

|A| = {f ∈ S : A is true at f} (= j(fix([[A]]))) ,

with the intuition (if the reader likes) that the truth value u breaks up into many different values lying (properly) between ∅ and S.

5An alternative would be to keep the truth value local, but to set |A|_{f} = {g ∈ S :

f[[A]]g} ∈ Power(S). There is then, however, no real difference with the dynamic interpretation [[A]], the compositionality of which carries over to |A|.

Rather than proceeding directly to |A|, let us try more slowly to relate j(fix([[A]])) to standard constructions in algebraic semantics. Towards this end, define

Ω = {U ⊆ S : (∀f ∈ U)(∀g ⊒ f) g ∈ U}
Ω_{j} = {j(U) : U ⊆ S} ,

the first set Ω consisting of subsets of S persistent with respect to ⊑, and the second set Ω_{j} of j-sets.

Theorem (Folklore).

(a) ⟨Ω, ∩, ∪, →, ∅⟩ is a complete Heyting algebra, where

U → U′ = {f ∈ S : (∀g ⊒ f) if g ∈ U then g ∈ U′}

for U, U′ ∈ Ω, and least upper bounds are given by union, and greatest lower bounds by intersection.

(b) ⟨Ω_{j}, ∩, ⊔, c, S, ∅⟩ is a complete Boolean algebra, where

U ⊔ U′ = j(U ∪ U′)
c(U) = {f ∈ S : (∀g ⊒ f) g ∉ U}

for U and U′ ∈ Ω_{j}, and

∐_{i∈I} U_{i} = j(⋃_{i∈I} U_{i})
∏_{i∈I} U_{i} = j(⋂_{i∈I} U_{i})

for {U_{i} : i ∈ I} ⊆ Ω_{j}. Next, to provide an algebraic semantics for L-sentences relative to a fixed L-model M, it is customary to extend the signature L to a signature L_{M} by throwing into L constants naming elements in |M| (identifying m ∈ |M| with its name). Such a step will not be required here, although L can, if the reader wishes, be assumed to have names for all objects in |M|. In any case, we will interpret not only L-sentences (without free variables), but also arbitrary formulas from L(Var) (possibly with free variables from Var). Or, put another way, the variables in Var will be treated as constants, which, as we will see, will serve as the usual witnesses.

Another point the reader familiar with algebraic semantics might raise is that the double negation translation j is commonly applied to a Heyting algebra — for example, the Heyting algebra Ω at hand. Although neither fix([[A]]) nor dom([[A]]) is necessarily in Ω, Theorem 4 suggests defining a (persistent) forcing relation ||− between f ∈ S and A ∈ L(Var) by either

f ||−A iff (∀g ⊒ f) g ∈ dom([[A]]) ,

or (non-equivalently)

f ||−A iff (∀g ⊒ f) g[[A]]g .

Unfortunately, neither alternative provides (for instance) a decomposition of {f : f ||−A∨B} as the union (the join in the Heyting algebra Ω) of {f : f ||−A} and of {f : f ||−B}. (Consider the case where A is (ϵx: C) = (ϵx: C) and B is ¬A.) Some Heyting algebra other than Ω is called for; but the only natural one the present author has found is the Boolean algebra Ω_{j} of j-sets!

A final point before presenting our Boolean-valued analysis of truth concerns our treatment of quantification. Following our coding of guarded assignments in terms of equality, the range of quantification is restricted to objects m that “exist” in the sense that m = m. Also, note that for every family U ⊆ Ω_{j}, if ⋃ U ∈ Ω_{j} (i.e., ⋃ U = j(⋃ U)), then ⋃ U = ∐ U.

Theorem 8 (Boolean-valued semantics). For all A, B ∈ L(Var),

|A&B| = |A| ∩ |B|
|A ∨ B| = |A| ⊔ |B| (= j(|A| ∪ |B|))
|¬A| = c(|A|)
= j(S − |A|)
|∃x A| = |(ϵx:A) = (ϵx:A)|
= ⋃ {|v = v & A[v/x]| : v ∈ Var}
= ⋃ {|A[m/x]| : m ∈ |M|} if L names all

objects in M.

Proof. Use monotonicity (Proposition 1) and the various characterizations of |A| provided by Theorem 4. For example, to see that f ∈ |A&B| implies f ∈ |B|, fix a g ⊒ f and conclude (as required by Theorem 4(ii)) that there must be some h ⊒ g in dom([[B]]) since f ∈ |A&B|. Assuming that |A&B| = |A| ∩ |B| has been established, then we can appeal to static projection (Corollary 5) to reduce |A∨B| = |A|⊔|B| to |¬A| = c(|A|), since [[¬¬(A∨B)]] = [[¬(¬A&¬B)]]. By definition, |¬A| = j(S − dom([[A]])), and so by eventual stability (Lemma 3), |¬A| = {f ∈ S : (∀g ⊒ f) g ∉ |A|}. Note that eventual stability also yields j(S − dom([[A]])) = j(S − |A|).

Turning finally to quantification, these equations are consequences of the careful bookkeeping and coding that has gone into labelling, as well as our restriction of S to the substitutions accessible from ∅. The point is that witnesses are persistent in the sense that for all f ∈ S,

(ϵx:A) ∈ dom(f) implies f ∈ dom([[∃x A]]) .

Note the restriction in quantification to v = v is required since quantified formulas translate to programs that always initialize the (translations of) variables bound by quantifiers. (Consider, for example, ∃x ¬x = x.) ⊣

Theorem 8 provides some evidence that our notion of truth is natural. A further argument is presented next, consisting of a construction along the partial order ⊑ on S, that will again force us to face the complications with existence and identity above.

4.3. Constructing generic models from states. To understand just what the double negation translation j is, we might ask what constraints on information growth from f are implied by f ∈ j(U)? Call a sequence {f_{α} : α < κ} ⊆ S (for some cardinal κ) a maximal ⊑-chain from f if

(i) f ⊑ f_{0},

(ii) for all α < κ and β < α, f_{β} ⊑ f_{α}, and (iii) there is no g ∈ S such that for all α < κ, f_{α} ⊏ g. Now, it is true enough that if every maximal ⊑-chain from f intersects U, then f ∈ j(U). On the other hand, the converse need not hold: given a maximal ⊑-chain f = f_{0} ⊏ f_{1} ⊏ f_{2} ⊏ ⋯, the maximal chain {f_{2i} : i ∈ ω} does not intersect U = {f_{2i+1} : i ∈ ω}. For a more pleasing fit with information growth, we must consider not only the partial order ⊑ on S, but also the formulas A in L(Var). In particular, we will adapt the theory of generic models described in [15] (going back to [18]).

It will be convenient to define the basic notions from [15] in our setting as follows. A subset U of S is a generic set if

(i) for all f, f′ ∈ U, there is a g ∈ U such that f ⊑ g and f′ ⊑ g, and (ii) for every A ∈ L(Var), there is an f ∈ U such that f ∈ |A| ∪ |¬A| .

Defining the theory T h(U) of U to be

T h(U) = {A ∈ L(Var) : (∃f ∈ U) f ∈ |A|} ,

observe that condition (i) (in the definition of a generic set) is a consistency criterion, while (ii) is a completeness criterion. Next, given a signature L, define an L-free model to be an L-model N, except that equality is construed as a non-logical symbol ≈ that is interpreted by N as some restriction of true equality

≈^{N} = {(n, n) : n ∈ dom(≈^{N})} .

The term “free” here should be construed not in the usual algebraic sense but rather as in “free logic” (e.g. [3]), the intuition being that dom(≈^{N}) consists of the objects that exist. The notion of an L-free model N satisfying an Lsentence A, N ⊧ A, is defined as in the familiar Tarskian manner (with ≈ regarded as a non-logical symbol), except that quantification is restricted to the domain of ≈^{N}

N ⊧ ∀xA iff (∀n ∈ dom(≈^{N})) N ⊧ A[n/x]
N ⊧ ∃xA iff (∃n ∈ dom(≈^{N})) N ⊧ A[n/x] .

Now, treating Var as a set of constants, a generic model for a generic set U is an L(Var)-free model N such that all its objects are named in Var

|N| = {v^{N} : v ∈ Var} ,

and every L(Var)-sentence in T h(U) is satisfied by N. If, moreover, f ∈ U, then N is said to be a generic model for f.

Theorem 9 (Generic Model Theorem). Every f ∈ S has a generic model; i.e., for every f ∈ S, there is a generic model for f.

Proof. The proof is similar to pp. 101 and 102 of [15] except that (i) a generic set is constructed in a different way below (to avoid requiring that L(Var) be countable), (ii) conjunction, rather than disjunction, is taken to be primitive (since ∨ cannot be interpreted as union), and (iii) quantification must be restricted to objects n such that n ≈ n. (Note that j turns DRT/DPL negation into intuitionistic negation.) More precisely, Theorem 9 is an immediate consequence of the following two lemmas (applied in sequence).

Lemma. Every f ∈ S belongs to a generic set. Proof. From an enumeration {A_{α} : α < κ} of L(Var),construct a generic set U = {f_{α} : α < κ} by taking f_{0} to be f, and choosing f_{α} as follows, for 0 < α < κ. Following the notation of the proof of Lemma 3, let Var_{α} be the (finite) set of all variables occuring in some B ∈ Fmla_{A_{α}}. Let g be the substitution

{(v, m) ∈ Var_{α} × |M| : (∃β < α) v ∈ dom(f_{β})
and f_{β}(v) = m}

and pick a ĝ such that g[[A′_{α}]]ĝ, where A′_{α} is the A′ in the proof of Lemma 3, with A replaced by A_{α}. Set f_{α} to ĝ. ⊣

Lemma. Every generic set has a generic model. Proof. Given a generic set U, define a (partial equivalence) relation ≡ on Var by

v ≡ v′ iff v ≈ v′ ∈ T h(U) ,

and form an L(Var)-free model N by taking as its universe |N| the set {v^{≡} : v ∈ Var} of (partial equivalence) classes v^{≡} = {v′ ∈ Var : v ≡ v′} for v ∈ Var. (Note that ∅ ∈ |N|.) Interpret the kary relation symbols R of L (inlcuding ≈) and the l-ary function (including constant) symbols F of L ∪ Var according to

R^{N}(v_{1}^{≡}, …, v_{k}^{≡}) iff R(v_{1}, …, v_{k}) ∈ T h(U)
F^{N}(v_{1}^{≡}, …, v_{l}^{≡}) = y_{x=F (v_{1},... ,v_{l}),x}^{≡} for some
x ∈ X − {v_{1}, …, v_{l}} .

These are legitimate definitions (i.e., independent of the choice of representatives v of v^{≡}), since T h(U) respects the laws of equality restricted to dom(≈^{N}) and the witnessing on variables. Notice that every term τ has a denotation τ^{N}, and that τ^{N} = ∅ precisely if τ ≈ τ ∉ T h(U). Luckily, ∅≉^{N}∅, and we have no way of expressing equality in L(Var) except by its approximation ≈.) The expected equivalence

N ⊧ A iff A ∈ T h(U)

can be established by a routine induction on A, appealing to the consistency criterion (i) of a generic set. ⊣

⊣

Corollary 10. Let A ∈ L(Var) and f ∈ S. A is true at f (i.e., f ∈ |A|) iff A is satisfied by every generic model for f.

Proof. As in pp. 102 and 103 of [15], the forward direction is trivial, while the converse follows from Theorem 9. ⊣

Lastly, let us remark that the underlying L-model M (relative to which [[·]] and S are defined) is an elementary extension of N^{∘}, for every generic model N (based on M), where ·^{∘} is the obvious map from L(Var)-free models to L-models (obtained by throwing out all “non-existent” objects). Conversely, every countable elementary substructure of M can be obtained as such.

5. Discussion

A basic objection that might be raised against the double negation translation j on which our notion of truth rests is that it abstracts away the temporary instability of a formula (as Lemma 3 and ultimately Theorem 8 suggest). How is the doctrine that

the meaning of a formula is the change it induces

served by trivializing that very change? But, ideologies aside, if we refrain from reducing meaning to truth, and instead agree that truth is a “static” abstraction of meaning, then the objection loses much of its force. The question becomes, quite innocently, what does our notion of truth fail to abstract away? One answer is the partiality of L(Var). For although a good deal of effort was put above into developing the Boolean-valued character of the notion of truth proposed, the formally bivalent (i.e. 2-valued) interpretation in §4.3 is achieved only at the cost of a non-logical treatment of equality and a somewhat non-standard interpretation of quantification. Furthermore, as demonstrated in §4.1, one can define translations that have the effect of re-interpreting the logical connectives (for instance, negation^{6}) to support some partiality. Let us conclude by briefly considering these points in relation to presuppositions, and turning to a richer notion of state similar to that in [19] (concerning which an additional sense in which the double negation translation is persistent will be established).

6Observe, however, that even though a negation ∼ different from DRT/DPL negation ¬ is introduced in §4.1, DRT/DPL negation is still useful for ∀ and presumably implication.

5.1. Truth gaps. With regard to truth gaps implicated in presupposition failure, two sources of partiality then remain:

(i) the partiality of the substitutions f, particularly relative to labelled variables (or epsilon terms), some of which cannot be initialized, and

(ii) the possibility of defining negation translations based on extension/anti-

extension pairs that need not be full Boolean complements. Comparing DRT/DPL negation ¬ with the negation translation ∼ employed in §4.1 to define falsehood, note that whereas A ∨ ¬A is always true, A ∨ ∼A may fail to be true even if for every k-ary R ∈ L, R^{M} = |M|^{k} − R̂^{M} (in which case, R^{N} = dom(≈^{N})^{k} − R̂^{N} holds for every generic model N based on M). There remains the possibility of an epsilon term that can never be initialized — for example, ϵx: wife(x,John), where John has no wife (in M). Such truth gaps provide natural opportunities for giving accounts of simple (existential) cases of presupposition failure. Interpreting R̂ to be less than the full complement of the interpretation of R offers further possibilities.

5.2. Information states. The analysis above is predicated on a notion of state that is somewhat impoverished, next to [10]’s set of “sequence-world-pairs”, commonly used in accounts of presuppositions. (This is a non-trivial matter inasmuch as our notion of truth is conditioned by it.) A sequenceworld-pair is simply a substitution f, coupled with the first-order model M that structures the range of f. (It becomes important to keep track of M, when a state is built from different M’s.) For a sufficiently large set M of L-models, let

S = {(f, M) | M ∈ M and f is an M-substitution} .

The richer notion of a state as a subset of S can be obtained from the interpretation [[·]] above, as in the classic construction of deterministic finite automata from non-deterministic ones (e.g. [11]). More precisely, given an A ∈ L(Var), lift the binary relation

[A] = {((f, M), (g, M)) | M ∈ M and f[[A]]_{M}g}

on S to the binary relation D[A] on Pow_{+}(S) (= Pow(S) − {∅}), given by

D[A] = {(U, V) ∈ Pow_{+}(S) × Pow_{+}(S) |
V = {t | (∃s ∈ U)s[A]t}}.

(Let us agree to exclude the empty set from the field of D[A], as that arises from the impossibility of an [A]-transition.) This lifting is feasible because all programs involved above are so-called distributive (i.e., definable at the level of single substitutions). We will attend later to the non-distributive programs might A of [19]. As D internalizes the non-determinism of [[A]] in states (from Pow_{+}(S)), it is natural to lift a pre-order ≤ on S comparing information content to its so-called Smyth pre-order

≤_{D} = {(U, V) ∈ Pow_{+}(S) × Pow_{+}(S) |
(∀t ∈ V) (∃s ∈ U) s ≤ t} .

Next, let us write J for the double negation translation j^{⊑_{D}} defined relative to the Smyth pre-order ⊑_{D} of

{((f, M), (g, M)) | M ∈ M and f ⊑_{M} g} ,

where ⊑_{M} is the partial order ⊑ used to define truth in section 3 for a fixed L-model M. Finally, define an A ∈ L(Var) to be true at a state U ∈ Pow_{+}(S) if U ∈ J(fix(D[A])).

Theorem 11. Given an A ∈ L(Var) and a U ∈ Pow_{+}(S), the following are equivalent.

(i) A is true at U.

(ii) U ∈ J(dom(D[A])). (iii) For every s ∈ U, A is true at {s}. (iv) For every s ∈ U, A is true at s (according to section 4).

Proof. Argue that (i) implies (ii), (ii) implies (iii), (iii) implies (iv), and finally (iv) implies (i). The first implication is immediate. The others hold because every V ∈ Pow_{+}(S) is ⊑_{D}-dominated by some singleton (even though every singleton is also dominated by a non-singleton) and by appealing to Theorem 4. The universal quantifier in J leads to the universal (rather than existential) force in (iii) and (iv). (Observe that the theorem is quite robust under revisions of the interpretation [[A]]_{M}.) ⊣

A final remark (which the present author plans to expand upon elsewhere) concerns [19]’s program construct might, two features of which would appear to be at odds with the analysis above — viz., non-persistence and nondistributivity. Just how useful our persistent notion of truth is in analyzing the non-persistence of might remains to be seen. As for the second feature, in the same way that modality can be treated syntactically (an approach advocated in [1] for propositional attitudes), a distributive analysis of might is possible, so long as updates are added to the underlying first-order model (exactly as sets are treated in generalized Henkin models for higher-order logic). The introduction of abstract objects into first-order models is argued and investigated at length in [2]. In the case of might, the alternative syntactic approach promises to be of interest, given complications with quantification defined at the richer level of Pow_{+}(S)-states (addressed in [8]) — complications that the present author suspects vanish in a distributive setting.

Acknowledgments. Although the present paper was completed in Stuttgart, much of the work was carried out while I was a visiting researcher at ITK, Tilburg, where I profited from discussions with Emiel Krahmer. I also thank David Israel and Fernando Pereira for comments following my talk on this subject at the fourth conference on situation theory and its applications.

References

[1] N. Asher and H. Kamp. Self-reference, attitudes, and paradox. In G. Chierchia, B.H. Partee, and R. Turner, editors, Properties, Types and Meaning, volume 1. Kluwer Academic Publishers, Dordrecht, 1989.

[2] Nicholas Asher. Reference to Abstract Objects in Discourse. Kluwer Academic Publishers, Dordrecht, 1993.

[3] Ermanno Bencivenga. Free logics. In D. Gabbay and F. Guenthner, editors, Handbook of Philosophical Logic, volume 3. Reidel, Dordrecht, 1986.

[4] Johan van Benthem. Logic and the flow of information. In D. Prawitz et al., editor, Proc. 9th International Congress of Logic, Methodology and Philosophy of Science. North-Holland, Amsterdam, 1991.

[5] Robin Cooper. Situation theoretic discourse representation theory. Manuscript, HCRC, Edinburgh, 1992.

[6] Tim Fernando. What is a DRS? In R. Cooper and J. Groenendijk, editors, Integrating Semantic Theories II. Dyana deliverable R2.1.B, 1994. Presented in a Computational Semantics workshop at Tilburg, December 1994.

[7] J. Groenendijk and M. Stokhof. Dynamic predicate logic. Linguistics and Philosophy, 14, 1991.

[8] J. Groenendijk, M. Stokhof, and F. Veltman. This might be it. In J. Seligman and D. Westerståhl, editors, Logic, Language and Computation, volume 1. CSLI Lecture Notes Number 58, Stanford, 1996. Also appears in Dyana deliverable R2.1.B, Integrating Semantic Theories II , (R. Cooper and J. Groenendijk, editors), 1994.

[9] David Harel. Dynamic logic. In D. Gabbay and F. Guenthner, editors, Handbook of Philosophical Logic, volume 2. Reidel, Dordrecht, 1984.

[10] Irene Heim. On the projection problem for presuppositions. In M. Barlow, D.P. Flickinger, and M.T. Westcoat, editors, Proc. West Coast Conference on Formal Linguistics, volume 2. Stanford Linguistics Association, California, 1983.

[11] J.E. Hopcroft and J.D. Ullman. Introduction to Automata Theory, Language and Computation. Addison-Wesley, 1979.

[12] David Israel. The very idea of dynamic semantics. In P. Dekker and M. Stokhof, editors, Proc. Ninth Amsterdam Colloquium. ILLC, University of Amsterdam, 1994.

[13] H. Kamp and U. Reyle. From Discourse to Logic. Kluwer Academic Publishers, Dordrecht, 1993.

[14] Hans Kamp. A theory of truth and semantic representation. In J. Groenendijk, T. Janssen, and M. Stokhof, editors, Formal Methods in the Study of Language. Mathematical Centre Tracts 135, Amsterdam, 1981.

[15] H. Jerome Keisler. Forcing and the omitting types theorem. In M. Morley, editor, Studies in Model Theory. The Mathematical Association of America, 1973.

[16] David Nelson. Constructible falsity. J. Symbolic Logic, 14, 1949.

[17] P. Pagin and D. Westerståhl. Predicate logic with flexibly binding operators and natural language semantics. J. Logic, Language and Information, 2(2), 1993.

[18] H. Rasiowa and R. Sikorski. The Mathematics of Metamathematics. Warsaw, 1963.

[19] Frank Veltman. Defaults in update semantics. In H. Kamp, editor, Conditionals, Defaults and Belief Revision. Edinburgh, Dyana deliverable R2.5.A, 1990.

92 Tim Fernando