Build a "rich" first-order logic within a given category

Question

I would like to know a mathematical framework with an internal logic where isomorphic objects can be considered equal.

For example, consider the rationals $\mathbb{Q}$. With this set we can construct the reals number in two different ways: define $\mathbb{R}$ as the completion of the metric space $\mathbb{Q}$ or construct $\mathbb{R}'$ using Dedekind cut.

It's well know that there's an algebra isomorphism between $\mathbb{R}'$ and $\mathbb{R}$. However, the proposition $\forall x(x\in \mathbb{R}\color{red}{'}\Rightarrow \exists y,z(y,z\subseteq \mathbb{Q}\wedge x=(y,z)$)) is true for $\mathbb{R}'$ and false for $\mathbb{R}$.

Because of that I would to know, for example, if there's a mathematical framework with an internal logic such that every proposition using this logic is true using $\mathbb{R}$ if, and only if, is also true using $\mathbb{R}'$.

I heard that category theory has an internal logic. I tried to find some material showing what I'm seeking but I didn't find any.

---

I hope I've made myself clear.

Thank you for your attention!

---

EDIT:

I'll try to explain what I really want.

I concluded that the framework I want to work with is category theory.

Let $C$ be a category. In this category I want to build a rich first-order logic ("rich" means I want a first-order logic as close as possible to the usual first-order logic we use in ZFC) such that, given two isomorphic objects $X,Y\in C$ and a proposition $P(x)$ with a free variable constructed using that logic, $P(X)$ is true if, and only if, $P(Y)$ is true.

I also would like that some properties of these logics are preserved by functors.

Obs.: I changed the title of the question.

Answer 1

I think you'll find it difficult to whip up (or find in the literature) a system which fully has the property you want. The reason is that any such framework would have to (be extremely limited or) disallow reducts. Consider for example the subsets $\mathbb{Q}[\pi]$ and $\mathbb{Q}[e]$ of $\mathbb{R}$. Considered with addition alone, these are isomorphic, but they are clearly (and importantly) different subsets of $\mathbb{R}$. If we really want isomorphism to coincide with equality, we would need to disallow the process of forgetting non-additive structure. But this makes things quite inconvenient.

A more pleasant solution in my opinion is to have a good notion of "structural language" - a well-defined way to assign to any structure $\mathfrak{A}$ a set of sentences $\mathit{Lang}(\mathfrak{A})$ such that $\mathfrak{A}\cong\mathfrak{B}$ implies that $\mathit{Lang}(\mathfrak{A})=\mathit{Lang}(\mathfrak{B})$ and that $\mathfrak{A}$ and $\mathfrak{B}$ satisfy the same sentences in this set. Basically, sentences in $Lang(\mathfrak{A})$ shouldn't be allowed to refer to details extraneous to $\mathfrak{A}$ as a structure on its own.

One thing that's nice about this approach is that not only is it compatible with $\mathsf{ZFC}$, it actually is helped along by $\mathsf{ZFC}$. Specifically, suppose we're living in a universe $V$ satisfying $\mathsf{ZFC}$. For each structure $\mathfrak{A}\in V$ we can definably-in-$V$ form a "cumulative hierarchy with urelements" $V[\mathfrak{A}]$. Isomorphic structures yield isomorphic extended hierarchies: $$\mathfrak{A}\cong\mathfrak{B}\implies V[\mathfrak{A}]\cong V[\mathfrak{B}].$$ This means that anything that can be stated in "ordinal-order logic" is appropriately isomorphism-invariant. Practically, this means the following:

To check - in $\mathsf{ZFC}$ - that the question of whether $\mathfrak{A}$ has property $P$ depends only on the isomorphism type of $\mathfrak{A}$ as opposed to the details of $\mathfrak{A}$'s set-theoretic construction, we just need to show that $P$ is expressible in the context of $V[\mathfrak{A}]$.

See this MO discussion for more details.

Answer 2

Even if you use the exact same rule(s) to construct objects, that does not mean the resulting objects are the same.

Take for example the Euclidean plane $\Bbb R^2$ which contains the $x$-axis and the $y$-axis. Both axes are clearly isomorphic to $\Bbb R$ and isomorphic to each other by identifying $(x,0)$ with $(0,x)$. Yet, it's oviously that the $x$-axis is not the same as the $y$-axis.