/sci/ - Science & Math

>>11772160
Why not.
Do 20 minutes.


>>11772089
Bishops theory makes use of some choice and Brouwers intuitionism doesn't even have a formal logic, pic related (but it a student of his said fuck this guy and formalized it)

The number 3 >>11772216 is the Existence Property, and a bit harder to prove metalogically for some theories.
If you read it it says:

A theory has this property, if when
[math] \exists x. P(x) [/math]
is provable for some predicate, then there's actually a describing predicate [math] X [/math] (a mathematical statement that expresses a property), such that the theory T also proves
[math] \exists !x. X(x)\land P(x) [/math]

I.e. for a nice theory that has the existence property, it can't happen that it's provable that [math] \exists x. P(x) [/math] but this [math] x [/math] that's provable to exist can't actually be described (such as some quirky orderings that "exist" by the axiom of choice, but can't really be talked about as such, here's a SE question relating to that example btw., but of course that's just one example - https://math.stackexchange.com/questions/6501/is-there-a-known-well-ordering-of-the-reals))

If you want to know a weak variant of ZF that has the existence property, here's the axioms (no LEM assumed):
- Extensionality (having equal members implies equality) - this is also part of ZF
- Pairing (the pair {x,y} exist for each set x and y) - this is also part of ZF
- Union (the union in a set exists) - this is also part of ZF
- Bounded Separation (cut out new sets from bigger ones, but don't use \forall ranging over the whole universe) - ZF has a strong version of this (not predicative)
- Strong Infinity (an infinite set exists) - a variant of the infinity axiom that ZF also has/proves
- Strong Collection (generate sets with relation predicates) - a strong variant of replacement, I think ZF also proves this
+ Exponentiation (function spaces exist) - a weak version of power set