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

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.

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.

• Could you outline why your quantified statement is false for the reals as the completion of the rationals? Thanks. May 19, 2022 at 15:05
• @coffeemath In this case the elements of $\mathbb{R}$ are equivalences classes whose elements are sequences of rationals (i.e., maps $a:\mathbb{N}\to \mathbb{Q}$). May 19, 2022 at 15:44
• You might be interested in homotopy type theory, which includes an axiom asserting that (in a certain precise sense) "identity is equivalent to equivalence".
– Karl
May 19, 2022 at 17:07

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.

• please, see the "EDIT" part I added in my question! I liked you answer. See my edited question because maybe you know exactly what I want. May 19, 2022 at 18:45

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.

• I know this. In fact, I gave an example of it in my question. That's why I want to know if there's a mathematical framework with an interval logic in which isomorphic objects can be considered equal. May 19, 2022 at 16:22
• @rfloc: you are using two different ways to construct?: Dedekind cuts and completion. May 19, 2022 at 16:51
• @rfloc I think the point being made here is that we have two isomorphic objects (the axes) which are distinct subsets of the plane, so they differ, for example, on the question "is $(1,0)$ an element"? Anytime we have a mathematical object $A$ containing multiple distinct isomorphic copies of an object $B$, this will be an obstruction to (at least a naive formulation of) what you are asking for. May 19, 2022 at 17:12
• @AlexKruckman Please, see the "EDIT" part I added in my question! May 19, 2022 at 18:39