4

There are multiple languages to describe all of mathematics, and there are some equivalences between them, some more successful then others. My question is can we describe some requirements (in some logic system) that any foundational language must satisfy?

In praticular, I have been thinking about two requirements:

  1. It can describe the logic system it lives in, for example in category theory we have the notion of a topos.

  2. It can talk about itself, this is some kind of version of large-cardinal axioms: This is going to be very vague, but please bear with me: Let $\cal{L}$ be a language (in whatever logic system we need to make this rigurous). We can extend it to include another generic object, $\cal{L}[U]$ which would serve as the universe. We require the following template of axioms on $\cal{L}[U][E]$: Every predicate in $\cal{L}$ can be extended to one on $\cal{L}[U][E]$, we reuqiure it has an interpretation in every "internal universe" $U$ and is satisfied in $\cal{L}$ iff it is satisfied in every $U$

In set theory, those $U$ are inaccessible cardinals and this axiom is both the existance of arbitrarly large inaccessible ones, and the fact that to prove a theorem in set theory, is the same as proving it in every inaccessible cardinal. So in a sense, GNB set theory satisfies these axioms.

Can we make this rigorous? Is there a logic system that we can formulate this in? Another thing to ask, are all "universes" that can internalize the logic system they are defined in equivalent?

Omer Rosler
  • 753
  • 3
    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. – Asaf Karagila Mar 06 '18 at 19:09
  • @AsafKaragila I was trying to mimic Model theoretic notation of forcing, where adjoining a generic filter is similar. – Omer Rosler Mar 06 '18 at 20:42
  • 1
    Might as well use a proper font, then. $\cal L$ or $\scr L$, for example. – Asaf Karagila Mar 06 '18 at 20:44
  • 5
    I would call a theory "foundational" if and only if it interprets Andreas Blass's Theory $T$: https://mathoverflow.net/a/90945/2126. – Alex Kruckman Mar 06 '18 at 21:19
  • 3
    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. – Not_Here Mar 07 '18 at 08:19
  • @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) – Omer Rosler Mar 07 '18 at 17:31
  • 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"? – Not Mike Mar 10 '18 at 02:26
  • @Not Mike I made a little word salad, fixed now – Omer Rosler Mar 11 '18 at 22:32
  • 6
    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. – Joel David Hamkins Mar 11 '18 at 23:00
  • 5
    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. – Joel David Hamkins Mar 11 '18 at 23:59
  • @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 – Omer Rosler Mar 12 '18 at 06:30
  • 1
    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 – Thomas Benjamin Mar 14 '18 at 11:52
  • 1
    (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 – Thomas Benjamin Mar 14 '18 at 12:10
  • (cont.) 'foundational'? – Thomas Benjamin Mar 14 '18 at 12:11
  • 1
    (cont.) and how to adequately define 'foundational'? – Thomas Benjamin Mar 14 '18 at 14:14
  • @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. – Alex Kruckman Mar 18 '18 at 17:28

0 Answers0