Patrick Suppes' "Introduction to Logic" provides rules for formal definitions in chapter 8. 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 a prior mention of the Law of Identity:
If x is anything whatsoever, then $x=x$.
Now let's suppose that you have the following definition:
$$
\forall f,x,y[f_x = y \iff f \text{ is a function } \land \langle x,y \rangle \in f]
$$
Let's also assume that you have previously defined functions and ordered pairs such that you may prove $\exists !y[S]$ with extentionality, so it follows rule (iv).
Here's the problem: Within the bounds of this ruleset, it seems like one can use the Law of Identity with any variable, say $A$, to claim that $A_x=A_x$ and use that to claim that $A \text{ is a function } \land \langle x,A_x \rangle \in A$, and so, that $A$ is a function, even though we know nothing about it. That logic can be used with any variable, be it a normal relation, a simple set, or even a urelement, so this deduction must be wrong.
At first, I thought I was breaking rule (iii), as the statement "$A \text{ is a function } \land \langle x,A_x \rangle \in A$" has a not previously defined symbol in it, $A_x$, which is defined in the statement itself, so it would not be valid.
However, consider the following definition:
$$
\newcommand\liff{\leftrightarrow}
\newcommand\lif{\rightarrow}
\newcommand\lfi{\leftarrow}
\newcommand\ordp[2]{\langle #1,#2 \rangle}
\newcommand\mset[1]{\{ #1 \}}
\newcommand\isRel[1]{#1 \text{ is a relation}}
\newcommand\isFunc[1]{#1 \text{ is a function}}
\newcommand\isOneOne[1]{#1 \text{ is one-one}}
\mset{a} = p \iff \forall x[x \in p \liff x = a]
$$
It is unique by extentionality. It seems a clear consequence from it that $\mset{a} = \mset{b} \lif a = b$, but the only way I see to prove it is by using $\mset{a} = \mset{b}$ to get $\forall x[x \in \mset{b} \liff x = a]$, which would be disallowed if my interpretation was correct, so I don't think that is the answer.
My second instinct was that rule (i) is being broken, that $f_x = f_x$ doesn't count as being distinct variables. However, from the definition above it also seems that $a \in \mset{a}$ should follow. The only way I see to prove this is to use $\mset{a} = \mset{a}$ with the definition, which would be disallowed if this was the case, so I don't feel that's the solution either.
So my question is: What is the actual culprit of the fallacy?
Edit: After extended discussion, I'm adding some information to hopefully clarify what this question is and is not about.
This is not about set theory. My problem is with about the formal language of first-order logic provided by the book. To avoid the focus on set theory, I'll provide a second example. Let's suppose we have the following statements:
$$
\forall a,b,x,y[\text{isSingleChild}(x) \land \text{parentsOf}(a,b,x) \land \text{parentsOf}(a,b,y) \Rightarrow x = y] \\
\forall a,b,x[\text{son}\{a,b\} = x \iff \text{isAdult}(a) \land \text{isAdult}(b) \land \text{parentsOf}(a,b,x) \land \text{isSingleChild}(x)]
$$
The first statement guarantees that $x$ is unique in the definition of $\text{son}$.
The definition of $\text{son}\{a,b\}$ seems to follow all of the rules provided. It is not intended to state that any variable follows any specific predicate, but simply stating their logical relationship. However, if you use it together with the Law of Identity, you may derive:
$$
\newcommand{\fitch}[1]{\begin{array}{rlr}#1\end{array}}
\newcommand{\fcol}[1]{\begin{array}{r}#1\end{array}} %FirstColumn
\newcommand{\scol}[1]{\begin{array}{l}#1\end{array}} %SecondColumn
\newcommand{\tcol}[1]{\begin{array}{l}#1\end{array}} %ThirdColumn
\newcommand{\subcol}[1]{\begin{array}{|l}#1\end{array}} %SubProofColumn
\newcommand{\subproof}{\\[-0.25em]} %adjusts line spacing slightly
\newcommand{\fendl}{\\[0.037em]} %adjusts line spacing slightly
\small
\fitch{
\fcol{1:\fendl 2:\fendl 3:\fendl\fendl 4:\fendl 5:\fendl 6:\fendl 7:\fendl 8:\fendl
}
& \scol {
\forall a,b,x[\text{son}\{a,b\} = x \iff \text{isAdult}(a) \land \text{isAdult}(b) \land \text{parentOf}(a,b,x) \land \text{isSingleChild}(x)] \\
\forall x[\text{son}\{a,b\} = x \iff \text{isAdult}(a) \land \text{isAdult}(b) \land \text{parentOf}(a,b,x) \land \text{isSingleChild}(x)] \\
\text{son}\{a,b\} = \text{son}\{a,b\} \\\quad\iff \text{isAdult}(a) \land \text{isAdult}(b) \land \text{parentOf}(a,b,\text{son}\{a,b\}) \land \text{isSingleChild}(\text{son}\{a,b\}) \\
\forall x[x = x] \\
\text{son}\{a,b\} = \text{son}\{a,b\} \\
\text{isAdult}(a) \land \text{isAdult}(b) \land \text{parentOf}(a,b,\text{son}\{a,b\}) \land \text{isSingleChild}(\text{son}\{a,b\}) \\
\text{isAdult}(a) \\
\forall a [\text{isAdult}(a)] \\
}
& \tcol{
\text{P} \fendl
1\ \forall\text{E}\ \fendl
2\ \forall\text{E}\ \fendl\fendl
\text{T}\ \fendl
4\ \forall\text{E}\ \fendl
3,5\ {\liff}\text{E}\ \fendl
6\ {\land}\text{E}\ \fendl
7\ \forall\text{I}\ \fendl
}}
$$
So from that definition, you may deduce that everyone is an adult. Note what I am not saying. I'm not saying that this argument is sound, nor defending it, I'm saying that the ruleset given in the book permits it (It probably doesn't, but I don't see any rule of logical deduction being broken). I know the argument is illogical, but the formal rules are being followed. My question is not about the soundness of the argument, but the soundness of the system provided in the book.
Also note that the assertion is not about set theory, nor "family theory", it is about the logic itself. My assertion is that (apparently) within the formal system given, any statement of the following form applies:
$$
\forall a,b,x[\text{entityFrom}\{a,b\} = x \iff \text{hasSomeProperty}(a) \land \text{uniqueRelation}(a,b,x)] \vdash \forall a[\text{hasSomeProperty}(a)]
$$
I understand that the definition doesn't entail the conclusion. Nonetheless, within the system, the conclusion seems to be deducible from it.
There are only three options. Either the formal system provided in not sound, the definition actually entails the conclusion, or I'm missing/misinterpreting some rule on the Law of Identity/Rules for Definition/Rules for Quantifiers.
The book and is more than 50 years old, any possible oversights in the system would have been noticed by this point (it also was written by Suppes, so I doubt there is any), thus I'm sure it's not the first one. The definitions also seem well formed and feel like they shouldn't lead directly to the conclusion, so it's probably not the second one as well. Leading to the conclusion that I am probably missing or misinterpreting some proviso/rule that would make that argument not valid. The question is, which one?
What will not answer the question:
- "In set theory, functions have a specific domain and need to have [some set properties], so it is not possible for all variables to be functions."
- "Your definition of parenthood does not describe the idea of parents correctly, as it does not imply that all children have parents and [some parenthood properties], so the definitions are not correct descriptions."
The solution cannot be about the unsoundness of the argument in one specific theory, that will not get to the root of the problem. A specific context may be used as an example, but the solution has to be on the level of the formal language.
What might answer the question:
- "The ruleset given by the book is actually incomplete, because a definition with equality containing [some syntatic property] may lead to a fallacy. However, you may avoid it by adding a new rule that requires your definition to have [new definition contraint]"
- "Your definitions logically entail the conclusion. Think about it, if your definition is [this], then [explanation of why the definition should logically lead to the conclusion], so the argument and conclusion are valid. I doubt that's what you intended to conclude with your definition though. I think what you actually mean is [well behaved definition]." $^{\dagger}$
- "You've misinterpreted rule [n], perhaps you think it means [interpretation] when it actually says [different interpretation]. If you take that into account, line [x] of your argument is not valid."
- "You are forgetting that you cannot substitute for defined terms like you do variables. You can only substitute for a defined term if [some syntatic condition] applies, so step $3$ of your deduction is invalid."
- "The Law of Identity does not require only uniqueness, but also [some variable property], so you may not use it as in line $5$, since the variable in your definition doesn't follow this constraint."
Your answer need not be any of the above. I'm just presenting the types of answers I feel will most likely be useful: Answers that focus on the formal language.
Thank you for reading till the end, and I hope this makes clear enough the problem I'm wanting to solve.
$\dagger$ As pointed out by Mauro ALLEGRANZA, this case specially makes sense. As he put it:
Think about it: is there some axioms in your theory saying that not every object is an Adult?
Which I agree with. However, there's one problem: The ruleset shouldn't allow this.
Earlier in the same chapter, before the rules are established, their objective is laid out. The "Criteria for proper definitions". The objective is to separate an axiom from a definition. The first one (Criterion of Eliminability) is not important for this discusion, but the second is.
The Criterion of Non-Creativity states that a definition $S$ is non-creative if and only if:
There is no formula $T$ in which the new symbol does not occur such that $S \rightarrow T$ is derivable from the axioms and preceding definitions of the theory but $T$ is not so derivable.
The objective of the ruleset is to guarantee that our definitions follow both of these criteria. As stated in page 155: "[…] we turn to the task of stating rules of definition which will guarantee satisfacition of the two criteria of eliminability and non-creativity"
In my parenthood example, we have the first statement as an axiom, and the second as a definition. However, within that theory, the statement $\forall a [\text{isAdult}(a)]$ does not contain the new symbol and is derivable from the new definition, but not from the axioms alone, which would make the definition creative.
So in that case, my question then becomes: How come the definition is creative, when the ruleset is supposed to guarantee non-creativity?
Best Answer
The ruleset given by the book is not incomplete. The example derivation you give holds up to scrutiny as well. You get (seemingly) paradoxical conclusions because restriction (iv) does not actually hold in any of your examples.
In your first example, the formula $S$ denotes the following: "$v_2 \text{ is a function } \wedge \langle v_1,w \rangle \in v_2$". So restriction (iv) is not satisfied unless the following is a theorem of the theory under consideration:
$$\exists! w. v_2 \text{ is a function } \wedge \langle v_1,w \rangle \in v_2 $$
which, since $v_1,v_2$ are distinct free variables, holds precisely if
$$\forall v_1. \forall v_2. \exists! w. v_2 \text{ is a function } \wedge \langle v_1,w \rangle \in v_2 $$
is a theorem of your theory as well. Needless to say, this latter statement is very much not a theorem of any reasonable set theory. In particular it would imply "$\forall v. v \text{ is a function }$" by itself.
In your second example, the formula $S$ denotes the following: "$\text{isAdult}(v_1) \wedge \text{isAdult}(v_2) \wedge \text{parentsOf}(v_1,v_2,w) \wedge \text{isSingleChild}(w)$". As above, restriction (iv) is not satisfied unless the following is a theorem of the theory under consideration:
$$ \forall v_1. \forall v_2. \exists! w. \text{isAdult}(v_1) \wedge \text{isAdult}(v_2) \wedge \text{parentsOf}(v_1,v_2,w) \wedge \text{isSingleChild}(w) $$
But if the sentence given above is a theorem of your theory, then you can already prove (directly, starting from the sentence above as a premise, and using $\forall E$, $\wedge E$ and $\forall I$) that $\forall v_1. \text{isAdult}(v_1)$ is a theorem of your theory.