Timeline for Feferman's extensional and intensional applications of the method of arithmetization
Current License: CC BY-SA 3.0
8 events
when toggle format | what | by | license | comment | |
---|---|---|---|---|---|
Sep 4, 2023 at 5:04 | comment | added | plm | The best explanation i found is in Buss's survey citeseerx.ist.psu.edu/… , p113. For instance to prove Gödel's second incompleteness theorem one needs reflection, formalized reflection, and formalized modus ponens -see Enderton's excellent textbook p267. Intensionality is a constraint on the representations of r.e. functions/relations/sets in a theory T: that you can work with those in T to prove desired results. Formalizing this would be specifying exactly what the desired results on those arithmetizations are. | |
May 13, 2011 at 6:38 | vote | accept | Marc Alcobé García | ||
May 12, 2011 at 15:08 | comment | added | Emil Jeřábek | “Results of intentional type” presumably mean results involving some intensionally arithmetized concept whose choice can affect validity of the result. For example, reflexivity of $T$ is an intensional result because its statement depends on the choice of the arithmetization of consistency, a theory may be reflexive for one choice of the arithmetization of consistency and nonreflexive for another one. OTOH, incompleteness or finite non-axiomatizability of $T$ do not refer to any arithmetization, they are properties of $T$ alone. | |
May 12, 2011 at 15:04 | answer | added | Andreas Blass | timeline score: 6 | |
May 12, 2011 at 14:58 | comment | added | Emil Jeřábek | There is no precise definition of these notions in this context, they are used informally. (The terminology refers to intension and extension in semantics, see en.wikipedia.org/wiki/Sense_and_reference.) I don’t know how to explain it other than basically repeating what Feferman wrote: a concept $C$ is arithmetized extensionally by a formula $F$ if the relation defined by $F$ in the standard model $\mathbb N$ gives $C$, and it is arithmetized intensionally if moreover the given theory $T$ proves that $F$ obeys some basic properties that $C$ is expected to have (based on context). | |
May 12, 2011 at 14:23 | history | edited | Sergei Tropanets |
edited tags
|
|
May 12, 2011 at 13:21 | history | edited | Marc Alcobé García |
added tag
|
|
May 12, 2011 at 13:01 | history | asked | Marc Alcobé García | CC BY-SA 3.0 |