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

Question

I wanted to write the simplest proof in Mizar mathematical theorem prover language I could think of. So I thought of the following:

there exists x \in Nat : x = 1

there isn't anything simpler that I could think of. I gave it the following attempt:

:: example of a comment
environ
  vocabularies MY_MIZAR;
  :: adding Natural Numbers
  requirments SUBSET, NUMERALS, ARITHM;
::>         *210
begin

theorem Th1:
    ex x being Nat st x=1
proof
    ::consider x = 1
    :: proof is done
    x = 1;
    thus Th1;
end;
::>
::> 210: Wrong item in environment declaration

but as you can see Mizar doesn't like my proof. What am I missing?

---

This still doesn't work:

::: example of a comment
environ
  vocabularies MY_MIZAR;
  ::: adding Natural Numbers
  requirements SUBSET, NUMERALS, ARITHM;
::>                 *856      *825
begin

theorem Th1:
    ex x being Nat st x=1
proof
    :::consider x = 1
    ::: proof is done
    set x=1;
    take x;
    thus thesis;
end;
::>
::> 825: Cannot find constructors name on constructor list
::> 856: Inaccessible requirements directive

Answer 1

You can try the following:

1) Fix the 210: error:

x  requirments (wrong spelling)
o  requirements

2) There will probably be some new errors about the contents of that line now, so when you are starting out, it is usually good to "borrow" an environ that already works, e.g., you can use the environ lines from one of the Mizar articles on natural numbers like NAT_1.miz:

environ
:: adding Natural Numbers
vocabularies NUMBERS, ORDINAL1, REAL_1, SUBSET_1, CARD_1, ARYTM_3, TARSKI,
  RELAT_1, XXREAL_0, XCMPLX_0, ARYTM_1, XBOOLE_0, FINSET_1, FUNCT_1, NAT_1,
  FUNCOP_1, PBOOLE, PARTFUN1, FUNCT_7, SETFAM_1, ZFMISC_1;
notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, SETFAM_1, ORDINAL1,
  FINSET_1, CARD_1, PBOOLE, NUMBERS, XCMPLX_0, XREAL_0, XXREAL_0, RELAT_1,
  FUNCT_1, PARTFUN1, FUNCOP_1, FUNCT_2, BINOP_1;
constructors NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, CARD_1, WELLORD2, FUNCT_2,
  PARTFUN1, FUNCOP_1, FUNCT_4, ENUMSET1, RELSET_1, PBOOLE, ORDINAL1,
  SETFAM_1, ZFMISC_1, BINOP_1;
registrations SUBSET_1, ORDINAL1, NUMBERS, XXREAL_0, XREAL_0, CARD_1,
  RELSET_1, FUNCT_2, PBOOLE;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions SETFAM_1, TARSKI, XBOOLE_0, RELAT_1;
equalities ORDINAL1, XBOOLE_0, CARD_1;
expansions SETFAM_1, ORDINAL1, TARSKI, XBOOLE_0;
theorems AXIOMS, ORDINAL1, XCMPLX_1, XREAL_1, XXREAL_0, TARSKI, ORDINAL2,
  XBOOLE_0, CARD_1, FUNCT_2, FUNCT_1, FUNCOP_1, PBOOLE, RELSET_1, RELAT_1,
  PARTFUN1, SUBSET_1, NUMBERS, ENUMSET1, XBOOLE_1;
schemes SUBSET_1, ORDINAL2, FUNCT_2, PBOOLE, BINOP_1;

3) To use "1" as your example, you can use "set", "take":

proof
  set x=1;
  take x;
  thus thesis;
end;

Hope this helps.

Answer 2

There are several ways to do this:

Although it is not quite your statement here is an example (It is not quite your statement because you use a "Nat" type).

environ

 vocabularies NUMBERS;
 constructors ARYTM_0;
 notations NUMBERS;
 registrations ORDINAL1;
 requirements NUMERALS, SUBSET, BOOLE;

begin

1 in NAT;

ex x be object st x = 1;

ex x be object st x in NAT & x = 1;

The 3 statements are verified by mizar as valid, true, demonstrate.

If this is not demonstrated (in the mizar sense), it would indicate the *4 error or even sometimes the *1 error.

In the case of the 3 statements here, the evidence is not explicitly stated. It is contained in the environment because Mizar does not require you to indicate all the steps, some of them are automatic.

It is possible to present in this way, acceptable also to Mizar.

environ

 vocabularies NUMBERS;
 constructors ARYTM_0;
 notations NUMBERS;
 registrations ORDINAL1;
 requirements NUMERALS, SUBSET, BOOLE;

begin

1 in NAT
proof
  thus thesis;
end;

ex x be object st x = 1
proof
  thus thesis;
end;

ex x be object st x in NAT & x = 1
proof
  thus thesis;
end;

But in this situation, the full expression

proof
  thus thesis;
end;

is redundant.

To return to the initial problem, and using the suggestion (user10715283 & user10715216). "can we take an environ that is smaller [...]": yes with a specific tool (clearenv.pl, provide with Mizar-System)

environ

 vocabularies NAT_1;
 constructors NUMBERS, XCMPLX_0, XREAL_0, BINOP_1;
 notations ORDINAL1;
 registrations ORDINAL1;
 requirements NUMERALS, SUBSET;

begin

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