Re: a question

Dear Adem,

On Tue, 22 Dec 2009, Ozyavas, Adem wrote:

> I asked the group a question on how to write recursive predicates in Mizar. The following is the
>
> result of correspondce of emails back and forth. It gives a definition for an inductive factorial predicate.
>
> definition
>  let n,x be natural number;
>  pred factorial(n,x) means
>   for Y being set st
>   [0,1] in Y & (for k,y being natural number st [k,y] in Y holds [k+1,y*(k+1)] in Y)
>   holds [n,x] in Y;
> end;
>
>
> First of all, there is not a unique set that satisfies the above definition. A set
> {[0,0!], [1,1!], [2,2!], ..., [n,n!]} \/ [3,3] would satisfy the set consructed with the above
> definition so that it is not possible to disprove
>
> factorial 3,3.

No, it _is_ possible to disprove it, below is the proof :-))

environ
  vocabularies FACTOR,ORDINAL1,CARD_1,ARYTM_3,RELAT_1,REALSET1,ZFMISC_1,NUMBERS;
  notations TARSKI,ORDINAL1,CARD_1,NUMBERS,NAT_1,NEWTON,ZFMISC_1;
  constructors ORDINAL1,CARD_1,NAT_1,NEWTON,ZFMISC_1,REAL_1;
  registrations ORDINAL1;
  requirements BOOLE,SUBSET,NUMERALS,ARITHM;
  schemes XBOOLE_0;
  theorems ZFMISC_1,STIRL2_1,NEWTON;
begin

definition
   let n,x be natural number;
   pred factorial n,x means :def1:
    for Y being set st
    [0,1] in Y & (for k,y being natural number st [k,y] in Y holds 
[k+1,y*(k+1)] in Y)
    holds [n,x] in Y;
end;

factorial 3,6
proof
   let Y be set;
   assume a: [0,1] in Y & (for k,y being natural number st [k,y] in Y holds 
[k+1,y*(k+1)] in Y);
   then [0+1,1*(0+1)] in Y;
   then [1+1,1*(1+1)] in Y by a;
   then [2+1,2*(2+1)] in Y by a;
   hence thesis;
end;

not factorial 3,3
proof
   assume a: not thesis;
   defpred P[set] means ex n being natural number st $1 = [n,n!];
   consider X being set such that
   x: for x being set holds x in X iff x in [:NAT,NAT:] & P[x] from 
XBOOLE_0:sch 1;
   z: [0,1] in [:NAT,NAT:] by ZFMISC_1:def 2;
   b: [0,1] in X by x,z,NEWTON:18;
   now
     let k,y be natural number;
     assume [k,y] in X; then
     consider l being natural number such that
     l: [k,y]=[l,l!] by x;
     y: k=l & y=l! by l,ZFMISC_1:33;
     n: [k+1,y*(k+1)] in [:NAT,NAT:] by ZFMISC_1:def 2;
     [k+1,(k+1)!]=[k+1,y*(k+1)] by y,NEWTON:21;
     hence [k+1,y*(k+1)] in X by n,x;
   end;
   then [3,3] in X by a,b,def1; then
   consider n being natural number such that
   n: [3,3]=[n,n!] by x;
   n=3 & n!=3 by n,ZFMISC_1:33;
   hence contradiction by STIRL2_1:60;
end;


> Most of the time, a third item is mentioned in an inductive definition (after (i) base case, (ii)
> inductive case) which is "the minimal set that satifies the first and second items (or the
> generalized intersection of all sets that satify (i) and (ii))".

It's not needed - the "for Y" in the definition guarantees, that the 
condition also holds for the 'minimal' set.

Best,

Adam Naumowicz

=======================================================================
Dept. of Programming and Formal Methods  Fax: +48(85)7457662
Institute of Informatics                 Tel: +48(85)7457559 (office)
University of Bialystok                  E-mail: [email protected]
Sosnowa 64, 15-887 Bialystok, Poland     http://math.uwb.edu.pl/~adamn/
=======================================================================