In On the Axiom of Extensionality, Part II, The Journal of Symbolic Logic, Vol. 24, No. 4 (Dec., 1959), https://doi.org/10.2307/2963897, pp. 287-300, R. O. Gandy shows that a class theory X containing NBG minus extensionality is not weaker than NBG; X includes a use of class-abstraction denoted with $\lambda$, so that $\lambda x(x=x)$ is a universal class. Gandy does have identity. It is worth noticing that one can show (use A2 p. 289 and I29 p. 290) that $x\in \lambda z\phi(z)\leftrightarrow \exists y(x\in y)\wedge\phi(x)$. Is X a first-order theory with signature $(\in, \lambda)$?
$\begingroup$
$\endgroup$
6
asked Mar 21, 2021 at 22:25
-
5$\begingroup$ First-order logic is usually not defined in a way that would allow for an operator that turns formulas into terms. This formalism can be encoded in first-order logic, but would require a larger language with a function symbol for each $\lambda$ expression. $\endgroup$– James E HansonCommented Mar 21, 2021 at 23:05
-
1$\begingroup$ @JamesHanson is completely correct, but adding $\lambda$ is a definitional extension: recursively replace $x \in \lambda z\phi(z)$ by $\phi(x)$ to obtain an equivalent first-order formula for the $\in$-language. I forget exactly how Gandy approaches it, but this does not work for the language with equality but it does work if $x = y$ is interpreted in the $\in$-language as $\forall z(z \in x \leftrightarrow z \in y)$. (IIRC, this is one of Gandy's key observations.) $\endgroup$– François G. DoraisCommented Mar 21, 2021 at 23:22
-
1$\begingroup$ You're right, the correct translation for $x \in \lambda z\,\phi(z)$ is $\exists y(x \in y \land \phi(z))$ since we need to ensure that $x$ is a set and not a proper class. $\endgroup$– François G. DoraisCommented Mar 21, 2021 at 23:46
-
1$\begingroup$ The problem with equality is correctly translating $x = \lambda z\,\phi(z)$ which is where extensionality comes into play... $\endgroup$– François G. DoraisCommented Mar 21, 2021 at 23:47
-
1$\begingroup$ From Gandy's extract on doi.org/10.2307/2963897: "In this paper it is shown that, if a certain form of Gödel-Bernays set theory which does not include the axiom of extensionality is consistent, then so is the whole system of set theory. The general line of argument is similar to that used in Part I. § 1 describes a reformulation of set theory in which the class-existence axioms are replaced by the use of abstracts." $\endgroup$– Frode Alfson BjørdalCommented Mar 21, 2021 at 23:52
|
Show 1 more comment
1 Answer
$\begingroup$
$\endgroup$
19
A signature of first order logic is usually taken to be a list of extra-logical symbols that range over specific elements (for constants) or over specific subsets (for n+1 ary functions, predicates) of the universe of discourse. The class-abstraction symbol $\lambda$ here doesn't fit into any of those. I'm not sure if it can be considered among symbols of the underlying logic, but by then that kind of logic won't be called just first order, one may call it first order logic with class-abstractions, or something to that effect. That said, I think the signature of Gandy's theory if described in terms of first order logic then it would be very extensive (in agreement with comment by James Hanson), so if $ \{x_i: i \in \mathbb N \}$ is the set of all variable symbols in a langauge, and $\{\phi_j(x_i): i,j \in \mathbb N \}$ is the set of all formulas in one free variable in the language then the signature would be something like: $(=,\in, \lambda x_i \phi_j(x_i): i,j \in \mathbb N)$, a countably infinite signature! Where each $\lambda x_i \phi_j(x_i)$ is a constant (zero place function) symbol, i.e. an argumentless (doesn't take an element of the universe of discourse as argument) expression that range over a single element of the universe of discourse. However, if $n$ many free variables other than $x_i$ are allowed to occur in $\phi_j(x_i)$, then the expression $\lambda x_i \phi_j(x_i)$ would become an $n$-ary function symbol. In nutshell X is a first order theory with signature $(=,\in, \lambda x_i \phi_j(x_i): i,j \in \mathbb N)$
answered Mar 22, 2021 at 21:56
-
$\begingroup$ Gandy's theory X seems to be precisely NBG-set theory without extensionality plus set abstracts. NBG is first order. Notice, as I point out in the last paragraph of the question, that the $\lambda-terms$ do not in general support the naive abstraction schema. Let for instance $R$ be $\lambda y(y\notin y)$. We will have $\forall x(x\in R\leftrightarrow(\exists y(x\in y)\wedge x\notin x)$, so $R\notin R$ and $\lnot \exists y(R\in y)$. So the extensions of the lambda-terms do not correspond exactly to the defining conditions. Why should we think that X is not first order? $\endgroup$ Commented Mar 23, 2021 at 16:51
-
$\begingroup$ @FrodeAlfsonBjørdal, I don't understand the question in your comment. OF course X is first order but its first order with the extensive signature I've written, it is an extension of first order language with $\lambda x_i \phi_j(x_i)$ constants. $\endgroup$ Commented Mar 23, 2021 at 18:13
-
$\begingroup$ @FrodeAlfsonBjørdal, is the first order language Gandy use for NBG-Extensionality theory mono-sorted or bi-sorted? $\endgroup$ Commented Mar 23, 2021 at 18:16
-
2$\begingroup$ Why is $\lambda x_i\,\phi_j(x_i)$ a constant? Does that mean that $\phi_j$ has no free variables other than $x_i$? Why can't we have free variables here? $\endgroup$ Commented Mar 23, 2021 at 22:57
-
1$\begingroup$ In sum, may the signature be $(=,\in,\lambda x_i\phi_j)$, $i, j\in \mathbb{N}$, where $\{\phi_j|j\in\mathbb{N}\}$ is the set of all formulas (primitive propositional functions, p. 288)? $\endgroup$ Commented Mar 24, 2021 at 2:50