「‍」 Lingenic

Partial Logic

(⤓.md ≡ ◇.md); γ ≜ [2026-07-17T135416.643, 2026-10-22T054143.488] ∧ |γ| = 3

Partial Logic

Origin. Kleene's partial recursive functions and three-valued tables (1938, 1952) gave the computational motive: a predicate defined by an unbounded search has no value where the search does not halt. Bas van Fraassen, "Singular terms, truth-value gaps, and free logic" (1966), gave the semantic motive and the supervaluational treatment of empty descriptions. Dana Scott's domain theory supplied the information ordering with ⊥ at the bottom. Blamey's survey "Partial logic" (Handbook of Philosophical Logic, 1986) named and organized the field; Langholm, Partiality, Truth and Persistence (1988), and Muskens (1995) for the type-theoretic version, are the standard developments.

Models. Interpretations that need not decide every atom. A partial valuation assigns a pair of disjoint sets — the extension and the anti-extension — and leaves the remainder undecided, so a sentence may be neither true nor false. Two sources of undecidedness are kept apart: a term may fail to denote, and a formula may fail to receive a value even where its terms denote. The models are ordered by information rather than by truth, with a total interpretation a maximal point, and the connectives are chosen to be monotone in that ordering so that adding information never retracts a verdict.

Formalism.

Partiality sources: Partial functions: f(a) undefined. Empty descriptions: ιx.φ undefined. Presupposition failure. Non-terminating computation.

Denotation: [[t]] ∈ D ∪ {↑}. ↑: undefined. Terms may lack denotation.

Partial valuation: v = (T, F) with T ∩ F = ∅. T: the extension. F: the anti-extension. Neither: the gap. Total iff T ∪ F is everything.

Atomic formulas: P(t₁,...,tₙ) undefined if some tᵢ undefined. Undefinedness propagates. Gap at atomic level.

Logic options: Strong Kleene: gaps propagate. Weak Kleene: gaps dominate. Supervaluations: classical on all completions. Blamey: transvaluation.

Kleene approach: Third value: neither true nor false. Connectives as in strong Kleene. Gaps preserved compositionally.

Supervaluation approach: φ supertrue if true in all completions. φ superfalse if false in all completions. Otherwise gap. Classical validities preserved.

Existence predicate: E!(t): t is defined. E!(t) ↔ t = t (sometimes). Explicit definedness. Quantifier rules restricted: from ∀x φ(x) and E!(t), infer φ(t).

Scott's approach: Information ordering. ⊥ ⊑ true, ⊥ ⊑ false. Monotonicity. Domain theory connection.

Monotonicity and fixed points: v ⊑ v′ implies [[φ]]_v ⊑ [[φ]]_v′ for Kleene connectives. A monotone operator on partial valuations has a least fixed point (Knaster–Tarski). Kripke (1975) for truth; Fitting (1985) for logic programs.

Symbols.

SymbolUnicodeNameMeaning
↑U+2191Upwards arrowUndefined: a term with no denotation
⊥U+22A5Up tackBottom of the information ordering
⊑U+2291Square image of or equal toInformation ordering: less defined than
⊨U+22A8TrueSatisfaction at a partial valuation
ιU+03B9IotaDefinite description operator, ιx.φ
φU+03C6PhiA formula
∅U+2205Empty setT ∩ F = ∅, extension and anti-extension disjoint
∩U+2229IntersectionDisjointness of extension and anti-extension
→U+2192Rightwards arrowMaterial conditional, defined as ¬A ∨ B; gappy when either side is
↔U+2194Left right arrowMaterial biconditional, as in E!(t) ↔ t = t
E!—Existence predicateE!(t): t is defined
[[t]]—DenotationValue of a term, possibly ↑
(T, F)—Partial valuationExtension and anti-extension

Metatheory. The Kleene schemes are monotone in the information ordering: refining ⊥ to true or to false never changes a verdict already reached. Monotonicity is what makes the framework work, since by Knaster–Tarski every monotone operator on partial valuations has a least fixed point, and that is the construction behind Kripke's 1975 theory of truth and Fitting's Kripke–Kleene semantics for logic programs. It also settles the propositional decision problems: a formula is satisfiable under the strong Kleene scheme iff it is classically satisfiable, since any classical refinement of a satisfying partial valuation still satisfies it, so satisfiability is NP-complete, while validity is empty — the valuation leaving every atom undefined makes every formula undefined. Supervaluation goes the other way. Over the purely classical connectives its supertruths are exactly the classical tautologies and its consequence relation is exactly classical consequence; the divergence appears only when a determinacy operator is added, and Williamson (1994) showed that supervaluational consequence with such an operator invalidates conditional proof, contraposition, reductio, and argument by cases.

Applies to. Partial recursive functions and the semantics of non-terminating computation, where undefinedness is the halting failure itself. Kripke's theory of truth and the fixed-point constructions that give a language its own truth predicate. Logic programming, where the Kripke–Kleene and well-founded semantics assign a third value to atoms that neither succeed nor fail. Database query languages with null values, SQL's three-valued conditions being the applied case. Free logic and the semantics of non-denoting singular terms, definite descriptions and presupposition failure. Program verification with partial functions and precondition-guarded specifications. Denotational semantics, where the information ordering with ⊥ is the domain-theoretic setting.

Limitations. A Kleene-style partial logic has no valid formulas at all, so validity cannot be axiomatized in Hilbert style and everything must be stated as consequence; the deduction theorem fails outright, since A ⊨ A while A → A takes a gap when A does. Nothing in the notion of partiality decides between the strong and weak schemes — both extend the classical tables monotonically, and the choice is made on grounds external to the logic. Gaps are not detectable from inside: no monotone truth function returns true exactly at ⊥, so "t is undefined" is inexpressible in the object language, and adding a definedness operator destroys monotonicity and with it the least-fixed-point construction. Identity becomes partial, so t = t is not valid and the quantifier rules must be relativized to E!, making the logic free. And the strengthened Liar survives: a gap theory cannot say inside its own language that the Liar is gappy.

© 2026 Lingenic LLC