Re: How does one prove there is a Natural number equal to 1 in Mizar (mathematical theorem proving language)?

Brando,

On Wed, 28 Nov 2018, Miranda, Brando wrote:

> I am very used to hands on tutorials that have me write code immediately 
> so I was trying to do that with mizar. I tried doing the simplest proof 
> I could think of, proving some Nat is 1. I wrote some Mizar but it 
> didn’t work. I linked the code here:
>
> https://stackoverflow.com/questions/53512157/how-does-one-prove-there-is-a-natural-number-equal-to-1-in-mizar-mathematical-t
>
> anyone know whats missing?

First, please note the typo in your 'requirments'.

To have the text accepted by the Mizar checker you should specify where to 
look for the 'Nat' symbol (vocabularies NAT_1), how to use it (notations 
NAT_1) and what is its actual meaning (constructors NAT_1). Also, Mizar 
knows that the numerals are of the required type only if you import some 
extra type information (requirements SUBSET,NUMERALS and registrations 
ORDINAL1) - initially numerals are just objects/sets, but with these 
additional directives the checker interprets them as 'Element of NAT' and 
consequently ans 'natural number' which is abbreviated to 'Nat'.

So the minimal Mizar text to prove your statement would be:

environ
vocabularies NAT_1;
notations NAT_1;
constructors NAT_1;
registrations ORDINAL1;
requirements SUBSET,NUMERALS;

begin

theorem Th1:
     ex x being Nat st x=1
proof
     ::consider x = 1
     take x = 1;
     :: proof is done
     thus thesis;
end;


Best regards,

Adam

===========================================================================
Dept. of Programming and Formal Methods      Fax: +48(85)738-83-33
Institute of Informatics                     Tel: +48(85)738-83-06 (office)
University of Bialystok                      E-mail: [email protected]
Ciolkowskiego 1M, 15-245 Bialystok, Poland   http://math.uwb.edu.pl/~adamn/
===========================================================================