Metamath Proof Explorer


Theorem hta

Description: A ZFC emulation of Hilbert's transfinite axiom. The set B has the properties of Hilbert's epsilon, except that it also depends on a well-ordering R . This theorem arose from discussions with Raph Levien on 5-Mar-2004 about translating the HOL proof language, which uses Hilbert's epsilon. See https://us.metamath.org/downloads/choice.txt (copy of obsolete link http://ghilbert.org/choice.txt) and https://us.metamath.org/downloads/megillaward2005he.pdf .

Hilbert's epsilon is described at http://plato.stanford.edu/entries/epsilon-calculus/ . This theorem differs from Hilbert's transfinite axiom described on that page in that it requires R We A as an antecedent. Class A collects the sets of the least rank for which ph ( x ) is true. Class B , which emulates Hilbert's epsilon, is the minimum element in a well-ordering R on A .

If a well-ordering R on A can be expressed in a closed form, as might be the case if we are working with say natural numbers, we can eliminate the antecedent with modus ponens, giving us the exact equivalent of Hilbert's transfinite axiom. Otherwise, we replace R with a dummy setvar variable, say w , and attach w We A as an antecedent in each step of the ZFC version of the HOL proof until the epsilon is eliminated. At that point, B (which will have w as a free variable) will no longer be present, and we can eliminate w We A by applying exlimiv and weth , using scottexs to establish the existence of A .

For a version of this theorem scheme using class (meta)variables instead of wff (meta)variables, see htalem . (Contributed by NM, 11-Mar-2004) (Revised by Mario Carneiro, 25-Jun-2015)

Ref Expression
Hypotheses hta.1 A=x|φy[˙y/x]˙φrankxranky
hta.2 B=ιzA|wA¬wRz
Assertion hta RWeAφ[˙B/x]˙φ

Proof

Step Hyp Ref Expression
1 hta.1 A=x|φy[˙y/x]˙φrankxranky
2 hta.2 B=ιzA|wA¬wRz
3 19.8a φxφ
4 scott0s xφx|φy[˙y/x]˙φrankxranky
5 1 neeq1i Ax|φy[˙y/x]˙φrankxranky
6 4 5 bitr4i xφA
7 3 6 sylib φA
8 scottexs x|φy[˙y/x]˙φrankxrankyV
9 1 8 eqeltri AV
10 9 2 htalem RWeAABA
11 10 ex RWeAABA
12 simpl φy[˙y/x]˙φrankxrankyφ
13 12 ss2abi x|φy[˙y/x]˙φrankxrankyx|φ
14 1 13 eqsstri Ax|φ
15 14 sseli BABx|φ
16 df-sbc [˙B/x]˙φBx|φ
17 15 16 sylibr BA[˙B/x]˙φ
18 7 11 17 syl56 RWeAφ[˙B/x]˙φ