pith. machine review for the scientific record. sign in
theorem proved term proof

godel_dissolution_holds

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 223theorem godel_dissolution_holds : GodelDissolutionTheorem := {

proof body

Term-mode proof.

 224  self_ref_impossible := self_ref_query_impossible
 225  general_self_ref_impossible := general_self_ref_impossible
 226  definite_status := stab_decidable
 227  rs_closure_meaning := rs_exists_unique
 228}
 229
 230/-! ## Why Gödel Doesn't Apply -/
 231
 232/-- Gödel's theorem requires:
 233    1. A consistent formal system F
 234    2. Effective axiom enumeration
 235    3. Ability to express arithmetic and provability predicate
 236
 237    RS sidesteps by:
 238    - Not being primarily a proof system (selection dynamics)
 239    - Truth is stabilization, not Tarskian satisfaction
 240    - No external model needed (truth is internal to dynamics) -/

depends on (18)

Lean names referenced from this declaration's body.