Re: Mizar's scheme is very useful but maybe have a bug

[Andrzej Trybulec <trybulec@math.uwb.edu.pl>]

On Fri, 21 Apr 2000, CHENJINGCHAO wrote:
...

>  I think Mizar's scheme form is to describe the high order logic problem,
> while Mizar's theorem form is to describe the first order logic problem.

It is very close to first order logic, basically a scheme is a generic
form of infinite number of theorems (or axioms). Because second order
variables must be free (or rather bound on the begining of the scheme) it
is less than second order. Andrzej Grzegorczyk proposed to call it 1.5
order logic, on QED Workshop 2 somebogu said that 1.1 or 1.01 might be
even better. 

> Hoare's Axiom system is a high order logic problem,so I must use Mizar's
> scheme to describe it.However, I found several scheme form is not
> available. I guess this may be a Mizar's bug.

Perhaps not a bug because it is schematizer acts according to design, but
defenitely a shortcoming. We call it an "incorporation of an argument".
The problem is that schemtizer analysis, the formulas (or terms) with the
same scheme constructor (predicate or functor) comparing them with
fromulas occuring in a specific scheme justification, e.g.

      P[tau_1]         with    alpha_1
       ....
      P[tau_k]         with    alpha_k

in attempt to reconstruct the meaning of the predicate P in this
particular instance. To do this it takes common part of alpha's (if you
treat alpha's as trees it is the maximal subtree strating with the root
common for all of them), the remaining part are place holders that must be
compared with the argumnets tau_1, ...,tau_k. If there is a common 
starting subtree for all arguments it is incorporated into tha definition
of the predicate, and the attempt to reconstruct the meaning of the
predicate  fails.
As yet it was considered not very important problem even if it hinders the
use of some schemes, mostly related to structural induction. 

> For example,we can define the following scheme:
> 
>  scheme HoareRule{ F(set)-> Nat,P[set],...}:
>     Q[F(g(x))] & P[g(x)]
> provided
> C1:  R[F(...)]
> C2:  P[x] 
> C3:  .....

In your example (I do not know what C3 is) the problem might be with Q
(a part of the definition of F() might be incorporated) or with R (the
same)

> 
> If we cite this scheme by form "from HoareRule(C1,C2,C3)", error 23
> occurs. error 23 is Impossible reconstruction of the definiens of 
> a predicate.
> When I change the above definition into following form,no error occrs.
> 
>  scheme HoareRule{ F(set)-> Nat,P[set],...}:
>     F(x)=F(x) & (P[x] or not P[x]) 
>     Q[F(g(x))] & P[g(x)]
> provided
> C1:  R[F(...)]
> C2:  P[x] 
> C3:  .....

I would rather put the conditions F(x) = F(x) and/or
P[x} or not P[x] among premises. Still not natural but looks a bit better
and will simplify the revision (I mean, sooner or later we will correct
it).

Could you send us the complete example.

Regards,
Andrzej

Andrzej Trybulec
Institute of Computer Science
University of Bialystok
ul. Akademicka 2
Bialystok, Poland