Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

RFD 0068 — Native four-valued temporal comparison: decidability of a paraconsistent metric reasoner over ℤ

Scope. RFD 0067 §5 settled the temporal value dispositions and flagged one — native four-valued temporal comparison — as the sole open research obligation, gating claiming (not shipping) the four-valued lift. This RFD funds that campaign, records the mechanized result that discharges its load-bearing question, and fixes the binding implementation constraint the mechanization forces.

  • State: discussion (campaign funded)
  • Extends: RFD 0067 (temporal literal surface — Open-Question #1, the four-valued comparison frontier), which ships 2-valued-plus-refusal comparison today.
  • Relates to: RFD 0007 (missing-value semantics — Can vs NA), RFD 0024 (Allen library — the ω-admissibility sub-obligation), RFD 0060 (Lean substrate architecture — where the eventual merged proof lands), the @[language_interface] drift gate (Truth4 four-values lock).
  • Tracks: the four-valued-metric-decidability obligation (RFD 0067 Open-Question #1).
  • Prior art: Belnap–Dunn FDE (the four-valued codomain); Rivieccio–Jung–Jansana (twist structures / four-valued modal logic — the coordinate-wise reduction); Wałęga–Cuenca Grau–Kaminski et al., “DatalogMTL over the integers” (KR 2020 / TPLP 2023 — the ℤ-restores-decidability result and the per-coordinate ruler bound this imports); Wałęga–Zawidzki–Wang–Grau (AAAI 2023 — DatalogMTL saturation, the multi-page 2-valued periodicity argument); Pollaci 2026 (three-valued WFS DatalogMTL over ℤ — the adjacent occupied cell); Denecker–Marek–Truszczyński (AFT); Fitting (interlaced bilattices); Małuszyński–Szałas 4QL (four-valued Datalog PTIME on a finite lattice — four-valuedness is not the cost); Gabbay–Kurucz–Wolter–Zakharyaschev (the Σ¹₁ two-metric bound — why one timeline); Kolaitis–Vardi (the four-valued-= obstruction — why identity stays rigid while comparison goes four-valued).

Question

Argon’s comparison verdicts are four-valued (Truth4 = Belnap–Dunn FDE): Is / Not / Can / Both. Temporal comparison is structurally four-valued — a zoneless DateTime vs an absolute Instant, an offset-unknown value, or two values inside the XSD ±14h window are genuinely incomparable (a Can no total order can produce); standpoint disagreement over a temporal fact is Both. RFD 0067 ships the interim: 2-valued comparison plus loud-refusal of the incomparable cases. Going native — letting temporal comparison return Can/Both into the metric reasoner — raises the question that gates the claim:

Does a designated, non-explosive Both (paraconsistency) break the integer-timeline decidability that 2-valued DatalogMTL over ℤ enjoys — and if not, what does soundness of the four-valued lift require of the metric operators?

Context

Why this is not free

2-valued DatalogMTL over ℤ is decidable (Wałęga et al.) on three pillars: (a) a least fixpoint over derived atoms, (b) consistency ≡ ⊥-never-derived, (c) ultimate periodicity of the canonical model (the “ruler” bound), reducing entailment to a bounded check. Dense (ℚ/ℝ) time is undecidable (RFD 0067 §Context). A designated, non-explosive Both — the whole point of a paraconsistent codomain — attacks all three: (b) is literally “⊥ (Both) may be derived and is not explosive,” and (c) is stated over the 2-valued model. A priori it was open in every direction whether the four-valued lift stays decidable, or whether the dense-time lower bound even survives paraconsistency.

What is not the cost

Four-valuedness per se is complexity-neutral: Fitting/AFT over a finite interlaced bilattice, and 4QL keeps plain four-valued Datalog PTIME. The threat is specific — the interaction of the designated Both with the metric fixpoint and the periodicity argument, not the extra truth values.

The substrate this must respect (RFD 0067, kernel-checked)

One ℤ metric timeline = the valid-time axis; transaction-time a non-metric selector; Truth4 negation De Morgan + involutive (Foundation/Truth4.lean); the least-fixpoint lattice is Approx = Belnap FOUR = 2 ⊠ 2ᵒᵈ (Reasoning/Datalog/AFT.lean), never MetaValue (which has no complete lattice — is ⊕ not = both escapes K3). The four-valued reasoner is AFT over the twist/Approx space; the campaign’s question is whether that space’s metric closure is periodic.

Decision

1. Fund native four-valued temporal comparison as the target; the loud gate extends to the reasoner

Commit to native Can/Both temporal comparison as the intended surface — genuine incomparability returns Can, standpoint conflict returns Both, both flowing into the metric reasoner — replacing the interim 2-valued-plus-refusal once the decidability obligation is mechanically discharged. The loud-gate discipline extends from the compiler to the reasoner: the four-valued metric lift is not claimed decidable, and does not ship, on an unproven pillar. A scratch-first Lean campaign (never-merged until sorry-free and lead-signed-off) is the gate.

2. The load-bearing question is answered: the paraconsistent Both does NOT break periodicity (mechanized)

Established in the campaign scratch (Truth4MetricDatalog.lean), each result firsthand #print axioms-verified kernel-clean ([propext, Classical.choice, Quot.sound], no sorryAx):

  • coupling_preserves_periodicity — the campaign’s central open question: if each of the two twist coordinates is ultimately periodic, then the joint four-valued canonical model is (product period π₁·π₂). The designated Both inherits periodicity as a bit-pattern of the two coordinates (belnapAt_congr); it introduces no new aperiodicity. This is the coordinate-wise twist reduction (Rivieccio–Jung–Jansana), established for qualitative box/diamond, here carried to the metric ℤ ruler.
  • canonicalModel_isLeastFixpoint — the four-valued canonical model is a well-defined least fixpoint over Approx. This is pillar (b) reformed for paraconsistency: well-definedness with Both present, not ⊥-absence.
  • both_feeds_metric — a Both verdict at one time point propagates through a nonzero metric shift (the non-vacuity witness; see §3).
  • The reduction chain canonicalModel_ultimatelyPeriodic_of_twoValued → entails_periodic carries decidability from per-coordinate periodicity to bounded entailment.

Consequence. Decidability of four-valued metric DatalogMTL over ℤ reduces to (a) the published 2-valued per-coordinate ruler bound (Wałęga et al. — imported, TwoValuedRulerBound), and (b) the effective finite-domain check (entails_decidable). Neither is a new mathematical obstruction; both are named, remaining sorrys in the scratch. No place where the paraconsistent Both obstructs periodicity was found — the a-priori threat is refuted.

3. Binding implementation constraint: metric operators propagate the full Belnap pair

The mechanization forces a soundness constraint on the reasoner (both_feeds_metric, kernel-clean): a metric temporal operator (◇/□/since/until and the bounded variants) must propagate the full Belnap pair — both the positive-evidence coordinate and the negative-evidence coordinate — not just positive derivations. A metric operator that forwards only positive evidence drops the Both/Can content and is unsound under the four-valued lift. This is binding on any oxc-reasoning implementation of four-valued metric operators, and is a review checkpoint on any four-valued-lift PR.

4. The decidable fragment requires shift-invariance (faithfulness correction)

The periodicity statement is false over an arbitrary ground metric program: a program with facts at square times (0, 1, 4, 9, …) is finite-predicate, well-typed, and has no ultimately-periodic model (unbounded gaps) — firsthand-verified in the scratch (sqProg). Ultimate periodicity — hence decidability — holds for shift-invariant finite metric programs (FiniteMetricProgram.shiftInv): the ℤ-orbit of finitely many rule schemas, which is exactly what a rule program (as opposed to an infinite fact set) is. The decidable fragment is the shift-invariant one; the statement was corrected to carry this hypothesis before it was proved, not after. This bounds the claim and is the honest statement.

Rationale

  • Decidability was the only thing gating the claim; it is now essentially in hand. RFD 0067 §Consequences reduced the owner-decisions to five-resolved + this one research obligation. The mechanized coupling result removes the genuine unknown (does paraconsistency break periodicity — no); what remains is importing a published theorem and wiring an effective procedure — both proof-engineering, not open mathematics.
  • Scratch-first, lead-signed-off, never-weakened (the Lean operating model). The statement was strengthened to faithfulness (shift-invariance) before proving; non-vacuity was discharged first (both_feeds_metric and the bothAtZero witnesses show the four-valued content is not degenerate); the axiom hygiene was verified firsthand (#print axioms), not taken on the prover’s word. The two remaining sorrys are named import points, not scattered gaps.
  • The Belnap-pair constraint is not a style choice. both_feeds_metric shows a positive-only metric operator drops the four-valued content; §3 is the mechanized content of “the four-valued lift is real,” not aesthetic guidance.
  • Shift-invariance is where the dense-time analogue’s teeth actually are for a program. The undecidability cliff is density; the aperiodicity a ground fact-set can inject (square times) is a distinct failure the fragment restriction rules out. Naming it keeps the decidable-fragment claim honest rather than quietly true-only-for-rule-programs.

Alternatives considered

  • Keep 2-valued-plus-refusal permanently (never go native). Rejected as the target (kept as the shipping interim): refusing every genuinely-incomparable temporal comparison forces the modeler to pre-resolve incomparability the substrate exists to represent (Can), and discards standpoint conflict (Both) that the federation layer produces. The four-valued codomain exists precisely for these.
  • Three-valued WFS (K3, no Both). The adjacent occupied cell (Pollaci 2026). Rejected: drops paraconsistency — standpoint conflict collapses to undetermined (or, classically, to explosion); Argon’s federation semantics needs a designated non-explosive conflict value. (WFS-over-ℤ remains relevant prior art for the effective procedure entails_decidable.)
  • Re-prove the 2-valued ruler bound in-repo. Rejected: it is an established, multi-page published result; importing it (a cited axiom per the substrate’s citation rule, or a vendored mechanization) is correct. Re-deriving it is not this campaign’s contribution — the contribution is that the four-valued lift preserves it.
  • Native four-valued = (counterpart identity). Out of scope and separately rejected (RFD 0067 §5; Kolaitis–Vardi — a four-valued = breaks the join engine). Comparison is four-valued; identity stays rigid two-valued.

Consequences

  • Ships now (RFD 0067): 2-valued comparison + loud-refusal of incomparable cases. Unchanged.
  • The mechanization campaign (this RFD):
    • Scratch preserved at .local/research/datetime-literal/lean-scratch/Truth4MetricDatalog.lean (discharged content kernel-clean; 2 named sorrys).
    • Remaining to close before claiming decidable: import TwoValuedRulerBound (the published 2-valued periodicity — vendor or cite-axiom), and discharge entails_decidable (computable bound N, period π, Pred-enumeration → an effective procedure).
    • When sorry-free + lead-signed-off, promote from scratch into spec/lean/Argon/ (RFD 0060 architecture; under Reasoning/Datalog/ or Decidability/), where it becomes drift-gated substrate.
  • Binds the implementation: four-valued metric operators in oxc-reasoning must propagate the full Belnap pair (§3).
  • Then ships: native Can/Both temporal comparison, replacing the interim refusal, behind the proof.

Open questions

  • The two named imports (above): TwoValuedRulerBound, entails_decidable. Proof-engineering, not obstruction — but real work, and the effective procedure fixes the reasoner’s actual complexity bound.
  • Mechanized totality of the multi-carrier kind function κ (RFD 0067). κ is total/refusing by construction in Rust; no published multi-carrier “kind inferred from inner shape” grammar has a mechanized totality proof — a new (small) result, adjacent to this campaign.
  • ω-admissibility of the Allen layer over discrete ℤ. Allen interval relations are proven admissible over the dense line; the discrete-ℤ analogue (RFD 0024’s library over interval.rs’s fixed step) is unproven.
  • The value-half of comparison is itself four-valued at construction. A DST gap is a no-Is-witness (Can), a fold is Both — today collapsed to a strategy parameter (RFD 0067 §5). Surfacing them as genuine Truth4 verdicts is the write-side analogue of this read-side campaign.
  • Incomparability composition (carried from RFD 0067): whether the distinct incomparability causes (offset-unknown, cross-kind, calendar-vs-fixed duration, causal concurrency) collapse into one Truth4 algebra or need a product/bilattice of per-cause comparison relations.