Re: [mizar] referring to unlabeled theorems

[Jesse Alama <alama@stanford.edu>]

Adam Naumowicz <adamn@math.uwb.edu.pl> writes:

> On Sat, 17 Feb 2007, Jesse Alama wrote:
>
>> One thing that annoys me slightly is that the .miz form of a MIZAR
>> article doesn't necessarily have labels for all theorems.  I prefer to
>> look at MIZAR articles (not abstracts) in emacs, and sometimes I find
>> an unlabeled theorem that I want to use.  In these situations I have
>> to look at, e.g., the semantic presentation of that article or the
>> abstract to find out how to refer to that theorem.  It would be nice
>> if theorems in .miz files were labeled as they are in the abstracts
>> and the semantic presentation.
>
> It's because all articles are as a rule cleansed of all unnecessary
> labels, i.e statements not referred to in the current article
> shouldn't be labelled. Theorems are no exception here.

When I was studying GOEDELCP a while ago, I was surprised to see that
the final theorem of the article, (a version of) the completeness
theorem for first-order logic, didn't get a label.  But (I thought
then) what if I want to work on, say, a proof of compactness for
first-order logic?  How would I refer to the completeness theorem?  As
a beginner to the world of MIZAR, I found it baffling that theorems
and lemmas needed to prove the completeness theorem are given labels,
but that the completeness theorem itself was unlabeled.  If anything
deserves a label in that file, it's that theorem!

It would be great if the .miz files were not cleaned up as you say
they are; adding the labels would be, in my opinion, a small
improvement to the (.miz file) presentation of the MML.

Jesse

-- 
Jesse Alama (alama@stanford.edu)
*102: Unknown predicate (http://www.mizar.org)