Can we take definability and existence as primitive notions of a theory?

Question

One of my friend tries to develop an alternative viewpoint of Set Theory. For this he has taken the terms binary relation, set, existence and definability as primitive notions of his Set Theory. After that he attempted to define all the concepts in terms of binary relations.

However, in his theory, right after stating the primitive notions, he says that whenever a relation $\mathscr{R}$ is definable from a set $A$ to a set $B$ we will write $\mathscr{R}:A\to B$. Then he gives the following definition,

Identity of Two Relations. Let $\mathscr{R}$ and $\mathscr{S}$ be two relations. We will say that $\mathscr{R}=\mathscr{S}$ if $\mathscr{R} : A\to B$ is definable iff $\mathscr{S} : A\to B$ is.

I asked him the following two questions,

1. What does he mean by the phrase "$\mathscr{R}$ is definable..."?
2. How does he preserve the order property of binary relations that is found in other set theories (at least in $\sf{ZFC}$)?

He gave the following answers,

1. The phrase "$\mathscr{R}$ is definable..." is synonymous to the phrase "$\mathscr{R}$ has definability..." which according to him need not be explained and in fact can't be because definability is a primitive notion of his theory.

2. We simply observe whether $\mathscr{R}$ is definable from $A$ to $B$ or is it from $B$ to $A$.

My Questions

• I have never seen for any theory (at least the theories which I know) to take the concepts existence and definability considering as primitive concepts. Can we take those as primitive concepts of a theory? Why?

• Are his answers to my questions correct? If not then why not?

---

Note: $\color{red}{\text{Please note that since my understanding of formal logic is not so great, if there is anything}\\\text{wrong in the post, please let me know. And please if you wish to downvote, you can of course,}\\ \text{but please leave a comment clarifying the reason.}}$

Answer 1

Technically in first-order logic there is no such thing as "define". All you have are formulae that you can prove from the axioms via inference rules. In practice that is ridiculous, so one can add what is called full abbreviation power in the following way: $\def\imp{\rightarrow}$ $\def\eq{\leftrightarrow}$

Given any first-order theory $T$, we allow each step in a proof to be either derivation of a formula or sentence as per normal or extension of $T$ by adding a fresh constant or function or predicate symbol and an axiom defining it. Specifically:

• Given a $1$-parameter sentence $φ$ over $T$ such that $T \vdash \exists x\ ( φ(x) )$, we can extend $T$ by adding a constant symbol $c$ and an axiom $φ(c)$.

• Given a $k+1$-parameter sentence $φ$ over $T$ such that $T \vdash \forall x_{1..k}\ \exists! y\ ( φ(x_{1..k},y) )$ then we can extend $T$ by adding a $k$-input function symbol $f$ and an axiom $\forall x_{1..k},y\ ( f(x_{1..k})=y \eq φ(x_{1..k},y) )$.

• Given a $k$-parameter sentence $φ$ over $T$ then we can extend $T$ by adding a predicate symbol $P$ and an axiom $\forall x_{1..k}\ ( P(x_{1..k}) \eq φ(x_{1..k}) )$.

This is how definitions are incorporated into normal first-order theories. Your question is too vague to be answered, because a formal system must be precisely syntactically specified before it can be discussed. Just for example, here are some responses to your enquiries:

he has taken the terms binary relation, set, existence and definability as primitive notions of his Set Theory

"primitive notions" always come with axiomatizations of those notions. What on earth are those axioms?

whenever a relation R is definable from a set A to a set B we will write R:A→B.

Is this an axiom or not? Furthermore, he didn't define "whenever" and "a" and "is" and "from" and "to" and "we" and "will write"...

Let R and S be two relations.

What if I don't believe there are even two relations?

How does he preserve the order property of binary relations that is found in other set theories (at least in ZFC)?

What order property are you talking about?

I have never seen for any theory (at least the theories which I know) to take the concepts existence and definability considering as primitive concepts. Can we take those as primitive concepts of a theory? Why?

Erm... First-order theories all take for granted first-order logic, which includes as primitive notions negation, conjunction, disjunction, existential quantification, universal quantification, equality, functions, predicates and brackets. How can you say that existence is not a primitive concept? What existence are you talking about?

The bottom line is that formal systems are very precise things in logic, and not vague things like in philosophy. I recommend you read up on logic, say starting with the books I mention in this post, and after that read this post about how one can build formal systems from scratch (well not entirely from scratch because that's impossible).