You can only if P8: is defined in your theory. Otherwise, do equivalence or some other logic axioms. Or embed Prov_T() in Prov_U().My question is this. How do we add the reflection schema to a theory such that the proof predicate Prov_U() includes the reflection schema itself. Would the following do the trick?
P8: P_1 & P_2 & … & P_7 & Prov_T(⌜phi⌝) → phi — Newberry
There are many competent mathematical philosophers reading the forum who aren't necessarily proficient in a system of logical symbolism — alan1000
My question is this. How do we add the reflection schema to a theory such that the proof predicate Prov_U() includes the reflection schema itself. Would the following do the trick?
P8: P_1 & P_2 & … & P_7 & Prov_T(⌜phi⌝) → phi — Newberry
Yeah. He's defining U in terms of T.I read the post. Then I went back to the first place that, as far as I can tell, he doesn't make sense. His theory U is not defined; his proposed definition is circular, so such questions that mention it are nugatory unless we first fix that definition. — TonesInDeepFreeze
He's defining U in terms of T. — L'éléphant
Recursive definitions also look circular, but they are not. — Newberry
a fixed point of the hierarchy of theories
T' = T + (Ex)Prf_T(x, ⌜F⌝) --> F
T" = T' + (Ex)Prf_T'(x, ⌜F⌝) --> F — Newberry
even if a proof “exists” it could be infinitely long — Newberry
Also, what fixed point do you have in mind? — TonesInDeepFreeze
Get involved in philosophical discussions about knowledge, truth, language, consciousness, science, politics, religion, logic and mathematics, art, history, and lots more. No ads, no clutter, and very little agreement — just fascinating conversations.