A new semantics for constructible falsity

Anna Patterson

Computer Science Department, Stanford University, Stanford CA 94305, Email annap@cs.stanford.edu

Abstract

Constructive mathematics preserves the symmetry of Boolean logic’s two truth values when it allows a proposition to be undecided: “could be either true or false”. Intuitionistic logic destroys this symmetry by focusing on truth and offering only a nonconstructive “negation as failure”, ∼ p = p ⊃ ⊥. Nelson’s system N[1] of constructible falsity restores symmetry to intuitionistic logic with an involutory strong negation ¬p asserting the actual falsity of p. (cf. Zaslavskiǐ[3] for another symmetrization.) Thomason[2] proposes a Kripke structure interpretation with three truth values for which he shows that N is sound and complete.

We give a Kripke model having only two truth values for which we show that N is sound and complete. Truth is defined on intervals (w_{t}, w_{f}) in the Kripke structure such that w_{f} is accessible from w_{t}. Truth is judged from one end w_{t}, falsity from the other w_{f}. A formula φ holds at an interval if and only if it holds at all non-trivial subintervals. We interpret strong negation as dualizing the Kripke structure with respect to both truth and accessibility. We formalize this as follows. We use a fact from [2] that every φ ∈ N is equivalent to a formula where ¬ only scopes propositional atoms. For formulas of this form, let A = ⟨W, R, V: W × P → 2⟩ be a Kripke model for I, then for any w_{t} ≠ w_{f} ∈ W such that w_{t} R w_{f},

\begin{aligned}p & (w_{t}, w_{f}) ⊧_{A} p & ≡ & V (w_{t}, p) = 1 \\ φ ∧ ψ & (w_{t}, w_{f}) ⊧_{A} φ ∧ ψ & ≡ & (w_{t}, w_{f}) ⊧_{A} φ and (w_{t}, w_{f}) ⊧_{A} ψ \\ φ ∨ ψ & (w_{t}, w_{f}) ⊧_{A} φ ∨ ψ & ≡ & (w_{t}, w_{f}) ⊧_{A} φ or (w_{t}, w_{f}) ⊧_{A} ψ \\ φ ⊃ ψ & (w_{t}, w_{f}) ⊧_{A} φ ⊃ ψ & ≡ & ∀w′, w′′. w_{t} R w′ R w′′ R w_{f} (w′, w′′) ⊧_{A} φ → (w′, w′′) ⊧_{A} ψ \\ ¬p & (w_{t}, w_{f}) ⊧_{A} ¬p & ≡ & V (w_{f}, p) = 0 \end{aligned}

The atoms that Thomason assigns the third value are those propositional atoms which are assigned 0 at w_{t} and 1 at w_{f}.

Our completeness theorem below asserts that any underivable formula is refutable in a canonical model. In fact, the canonical refutation model K for I is the canonical refutation model for N. Any underivable formula in N can be extended to a complete underivable sequent Γ ⇒ Δ that can be syntactically partitioned into Γ_{p}, Γ_{n}, Γ_{o} ⇒ Δ_{p}, Δ_{n}, Δ_{o} where each φ in Γ_{p} ∪ Δ_{p} is a formula that does not contain ¬, and each φ in Γ_{n} ∪ Δ_{n} is a formula of the form ¬ψ where ψ is a formula without ¬. Then Γ_{p} ⇒ Δ_{p} is a complete sequent for I; hence Γ_{p} ⇒ Δ_{p} is a world in K. The contrapositive of Γ_{n} ⇒ Δ_{n}, denoted (Γ_{n} ⇒ Δ_{n})^{∗}, is also a world in K.

Theorem: If N ⊬ φ then φ can be extended to a complete sequent, Γ ⇒ Δ, such that (Γ_{p} ⇒ Δ_{p}, (Γ_{n} ⇒ Δ_{n})^{∗}) |̸=_{K} φ.

[1] David Nelson. Constructible falsity. Journal of Symbolic Logic, 14:14–26, 1949.

[2] R.H. Thomason. A semantical study of constructible falsity. Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, 15:247–257, 1969.

[3] I.D. Zaslavskiǐ. On Predicate and Arithmetic Calculi of Symmetric Constructive Logic. Soviet Math. Doklady, 14:751-754, 1973.