Re: Choice Axiom

[Andrzej Trybulec <trybulec@edserve.cs.shinshu-u.ac.jp>]

What I want to comment is not what Rundnicki wrote but what Harrison
wrote. That is the reason for ">>".
(I should commment John's message, but I have not it here)
> Subject: Re: A simpler proof
> Date: Mon, 8 Sep 1997 23:10:36 -0600 (MDT)
> From: Piotr Rudnicki <piotr@cs.ualberta.ca>
> To: John.Harrison@cl.cam.ac.uk (John Harrison)
> CC: torkel@sm.luth.se (Torkel Franzen), trybulec@edserve.cs.shinshu-u.ac.jp

> > 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.

This is what I had believed in.

If you allow for an anecdote ...

I did a rehearsal of my lecture in Turku (a HOL conference) and
I wanted to say as usual: "We need TG to develop properly the category
theory. As a bonus we get that AC is a theorem in it and ..."

Then I recalled Rudnicki's functor "choose" (I believe it has been
first defined in a student work, not in WELLFND1), and I saw that to
prove AC in Mizar I do not need TG at all.

Because there are some doubts about it I have attached the proof
of AC (actually the existence of Kuratowski's function) to this
message (less than 40 lines).
I use only the Lambda scheme (FUNCT_1) and concepts from RELAT_1 and
FUNCT_1. The first time Tarski's Axiom A (TARSKI:9) was used, is in
WELLORD2 and the articles RELAT_1 and FUNCT_1 do not depend on it.
(they had been submitted before WELLORD2). 

It was a horrible experience. Earlier I had supposed that I know
what one can or cannot prove in Mizar. What else can be proved ?

There is a question what is the reason that one can prove AC
in Mizar.
One needs basically three ingredients:
 permissiveness
 Replacement
 and types (at least "Element of ...").
Piotr Rudnicki argued that permissivness is not creative, then it does
not matter. It depends in which theory.
It is not creative in pure predicate calculus, one can always put
false (in Mizar "contradiction"), or true as well, if the assumptions
of the definition are not met.
It is not creative in 1-sorted theories, at least if one can has a name
for an element of the universe. In set theory one can put the empty set
as the value if conditions are not met, in the arithmetics - 0.
I doubt if permissiveness + types is enough. Perhaps the
Relacement (the Fraenkel scheme) in Mizar it too strong ?

I should mention that the first person that warned me that one
have to be careful with permissiveness is Marcin Mostowski. 
His example:
Let us take a decidable theory (e.g. unary predicate calculus)
and let us allow permissive definitions of functors. Then we
may define a binary functor (e.g. absolutively permissive, i.e.
with "assume contradiction") and what we get is an undecidable
theory. It is not creative, of course, but the situation changed
dramatically.

Andrzej Trybulec

environ
 vocabulary FUNC,FUNC_REL,NEWTON;
 constructors RELAT_1,FUNCT_1;
 notation RELAT_1,FUNCT_1;
 schemes FUNCT_1;
begin

:: Compare WELLFND1

definition
   let S be set; assume
0_0: contradiction;
 func choose S -> Element of S means
  not contradiction; :: whatever, no need for a label
 correctness by 0_0;
end;

:: Compare PBOOLE

scheme Kuratowski_Function{A()-> set, F(Any) -> Any}:
 ex f being Function st dom f = A() &
  for e being Any st e î A() holds f.e î F(e)
 provided
Z: for e being Any st e î A() holds F(e) is not empty
  proof
   consider f being Function such that
W1: dom f = A() and
W2: for e being Any st e î A() holds f.e = choose F(e) from Lambda;
   take f;
   thus dom f = A() by W1;
    let e be Any;
    assume
ZZ:   e î A();
     then reconsider Fe = F(e) as non empty set by Z;
     f.e = choose Fe by W2,ZZ;
    hence f.e î F(e);
  end;