New answers tagged foundations
-1
votes
Accepted
Is Bounding Reflection consistent?
Bounding reflection is a theorem scheme of $\sf ZFC$.
For any formula $\varphi$ having all its free variables among $v_1, \dots, v_n$, we can get an equivalent formula "$(\exists x_1: x_1=v_1 \...
5
votes
Accepted
Does inductive definitions must be supported by the set theoretical definition of natural numbers?
It depends on whether you wish to define a finite ordered tuple, say, a $3$-tuple $w=(x,y,z)$ at the metalanguage level or at the object language level.
In the first case, saying $w=(x,y,z)$ is simply ...
1
vote
Can this form of reflection be consistent?
Edit, Mar 3: After some discussion with Zuhair Al-Johar, the full answer (that $\mathrm{Reflection}^*$ is a theorem schema of $\mathrm{ZFC}$) appears in the last line of this answer.
Here is a partial ...
8
votes
Accepted
What is the proof of consistency of anterior reflection?
This is a consequence of ZF as follows.
Assume that all quantifiers of $\varphi$ appear at the front as in the normal forms. Suppose that $\varphi(\vec v)$ has complexity at most $\Sigma_n$ for some ...
5
votes
Accepted
Is this form of replacement suitable for ZF - Powerset + well-ordering principle?
The answer is no.
Your version of replacement is a weakening of ordinary replacement. To see this assume that replacement holds (but perhaps not power set or collection), and then observe that for any ...
6
votes
What's the earliest result (outside of logic) that cannot be proven constructively?
A somewhat different type of example, not as early as the ones in Andrej Bauer's answer, but perhaps a bit more resistant to "moving the goalposts," is an ineffective result in number theory....
-1
votes
What's the earliest result (outside of logic) that cannot be proven constructively?
IIRC "If two angle bisectors of a triangle are congruent, then the triangle is isoscles." is a theorem that has only been proven non-constructively.
16
votes
What's the earliest result (outside of logic) that cannot be proven constructively?
According to Wikipedia, in 5th century BCE, Bryson of Heraclea spoke of a special case of the intermediate value theorem. If we're very generous, that would be an early occurrence of a constructively ...
5
votes
In HoTT with LEM, are sets and pointed sets the same thing?
I will give a somewhat philosophical answer, which is no, in HoTT with LEM, pointed sets and sets are not the same thing. That is when you are working in HoTT, you always know when you are working ...
7
votes
Is univalence equivalent to every type function being a functor over equivalence?
Your axiom does not entail univalence.
It is consistent to add to type theory the isomorphism reflection rule
$$\frac{\Gamma \vdash e : A \simeq B}{\Gamma \vdash A \equiv B}$$
which states that ...
Top 50 recent answers are included
Related Tags
foundations × 311lo.logic × 186
set-theory × 145
ct.category-theory × 57
mathematical-philosophy × 43
reference-request × 29
soft-question × 26
type-theory × 22
model-theory × 21
axioms × 21
homotopy-type-theory × 18
proof-theory × 17
constructive-mathematics × 15
theories-of-arithmetic × 14
ho.history-overview × 12
reverse-math × 9
ordinal-analysis × 9
mg.metric-geometry × 8
computability-theory × 8
large-cardinals × 8
ordinal-numbers × 8
topos-theory × 7
ultrafinitism × 7
higher-category-theory × 6
metamathematics × 6