Return to Question

What is the name of the following property that a system $T$?

If $\vdash_{T}\exists x F(x)$ then there is a term $a$ such that $\vdash_{T} F(a)$

If I recall correctly Heyting Arithmetics has the property, and clearly also Omega Logic has it. Are there other important examples?

What is the name of the following property of a system $T$?

If $\vdash_{T}\exists x F(x)$ then there is a term $a$ such that $\vdash_{T} F(a)$

If I recall correctly Heyting Arithmetics has the property, and clearly also Omega Logic has it. Are there other important examples?

What is the name of the property that a system $T$ has if $\vdash_{T}\exists x F(x)$ only if there is a term $a$ so that $\vdash_{T} F(a)$?

If I recall correctly Heyting Arithmetics has the property, and clearly also Omega Logic has it. Are there other important examples?

What is the name of the following property that a system $T$?

If $\vdash_{T}\exists x F(x)$ then there is a term $a$ such that $\vdash_{T} F(a)$

If I recall correctly Heyting Arithmetics has the property, and clearly also Omega Logic has it. Are there other important examples?