[no subject]

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

A modification of the language is proposed: to allow only for Proof
in the justification of a Scheme.

Arguments:

Pro:

A simple justification of a scheme looks awful:

scheme UI1{x1()->set,P[set]}:
  P[x1()]
provided a1: for x1 holds P[x1] by a1;

It looks rather as a justification of the premise a1. With a proof
it looks nicer:

scheme UI1{x1()->set,P[set]}:
  P[x1()]
provided a1: for x1 holds P[x1]
 proof thus thesis by a1; end;

Contra:

1. Articles become longer.
2. Grammar is less regular.

ad 1
 Schemes with the justification other than a proof are very rare and
 not very useful. As far as I know they occur in ENUMSET1 and SCHEMS_1.
 Schemes proved in SCHEMS_1 are nowhere used. Schemes proved
 in ENUMSET1 are used in some articles but only because the implementation
 of the checker is not efficient (the logical power of the checker is
 sufficient to avoid the use of these schemes).

 Moreover, if the justification by proof is obligatory then we may allow
 for omitting the word "proof", i.e. syntax like

scheme UI1{x1()->set,P[set]}:
  P[x1()]
provided a1: for x1 holds P[x1];
 thus thesis by a1;
end;

ad 2
 The argument is more serious. However similar restrictions are already
 used, in some places justification by proof is not allowed:
 (in Iterative Equality, the justification of "per cases", the justification
  of Choice Statement and Type Changing Statement must be Simple
  Justification)


Any comment ?

Andrzej Trybulec