[Date Prev][Date Next] [Chronological] [Thread] [Top]

Re: [mizar] then per cases;

Hi,

On Tue, 9 Jan 2007, Jesse Alama wrote:


I recently discovered what seems to me to be an asymmetry of "per
cases".  Consider, for example, in the context of some proof:

A1: <statement1> or <statement 2>;
then per cases;
 suppose <statement1>;
   <proof1>;
 end;
 suppose <statement2>;
   <proof2>;
 end;
end;

It seemed natural to me to write "then per cases" in the proof that I
was working on; I was surprised that this kind of statement is
rejected.  I get errors 178 ("Link assumes a straightforward
justification"), 391 ("Incorrect beginning of a text item") and 4
("This inference is not accepted") when writing something like this.
However, the proof

A1: <statement1> or <statement 2>;
per cases by A1;
 suppose <statement1>;
   <proof1>;
 end;
 suppose <statement2>;
   <proof2>;
 end;
end;

is just fine.  It seems to me that there is an asymmetry between "per
cases" and other statements which require justification.  For the
latter we can either label the previous statement and include that
label in a list of labels following "by" or indicate that the previous
statement is to be counted as a justification by using "then".  But
for per cases this isn't true.  Is there any significant reason behind
this asymmetry?
You may be surprised to see that there are more contexts in which "then" doesn't work exactly the same as putting a label to a previous sentence and then refering to it - these are "consider ... such that ...", "given ... such that", "assume that ...". You may find some kind of explenation to this fact in the mizar-forum archives, e.g. 
http://mizar.uwb.edu.pl/forum/archive/0104/msg00006.html
I don't know the motivation behind disallowing linking with the "per cases" construct, however ;-) 

Best,

Adam Naumowicz

======================================================================
Department of Applied Logic            fax. +48 (85) 745-7662
Institute of Computer Science          tel. +48 (85) 745-7559 (office)
University of Bialystok                e-mail: adamn@mizar.org
Sosnowa 64, 15-887 Bialystok, Poland   http://math.uwb.edu.pl/~adamn/
======================================================================