Truth-Maker Semantics for Intuitionistic Logic

Abstract

I propose a new semantics for intuitionistic logic, which is a cross between the construction-oriented semantics of Brouwer-Heyting-Kolmogorov and the condition-oriented semantics of Kripke. The new semantics shows how there might be a common semantical underpinning for intuitionistic and classical logic and how intuitionistic logic might thereby be tied to a realist conception of the relationship between language and the world.

Technical Appendix

A (sentential) atom is either one of the sentence letters p₁, p₂, or the falsum constant ⊥. We use α, β, γ, … for atoms and p, q, r, … for sentence letters. Formulas are constructed from the atoms in the usual way by means of the connectives ∨, ∧ and ⊃.

Recall that a relational structure (S, ⊑), for S a set and ⊑ a binary relation on S, is a partial order if ⊑ is a reflexive, transitive and antisymmetric relation on S. A K-frame is a partially order set (S, ⊑) and a K-model is a triple (S, ⊑, φ), where (S, ⊑) is a K-frame and φ (valuation) is a relation between the states of S and the sentence letters, subject to:

• Hereditary Condition $\varphi s\mathrm{p} \& s\sqsubseteq t\Rightarrow \varphi t\mathrm{p}.$

Relative to a K-model (S, ⊑, φ), we define what it is for a formula A to be verified by a state s of S (s |= A):

$$ \begin{array}{*{20}c} {\left. {\mathrm{K}\left( \mathrm{i} \right)\left( \mathrm{a} \right)s} \right|=\mathrm{p}\;\mathrm{if}\;\varphi s\mathrm{p}} \hfill \\ {\quad \quad \left. {\left( \mathrm{b} \right)s} \right|=\bot\;\mathrm{never}} \hfill \\ {\mathrm{K}\left( {\mathrm{ii}} \right)\quad \left. {\;s} \right|=\mathrm{B}\vee \mathrm{C}\;\mathrm{if}\;s\left| {=\mathrm{B}\;\mathrm{or}\;s} \right|=\mathrm{C};} \hfill \\ {\left. {\mathrm{K}\left( {\mathrm{ii}\mathrm{i}} \right)\quad s} \right|=\mathrm{B}\wedge \mathrm{C}\;\mathrm{if}\;s\left| {=\mathrm{B}\;\mathrm{and}\;s} \right|=\mathrm{C};} \hfill \\ {\left. {\mathrm{K}\left( {\mathrm{iv}} \right)s} \right|=\mathrm{B}\supset \mathrm{C}\ \mathrm{i}\mathrm{f}\;t\left| {=\mathrm{C}\;\mathrm{whenever}\;t} \right|=\mathrm{B}\;\mathrm{and}\;s\sqsubseteq t.} \hfill \\ \end{array} $$

The following standard result is proved by induction on the formula A:

• Lemma 1 (Hereditary) For any K-model (S, ⊑, φ) and states s and t of S,

  $$ \left. s \right|=\mathrm{A}\;\mathrm{and}\;s\sqsubseteq t\;\mathrm{implies}\;t\left| {=\mathrm{A}} \right. $$

• Where Δ is a set of formulas, we say s |= Δ (relative to a model) if s |= A for every A in Δ, and we say that the formula C is an (intuitionistic) consequence of the set of formulas Δ - in symbols, Δ |=_I C - if, for any model M = (S, ⊑, φ) and state s in S, s |= C whenever s |= Δ. Let us use Δ ⊢_I C to denote that C is derivable from Δ under some standard system for intuitionist logic. We state without proof:

  Theorem 2 (Soundness and Completeness) $\left. \varDelta \right|{=_{\mathrm{I}}}\mathrm{C}\;\mathrm{iff}\;\varDelta {\vdash_{\mathrm{I}}}\mathrm{C}$

We turn to the corresponding exact semantics. Recall that a partial order (S, ⊑) is said to be complete - or to be a complete semi-lattice - if each subset T of S has a least upper bound. We denote the least upper bound of each subset T of a complete semi-lattice (S, ⊑) by ⨆T (and also use obvious variants of this notation). It is readily shown that each subset T in a complete semi-lattice (S, ⊑) will also have a greatest lower bound (glb), which we denote by ⊓T; for ⊓T may be defined as ⨆{u: u ⊑ t for each t ∈ T}.

Given two states s and t in a complete partial order, their residuation s → t is defined to be$\sqcap \left\{ {u:s\sqcup u\sqsupseteq t} \right\}$ (I called these states conditional connections in the informal exposition above) and the order itself is said to be residuated if it satisfies:

• Residuation Condition s $\sqcup \left( {s\to t} \right)\sqsupseteq t.$

Let us note the following facts about residuation (use of which will often be implicit):

• Lemma 3 For any elements s, t, u of a complete residuated semi-lattice (S, ⊑):

  • (i) $\left( {s\to t} \right)\sqsubseteq t$

  • (ii) $s\sqcup \left( {s\to t} \right)\sqsubseteq s\sqcup t$

  • (iii) $t\sqsubseteq u\Rightarrow \left( {s\to t} \right)\sqsubseteq \left( {s\to u} \right)$

  • (iv) $s\to \left( {s\sqcup t} \right)\sqsubseteq \left( {s\to t} \right).$

• Proof

  • (i) (s → t) is the glb of {u: s ⊔ u ⊒ t} and so, since s ⊔ t ⊒ t, (s → t) ⊑ t.

  • (ii) Since s ⊑ s and since, by (i) above, (s → t) ⊑ t, s ⊔ (s → t) ⊑ s ⊔ t.

  • (iii) s → t is the glb of {v: s ⊔ v ⊒ t} and s → u the glb of {v: s ⊔ v ⊒ u}. But given t ⊑ u, {v: s ⊔ v ⊒ u} ⊇ {v: s ⊔ v ⊒ t}; and so (s → t) ⊑ (s → u).

  • (iv) From (ii), s ⊔ (s → t) ⊑ s ⊔ t; and so, given that s → (s ⊔ t) is the glb of {u: s ⊔ u ⊑ s ⊔ t}, s → (s ⊔ t) ⊑ (s → t).

A E-frame (‘E’ for exact) is a partial order (S, ⊑) which is residuated and complete. An E-model is an ordered triple (S, ⊑, φ), where (S, ⊑) is an E-frame and φ (the valuation) is a relation holding between the members of S and the sentential atoms, subject to:

• Falsum Condition φs⊥ implies φs′p for some state s′ ⊑ s.

There would be no difference in the notions of consequence and validity if we strengthened the condition to:

• Strict Falsum Condition φs⊥ implies φsp.

A state s in a E-model (S, ⊑, φ) is said to be contradictory if φs⊥, to be inconsistent if s ⊒ t for some contradictory state t, and to be consistent otherwise. Two states s and t are said to be compatible if their fusion s ⊔ t is consistent and incompatible otherwise. Note that we do not impose the Hereditary Condition on E-models. However, there would be no difference in the notions of consequence and validity if we insisted upon this condition for the falsum constant ⊥:

• Hereditary Condition forx ⊥ φs⊥ & s ⊑ t ⇒ φt⊥.

We have the following clauses for when a formula A is exactly verified by a state in a E-model (S, ⊑, φ):

$$ \begin{array}{*{20}c} {\left. {\mathrm{E}\left( \mathrm{i} \right)s} \right\|-\alpha\;\mathrm{if}\;\varphi s\alpha; } \hfill \\ {\left. {\mathrm{E}\left( {\mathrm{ii}} \right)s} \right\|-\mathrm{B}\vee \mathrm{C}\;\mathrm{if}\;s\left| {\left| {-\mathrm{B}\;\mathrm{or}\;s} \right|} \right|-\mathrm{C};} \hfill \\ {\left. {\mathrm{E}\left( {\mathrm{ii}\mathrm{i}} \right)s} \right\|-\mathrm{B}\wedge \mathrm{C}\;\mathrm{if}\;\mathrm{for}\;\mathrm{some}\;{s_1}\;\mathrm{a}\mathrm{nd}\;{s_2},{s_1}\left| {\left| {-\mathrm{B},{s_2}} \right|} \right|-\mathrm{C}\;\mathrm{a}\mathrm{nd}\;s={s_1}\sqcup {s_2};} \hfill \\ {\left. {\mathrm{E}\left( {\mathrm{iv}} \right)s} \right\|-\mathrm{B}\supset \mathrm{C}\;\mathrm{if}\;\mathrm{there}\;\mathrm{is}\;\mathrm{a}\;\mathrm{function}\;\mathrm{taking}\;\mathrm{each}\;t\left| {\left| {-\mathrm{B}\;\mathrm{into}\;\mathrm{a}\;{u_t}} \right|} \right|-\mathrm{C}\;\mathrm{for}\;\mathrm{which}} \hfill \\ {\quad \quad \quad \quad \quad \quad \quad s=\sqcup \left\{ {t\to {u_t}:t||-\mathrm{B}} \right\}.} \hfill \\ \end{array} $$

It is illuminating to state the clauses in ‘algebraic’ form. Relative to a E-model (S, ⊑, φ), let us use [A] for {s: s ||- A}. For subsets T and U of S, let T ⊔ U = {t ⊔ u: t ∈ T and u ∈ U} and let T → U = {s: s = ⨆{t → u _t : t ∈ T} for some function u: T → U}. We then have the following identities:

$$ \begin{array}{*{20}c} {\left[ {\mathrm{B}\vee \mathrm{C}} \right]=\left[ \mathrm{B} \right]\cup \left[ \mathrm{C} \right]} \hfill \\ {\left[ {\mathrm{B}\wedge \mathrm{C}} \right]=\left[ \mathrm{B} \right]\sqcup \left[ \mathrm{C} \right]} \hfill \\ {\left[ {\mathrm{B}\supset \mathrm{C}} \right]=\left[ \mathrm{B} \right]\to \left[ \mathrm{C} \right].} \hfill \\ \end{array} $$

Note that the clause for [A] in each case provides us with a description of how the members of [A] are constituted from the verifiers for the component formulas and in such a way as to make clear that they are indeed verifiers for A.

We say s ||> A (s inexactly verifies A) if s′ ||- A for some s′ ⊑ s. It can then be shown that inconsistent states inexactly verify every formula:

• Lemma 4 (Quodlibet) For any formula A and inconsistent state s in a E-model, s ||> A.

• Proof By induction on the complexity of the formula A.

• A = α Given that s is inconsistent, there is a contradictory state s′ ⊑ s. But s′ ||- ⊥ by definition; so s′′ ||- α for some s′′ ⊑ s′ by the Falsum Condition; and so s ||> α.

• A = B ∨ C By IH, s ||> B. But then s′ ||- B for some s′⊑ s; so s′ ||- B ∨ C; and so s ||> B ∨ C.

• $\mathrm{A}=\mathrm{B}\wedge \mathrm{C}$ By IH, s ||> B and s ||> C. So s′ ||- B and s′′ ||- C for some s′, s′′ ⊑ s. But then s′⊔ s′′ ||- B ∧ C; and, since s′⊔ s′′ ⊑ s, s ||> B ∧ C.

• $\mathrm{A}=\mathrm{B}\supset \mathrm{C}$ By IH, s ||> C. So s′ ||- C for some s′⊑ s. For each t ||- B, we set ${u_t}=s\prime$. So $t\to {u_t}=t\to s\prime \sqsubseteq s\prime \sqsubseteq s$. But ⨆(t → u _t ) ||- B ⊃ C; and since ⨆(t → u _t ) ⊑ s, s ||> B ⊃ C.

Let us now show how to go from an E-model to a K-model and from a K-model to an E-model. This will enable us to transfer completeness for the one kind of modeling to the other.

Given an E-model $M=\left( {S,\sqsubseteq,\;\varphi } \right)$, we define a corresponding K-model ${M_{\mathrm{K}}}=\left( {{S_{\mathrm{K}}},{\sqsubseteq_{\mathrm{K}}},\;{\varphi_{\mathrm{K}}}} \right)$ by:

• (i) S _K = {s ∈ S: s is consistent};

• (ii) ⊑_K = ⊑↾S _K;

• (iii) φ_K = {(s, p): s ∈ S _K, p is a sentence letter, and, for some s′ ⊑ s, φs′p}.

It should be evident that M _K, as so defined, is indeed a K-model (it follows, in particular, from clause (iii) for φ_K that the Hereditary Condition will be satisfied). If we did not cut away the inconsistent points, then M _K would be a modified Kripke model in the sense of Veldman [10]. Thus the E-models provide a natural underpinning for the models that he uses in his completeness proof.

We now show that inexact verification in an E-model behaves in the same way as forcing in the corresponding K-model:

• Theorem 5 (E/K) Let $M=\left( {S,\sqsubseteq,\ \varphi } \right)$ be an E-model and ${M_{\mathrm{K}}}=\left( {{S_{\mathrm{K}}},{\sqsubseteq_{\mathrm{K}}},\ {\varphi_{\mathrm{K}}}} \right)$ the corresponding K-model. Then for any state s ∈ S _K and any formula A,

  $$ \left. s \right\|>\left. {\mathrm{A}\;\mathrm{in}\;M\;\mathrm{iff}\;s} \right|=\mathrm{A}\;\mathrm{in}\;{M_{\mathrm{K}}}. $$

• Proof By induction on A.

• A = ⊥ Never s ||> ⊥ in M since s is consistent; and never s |= ⊥ in M _K by clause K(i)(b).

• A = p s ||> p in M iff s′ ||- p in M for some s′ ⊑ s

• iff φs′p for some s′ ⊑ s

• iff φ_K sp

• iff s |= p in M _K.

• A = B ∨ C Suppose s ||> B ∨ C (in M). Then s′ ||- B ∨ C for some s′ ⊑ s. So s′ ||- B or s′ ||- C. By IH, s′ |= B or s′ |= C (in M _K). But then s′ |= B ∨ C; and so, by the Hereditary Lemma, s |= B ∨ C.

• Now suppose s |= B ∨ C (in M _K). Then s |= B or s |= C. By IH, s ||> B or s ||> C; and so for some s′ ⊑ s, s′ ||- B or s′ ||- C. In either case, s′ ||- B ∨ C; and so s ||> B ∨ C.

• A =B ∧ C Suppose s ||> B ∧ C. Then s′ ||- B ∧ C for some s′⊑ s. So for some $s_1^{\prime }$ and $s_2^{\prime }$, $s_1^{\prime }$ ||- B, $s_2^{\prime }$ ||- C and s′ = $s_1^{\prime }$ ⊔ $s_2^{\prime }$. By IH, $s_1^{\prime }$ |= B and $s_2^{\prime }$ |= C; by the Hereditary Lemma, s |= B and s |= C; and so s |= B ∧ C.

• Now suppose s |= B ∧ C. Then s |= B and s |= C. By IH, s ||> B and s ||> C; and so for some s ₁, s ₂ ⊑ s, s ₁ ||- B and s ₂ ||- C. But then s′ = s ₁ ⊔ s ₂ ||- B ∧ C; and, since s′ ⊑ s, s ||> B ∧ C. A = B ⊃ C Suppose s ||> B ⊃ C. Then s′ ||- B ⊃ C for some s′ ⊑ s of the form ⨆(t → u _t ) (where the t ||- B and the u _t ||- C). Consider now any consistent t ⊒ s for which t |= B (with a view to establishing t |= C). By IH, t ||> B; and so, for some t′ ⊑ t, t′ ||- B. Now t′ → u _t′ ⊑ s′ ⊑ s ⊑ t and also t′ ⊑ t. So u _t′ ⊑ (t′ → u _t′) ⊔ t′ ⊑ s′ ⊔ t′ ⊑ t. Since u _t′ ||- C, t ||> C and so, by IH, t |= C.

• Now suppose s |= B ⊃ C and consider a t ||- B (with a view to establishing s ⊔ t ||> C). We distinguish two cases:

  • (a) t is compatible with s. Then t, s ⊔ t ∈ S _K. Given t ∈ S _K, t |= B by IH; given s ⊔ t ∈ S _K, s ⊔ t |= B by the Hereditary Condition; given s |= B ⊃ C, s ⊔ t |= C; and so s ⊔ t ||> C by IH.

  • (b) t is incompatible with s. Then s ⊔ t is inconsistent; and so, by Quodlibet, s ⊔ t ||> C.

• Thus, in either case, s ⊔ t ||> C and so u ||- C for some u ⊑ s ⊔ t. For each t for which t ||- B, we set u _t = u. Then t → u _t = t → u ⊑ t → (s ⊔ t) ⊑ t → s ⊑ s. So s′ = ⨆(t → u _t ) ⊑ s and, given that s′ ||- B ⊃ C, s ||> B ⊃ C.

We turn to the transformation in the opposite direction. In this case, not every K-model can be straightforwardly transformed into an E-model and we need to impose some further conditions on the K-model.

Let (S, ⊑) be a partially ordered set. A subset T of S is then said to be downward-closed if t ∈ T and s ⊑ t implies s ∈ T. Let [t] = {u ⊑ t: u ∈ S}. A subset T of S is said to be principal if it is of the form [t] for some element t of S and is said to be non-principal otherwise. Two elements s and t of S are said to be comparable if either s ⊑ t or t ⊑ s and to be incomparable otherwise. An element s of (S, ⊑) is said to be root if s ⊑ t for each element t of S and (S, ⊑) itself is said to be rooted if it has a root. By the antisymmetry of ⊑, a root, if it exists, is unique and, clearly, in the case of a complete partial order, the root is identical to the null element. Finally, the partial order (S, ⊑) is said to be tree-like if:

• (a) no infinite ascending chain of elements s ₁ ⊏ s ₂ ⊏ … of S has an upper bound;

• (b) no two incomparable elements of S have an upper bound; and

• (c) there is a root.

The following result on tree-like structures will later be useful:

• Lemma 6 Given that the partial order (S, ⊑) is tree-like, no principal downward-closed subset of S contains a non-empty non-principal downward-closed subset of S.

• Proof Suppose that T is a non-empty non-principal downward-closed subset of S. Let t ₁ be a member of T. Then T ≠ [ t ₁] since otherwise T would be principal; and so, since T is downward-closed, [t ₁] ⊂ T. Let t ₂ be a member of T - [t ₁]. Then not t ₂ ⊑ t ₁ since otherwise t ₂ ∈ [t ₁]. If t ₁ and t ₂ were incomparable then we would be done since no principal downward-closed subset [t] could contain T without t being an upper bound for t ₁ and t ₂, contrary to (b) above.

  So t ₁ and t ₂ are comparable and hence t ₁ ⊏ t ₂. Continuing in this way, we may construct a chain t ₁ ⊏ t ₂ ⊏ t ₃ ⊏ … of members of T. If the chain is finite, then it is of the form t ₁ ⊏ t ₂ ⊏ t ₃ ⊏ … t _n with T the downward closure of {t ₁, t ₂, t ₃, …, t _n} and T = [t _n] is principal after all. If the chain t ₁ ⊏ t ₂ ⊏ t ₃ ⊏ … is infinite, then no principal downward closed subset of T can contain {t ₁, t ₂, t ₃, …} on pain of violating condition (a) above.

Given a K-model M = (S, ⊑, φ), we define a corresponding structure M _E = (S _E, ⊑_E, φ_E) by:

• (i) S _E = {T ⊆ S: T is non-empty and downward closed};

• (ii) ⊑_E = ⊆↾S _E

• (iii) φ_E = {([s], p): s ∈ S and φsp} ∪ {(T, α): T is a non-principal downward-closed subset of S _E}.

The transformation of M into M _E does indeed provide us with an E-model:

• Lemma 7 When M = (S, ⊑, φ) is a tree-like K-model, M _E = (S _E, ⊑_E, φ_E) is an E-model.

• Proof (i) Clearly, (S _E, ⊑_E) is a partial order.

  (ii) (S _E, ⊑_E) is complete.

• Pf. Suppose S ₁, S ₂, … are any number of non-empty downward closed subsets of S. Let S′ be s ₀, where s ₀ is the root element, if there are no S ₁, S ₂, …; and let S′ = S ₁ ∪ S ₂ ∪ … otherwise. Then s ₀ ∈ S′ and so S′ is also non-empty; clearly, S′ is downward-closed; and so S′ ∈S _E. Moreover, it is evident that S′ is the lub of S ₁, S ₂, … under the relation ⊑_E of set-theoretic inclusion on S _E.

  (iii) (S _E, ⊑_E ) is residuated.

• Pf. Take two non-empty downward closed subsets T and U of S. Let V = ⋃{[u]: u ∈ U - T} ∪ {s ₀}. Clearly, V ∈ S _E. Also, (T ∪ V) ⊇ U and hence (T ⊔_E V) ⊒_E U. For if s ∈ U then either s ∈ T ⊆ (T ∪ V ) or s ∈ U - T, in which case s ∈ [s] ⊆ V ⊆ (T ∪ V). Moreover, for any V′ ∈ S _E, T ∪ V′ ⊇ U implies V ⊆ V′ and hence (T ⊔_E V′) ⊒_E U implies V ⊑_E V′. For take any u ∈ U - T. Then clearly u ∈ V′, given T ∪ V′ ⊇ U. But then [u] ⊆ V′ given that V′ is downward-closed; and so V ⊆ V′. Thus V = (T →_E U) and satisfies the Residuation Condition.

  (iv) M _E conforms to the Falsum Condition.

• Pf. From the definition of φ_E.

Note that M _E is far from being a typical E-model. As is easily shown, it satisfies the Strict Falsum Condition and the Hereditary Condition; and this means that imposing either or both of these conditions on E-models will not result in the validity of any further formulas. But here, as is often the case, the intended models for our logic will far outstrip those required to establish completeness.

Rather than directly establishing the equivalence between the K-model M and the E-model M _E , we derive it from the corresponding equivalence between the E-model M and the K-model M _K. But first we show that the one transformation is, in a way, the inverse of the other.

Theorem 8 Suppose M = (S, ⊑, φ) is a tree-like K-model. Then the map taking each member s of S into [s] is an isomorphism from M onto (M _E)_K.

Proof Let (M _E)_K = (S _E/K, ⊑_E/K, φ_E/K). Then S _E/K consists of the consistent elements of S _E, i.e. of those elements of S _E that do not contain a contradictory element, i.e. of those elements of S _E that do not contain a non-empty non-principal subset of S. Each such element must itself be a principal subset of S and, by lemma 6, each principal subset of S _E will be such an element. Thus S _E/K = {[s]: s ∈ S}. Also for s, t ∈ S, [s] ⊑_E/K [t] iff [s] ⊆ [t], which holds iff s ⊑ t, given that [s] and [t] are downward-closed. Finally, for s ∈ S, never φ_E/K[s]⊥ and never φs⊥ and, for any sentence letter p, φ_E/K[s]p iff φ_E[s′]p for some [s′] ⊑ [s]. But given that M _E satisfies the Hereditary Condition, φ_E[s′]p for some [s′] ⊑ [s] iff φ_E[s]p; and φ_E/K[s]p iff φsp, as required.

Corollary 9 (K/E) Let M = (S, ⊑, φ) be a tree-like K-model and M _E = (S _E, ⊑_E, φ_E) the corresponding E-model. Then for any s ∈ S:

$$ \left. s \right|=\left. {\mathrm{A}\;\mathrm{in}\;M\;\mathrm{iff}\left[ s \right]} \right\|>\mathrm{A}\;\mathrm{in}\;{M_{\mathrm{E}}}. $$

Proof By the E/K theorem, [s] ||> A in M _E iff s |= A in (M _E)_K for each s ∈ S. By the isomorphism theorem above, s |= A in (M _E)_K iff s |= A in M. But then s |= A in M iff [s] ||> A in M _E, as required.

We turn to consequence. There are two somewhat different ways of defining the notion (and the cognate notion of validity) - one in terms of the preservation of verifiers and the other in terms of the preservation of truth - and there are variants on each approach, depending upon the form of verification or upon how the concept of truth is related to verification. Let us begin with the definitions in terms of verification.

We may say that the formula A is an exact consequence of the formulas A₁, A₂, … - in symbols, A₁, A₂, … |=_e C - if in any E-model M and any states s ₁, s ₂, … of M, s ₁ ⊔ s ₂ ⊔ … ||- C whenever s ₁ ||- A₁, s ₂ ||- A₂, .... The notion of exact consequence is of great interest in its own right. However, our interest is in modeling the more usual notions of consequence and we shall say no more about the exact notion.

Where Δ is a set of formulas, we say s ||> Δ (relative to an E-model) if s ||- A for each A ∈ Δ. Substituting inexact verification for exact verification, we obtain the following three notions of consequence:

• Δ |=_i1 C if in any E-model M and any state s of M, s ||> C whenever s ||- Δ;

• Δ |=_i2 C if in any E-model M and any consistent state s of M, s ||> C whenever s ||> Δ;

• Δ |=_i3 C if in any E-model M and for the null-state s of M, s ||> C whenever s ||- Δ.

These definitions differ in which states are taken to be relevant to establishing a countermodel to the argument from Δ to C, with the first allowing any state whatever, consistent or inconsistent, the second allowing only consistent states, and the third allowing only the null state. (I have given these definitions for the case in which the conclusion is required to be a single formula C, but they can be extended in the usual way to the case in which the conclusion is allowed to be an arbitrary set of formulas Γ, disjunctively interpreted.)

Although these various notions of inexact consequence are apparently of different strength, we may establish the equivalence of each of them to intuitionistic consequence. But first we need a standard result on ‘tree’ models. Suppose M = (S, ⊑, φ) is a K-model with root s ₀. We define the corresponding tree model M _t = (S _t, ⊑_t, φ_t) by:

• (i) S _t is the set of sequences s ₀ s ₁ s ₂ … s _n, n ≥0, for which s _i ⊑ s _i+1 for all i = 0, 1, …, n - 1;

• (ii) ⊑_t = {(s, t) ∈ S _t × S _t: s is identical to or an initial segment of t};

• (iii) φ_t = {(s, p): s ∈ S _t, p is a sentence letter and φsp, for s terminating in s}.

It should be clear that M _t is a tree model with root the unit sequence s ₀.

We now have a standard inductive proof of:

• Theorem 10 Suppose that M |= (S, ⊑, φ) is a rooted K-model and let M _t = (S _t, ⊑_t, φ_t) be the corresponding tree model. Then for any s ∈ S, any s ∈ S _t terminating in s, and any formula A:

  $$ \left. s \right|=\left. {\mathrm{A}\;\mathrm{in}\;M\;\mathrm{iff}\;s} \right|=\mathrm{A}\;\mathrm{in}\;{M_{\mathrm{t}}}. $$

From this, we obtain:

• Corollary 11 If not Δ |=_I C then, in some tree-like K-model with root s ₀, s ₀ |= Δ while not s ₀ |= C.

• Proof Given not Δ |=_I C, it is readily shown that in some K-model M with root s ₀, s ₀ |= Δ while not s ₀ |= C. From the previous theorem, it follows that in the corresponding tree model M _t, s ₀ |= Δ while not s ₀ |= C; and it is readily verified that M _t is tree-like with root s ₀.

We now have:

• Theorem 12 For any set of formulas Δ and formula C, the following are equivalent:

  • (i) $\left. \varDelta \right|{=_{\mathrm{i}1}}\mathrm{C}$

  • (ii) $\left. \varDelta \right|{=_{\mathrm{i}2}}\mathrm{C}$

  • (iii) $\left. \varDelta \right|{=_{\mathrm{i}3}}\mathrm{C}$

  • (iv) $\left. \varDelta \right|{=_{\mathrm{I}}}\mathrm{C}.$

• Proof It is evident from the definitions of |=_i1, |=_i2 and |=_i3 that (i) implies (ii) and (ii) implies (iii); and so it suffices to establish that (iii) implies (iv) and (iv) implies (i).

  (iii) implies (iv). Suppose not Δ |=_I C. By the previous theorem, in some tree-like K-model M = (S, ⊑, φ) with root s ₀, s ₀ |= Δ while not s ₀ |= C. We consider the corresponding E-model M _E. By corollary 9, [s ₀] ||> Δ in M _E while not [s ₀] ||> C. But [s ₀] is the null state of M _E; and so not Δ |=_i3 C.

  (iv) implies (i). Suppose not Δ |=_i1 C. Then for some E-model M and state s of M, s ||> Δ but not s ||> C. Consider the corresponding K-model M _K. Since not s ||> C, s is consistent and hence a state of M _K. By the E/K theorem, s |= Δ in M _K but not s |= C and hence not Δ |=_I C.

We turn to the truth-theoretic notion of consequence. A statement may be taken to be true if it has an actual verifier. We make this idea precise within the E-semantics (and we might also do so within the K-semantics) by singling out a subset R of S to represent the states that actually obtain. Thus we may say that M = (S, R, ⊑, φ) is a distinguished E-model - or, more simply, a D-model - if (S, ⊑, φ) is an E-model and R (for ‘reality’) is subject to the following four conditions:

• Non-Vacuity R is non-empty

• Consistency Each s ∈ R is consistent

• Part s′ ∈ R if s ∈ R and s′ ⊑ s

• Finite Fusion s ⊔ t ∈ R if s, t ∈ R.

We might think of the elements of R as the facts. Non-vacuity then says that there is a fact, Consistency that each fact is consistent, Part that parts of facts are facts, and Fusion that the fusion of any two facts is a fact. Non-vacuity, Part and Finite Fusion correspond, of course, to the defining conditions for an ideal.

These conditions are all very reasonable. But there are two other, somewhat more controversial conditions, which we may wish to adopt:

• Closure ⨆R′ ∈ R for each R′ ⊆ R

• Completeness For any state s ∈ S either s is a member of R or is incompatible with a member of R.

Closure tells us that the facts are closed under arbitrary fusions (not just finite fusions) and Completeness tells us that the facts are, in a certain sense, complete.

Clearly, Closure implies Fusion; and it also implies Non-Vacuity (upon letting R′ = ∅). Given Part, Closure is equivalent to:

• Totality ⨆R ∈ R.

We might call r _∞ = ⨆R (total) reality. Thus Closure tells us that total reality is itself a fact.

Given Totality and Part, R will be identical to {r: r ⊑ r _∞}. This means that, in the definition of a D-model, we may replace the set R with a single element r _∞ and talk of the parts of r _∞ instead of the members of R. Under this alternative definition, Non-Vacuity, Part, Fusion and Closure become redundant. Consistency becomes:

• (*) r _∞ is consistent

  and Completeness becomes:

• (**) any s ∈ S is either a part of r _∞ or incompatible with r _∞.

We might call an element w of S a (classical) world if it conforms to (*) and (**), i.e. if it is consistent and if any state s is a part of w or incompatible with w. Thus (*) and (**) amount to the assumption that reality is a classical world.

We may say that a D-model M = (S, R, ⊑, φ) is closed if R satisfies Closure, complete if R satisfies Completeness, and classical if R satisfies both Closure and Completeness.

Even if a given D-model is complete, let us say, or classical, it is not clear that there is any guarantee that it will be complete or classical, no matter how things might have turned out. So let us say that an E-model M = (S, ⊑, φ) is thoroughly complete (closed, classical) if for any consistent state s of S there is a complete (resp. closed, classical) D-model (S, R, ⊑, φ) in which s ∈ R. It is trivial that any E-model is thoroughly closed since we may let R = {r ∈ S: r ⊑ s}.

Perhaps somewhat surprisingly:

• Theorem 13 Any E-model is thoroughly complete.

• Proof Say that a subset R ₀ of S satisfies the finite consistency condition (fcc) if any finite fusion of members of R ₀ is consistent. We may then successively extend R ₀ to a complete subset of S (satisfying the other conditions) by taking each element of S in turn and adding it when, and only when, fcc is preserved. (The construction is exactly analogous to the construction of an ultrafilter from a set of elements in a Boolean algebra with the finite intersection property).

By contrast, in order for an E-model M = (S, ⊑, φ) to be thoroughly classical, each of its consistent states must be part of a classical world; and there is no general guarantee that the required classical worlds will exist.

We turn to the truth-theoretic definition of consequence. Given an E-model M = (S, R, ⊑, φ), say that A is true in M - |= _M A - if r ||- A for some r ⊑ R (A is exactly verified by some fact). Note that as long as R satisfies Part, this condition will be equivalent to saying that A is inexactly verified by some fact. Thus in the present context, there is no need to distinguish between exact and inexact verification.

Given a class X of D-models, say that C is a consequence of Δ relative to X - Δ |=_X C - if C is true in any model of X in which Δ is true. We may now extend our previous result on the ‘robustness’ of the notion of intuitionistic consequence:

• Theorem 14 Δ |=_X C is intuitionistic consequence for X the class of D-models, for X the class of closed D-models, and for X the class of complete D-models.

• Proof Clearly, if Δ |=_I C then Δ |=_X C for any X. Also Δ |=_X C implies Δ |=_X′ C for X′ ⊆ X; and so it suffices to show that Δ |=_X C implies Δ |=_I C for X the class of closed D-models and X the class of complete D-models.

  So suppose that not Δ |=_I C. Then from theorem 12, it follows that in some E-model M = (S, ⊑, φ) and for some element s of M, s ||> Δ while not s ||> C. But we may now set R = {r ∈ S: r ⊑ s} to obtain a closed model (S, R, ⊑, φ) in which Δ is true (since s ||> Δ) but C is not true (since not r ||- C for each r ⊑ s).

  It is a little more work to show that not Δ |=_X C for X the class of complete models. We appeal to the particular tree model M _t |= (S _t, ⊑_t, φ_t) defined above. We know that for some such model with root s ₀, s ₀ |= Δ while not s ₀ |= C and so, in the corresponding E-model (M _t)_E, s ₀ ||> Δ while not s ₀ ||> C. We now set R = {s: s is a sequence of s ₀’s}. Adding R to (M _t)_E, it is then readily verified that the resulting model is a complete D-model.

With X the class of classical models, things are quite different. First, we have that instances of Excluded Middle are verified at a classical world:

• Lemma 15 Let w be a classical world of the E-model M = (S, ⊑, φ). Then w ||> (p ∨ ¬p) for each sentence letter p.

• Proof Suppose not w ||> (p ∨ ¬p). Then not w ||> p and not w ||> ¬p and so, for some consistent v ⊒ w, v ||> p. But then v is compatible with w and yet not a part of w.

We now have:

• Theorem 16 Δ |=_X C is classical consequence for X the class of classical D-models.

• Proof From the previous lemma and the fact that C will be a classical consequence of Δ if it is an intuitionistic consequence of Δ plus all instances (p ∨ ¬p) of Excluded Middle.

Still, there is a way in which a classical conception of reality is still compatible with the endorsement of intuitionistic logic. Say that a formula A is degenerately valid relative to the class X of E-models if A is inexactly verified (and hence exactly verified) by the null state of each model of X. Then:

• Theorem 17 A is intuitionistically valid iff it is degenerately valid relative to the class of all thoroughly classical E-models.

• Proof The direction from left to right is straightforward. Now suppose A is not intuitionistically valid. By the finite model property for intuitionistic sentential logic, it follows that in some finite K-model M = (S, ⊑, φ) with root s ₀, not s ₀ |= A; and it may be shown that M can also be assumed to be tree-like (modify the construction of M _t by requiring the elements in the sequences s ₀ s ₁ s ₂ … s _n to be distinct). In the corresponding E-model (M _t)_E, [s ₀] is the null state and not [s ₀] ||> A; and given the finitude of S, it is readily shown that (M _t)_E is thoroughly classical.

I wish now to establish some results which bear on the question of how the exact verification of a statement might be seen to arise from the intrinsic content of the verifying state. To this end, we might identify the content of a state with the set of formulas either exactly verified or inexactly verified by the state. We want it to be apparent from the logical form of these formulas that they are prime, i.e. that they entail a disjunction only if they entail a disjunct, and are thereby suitable as the content of a state. We also want it to be apparent from the logical form of these formulas, along with initial information about the verifying states of the atoms, that the state will verify the formulas that it does.

Let us deal first with primal issues. A formula is said to be non-disjunctive if it is formed without the help of ∨, i.e. from ∧, ⊃ and ⊥, and a set of formulas Δ is said to be non-disjunctive if its members are non-disjunctive.

Lemma 18 Any non-disjunctive formula A is provably equivalent (within intuitionistic logic) to a conjunction of formulas of the form D ⊃ α for some non-disjunctive formula D and atom α that appears in A.

Proof By induction on A.

A = α A is then equivalent to (α ⊃ α) ⊃ α.

A = (B ∧ C) By IH on B and C.

A = (B ⊃ C) By IH, C is equivalent to a conjunction of formulas of the form D ⊃ α for D non-disjunctive and α an atom appearing in C; and so B ⊃ C is equivalent to a conjunction of formulas of the form B ⊃ (D ⊃ α), with α appearing in A and B non-disjunctive. But B ⊃ (D ⊃ α) is equivalent to ((B ∧ D) ⊃ α).

The set of formulas Δ is said to be prime if, for any formulas A and B, Δ |- B or Δ |- C (within intuitionistic logic) whenever Δ |- B ∨ C.

Lemma 19 Any non-disjunctive set of formulas Δ is prime.

Proof By the previous lemma, we can assume that each formula of Δ is of the form D ⊃ α for α an atom. Suppose that not Δ |- B and not Δ |- C (to show not Δ |- B ∨ C). By the completeness theorem for intuitionistic logic, there are K-models M ₁ = (S ₁, ⊑₁, φ₁) and M ₂ = (S ₂, ⊑₂, φ₂) with respective root s ₁ and s ₂, with Δ true at s ₁ in M ₁ and at s ₂ in M ₂ but with B not true at s ₁ in M ₁ and C not true at s ₂ in M ₂. Clearly, we may suppose that S ₁ and S ₂ are disjoint. Choose a element s _o in neither S ₁ nor S ₂ and define the model M = (S, ⊑, φ) by:

• (i) $S=\left\{ {{s_{\mathrm{o}}}} \right\}\cup {S_1}\cup {S_2}$

• (ii) ${\sqsubseteq_1}=\left\{ {\left( {{s_{\mathrm{o}}},s} \right):s\in S} \right\}\cup {\sqsubseteq_1}\cup {\sqsubseteq_2}$

• (iii) $\varphi =\left\{ {\left( {{s_{\mathrm{o}}},\mathrm{p}} \right):{\varphi_1}{s_1}\mathrm{p}\;\mathrm{and}\;{\varphi_2}{s_2}\mathrm{p}} \right\}\cup {\varphi_1}\cup {\varphi_2}.$

It is easy to show with the help of the Hereditary Condition that B ∨ C is not true at s _o in M. Suppose for reductio that Δ is not true at s _o in M. So some formula D ⊃ α of Δ is not true at s _o in M. It is readily shown that D is true at s _o in M while α is not. By the Hereditary Condition, D is true at s ₁ in M ₁ and at s ₂ in M ₂; and since D ⊃ α is true at s ₁ in M ₁ and at s ₂ in M ₂, it follows that α is true at s ₁ in M ₁ and at s ₂ in M ₂. So, clearly, α is not the falsum constant ⊥ but a sentence letter p and so, by the definition of M, φs _op and p is true at s _o in M after all.

As is well known, this result can also be established on the basis of the normalization theorem.

Let us now deal with the issue of content. To this end, we shall appeal to an extension of intuitionistic logic, which we might call hybrid intuitionistic logic (HH) after the corresponding nomenclature for modal logics with world-constants. The language of HH is obtained from that for intuitionistic logic by adding an arbitrary (finite or infinite) number of state constants s ₁, s ₂, .... We shall think of each state constant s _k as designating a particular state s _k in the sense that s _k is the sole verifier of s _k. Call a formula of HH definite if it is constructed from the state constants s ₁, s ₂, … by means of the connectives ∧ and ⊃. It is by means of the definite formulas that we shall make explicit the content of each state.

The logic of HH is obtained from minimal logic by adding the axiom scheme:

• Definiteness [(D ⊃ (B ∨ C)] ⊃ [(D ⊃ B) ∨ (D ⊃ C)], for any formulas B and C of the extended language and any definite formula D.

and by adding ⊥⊃ p for each sentence letter p (however, we do not add ⊥ ⊃ s for any of the state constants s). Using Lemma 18 above, we can show that it suffices to restrict D to definite formulas of the form (D′ ⊃ s).

We may show that definite formulas are like the state constants in designating a single state. Let us say that M = (S, ⊑, φ) is an E-model for the language of HH if (S, ⊑) is an E-frame and if, in addition, we have:

• Falsum Condition φs⊥ implies φs′p for some s′ ⊑ s; and

• Statehood for each state constant s _k there is a state s _k such that φs s _k iff s = s _k.

Note that the state constants are not subject to the Falsum Condition.

Given an E-model M = (S, ⊑, φ) for HH and a definite formula D, we use (D)*, or d, for the corresponding state of M. Thus:

• (i) $\left( {{{\mathrm{s}}_{\mathrm{k}}}} \right)*={s_{\mathrm{k}}};$

• (ii) $\left( {{{\mathrm{D}}_1}\wedge {{\mathrm{D}}_2}} \right)*=\left( {{{\mathrm{D}}_1}} \right)*\sqcup \left( {{{\mathrm{D}}_2}} \right)*;$

• (iii) $\left( {{{\mathrm{D}}_1}\supset {{\mathrm{D}}_2}} \right)*=\left( {{{\mathrm{D}}_1}} \right)*\to \left( {{{\mathrm{D}}_2}} \right)*.$

Thus s _k in the formula D is, in effect, replaced with s _k, ∧ with ⊔, and ⊃ with →.

Lemma 20 (Uniqueness) Given any E-model M = (S, ⊑, φ) for HH and definite formula D, d = (D)* is the sole exact verifier of D.

Proof By a straightforward induction on D.

E-models for HH verify Definiteness and hence HH is sound with respect to the class of such models:

• Lemma 21 [(D ⊃ (B ∨ C)] ⊃ [(D ⊃ B) ∨ (D ⊃ C)], for D a definite formula, is true at the root of any E-model M = (S, ⊑, φ).

• Proof By the Uniqueness Lemma, d is the sole verifier of D in M. Thus any verifier of (D ⊃ (B ∨ C) is of the form d → s, where s is a verifier of B or of C. In either case, it is clear that d → s is also a verifier of (D ⊃ B) ∨ (D ⊃ C). So we may associate each d → s with itself and the sum of all the (d → s)→ (d → s) will be the null state.

We use the state constants to indicate which states verify a given atom (p_k or ⊥). Accordingly, we take a state assignment to be a set of formulas of the form α ≡ (A₁ ∨ A₂ ∨ … ∨ A_n), n ≥ 1, one for each atom α, where A₁, A₂ , … , A_n are definite formulas. Our main interest will be in when the formulas A₁, A₂ , … , A_n are themselves state constants. A state assignment can be extended from atoms to all formulas.

Lemma 22 (Assignment) Let Δ be a state assignment. Then for each formula A of HH, there are definite formulas A₁, A₂, … , A_n, n ≥ 1, such that A ≡ (A₁ ∨ A₂ ∨ … ∨ A_n) is derivable from Δ within HH.

Proof By induction on A. The result is obvious when A is an atom. There are three other cases:

• A = (B ∧ C) By IH, B ≡ (B₁ ∨ B₂ ∨ … ∨ B_k) and C ≡ (C₁ ∨ C₂ ∨ … ∨ C_l) are derivable (with k, l ≥1 and definite formulas on the right). But then (B ∧ C) ≡ (B₁ ∨ B₂ ∨ … ∨ B_k) ∧ (C₁ ∨ C₂ ∨ … ∨ C_l) is derivable and we may use the Distributive Law to put the right hand side in the required form.

• A = (B ∨ C) Straightforward.

• A = (B ⊃ C) By IH, B ≡ (B₁ ∨ B₂ ∨ … ∨ B_k) is derivable (with k ≥ 1 and definite formulas on the right). But (B₁ ∨ B₂ ∨ … ∨ B_k) ⊃ C is provably equivalent within minimal logic to (B₁ ⊃ C) ∧ (B₂ ⊃ C) ∧ … ∧ (B_k ⊃ C) and so, by applying Distributivity, it suffices to consider the case in which k = 1. By IH again, C ≡ (C₁ ∨ C₂ ∨ … ∨ C_l) is derivable (with l ≥ 1 and definite formulas on the right). Using the Definiteness axiom, it follows that [B₁ ⊃ (C₁ ∨ C₂ ∨ … ∨ C_l)] ≡ [(B₁ ⊃ C₁) ∨ (B₂ ⊃ C₂) ∨ … ∨ (B_l ⊃ C_l)] is derivable, where the right hand side is of the required form.

Suppose that M = (S, ⊑, φ) is a regular E-model in which S is a finite set {s ₁, s ₂, …, s _n} containing at least one contradictory state. We extend M to an E-model M ⁺ = (S, ⊑, φ⁺) for HH by adding n new state constants s ₁, s ₂, …, s _n to the original language and letting φ⁺ = φ ∪{(s _k, s _k): k = 1, 2, …, n}. Let Δ _M be the state assignment that, for each atom α of the original language, contains the formula α ≡ (s _k1 ∨ s _k2 ∨ … ∨ s _km ), m ≥ 1, where s _k1, s _k2, …, s _km are the states that exactly verify α in M.

Putting together the previous results, we are in a position to show how each formula verified by a state in M ⁺ can be seen to be verified by the state on the basis of its content:

• Theorem 23 (Constitution) Let M ⁺ be an E-model for HH as previously defined. Suppose that the formula A from the unextended language is inexactly verified by a state s of M. Then A is derivable within HH from Δ _M ∪ {D: D is a definite formula inexactly verified by s in M ⁺}.

• Proof Suppose A is inexactly verified by s in M. By the Assignment Lemma, there are definite formulas D₁, D₂, … , D_m, m ≥ 1, such that A ≡ (D₁ ∨ D₂ ∨ … ∨ D_m) is derivable from Δ _M within HH. It should be evident that the formulas of Δ _M are true at the root of M ⁺. So by lemma 22, A ≡ (D₁ ∨ D₂ ∨ … ∨ D_m) is also true at the root. Given that A is inexactly verified by s, some D_j is inexactly verified by s. But now from A ≡ (D₁ ∨ D₂ ∨ … ∨ D_m) and D_j we can derive A.

Some comments on this result are in order:

• (1) It is important to the significance (and non-triviality) of the result that the underlying formulas D should be definite, since otherwise there is no guarantee that they are prime and hence can legitimately be taken to correspond to a verifying state.

• (2) The result has only been established for finite E-models. In order to extend it to infinite E-models (which would, in any case, be required in application to intuitionistic predicate logic), we would need to employ infinitary means to construct the underlying definite formulas.

• (3) It is unfortunate that we have had to resort to minimal logic in order to be able to differentiate the different states at which a contradiction may be true. I do not know if there is any reasonable way in which this partial appeal to minimal logic might be avoided.

• (4) It would be nice to be able to establish a version of Constitution Theorem with exact verification in place of exact verification. Thus when A is exactly verified by a state s, it will be required that A is derivable from Δ _M ∪ {D: D is a definite formula exactly verified by s}. There is a difficulty in establishing this result under the present semantics. For we will wish to strengthen the Assignment Lemma and show that A will be exactly equivalent to (A₁ ∨ A₂ ∨ … ∨ A_n) (and thereby have the same exact verifiers) whenever the same is true of the pairs of equivalent formulas under the assignment Δ. But when we examine the proof of the lemma, we see that this requires that (A ∨ A) ⊃ C, for example, should be exactly equivalent to (A ⊃ C) ∧ (A ⊃ C). But suppose that A has the one verifier s and C the two verifiers t and u. Then (s → t) ⊔ (s → u) will be a verifier of (A ⊃ C) ∧ (A ⊃ C) but not (as a rule) of (A ⊃ C). There is a similar difficulty with the Definiteness Axioms.

  We may overcome these difficulties by a modification to the semantics which is independently well-motivated. For we may take the verifiers of a formula to constitute a multi-set. Thus if [s] is the multi-set of verifiers for A, [s, s] will be the multiset of verifiers for (A ∨ A) (s will verify A ‘twice’, from the left and from the right). Similarly, the verifiers of (A ⊃ C) should be taken to encode a function from the multiset of verifiers for A into the multiset of verifiers for C. Thus if s verifies A twice we can associate s twice over with a verifier of C and if t verifies C twice, we can employ it twice in forming verifiers of (A ⊃ C) given a verifier of A.

  The above version of the condition-oriented semantics constitutes a closer approximation to the construction-oriented semantics, since it permits us to ‘select’ a left and right verifier for (A ∨ A), though without distinguishing one as left and the other as right; and perhaps we can think of there being a gradual transition in this way from the one form of the semantics to the other.

We shall not go into details but the above considerations and results can be extended to quantificational intuitionistic logic. To this end, the language should be enriched with an existence predicate E in addition to the quantifiers and an E-model should be equipped with a domain I of possible individuals. The clause for the universal quantifier then takes the form:

• s ||- ∀xA(x) if there is a function taking each individual i ∈ I and each state t ||- E[i] into a u _i,t ||- A[i] for which s = ⨆(t → u _i,t ).

The universal quantification ∀xA(x) is treated as equivalent, in effect, to the conjunction of the Ei ⊃ A(i) for each possible individual i. However, this clause is not altogether satisfactory from a philosophical point of view; and it would be preferable to have a clause that could be stated without appeal to the full range of possible individuals.