/sci/ - Science & Math

>>10855748
Just googled "Existential introduction for Hilbert calculus" and found the answer with 4 upvotes here
https://mathoverflow.net/questions/116671/existential-instantiation-in-hilbert-style-deduction-systems
saying that if
B(a) |-> S
for a particular, then the introduction weakens it as
(exists y) B(y) |-> S

Example:
If your mom gets banged by your neighbor means you'll soon have a new sister, then there is someone such that if he bangs your mom, you'll soon have a new sister.
The second sentence being weaker, as there's less info on who does the banging.

From this, I presume the proof will eventually look something along those lines:

1. [math] (\forall x) (x=x) [/math] (refl)
2. [math] a=a [/math] (a particular via 1.)
3. [math] b=a [/math] (introduce b)
4. [math] a=b [/math] (flip 3)
5. [math] (\exists y) a=y [/math] (via exists introduction, what above I called weakening)
6. [math] (\forall x) (\exists y) x=y [/math] (via forall introduction aka generalization)

pic related is your neighbor

>>10850392
for "crash course", watch this Vsauce clip and then come back with concrete questions.

https://youtu.be/SrU9YDoXE88

For theories with power set axiom, you usually get high but when you can't go further, you add a new axiom.
The most conservatzive studied set theory is
https://en.wikipedia.org/wiki/Kripke%E2%80%93Platek_set_theory
and then you usually add the countable infinite and with the power set you get the classical ZF theory.
If you want more you may add
https://en.wikipedia.org/wiki/Grothendieck_universe
and/or
https://en.wikipedia.org/wiki/Tarski%E2%80%93Grothendieck_set_theory
etc.