$%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?
