• Previous chapter
• Table of contents

Appendix 2: Mizar MSE Grammar

2.1: Notation

Name	(in italics) stands for a variable in the grammar, that is a non-terminal symbol.
token	(in typewriter font) a token, that is a terminal symbol.
|	separates alternative elements.
( )	groups elements together.
{ }	zero or more occurrences of what is between braces.
{ }+	one or more occurrences of what is between braces.
[ ]	zero or one occurrence of what is between brackets.

2.2: Grammar

Commentaries

Comment   ::=

== ArbitraryTextToEndOfLine

Article

Article   ::=

environ Environment [ begin TextProper ]

Environment   ::=

{ Axiom ; | Reservation ; | GlobalConstantsDeclaration ; }

TextProper   ::=

{ Statement ; }+

Environment Items

Axiom   ::=

LabelId : Formula

Reservation   ::=

reserve Identifier { , Identiifier } for SortId

GlobalConstantsDeclaration   ::=

given QualifiedObjects

Text Proper Items

Statement   ::=

CompactStatement | DistributedStatement | Choice

CompactStatement   ::=

Proposition ( SimpleJustification | Proof )

DistributedStatement   ::=

[ LabelId : ] now Reasoning end

Choice   ::=

consider QualifiedObjects [ such that Proposition ] SimpleJustification

Proposition   ::=

[ LabelId : ] Formula

SimpleJustification   ::=

[ by Reference { , Reference } ]

Reference   ::=

LabelId

Reasonings and Proofs

Proof   ::=

proof Reasoning end

Reasoning   ::=

{ SkeletonItem ; | Statement ; }+

SkeletonItem   ::=

Assumption | Generalization | Conclusion

Assumption   ::=

assume Proposition

Generalization   ::=

let ExplicitlyQualifiedObjects

Conclusion   ::=

thus CompactStatement

Formulas

Formula   ::=

AndOrFormula | ConditionalFormula | BiconditionalFormula | QuantifiedFormula

AndOrFormula   ::=

ConjunctiveFormula | DisjunctiveFormula

DisjunctiveFormula   ::=

ConjunctiveFormula { or ConjunctiveFormula }

ConjunctiveFormula   ::=

UnitFormula { & UnitFormula }

UnitFormula   ::=

{ not } ( AtomicFormula | ( Formula ) )

AtomicFormula   ::=

Equality | Inequality | PredicativeFormula | contradiction | thesis

Equality   ::=

Term = Term

Inequality   ::=

Term <> Term

PredicativeFormula   ::=

PredicateId [ [ Term { , Term } ] ]

Term   ::=

ObjectId

ConditionalFormula   ::=

AndOrFormula implies AndOrFormula

BiconditionalFormula   ::=

AndOrFormula iff AndOrFormula

QuantifiedFormula   ::=

UniversalFormula | ExistentialFormula

UniversalFormula   ::=

for QualifiedObjects [ st Formula ] holds Formula | for QualifiedObjects [ st Formula ] QuantifiedFormula

ExistentialFormula   ::=

ex QualifiedObjects st Formula

Object Declarations

QualifiedObjects   ::=

ImplicitlyQualifiedObjects | ExplicitlyQualifiedObjects | ExplicitlyQualifiedObjects , ImplicitlyQualifiedObjects

ImplicitlyQualifiedObjects   ::=

ObjectList

ExplicitlyQualifiedObjects   ::=

QualifiedSegment { , QualifiedSegement }

QualifiedSegment   ::=

ObjectList ( be | being ) SortId

ObjectList   ::=

ObjectId { , ObjectId }

Identifiers

LabelId   ::=

Identifier

SortId   ::=

Identifier

PredicateId   ::=

Identifier

ObjectId   ::=

Identifier

IdentifierChar   ::=

A..Z | a..z | 0..9 | _

Identifier   ::=

{ IdentifierChar }+ { ' }

Remarks

• Semicolon followed by begin, end or end-of-text can be omitted.

• A QualifiedSegment in Generalization must use be; in all other contexts, being must be used.

• A Reasoning must include at least one Conclusion.

• The Reservation construct lets us use ImplicitelyQualifiedObjects where the SortId is not specified explicitly for an ObjectId. The SortId of such an ObjectId is the one that has been reserved for the ObjectId in Reservation.

• The atomic formula thesis can save a lot of writing. thesis is always equivalent to the formula that still remains to be proven in order to complete the innermost Proof. Thus, any usage of thesis outside of a Proof is meaningless.

  Consider a Proof. Initially, the thesis is equivalent to the Proposition for which the Proof is written. The meaning of thesis is affected by each SkeletonItem in the way that to many appears mysterious. In a correct Proof, the last meaning of thesis should be not contradiction, that is true.

• The UniversalFormula has more variants than in BB version. The construct:
  for someQualifiedObjects st aFormula1 holds aFormula2;

  is equivalent to

  for someQualifiedObjects holds aFormula1 implies aFormula2;

  And also, if the scope of the quantifier is a QuantifiedFormula, then holds may be omitted.

2.3: Problems with syntax

2.3.1: A question

== You are given a number of syntactically incorrect formulas.
== Your job is to make them syntactically correct by inserting parentheses
== (no other visible symbols are permitted)
== in such a way that the formulas become not only syntactically correct 
== but also are accepted by the Mizar checker (without any errors).
== That is, all formulas you obtain should be tautologies.

environ
        given a being PERSON;

        == If you wish, you may understand the abbreviations as follows:
        == K[a]         a is a knight
        == N[a]         a is a knave
        == S[a]         a is short
        == T[a]         a is tall
        == H[a]         a is handsome
        == You should understand however that the above suggestion is
        == completely immaterial since tautologies are independent of the
        == interpretation.
begin
        == Example. For the syntactically incorrect

        1: K[a] implies T[a] & T[a] implies H[a] & K[a] implies H[a];

        == the solution can be:

        1: ((K[a] implies T[a]) & (T[a] implies H[a]) & K[a]) implies H[a];

        == End of example

 1: K[a] implies S[a] iff S[a] or not K[a];
  
 2: K[a] implies T[a] implies T[a] implies H[a] implies K[a] implies H[a];
        
 3: K[a] implies T[a] & T[a] implies H[a] implies K[a] implies H[a];

 4: K[a] implies T[a] implies K[a] implies K[a];

 5: K[a] implies S[a] & N[a] implies T[a] implies K[a] & N[a] implies
                                                                  S[a] & T[a];

 6: K[a] implies S[a] & N[a] implies T[a] & K[a] or N[a] implies S[a] or T[a];

 7: K[a] implies S[a] & N[a] implies T[a] & K[a] or N[a] & not S[a] implies
                                                                         T[a];

 8: K[a] implies S[a] & S[a] implies K[a] iff K[a] iff S[a];

 9: K[a] & S[a] or not S[a] & not K[a] iff K[a] iff S[a];

2.3.2: Its answer

  environ
    given a being PERSON;
  begin
        
  1: K[a] implies (S[a] iff S[a] or not K[a]);
        
  2: (K[a] implies T[a]) implies 
               ((T[a] implies H[a]) implies (K[a] implies H[a]));
        
  3: ((K[a] implies T[a]) & (T[a] implies H[a])) 
               implies (K[a] implies H[a]);
        
  4: (K[a] implies T[a]) implies (K[a] implies K[a]);
        
  5: ((K[a] implies S[a]) & (N[a] implies T[a])) 
               implies (K[a] & N[a] implies S[a] & T[a]);
        
  6: ((K[a] implies S[a]) & (N[a] implies T[a]) & (K[a] or N[a])) 
               implies S[a] or T[a];
        
  7: ((K[a] implies S[a]) & (N[a] implies T[a]) & (K[a] or N[a]) 
               & not S[a]) implies T[a];
        
  8: ((K[a] implies S[a]) & (S[a] implies K[a])) iff (K[a] iff S[a]);
        
  9: (K[a] & S[a] or not S[a] & not K[a]) iff (K[a] iff S[a]);

• Previous chapter
• Table of contents