validMoves
The definition supplies the set of propositions that can be verified next without contradicting the verified history in a proof state. Modelers of consciousness in Recognition Science cite it when formalizing free will as selection among consistent future paths. The definition is realized by a direct set comprehension that retains only those unverified propositions satisfying the consistency predicate.
claimFor a proof state $s$, the valid moves are the set of propositions $p$ in the unverified component of $s$ such that $p$ is consistent with the verified component of $s$.
background
A proof state consists of three disjoint sets of propositions: the verified set representing the immutable past, the current proposition under verification, and the unverified set representing potential futures. The module models consciousness as the verification cursor advancing from past through present into future, with free will realized as selection among paths that preserve ledger balance.
proof idea
The definition is a one-line set comprehension that intersects the unverified set with the subset of propositions satisfying the isConsistent predicate relative to the verified history.
why it matters in Recognition Science
This definition underpins the free_will_exists theorem and the NavigationPoint structure, which formalize choice at points where multiple consistent futures exist. It fills the free will postulate in the RRF consciousness model, where consciousness selects among valid moves to balance the recognition ledger. The construction touches the open question of formalizing the choice operator itself.
scope and limits
- Does not define the selection mechanism among the valid moves.
- Does not assert that the set is nonempty.
- Does not incorporate J-cost directly into the validity criterion.
- Applies only within the discrete proof-state model of recognition.
Lean usage
theorem demo (s : ProofState) (h : (validMoves s).Nonempty) : ∃ p, p ∈ validMoves s := free_will_exists s hformal statement (Lean)
93def validMoves (s : ProofState) : Set Prop :=
proof body
Definition body.
94 { p ∈ s.unverified | isConsistent s.verified p }
95
96/-- **HYPOTHESIS**: Free will as choice among valid moves.
97
98 STATUS: SCAFFOLD — While existence of valid moves is formally
99 defined as consistency with verified history, the mechanism of
100 conscious choice ("free will") is a core postulate of the model.
101
102 TODO: Formally define the choice operator and its relationship to J-cost. -/