Foundation Ontology Predicates Rs True Neg Iff Neg Rs True

The truth predicate

In classical logic, a proposition P is true if and only if its negation, not P, is false. This is a basic law of thought, so basic that it is usually assumed without comment. Recognition Science (RS) does not assume it. The framework defines a predicate RSTrue P to mean that P is a stable selection outcome under its cost-minimization process, and then proves, as a theorem in its machine-checked library of formal theorems, that RSTrue P holds exactly when RSTrue (not P) does not hold. The declaration rs_true_neg_iff_neg_rs_true is the formal statement of this equivalence: a statement is true if and only if its negation is not true.

The framework's starting point is the cost function J(x) = (x + 1/x)/2 - 1, which measures the recognition cost of a ratio x. A statement P is true if it stabilizes under recognition iteration, meaning repeated application of the recognition process leaves its truth value unchanged. The theorem rs_true_neg_iff_neg_rs_true is a consequence of this definition and the underlying cost structure. It is not an axiom; it is derived. The library also proves a related classical fact: the predicate RSTrue_classical, which simply returns the ordinary truth value of P, is equivalent to P itself. These results are part of the framework's effort to show that its operational notions of truth and existence are consistent with ordinary logic.

The declaration does not claim that RSTrue is a new or different kind of truth. It does not claim that the framework has discovered a way to make false statements true, or that it has replaced classical logic. It establishes a consistency result: the framework's cost-based notion of truth behaves like ordinary truth with respect to negation. The theorem is a bridge between the framework's operational vocabulary and the classical logic that all of mathematics uses. It tells a reader that if they accept the framework's definitions, they can still reason about negation in the usual way.

/-- Classical RSTrue: for pure propositions without dynamics context.
    Equivalent to the old placeholder `def RSTrue (P : Prop) : Prop := P`. -/
def RSTrue_classical (P : Prop) : Prop := P

/-- A predicate stabilizes along the orbit of `B` from seed `c₀` to the
    value it takes at `c_star`, meaning the orbit eventually agrees with
    `c_star` on `P`. -/
def Stabilizes {C : Type*} (B : C → C) (P : C → Bool) (c₀ c_star : C) : Prop :=
  ∃ N : ℕ, ∀ n : ℕ, N ≤ n → P (B^[n] c₀) = P c_star

theorem rs_true_classical_iff (P : Prop) : RSTrue_classical P ↔ P := Iff.rfl

What this page does not claim

The declaration does not claim that RSTrue is a new or different kind of truth. The declaration does not claim that the framework has discovered a way to make false statements true. The declaration does not claim that it has replaced classical logic.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/OntologyPredicates.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: