[Date Prev][Date Next]
[Chronological]
[Thread]
[Top]
Re: [mizar] 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: adamn@mizar.org
Ciolkowskiego 1M, 15-245 Bialystok, Poland http://math.uwb.edu.pl/~adamn/
===========================================================================