New answers tagged

-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 \...
Zuhair Al-Johar's user avatar
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 ...
Burak's user avatar
  • 4,105
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 ...
C7X's user avatar
  • 1,176
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 ...
Joel David Hamkins's user avatar
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 ...
Joel David Hamkins's user avatar
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....
Timothy Chow's user avatar
-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.
ralphmerridew's user avatar
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 ...
Andrej Bauer's user avatar
  • 47.7k
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 ...
Max New's user avatar
  • 785
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 ...
Andrej Bauer's user avatar
  • 47.7k

Top 50 recent answers are included