--- Begin Message ---
John:
I have rewritten your last proof in Mizar, see attached. It is long but
I have initially expected it to be even longer. The length of the proof
is mainly in defining the function f.
> I wonder if it is possible to avoid (even Dependent) Choice completely.
How else can you get the descending chain? Later on you just take the
minimum of a subset of NAT.
> Does the existing Mizar proof use it? I guess AC is plumbed into Mizar
> via the Tarski-Grothendieck Axiom so it gets hard to keep track of where
> it's used.
Good question. The original Mizar proof (the one with regular cardinals)
probably uses AC indirectly - noone did the archeological research.
> We have the same problem with HOL and its Hilbert operator.
It may be interesting that a version of the Hilbert operator was introduced
into Mizar when proving the equivalence of well-foundedness and
non-existence of descending chains (article WELLFND1).
Cheers,
Piotr
----------------------------------------------------------------------
î is \in, ó is <=
----------------------------------------------------------------------
:: J. Harrison's proof in Mizar
theorem for R being non empty RelStr
st for V being non empty set,
H being Function of
[:the carrier of R, PFuncs(the carrier of R, V):], V
ex F being Function of the carrier of R, V
st F is_recursively_expressed_by H
holds R is well_founded
proof let R be non empty RelStr;
set c = the carrier of R, r = the InternalRel of R,
PF = PFuncs(the carrier of R, NAT);
assume
0_0: for V being non empty set, H being Function of [:c, PFuncs(c, V):], V
ex F being Function of c, V st F is_recursively_expressed_by H;
assume not R is well_founded; then consider X being sequence of R such that
0'0: X is descending by OC;
X is Function of NAT, c; then
0'1: dom X = NAT by FUNCT_2:def 1;
:: Construction of the function f, longish
defpred P[Element of c, Element of PF, set] means
($1 \in rng X implies
ex p being Nat st X.p = $1 &
(for p' being Nat st p' < p holds X.p' <> $1) &
(X.(p+1) \in dom $2 implies
ex v being Nat st v = $2.(X.(p+1)) & $3 = 1+v) &
(not X.(p+1) \in dom $2 implies $3 = 0) )
& (not $1 \in rng X implies $3 = 0);
0'2'0: for x being Element of c, y being Element of PF
ex z being Element of NAT st P[x,y,z]
proof let x be Element of c, y be Element of PF;
per cases;
suppose S0: x \in rng X; then
consider p being set such that
L0: p \in dom X & x = X.p by FUNCT_1:11;
L1: ex p being Nat st X.p = x by L0, 0'1;
consider p being Nat such that
L2: X.p = x and
L3: for p' being Nat st X.p' = x holds p <= p' from Min(L1);
L4: for p' being Nat st p' < p holds X.p' <> x by L3;
thus ex z being Element of NAT st P[x,y,z]
proof
per cases;
suppose S1: X.(p+1) \in dom y;
reconsider v = y.(X.(p+1)) as Nat by S1, PARTFUN1:27;
take 1+v;
thus thesis by S0, S1, L2, L4;
suppose S1: not X.(p+1) \in dom y;
take 0;
thus thesis by S1, L2, L4;
end;
suppose S0: not x \in rng X;
take 0;
thus thesis by S0;
end;
0'2'1: for x being Element of c, y being Element of PF, z1,z2 being Nat
st P[x,y,z1] & P[x,y,z2] holds z1 = z2
proof let x be Element of c, y be Element of PF, z1, z2 be Nat
such that
L1: P[x,y,z1] and
L2: P[x,y,z2];
per cases;
suppose S0: x \in rng X;
consider p1 being Nat such that
N1: X.p1 = x and
N2: for p' being Nat st p' < p1 holds X.p' <> x and
N3: X.(p1+1) \in dom y implies
ex v being Nat st v = y.(X.(p1+1)) & z1 = 1+v and
N4: not X.(p1+1) \in dom y implies z1 = 0 by S0, L1;
consider p2 being Nat such that
M1: X.p2 = x and
M2: for p' being Nat st p' < p2 holds X.p' <> x and
M3: X.(p2+1) \in dom y implies
ex v being Nat st v = y.(X.(p2+1)) & z2 = 1+v and
M4: not X.(p2+1) \in dom y implies z2 = 0 by S0, L2;
p1 <= p2 & p2 <= p1 by N2, M2, N1, M1; then
p1 = p2 by AXIOMS:21;
hence z1 = z2 by N3, M3, N4, M4;
suppose S0: not x \in rng X;
thus thesis by S0, L1, L2;
end;
consider H being Function of [:c, PF:], NAT such that
0'2: for x being Element of c, p being Element of PF
holds P[x, p, H.[x,p]] from FuncEx2D(0'2'0, 0'2'1);
consider f being Function of c, NAT such that
0'3: f is_recursively_expressed_by H by 0_0;
defpred R[Nat] means ex n being Nat st $1 = f.(X.n);
R[f.(X.1)]; then
0'4: ex k being Nat st R[k];
consider k being Nat such that
0'5'0: R[k] and
0'5'1: for n being Nat st R[n] holds k <= n from Min(0'4);
consider n being Nat such that
0'5: k = f.(X.n) by 0'5'0;
0'6: f.(X.n) = H.[X.n, f|r-Seg (X.n)] by 0'3, Lrecur;
reconsider ff = f|r-Seg (X.n) as Element of PF by PARTFUN1:119;
X.n \in rng X by 0'1, FUNCT_1:12; then
consider p being Nat such that
0'7'0: X.p = X.n and
for p' being Nat st p' < p holds X.p' <> X.n and
0'7'1: X.(p+1) \in dom ff implies
ex v being Nat st v = ff.(X.(p+1)) & H.[X.n, ff] = 1+v and
not X.(p+1) \in dom ff implies H.[X.n, ff] = 0 by 0'2;
X.(p+1) <> X.p & [X.(p+1), X.p] \in r by 0'0, Lchain; then
0'7: X.(p+1) \in r-Seg (X.n) by 0'7'0, WELLORD1:def 1;
dom f = c by FUNCT_2:def 1; then X.(p+1) \in dom ff by 0'7, RELAT_1:86;
then consider v being Nat such that
0'8: v = ff.(X.(p+1)) & H.[X.n, ff] = 1+v by 0'7'1;
f.(X.n) = 1+v by 0'8, 0'6; then
0'9: k > v by 0'5, NAT_1:38;
f.(X.(p+1)) = ff.(X.(p+1)) by 0'7, FUNCT_1:72; then R[v] by 0'8;
hence contradiction by 0'9, 0'5'1;
end;
--- End Message ---