5
$\begingroup$

Is there a mathematical discipline that studies mathematical objects based on their behavior rather than their encoding?

I ask because a group is classically defined as a set with a binary operation and a handful of axioms. But I am learning type theory, and I am able to define a group as a type with a binary function and some constraints. The set theoretic and type theoretic formulations have different encodings, and yet I still believe I am working with the same mathematical object despite different foundational systems.

Is category theory or some other discipline capable of abstracting away the details of how an object like a group is encoded and instead define them on the basis of behavior that should be encoding-irrelevant?

$\endgroup$
5
  • 1
    $\begingroup$ See here. You can define a "group object" in terms of morphisms which describe what the object "does". $\endgroup$
    – wormram
    Commented Apr 27, 2020 at 6:57
  • $\begingroup$ one can actually have a some sort of Mega-theory that adds all primitives of mathematical concepts and directly adds them on top of some common logical background like for example first order logic, and add axioms about each concept directly, now with adequate separation on the domains of each concept, this can be done easily, and I guess this is the more bare kind of theory, it would be implementation free for each concept!!! This can be done easily, and possibly it is the most real kind of mathematics. $\endgroup$
    – Zuhair
    Commented Apr 27, 2020 at 9:21
  • $\begingroup$ @Sunyata, I don't see how this is encoding independent? still you are using categories, products, etc.., I think the only way to grasp the OP intentions is to formalize any mathematical concept directly on top of a suitable piece of logic, I mean we add the primitives of that mathematical concept and the important axioms that reflects the behavior of objects according to that concept, and so on.. without the need to formalize it on top of set theory or category or type theory or any other theory whose underpinnings are not related to the subject matter of the navigated concept $\endgroup$
    – Zuhair
    Commented Apr 27, 2020 at 11:22
  • 1
    $\begingroup$ @Zuhair I doubt even your 'solution' works uniformly regardless of the foundational systems, as type theory and set theory even differs from the logic-level: in set theory, logic is a primitive notion prior to sets. In type theory, however, logic is defined from types. $\endgroup$
    – Hanul Jeon
    Commented Apr 27, 2020 at 15:20
  • $\begingroup$ @HanulJeon, I didn't claim that it can exhaust all available systems, there are second order systems, and higher order systems. So definitely it cannot grasp all of what can belong to mathematics like set theory, type theory, category theory, etc..But I was actually largely speaking about mathematics prior to set theory, usually labeled as ordinary mathematics, so those can be put in such a mega-foundational system, you can add arithmetical primitives, geometric primitives etc.. with axioms about them each appropriately relativised. And this is NOT my invension. It's not original with me. $\endgroup$
    – Zuhair
    Commented Apr 27, 2020 at 16:00

1 Answer 1

2
$\begingroup$

I would argue that type theory is precisely such a discipline, that is we can view type theory as a language designed to manipulate certain types of objects independently of their encoding.

Let me be precise in what I mean by encoding here. To do mathematics we in any case need a foundational system. That is a system which tells us how to construct valid mathematical objects in a consistent manner. Set theory does this very well, because it allows us to define objects of just about any complexity. Let us call set theory System S. Let me be very explicit and remark that in System S with an appropriate set theoretic universe $U$, we usually define the set of monoids (for simplicity) as the set

$$\text{Mon}_S := \{x\in U\ |\ \exists m,\star\in\text{fun}(m\times m,m),1\in m. x = \langle m,\langle \star,1\rangle\rangle\wedge \phi(m,\star,1)\}$$

where $\phi(m,\star,1)$ ensures the identity and associativity axioms $\mathcal A$.

In particular, I prefer to think of the operations $\text{fun}(\cdot,\cdot)$,$\langle\cdot,\cdot\rangle$ and $\cdot\times\cdot$ as nothing but macros with the expansions \begin{align*} \langle x,y\rangle &:= \{x,\{x,y\}\}\\ x\times y &:=\{w\in U\ |\ \exists u\in x,v\in y. w = \langle u,v\rangle\}\\ \text{fun}(A,B)&:=\{\alpha\in \mathcal P(A\times B)\ |\ \forall u\in A. \exists! v\in B. \langle u,v\rangle\in\alpha\}. \end{align*}

Let us now suppose we have a type theory System M with universe $\text{Type}$, equality types $s =_A t$, dependent sums $\Sigma_{x:A}B$, and arrow types $A\to B$. In this system we would simply define the type of monoids as $$\text{Mon}_M := \Sigma_{M:Type}\Sigma_{\star:(M\times M\to M)}\Sigma_{1:M}P(M,\star,1)$$ where $P(M,\star,1)$ are the type-theoretic monoid axioms. $\newcommand{\llb}{[\![}\newcommand{\rrb}{]\!]}$

What is important here is that we can encode System M into System S as follows

  • For a suitable set universe $U$ we encode $$\llb \text{Type}\rrb_\sigma := U$$
  • The function space is encoded $$\llb A\to B\rrb_\sigma := \text{fun}(\llb A\rrb_\sigma,\llb B\rrb_\sigma)$$
  • Supposing $x:A\vdash t:B$ we encode lambda abstractions as $$\llb \lambda x:A.t\rrb_\sigma := \{w\in \llb A\rrb_\sigma\times \llb B\rrb_\sigma\ |\ \forall u\in\llb A\rrb_\sigma, v\in\llb B\rrb_\sigma. w = (u,v)\implies v = \llb t\rrb_{\sigma,x\mapsto u}\}$$
  • and a variable $x:A$ as $$\llb x\rrb_\sigma := \sigma(x).$$
  • Given a type family $B:A\to \text{Type}$ (written this way for simplicity), we encode dependent sums as $$\llb\Sigma_{x:A}B\rrb_\sigma :=\{z\in \llb A\rrb_\sigma\times\llb \text{Type}\rrb_\sigma\ |\ \forall x\in\llb A\rrb_\sigma,y\in\llb \text{Type}\rrb_\sigma. z = (x,y)\implies \\ y\in \llb B\rrb_\sigma(x)\}.$$
  • We can encode equality as $$\llb s =_A t\rrb_\sigma := \{x\in\{\emptyset\}\ |\ \llb s\rrb_\sigma = \llb t\rrb_\sigma\}$$
  • and a proof $p: s =_A t$ is encoded $$\llb p\rrb_\sigma := \emptyset.$$

And of course, one should check that for every $t : A$, the encoding satisfies $$\llb t\rrb_{[]} \in \llb A\rrb_{[]}\qquad\text{(for $[]$ the empty valuation)}.$$

Now if we take $M:\text{Mon}_M$, $\llb M\rrb_{[]}$ is the encoding of the monoid $M$ in System S, although this encoding is a bit more complicated than the definition of a monoid directly in System S described by $\text{Mon}_S$.

Now why should we bother going through all this effort? The reason is that the definition of a monoid in this type theory is much better behaved than that in set theory. What System M does is give a coarser abstraction layer above System S. So whereas it would make sense to ask a meaningless question such as whether $\emptyset \in \llb M\rrb$ in System S, such a question cannot even be stated within System M. In fact, the only things that can be stated about $M$ are statements in the theory of monoids, unless we add assumptions about $M$. This explains how type theory gives us a way to talk about objects independently of their encoding.

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .