Timeline for What are the requirements of a foundational theory?
Current License: CC BY-SA 3.0
20 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Mar 18, 2018 at 17:28 | comment | added | Alex Kruckman | @ThomasBenjamin I suggested such a criterion in my earlier comment, which does not assume that the foundational theory is any kind of set theory. Of course, I admit that it's both somewhat tautological and rather informal, since Blass's Theory T is not - and cannot be - precisely defined. | |
| Mar 14, 2018 at 14:14 | comment | added | Thomas Benjamin | (cont.) and how to adequately define 'foundational'? | |
| Mar 14, 2018 at 12:11 | comment | added | Thomas Benjamin | (cont.) 'foundational'? | |
| Mar 14, 2018 at 12:10 | comment | added | Thomas Benjamin | (cont.) language?)", and abstract such criteria as a definition of 'foundational' for some arbitrary first-order theory $T$. As an example of a non-set-theoretic foundation for classical mathematics (primarily a formal theory of analysis), one can have an archimdian foundation (as per Cauchy, Weierstrass, and Dedekind, which got us to $ZFC$) or a nonarchimedian foundation (nonstandard analysis, though I believe there is a set-theoretical foundation of non-standard analysis). The point is, Given a first-order theory $T$, what are the necessary and sufficient conditions for $T$ to be | |
| Mar 14, 2018 at 11:52 | comment | added | Thomas Benjamin | I find it interesting that everyone who commented so far basically assumed some kind of set theory as the 'foundation(s)' of mathematics (I realize that this is to be expected as set theory has been so successful in that role). The reason I mention this is because of Omer's fundamental question: "My question is can we describe some requirements (in some logic system) that any foundational language must satisfy?" . Applying the criterion of the question to $ZFC$, one might ask, "What is it about $ZFC$ that makes it such a great foundational theory (and {$\in$} such a great foundational | |
| Mar 12, 2018 at 6:30 | comment | added | Omer Rosler | @Joel You are of course right here, I should have been more precise: The point of those universes is to study the theory from within. Now if the theorem we are querying relates to those universes themselves, this is pointless. So we also need to require that the trooth of this theorem is indepedndent from the universe axioms. I need to edit the question accordingly | |
| Mar 11, 2018 at 23:59 | comment | added | Joel David Hamkins | Rather, the situation in set theory is that we have an enormous hierarchy of foundational theories, stratified by consistency strength, such as the large cardinal hierarchy, and one often seeks to measure the strength of a mathematical result by fitting it into this hierarchy. | |
| Mar 11, 2018 at 23:00 | comment | added | Joel David Hamkins | You say, "to prove a theorem in set theory, is the same as proving it in every inaccessible cardinal," but this is just not true. There are statements true in all such universes, for example, that are not provable in ZFC, which many like to take as the basic set theory. And if your set theory includes the statement that there are many inaccessible cardinals, then this statement itself will not generally be true in all such inaccessible cardinal universes. And Gödel-Bernays set theory (and even Kelley-Morse set theory, which is stronger) does not prove the existence of inaccessible cardinals. | |
| Mar 11, 2018 at 22:32 | comment | added | Omer Rosler | @Not Mike I made a little word salad, fixed now | |
| Mar 11, 2018 at 22:31 | history | edited | Omer Rosler | CC BY-SA 3.0 |
fixed word salad
|
| Mar 10, 2018 at 2:26 | comment | added | Not Mike | I'm not sure what you mean by "semantically provable in $\cal L$ iff it is syntactically provable in $U$". What do you mean by "semantically provable" and "syntactically provable"? | |
| Mar 7, 2018 at 17:31 | comment | added | Omer Rosler | @Not_Here Well, I'm starting to see the problem in some different logic systems (as we require the ability of the theory to ask questions about itself, which is unreasonable for constructive mathematics), so this might still offer requirements for a unifying theory inside formalism (so this might apply to ECTS + U and NGB) | |
| Mar 7, 2018 at 8:19 | comment | added | Not_Here | The foundations of mathematics, metamathematics, and the philosophy of mathematics are largely overlapping fields, so I think that this is strongly a philosophical question as well as mathematical. As such, an answer to "What are the requirements of a foundational theory?" is going to depend on what the "correct" philosophy of mathematics is. By which I mean, if a formalist, an ante rem structuralist, and a constructivist walk into a bar, they'll disagree vehemently about what the answer to this question is. For example, there are intuitionistic objections to your requirements. | |
| Mar 6, 2018 at 21:19 | comment | added | Alex Kruckman | I would call a theory "foundational" if and only if it interprets Andreas Blass's Theory $T$: mathoverflow.net/a/90945/2126. | |
| Mar 6, 2018 at 21:10 | history | edited | Omer Rosler | CC BY-SA 3.0 |
Font change
|
| Mar 6, 2018 at 20:44 | comment | added | Asaf Karagila♦ | Might as well use a proper font, then. $\cal L$ or $\scr L$, for example. | |
| Mar 6, 2018 at 20:42 | comment | added | Omer Rosler | @AsafKaragila I was trying to mimic Model theoretic notation of forcing, where adjoining a generic filter is similar. | |
| Mar 6, 2018 at 19:47 | review | Close votes | |||
| Mar 10, 2018 at 18:05 | |||||
| Mar 6, 2018 at 19:09 | comment | added | Asaf Karagila♦ | Using Roman $L$ and then $L[U]$ and so on is a rough deviation from the notation in set theory, especially since you mix large cardinals into this. | |
| Mar 6, 2018 at 18:41 | history | asked | Omer Rosler | CC BY-SA 3.0 |