[mizar] a question

["Ozyavas, Adem" <adem.ozyavas@ttu.edu>]

Dear All,

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.


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

What I want to prove actually is the uniqueness so that 

for i,m,n being Nat st factorial i,m & factorial i,n hols m = n

should hold.

I want to write the factorial definition in such a way that the above statement should be easy to 
prove. Also, factorial 3,3 should be easy to disprove...

I was asked why I am not writing this definition as a recursive function before. There is some issue 
of undecidablity of whether given an object, it is *not* decidable if it is in the domain of the 
function I am trying to define. Factorial is just an example I am trying to bring the issue to your attention. 

Thank you very much for all your help and hope you all are having a good break...

Adem Ozyavas
Texas Tech University