What is it that we are missing in defining the following in the following manner? Recently one of my friend and I are working on a project on a certain generalization of set theory. This is the same friend of mine of whom I talked in this post. However, the basic outline of his (modified) theory is as follows,

As usual, the logical symbols of our alphabet are,

*

*the quantifiers $\exists$ and $\forall$.


*the logical connectives  $\land,\lor,\iff,\implies$ and $\neg $.


*Parentheses, brackets, and other punctuation symbols.


*An infinite collection of variables which intuitively represents what we call abstract objects, a sub-collection of which is divided further into three sub-collections, namely mathematical objects, ordered objects and relational objects. We denote the variables representing mathematical objects by $a,b,c,A,B,C,\ldots$, the variables representing ordered objects by $\alpha,\beta,\gamma,\Phi,\Psi,\Theta,\ldots$, the variables representing relational objects by $\mathfrak{a,b,c,A,B,C,\ldots}$


*An equality symbol (sometimes, identity symbol) $=$.
and the non-logical symbols of our alphabet are,

*

*A predicate symbol $\color{crimson}{\text{P}}$ (or relation symbol) with number of arguments $2$.

Now we say that a relational objects $\mathfrak{R}$ is definable from $a$ to $b$ if, $$(\color{crimson}{\text{P}}ab)\land(\exists\gamma)[\color{crimson}{\text{P}}\gamma a\land \color{crimson}{\text{P}}\gamma b\land (\mathfrak{R}=\gamma)]$$

My question is can we do that? I have a feeling that my friend is missing something but since I am not so expert in formal logic, I can't say anything precisely on this matter.
Can anyone help?
 A: If your friend is attempting to construct a usable formal system, then it is necessarily one that can be implemented by a program. You need a program that given any input strings $p,x$ will always halt and output whether $p$ is a valid proof of $x$ (representing a theorem) or not. If you cannot see how this can be done (at least in theory), then it is unlikely that you have described any usable formal system at all.
As I suggested in my answer to your previous question, you should study logic and existing formal systems first before you attempt to build your own. Little of your question as stated makes sense, precisely because you're not precise enough:


*

*You say there are different kinds of objects. In logic that is called "sorts", and you need to specify clearly how various sorts interact.

*What are the inference rules for "P"?

*Is "definable" an internal symbol in your system or not?
It is not sufficient to be able to answer these questions in an intuitive way; you have to describe purely syntactical deterministic procedures, that can be unambiguously executed by anyone who can follow instructions on paper to manipulate strings, and will result in a definite conclusion to whether or not a purported proof $p$ of a purported theorem $x$ is valid or not. There must be no reliance at all on intuition or any mathematical knowledge.
Only after you have pinned down the syntax of your formal system in this way is it then possible for us to talk about it. In particular, we would then be interested in its semantics, namely whether or not there is a reasonable interpretation of the provable theorems. This is a completely separate question from that of syntactic consistency. For example in first-order logic a theory is said to be consistent iff it cannot prove a sentence of the (syntactic) form "$P \land \neg P$". As I mentioned in the post I linked to from my other answer, this only requires a weak meta-system to define. But if you have a strong enough meta-system you can further talk about models of a theory and can prove that consistency implies the existence of a model.
Yet consistency is not going to be enough if you desire a formal system that is foundational in any sense. Note that $PA + \neg Con(PA)$ is consistent but proves itself inconsistent, so it is simply useless for a foundation for mathematics or philosophy. What at least you would need for a system to be justifiable as foundational is that it has an ω-model, which at implies both arithmetical soundness and ω-consistency.
