The set of symbols that can be used in a Mizar Article is not fixed externally. The author of an article indicates which tokens are taken into account while tokenizing the article. By a lexicon of an article we mean the set of such tokens. The lexicon of an article consists of the basic lexicon and some additional lexicons. Additional lexicons are not associated with any single Mizar Article, they can be shared by many of them.
The basic lexicon includes the following tokens:
| according | aggregate | and | antonym |
| as | associativity | assume | asymmetry |
| attr | be | begin | being |
| by | canceled | case | cases |
| cluster | coherence | commutativity | compatibility |
| connectedness | consider | consistency | constructors |
| contradiction | correctness | def | deffunc |
| define | definition | definitions | defpred |
| end | environ | equals | ex |
| exactly | existence | for | from |
| func | given | hence | hereby |
| holds | idempotence | identify | if |
| iff | implies | involutiveness | irreflexivity |
| is | it | let | means |
| mode | non | not | notation |
| notations | now | of | or |
| otherwise | over | per | pred |
| prefix | projectivity | proof | @proof |
| provided | qua | reconsider | redefine |
| reflexivity | registration | registrations | requirements |
| reserve | sch | scheme | schemes |
| section | selector | set | st |
| struct | such | suppose | symmetry |
| synonym | take | that | the |
| then | theorem | theorems | thesis |
| thus | to | transitivity | uniqueness |
| vocabularies | when | where | with |
| wrt |
Note that 'be' and 'being' are synonyms and 'hereby' is just a shortcut for 'thus now'.
| , | ; | : | ( | ) | [ | ] | { | } | = | & | -> | ||
| .= | ... | $1 | $2 | $3 | $4 | $5 | $6 | $7 | $8 | $9 | $10 | (# | #) |
A numeral is a sequence of digits starting with a non-zero digit. Formally:
Numeral = Non-Zero-Digit { 0 | Non-Zero-Digit } .
Non-Zero-Digit =
1 | 2 | 3 |
4 | 5 | 6 |
7 | 8 | 9 .
Identifier is a string of letters, digits, underscores ( _ ) and apostrophes ( ' ), that is neither a reserved word nor symbol nor numeral. The case of letters is significant for Mizar.
File name is a Mizar identifier which may be used as a file name and consists of five to eight characters. The first character must be a letter and no apostrophes are allowed.
Additional lexicons are defined in vocabulary files. An additional lexicon is a set of symbols which are strings of arbitrary characters excluding control characters, space, and double colon. Symbols are grouped into the following classes: mode symbols, function symbols, left or right function brackets, structure symbols, selector symbols, attribute symbols and predicate symbols.
If an additional lexicon defines a symbol represented by a string of characters which forms an identifier, then the symbol overrides the identifier.
The symbols introduced in the vocabulary HIDDEN are put into the lexicon of every Mizar Article. Symbols from other vocabularies are put into the lexicon of an article with the help of the vocabularies Directive.
Last modified: April 22, 2008