pith. machine review for the scientific record. sign in
structure definition def or abbrev

GodelDissolution

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)

 274structure GodelDissolution where
 275  /-- RS is about selection, not proof -/
 276  rs_is_selection : Prop
 277  /-- Gödel is about proof, not selection -/
 278  godel_is_about_proof : Prop
 279  /-- Different targets → no obstruction -/
 280  different_targets : rs_is_selection → godel_is_about_proof → True
 281
 282/-- The Gödel dissolution holds: RS and Gödel are about different things. -/

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (5)

Lean names referenced from this declaration's body.