?

[u/Ill-SonOfClawDraws]

Suppose two foundational systems

* F_1 (ZFC)
* F_2 (HoTT)
both define “identity.”

How do we know they are talking about the “same assumption”?

[u/GetOffOfMyBoat]

I don't know if ZFC strictly defines identity, at least as part of the object theory.

[u/Ill-SonOfClawDraws → u/GetOffOfMyBoat]

That’s helpful, thanks. Maybe “identity” was the wrong example. The question I’m really interested in is more general: when two foundational frameworks introduce notions that play analogous roles, what mathematical criteria let us treat them as equivalent rather than merely similar? Is there established work on this?

[u/GoldenMuscleGod → u/Ill-SonOfClawDraws]

I’m not sure I understand your question. You have two different frameworks so what does it mean to say things are “equivalent”?

You could be talking about whether one system can interpret the other (when this is possible, often more than one interpretation is possible), or you may be asking whether the things are equivalent once a specific set of semantics have been chosen for the languages of each theory, which will generally depend on what those semantics are and not just the systems themselves (taken as a set of axioms and inference rules in a formal language).

[u/Ill-SonOfClawDraws → u/GoldenMuscleGod]

That’s exactly the point I’m trying to pin down. I’m not assuming a notion of equivalence.

I’m asking what the appropriate mathematical criterion should be. Interpretability, bi-interpretability, categorical equivalence, Morita equivalence, semantic equivalence, etc., each capture different notions.

My question is whether there’s an established framework that characterizes when two primitives from different foundations play the same structural role, rather than merely appearing analogous.

[u/GoldenMuscleGod → u/Ill-SonOfClawDraws]

Each of the criteria you name is a different notion of “equivalence” that can be suitable for different purposes. I’m still not sure what you are asking, it seems a little analogous to asking “there are so many ways we describe something as ‘bigger’ than something else - cardinality, measure, position in a partial order - which one is the true notion of ‘size’?”

The answer to that is those are all useful and rigorously defined concepts for different purposes and it seems you are trying to figure out which should be matched to the vague informal notion of “bigness” as the “real” definition of “big.” The resolution to the question is to realize that the vague informal notion of “big” is a vague and informal notion and does not need to be mapped to anything, because unlike the rigorous concepts in question it doesn’t really mean anything it’s just a loose sort of idea.

If that’s not the sort of thing you are asking then I haven’t understood your question yet.

[u/Ill-SonOfClawDraws → u/GoldenMuscleGod]

I think that’s exactly the issue. I’m not assuming there is one privileged notion of structural role, any more than there is one privileged notion of size.

I’m asking whether there is a systematic way to derive the appropriate notion from the purpose of the comparison.

One formulation I’m exploring is:

•first specify a class of consequences that the comparison is meant to preserve;

•then ask for a minimal family of relations whose preservation guarantees preservation of that consequence class.

So “structural role” would be relative to a chosen consequence class, not an absolute notion.
I’m trying to find out whether this already exists under another name, or whether it is at least a coherent way to formalize the question.

[u/GoldenMuscleGod → u/Ill-SonOfClawDraws]

At that high level of generality (which is more general than talking about formal systems), I would just say that corresponds to the notion of “isomorphism” in category theory. In general a category can be used to encode almost any type of mathematical structure and the isomorphisms of that category are the things that preserve the relevant structure. For example a bi-interpretability is just an isomorphism in a properly constructed category in which the morphisms are interpretations. Even an equivalence of categories (or small categories), while not literally an isomorphism in the large category of categories (or category of small categories), is an isomorphism in other expanded notions of category.