Frege's theorem in a constructive setting
By Frege's Theorem is meant the result, implicit in Frege's Grundlagen, that, for any set \(E\), if there exists a map \(v\) from the power set of \(E\) to \(E\) satisfying the condition \[ \forall XY[v(X)= v(Y)\leftrightarrow X\approx Y], \] then \(E\) has a subset which is the domain of a model of Peano's axioms for the natural numbers, where we write \(X\approx Y\) for ``there exists a bijection between \(X\) and \(Y\), and, more generally, \(f: X\approx Y\) for ``\(f\) is a bijection between \(X\) and \(Y\). (This result is proved explicitly, using classical reasoning, in Section 3 of the author's earlier paper [ibid. 60, No. 1, 209-221 (1995; Zbl 0829.03004)].) My purpose in this note is to strengthen this result in two directions: first, the premise will be weakened so as to require only that the map \(v\) be defined on the family of (Kuratowski) finite subsets of the set \(E\), and secondly, the argument will be constructive, i.e., will involve no use of the law of excluded middle. To be precise, we will prove, in constructive (or intuitionistic) set theory, the following: Theorem. Let \(v\) be a map with domain a family of subsets of a set \(E\) to \(E\) satisfying the following conditions: (i) \(\varnothing\in \text{dom}(v)\), (ii) \(\forall U\in \text{dom}(v) \forall x\in E-U\), \(U\cup x\in\text{dom}(v)\), (iii) \(\forall UV\in \text{dom}(v)\), \(v(U)= v(V)\Leftrightarrow U\approx V\). Then we can define a subset \(N\) of \(E\) which is the domain of a model of Peano's axioms.
- scientific article; zbMATH DE number 1550353
- scientific article; zbMATH DE number 5964375
- Frege's theorem
- Fregean Description Theory in Proof-Theoretical Setting
- A Logic for Frege’s Theorem
- Some free constructions in realizability and proof theory
- scientific article; zbMATH DE number 832104
- scientific article; zbMATH DE number 1550354
- Frege's Theorem and the Peano Postulates
- A constructive consistency proof of a fragment of set theory
- Frege's double correlation thesis and Quine's set theories NF and ML
- FRAGMENTS OF FREGE’SGRUNDGESETZEAND GÖDEL’S CONSTRUCTIBLE UNIVERSE
- FREGE MEETS BROUWER (OR HEYTING OR DUMMETT)
- scientific article; zbMATH DE number 4099273 (Why is no real title available?)
- scientific article; zbMATH DE number 1195909 (Why is no real title available?)
- scientific article; zbMATH DE number 832104 (Why is no real title available?)
- Finite sets and frege structures
- Fregean Description Theory in Proof-Theoretical Setting
- THE POTENTIAL IN FREGE’S THEOREM
This page was built for publication: Frege's theorem in a constructive setting
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4262566)
