$%PREAMBLE

newcommand{fitch}(1){begin{array}{rlr}#1end{array}}

newcommand{fcol}(1){begin{array}{r}#1end{array}} %FirstColumn

newcommand{scol}(1){begin{array}{l}#1end{array}} %SecondColumn

newcommand{tcol}(1){begin{array}{l}#1end{array}} %ThirdColumn

newcommand{subcol}(1){begin{array}{|l}#1end{array}} %SubProofColumn

newcommand{subproof}{\(-0.3em)} %adjusts line spacing slightly

newcommand{fendl}{\(0.037em)} %adjusts line spacing slightly

$

In the logic book I’m reading (Introduction to Logic by Patrick Suppes) some rules for formal definitions are established. The rules below are specified for a new operation symbol with equality:

An equivalence $D$ introducing a new n-place operation symbol $O$ is a proper definition in a theory if and only if $D$ is of the form:

$O(v_1, …, v_n) = w leftrightarrow S$

and the following restrictions are satisfied:

(i) $v_1, …, v_n, w$ are distinct variables.

(ii) $S$ has no free variables other than $v_1, …, v_n, w$.

(iii) $S$ is a formula in which the only non-logical constants are primitive symbols and previously defined symbols of the theory.

(iv) The formula $exists !w(S)$ is derivable from the axioms and preceding definitions of the theory.

There’s also mention of the *Law of Identity*:

If x is anything whatsoever, then $x=x$.

So, to stretch my understanding of these rules, I’ve made some elementary set theory definitions:

*Note: Extentionality is assumed as part of the theory.*

$$begin{array}{l}

text{(1)}: A text{ is a relation } leftrightarrow forall v(v in A rightarrow exists x exists y(v = langle x,y rangle)) \

text{(2)}: v in A^c leftrightarrow A text{ is a relation } land exists x exists y (v = langle y,x rangle land langle x,y rangle in A)\

text{(3)}: f text{ is a function } leftrightarrow f text{ is a relation } land forall x forall y forall z (langle x,y rangle in f land langle x,z rangle in f rightarrow y=z) \

text{(4)}: f text{ is one-one } leftrightarrow f text{ is a function } land forall x forall y forall z (langle x,z rangle in f land langle y,z rangle in f rightarrow x=y) \

text{(5)}: x in f^{-1} leftrightarrow x in f^c land f^c text{ is one-one } \

text{(6)}: f(x) = y leftrightarrow f text{ is a function } land langle x,y rangle in f

end{array}$$

However, after playing with those a bit (developing proofs of commonly known facts) I’ve noticed a problem. Within the bounds of this ruleset, it seems like one can use the *Law of Identity* to claim that $f(x)=f(x)$ and use that to claim that $f$ is a function, even though we know nothing about it. This is of course nonsense, as that logic can be used even with a variable that is not a function, leading to a contradiction.

The definition $(6)$ seems right, as from it you can prove that $y$ is unique. So my question is: What went wrong here?

Is my definition breaking any of the rules, am I missing some provisio on the *Law of Identity*, is the ruleset not complete, or is it something else entirely?