Timeline for Is this set theory used by Gandy first-order with signature $(\in, \lambda)$?
Current License: CC BY-SA 4.0
16 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Mar 26, 2021 at 2:42 | vote | accept | Frode Alfson Bjørdal | ||
| Mar 22, 2021 at 21:56 | answer | added | Zuhair Al-Johar | timeline score: 3 | |
| Mar 22, 2021 at 21:45 | history | edited | Frode Alfson Bjørdal | CC BY-SA 4.0 |
)
|
| Mar 22, 2021 at 7:56 | history | edited | YCor | CC BY-SA 4.0 |
formatting
|
| Mar 22, 2021 at 0:56 | history | edited | Frode Alfson Bjørdal | CC BY-SA 4.0 |
Elaborated title
|
| Mar 22, 2021 at 0:09 | history | edited | Frode Alfson Bjørdal | CC BY-SA 4.0 |
added 2 characters in body
|
| Mar 21, 2021 at 23:54 | history | edited | Frode Alfson Bjørdal | CC BY-SA 4.0 |
[Edit removed during grace period]
|
| Mar 21, 2021 at 23:52 | comment | added | Frode Alfson Bjørdal | 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." | |
| Mar 21, 2021 at 23:47 | comment | added | François G. Dorais | The problem with equality is correctly translating $x = \lambda z\,\phi(z)$ which is where extensionality comes into play... | |
| Mar 21, 2021 at 23:46 | comment | added | François G. Dorais | 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. | |
| Mar 21, 2021 at 23:42 | comment | added | Frode Alfson Bjørdal | @FrançoisG.Dorais 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 \land \phi(x))$. I will edit this into the question. | |
| Mar 21, 2021 at 23:38 | history | edited | Frode Alfson Bjørdal | CC BY-SA 4.0 |
Gandy does have identity. It is [...].
|
| Mar 21, 2021 at 23:22 | comment | added | François G. Dorais | @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.) | |
| Mar 21, 2021 at 23:05 | comment | added | James E Hanson | 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. | |
| Mar 21, 2021 at 22:34 | history | edited | Frode Alfson Bjørdal | CC BY-SA 4.0 |
doi
|
| Mar 21, 2021 at 22:25 | history | asked | Frode Alfson Bjørdal | CC BY-SA 4.0 |