Jaskinie Podróże Nurki Grafika Mizar Teksty Kulinaria Lemkov Namiary Mapa RSS English
Spelunka Trybików Mizar Syntaktyka Mizara-MSE YAC Software
  Wróæ

Mizar

Eddie

Artykuły

Syntaktyka Mizara-MSE

Syntaktyka Mizara-MSE
& (ampersand)

Conjunction of statements.

Syntax  

statement { "&" statement }

Examples  

:: Both p[] and q[] hold:
p[] & q[]; 

:: p[], q[], and r[] hold:
p[] & q[] & r[]; 

:: For every a, p[a] and q[a] hold:
for a holds p[a] & q[a]; 

Note  

The reserved word
and is used for conjunction of assumptions in a conditions clause.

See Also  

( )
iff
implies
not
or 



Góra

: (colon)

Follows the label identifier when defining a label.

Example  

proof
  . . .
A1: 
  for a holds NonZero[a]; 
  . . .
  hence NonZero[b] by A1;
end;

Note  

Axioms in the environment must be preceded by a label.

See Also  

by
hence
then




Góra

:: (double colon)

Is used to write comments in Mizar-MSE texts. A comment starts with the double colon and ends with the end of the line. These comments are ignored by the Mizar-MSE processor.

Example  

:: The empty set is a subset of all sets:
for A being set holds empty subset_of A
proof
  . . .
end;



Góra

; (semicolon)

Ends all statements in Mizar-MSE. The use of ; is forbidden after proof, now, environ, and begin.

Example  

thus thesis by Ax1;



Góra

, (comma)

Separates elements in lists of identifiers:
·in qualified lists, separates variables and lists of variables assigned to a given sort; also separates qualified lists,  
·separates labels in a simple justification,  
·separates elements in a predicate (sorts in the predicate's definition and variables / constants when using the predicate),  
·separates sorts in sort introductions,  
·separates variables in global reservations.  

Examples  

:: A qualified-list under a universal quantifier:
for a, b being LINE, p being PLANE holds . . .

:: A list of labels in a simple justification:
thus thesis by Ax10, Th20;

:: A list of sorts in a predicate definition:
pred set union_of set, set;

:: Lists of arguments in predicates:
P[a, b] implies Q[a, b]; 

:: A list of sorts in a sort definition:
sort POINT, LINE, PLANE;

:: A list of variables reserved for the sort POINT:
reserve a, b, c, d for POINT; 



Góra

[ ] (brackets)

Notation for predicates (unless infix notation is used).

The predicate's identifier is written before the opening bracket. The closing bracket ends the predicate.

The sort list (when defining the predicate) or the term list (when using it) is placed between brackets. In the second case, the sorts of variables / constants must be the same as the sort in the predicate's pred definition.

The list of arguments may also be empty (if such is the predicate's definition).

Examples  

for a holds P[a]; 

for b holds Q[b, b, b]; 

Z[] by Ax2; 

Note  

Brackets are not used in predicates defined with infix notation, i.e.

for A being set holds A subset_of A;

See Also  

pred



Góra

( ) (parentheses)

Parentheses are used to force higher priority for logical operators in case their priority is lower. not has the highest priority, next & followed by or. The priority of iff equals to the priority of implies and is lower than those mentioned above. The quantifiers for and ex have the lowest priority.

Examples  

not (p[A] or q[A]); 
:: Otherwise, not would apply to p[A] only.

(for A holds p[a]) & q[]; 
:: Otherwise, q[] would also be under the quantifier.

Notes  

Parentheses may also be used according to operator priority to enhance readability by grouping operators with higher priority, i.e.

(p[] & q[]) or (s[] & t[]);

Parentheses must be used to force the appropriate association of
iff and implies when these are used in statements next to each other, i.e.

(p[] implies q[]) iff r[]; 

See Also  

&
ex
for
iff
implies
not
or




Góra

= (equality)

Equality of variables and/or constants.

Syntax  

( variable | constant ) "=" ( variable | constant )

Example  

for a, b st a LE b & a GE b holds a = b; 

Note  

To express other properties, use predicates.

See Also  

<>
pred



Góra

<> (inequality)

Inequality of variables and/or constants.

Syntax  

( variable | constant ) "<>" ( variable | constant )

Example  

for a, b st a LT b or a GT b holds a <> b; 

Note  

To express other properties, use predicates.

See Also  

=
pred



Góra

and

Used for conjunction of assumptions when you want to have different labels for every statement.

Examples  

assume that a: A[] and b: B[];

given x such that a: A[x] and b: not A[x];

consider y such that a: y = x and b: B[y, y]; 

let x be ANY such that a: x = y and b: A[y]; 

Notes  

Note that
& is used for conjunction of statements, not and.

The two following statements are equivalent logically, however the conjuncts can be referenced independently in the first case:

assume that a: A[] and b: B[];
assume a: A[] & B[];

See Also  

&
assume
consider
given
let
such
that



Góra

assume

Assumption.

Syntax  

"assume"
  1. [ label ":" ] statement ";"
  2. conditions ";"

Examples  

assume p[];

assume that p[];

assume A: p[] & q[];

assume that A: p[] and q[];

assume that A: p[] and B: q[];

Note  

Linking to
assume is not allowed if followed by conditions.

See Also  

and
given
that



Góra

be / being

Used for the introduction of the sort of a variable in a qualified list when introducing a new variable or when redefining the sort of a reserved variable.

A qualified list of variables consists of variables with sorts specified after be / being (possibly repeated for different sorts) followed by (optionally) a list of variables reserved in the environment.

Syntax  

1. implicitly-qualified-list
2. explicitly-qualified-list
3. explicitly-qualified-list { "," explicitly-qualified-list } "," implicitly-qualified-list

where each
explicitly-qualified-list is followed by 

( "being" | "be" ) sort

and
implicitly-qualified-list is a list of variables reserved in the environment.

Examples  

:: An explicit qualification followed by an implicit qualification 
:: (x, y were reserved in the environment):
consider A, B being LINE, x, y such that . . .

:: Two explicit qualifications in a generalization:
let be POINT, P be PLANE; 

:: Two explicit qualifications followed by an implicit qualification
:: in an existential assumption:
given L be POINT, P being PLANE, x, y such that . . . 

:: An explicit qualification under a universal quantifier:
for E, F being SET holds . . . 

:: An implicit qualification under an existential quantifier:
ex F, G st . . .

Notes  

be and being can be used interchangeably - usually the version that fits the rest of the sentence is chosen (be for let and being for assume, given, consider, ex, and for).

Even if a variable is reserved for a given sort in the environment, you can later redefine its sort by using
be / being. However, redefinitions should not be encouraged (they don't enhance readability).

See Also  

reserve
sort



Góra

begin

The beginning of the text proper. The environment must end with the word begin. From now on you can prove your theorems based on definitions introduced in the environment.

See Also  

environ



Góra

by

Simple justification. It should be followed by references to labels of previously introduced propositions (axioms, global constant definitions, proven theorems or proven steps) from which the current statement can be derived.

Syntax  

statement "by" identifier-list

Example  

In the example below, assume that statements labeled with
Axiom2, Axiom3, and Theorem6 were introduced earlier in the article:

for a, A st q[a] holds p[A]
proof
  let a, A;
  assume
A:  q[a];
  q[A] by Axiom3, Theorem6;
  hence thesis by A, Axiom2;
end;

Notes  

To justify by the previous statement,
then or hence may be used.

If a label is defined on a lower level than the current statement (nested in a
proof or now), it cannot be referenced, i.e.

p[] implies [q]
proof
  assume A: p[];
  hence thesis by Ax1;
end;
p[] by A;

is incorrect syntactically (unless the label A was declared earlier for another statement at this level or a higher level).

See Also  

:
hence 
proof
then



Góra

consider

Used for introduction of local constants.

Syntax  

"consider" qualified-list "suchconditions [ simple-justification ]

Examples  

:: Justified by Ax1:
consider A, B being POINT such that 
  A: NE[A, B] by Ax1;

:: Justified by the previous statement:
then consider A, B, C being POINT such that 
  A: NE[A, B] and 
  B: NE[B, C];

Note  

Linking to
consider is not allowed, although consider can be linked to the previous statement, i.e.

assume ex A st p[A];
then consider A such that T: p[A];

See Also  

and
ex
given
such
that



Góra

contradiction

The sentence that is always false. Mostly used as a conclusion when you try to prove something by contradiction.

Examples  

:: Proof by contradiction:
p[] implies q[]
proof
  :: thesis: p[] implies q[]
  assume that 
A:  p[] and
B:  not q[];
  :: thesis: contradiction
  thus contradiction by Axiom;
  :: the above could also read: 
  :: thus thesis by Axiom;
end;

:: Introduction of a local constant:
consider A being POINT such that not contradiction
:: The statement above could also read:
:: consider A being POINT;

See Also  

thesis



Góra

end

Indicates that a proof opened by proof or now is closed. This word must be followed by a semicolon.

Example  

for A holds P[A] implies Q[A]
proof 
  let A be ANY; 
  thus thesis
  proof
    assume P[A];
    hence Q[A] by Ax1;
  end
end

Note  

Since each
proof and now must have a corresponding end, it's good practice to indent the text between proof / now and end so that proof / now and end are in the same columns ("see" each other) and that text between them is indented by a blank or two.

See Also  

;
now 
proof 



Góra

environ

The beginning of the environment. You cannot omit this word in your text, even when the environment is empty. This word may occur only at the beginning of the text (excluding comments).

In the environment, the following items may be introduced:
·sorts  
·predicates  
·global reservations  
·axioms (statements preceded by labels that are assumed to be true)  
·global constants  

The environment ends with the
begin reserved word (that also starts the text proper).

Examples


Shortest possible text:

environ
begin

Another example:

environ

:: Everything is a set:
sort set;

:: A set is an element of another set:
pred set in set;

:: From now on, x, A, B can be used 
:: without the need of declaring their sorts:
reserve x, A, B for set;

:: The empty set:
given empty being set such that
AxEmpty:
  not ex x st x in empty;

:: Equality of sets:
AxEquality:
for A, B holds
  A = B iff 
    for x holds x in A iff x in B;

begin

. . .

See Also  

begin 
given
pred
reserve
sort



Góra

ex

Existential quantifier.

Syntax  

"ex" qualified-list "st" statement

Examples  

ex a, b st p[a, b] & q[a, b]; 

ex x, y being Number st x LT y;

See Also  

for
st



Góra

for

This word has two meanings.

1) Universal quantifier.

Syntax  

"for" qualified-list [ "st" statement ] 
  1. "holds" statement
  2. [ "holds" ] ( quantified-statement )

Examples  

:: holds is obligatory here:
for A being Point holds Z[A]; 

:: Additional constrains are placed after st
:: holds is obligatory here:
for A, B st P[A] holds Q[A] iff R[B]; 

:: Because the statement under the quantifier
:: is also a quantified statement,
:: holds is optional:
for A st P[A] ex B st Q[A, B];

:: But may be used if it enhances readability:
for A st P[A] holds 
  ex B st Q[A, B];

:: holds was not used, because ex B ...
:: is a quantified statement:
for A ex B st P[A, B];

:: After long qualified lists, holds usually enhances readability 
:: by showing clearly where the statements under the quantifier starts:
for x being POINT, y being LINE, z being PLANE holds 
  A[x, y, z];

Note  

st under a universal quantifier is equivalent to implies under holds, i.e. the following statements are equivalent:

for A, B st p[A] & p[B] holds q[A, B]; 
for A, B holds p[A] & p[B] implies q[A, B]; 

See Also  

be / being
ex 
holds
st

2) Global reservation of variables for sorts, allowed only in the environment. The sorts must be declared earlier with the
sort reserved word.

Syntax  

"reserve" variable-list "for" sort ";"

Example  

:: From now on, the variables declared below
:: can be used without the need of declaring their sorts:
reserve L, L1, L2, K for LINE;
reserve A, B, C, D, E for POINT;
reserve P, P1, P2, Q for PLANE;

See Also  

be / being
reserve
sort



Góra

given

Introduction of global constants (when in the environment) or an existential assumption (when in proof, instead of assume, then consider).

Syntax  

"given" qualified-list [ "suchconditions ]

Examples  

:: An example from SETS.mse - 
:: introduction of the empty set:
given empty being set such that
AxEmpty:
  not ex x being set st in[empty, x];

:: An existential assumption:
given A being POINT, L being LINE such that 
  A: A on L; 

Notes  

The two examples above show that both uses of
given (global constant and existential assumption) have exactly the same syntax.

When proving a theorem, you may use the construction above instead of the longer form:

assume ex A being POINT st ON[A, L]; 
then consider A being POINT such that A: ON[A, L]; 

Linking to
given is not allowed.

See Also  

and
assume 
consider
ex
such
that



Góra

hence

Justification of a conclusion by the previous statement (linking).

Syntax  

"hence" statement [ simple-justification ]

Example  

now
  let x;
  assume x in C;
  then x in B by CB, AxSubset;
  hence x in A by BA, AxSubset;
end;

Notes  

For justifying statements other than conclusions by linking,
then may be used.

A link can always be substituted with a simple justification:

p[];
hence q[];

is equivalent to

A: p[];
thus q[] by A;

Linking is forbidden to
assume followed by that, as well as to consider, given, and let.

If a statement is being justified by
proof or now, it may not be linked to the previous statement, i.e.

hence p[]
proof
  . . .
end;

is incorrect syntactically.

However, a statement justified by
proof or now can be linked to, i.e.

p[]
proof
  . . .
end;
hence q[] by Ax1;

See Also  

by
then
thus



Góra

holds

Used only under a universal quantifier. It specifies the conditions that are met by the quantified variables.

Examples  

for A holds p[A] implies q[A];

for A st p[A] holds q[A];

Notes  

The two statements above are equivalent - conditions on the variables under a universal quantifier may also be introduced before
holds using the st reserved word.

Some universally quantified statements may be formulated without
holds, although it still may be used, i.e. the following statements are equivalent:

for A ex B st A = B;
for A holds ex B st A = B;

See Also  

for
st



Góra

iff (if and only if)

Equivalence of statements.

Syntax  

statement "iff" statement

Examples  

p[] iff q[]; 

(p[] iff q[]) implies (q[] iff p[]); 

Note  

Associative notation is not allowed for
iff and implies, i.e.

p[] iff p[] iff p[];
p[] iff p[] implies p[];

are incorrect syntactically. Here follow the correct notations:

(p[] iff p[]) iff p[];
p[] iff (p[] iff p[]);
(p[] iff p[]) implies p[];
p[] iff (p[] implies p[]);

See Also  

&
( )
implies
not
or



Góra

implies

Implication of statements.

Syntax  

statement "implies" statement

Examples  

p[] implies q[]; 

not p[] & p[] implies p[]; 

Notes  

Associative notation is not allowed for
implies and iff, i.e.

p[] implies p[] implies p[];
p[] iff p[] implies p[];

are incorrect syntactically. Here follow the correct notations:

(p[] implies p[]) implies p[];
p[] implies (p[] implies p[]);
(p[] iff p[]) implies p[];
p[] iff (p[] implies p[]);

st under a universal quantifier is equivalent to implies under holds, i.e. the following statements are equivalent:

for A, B st p[A] & p[B] holds q[A, B]; 
for A, B holds p[A] & p[B] implies q[A, B]; 

See Also  

&
( )
iff 
not
or



Góra

let

Used for generalization of variables when proving general sentences.

Syntax  

"let" qualified-list [ "suchconditions ]

Examples  

let A be POINT; 

let A, B be POINT such that A: P[A, B]; 

let A be POINT, L be LINE such that A: ON[L, A];

Note  

Linking to
let is not allowed.

See Also  

and
be / being 
such
that



Góra

not

Negation of a statement.

Syntax  

"not" statement

Examples  

not p[]; 

not (p[] or q[]) iff not p[] & not q[]; 

See Also  

& 
( )
iff 
implies 
or 



Góra

now

The beginning of a diffuse statement. The Mizar-MSE processor will build a theorem based on the given proof skeleton.

A diffuse statement ends with the corresponding end and ; (and this is obligatory).

Example  

now 
  :: theorem: not contradiction;
  let A be POINT; 
  :: theorem: for A begin POINT holds not contradiction;
  assume p[A]; 
  :: theorem: for A begin POINT st p[A] holds not contradiction;
  thus q[A]; 
  :: theorem: for A begin POINT st p[A] holds q[A];
end

Notes  

The example above is equivalent to the following proof:

for A being POINT st p[A] holds q[A]
proof
  :: thesis: for A begin POINT st p[A] holds q[A];
  let A be POINT;
  :: thesis: p[A] implies q[A];
  assume p[A];
  :: thesis: q[A];
  hence thesis;
  :: thesis: not contradiction;
end;

Linking of
now to the previous statement is not allowed.

See Also  

end 
proof 



Góra

or

Disjunction of statements.

Syntax  

statement { "or" statement }

Examples  

p[] or q[] implies r[]; 

p[] or q[] or r[]; 

See Also  

& 
( )
iff 
implies 
not 



Góra

pred

Introduction of predicates, allowed only in the environment. Except for equality and inequality of variables and constants, all facts introduced as axioms in the environment or proven in the text proper are expressed using predicates.

Syntax  

"pred" 
1. identifier "[" [ sort-list ] "]"
2. sort-list identifier sort-list

Examples  

:: A predicate stating the p holds:
pred p[];

:: A predicate stating that a set is empty:
pred empty[set];

:: A predicate stating that a set is an element of another set:
pred in[set, set];

:: The same predicate defined using infix notation:
pred set in set;

:: A predicate stating that a set is the union of two other sets:
pred set union_of set, set;

Note  

The predicate definition itself does not assign any meaning to the predicate - it is just a declaration of notation that will be used in the article. Use axioms and global constants in the environment to define semantics of the introduced predicates.

See Also  

[ ]
sort



Góra

proof

Complex justification - the beginning of a proof.

A proof ends with the corresponding end and ; (and this is obligatory).

Example  

for A being POINT st p[A] holds q[A]
proof
  :: thesis: for A begin POINT st p[A] holds q[A];
  let A be POINT;
  :: thesis: p[A] implies q[A];
  assume p[A];
  :: thesis: q[A];
  hence thesis;
  :: thesis: not contradiction;
end;

Notes  

The example above is equivalent to the following diffuse statement:

now 
  :: theorem: not contradiction;
  let A be POINT; 
  :: theorem: for A begin POINT holds not contradiction;
  assume p[A]; 
  :: theorem: for A begin POINT st p[A] holds not contradiction;
  thus q[A]; 
  :: theorem: for A begin POINT st p[A] holds q[A];
end

Linking to
proof to the previous statement is not allowed.

Simple justifications can be expressed with the
by reserved word.

See Also  

end
now
thesis



Góra

reserve

Global reservation of variables for sorts, allowed only in the environment. When reserving a variable, you must specify its sort - sorts can be introduced through the sort reserved word.

Syntax  

"reserve" variable-list "forsort

Examples  

reserve x, y, z, A, B, C for set;

reserve L, L1, L2, K for LINE;
reserve A, B, C, D, E for POINT;
reserve P, P1, P2, Q for PLANE;

Notes  

Even if a variable is reserved for a given sort in the environment, you can later redefine its sort by using
be / being. However, redefinitions should not be encouraged (they don't enhance readability).

Also, if a variable is not reserved at all, it can be later introduced by using
be / being.

Usually, only commonly used variables are reserved in the environment; variables that are used seldom are usually assigned to sorts in qualified lists.

See Also  

be / being
for
sort



Góra

sort

Introduction of sorts (or types), allowed only in the environment. If you want to use constants and / or variables (including predicates with arguments), you must introduce some sorts.

Syntax  

"sort" sort-list

Examples  

sort set;

sort LINE, POINT, PLANE;

Notes  

The sort definition itself does not assign any meaning to the sort - it is just a declaration of notation that will be used in the article. Use predicates, axioms and global constants in the environment to define semantics of the introduced sorts.

Multiple sorts can be introduced in a single instruction or multiple instructions.

See Also  

be / being
pred
reserve



Góra

st

st means "such that" and is used under a quantifier.

Examples  

ex A st p[A]; 

for A, B st p[A] & p[B] holds q[A, B]; 

Notes  

st and such that have different meanings. The first word is used under a quantifier, while the other in the conditions clause (assume, consider, given, and let).

st under a universal quantifier is equivalent to implies under holds, i.e. the following statements are equivalent:

for A, B st p[A] & p[B] holds q[A, B]; 
for A, B holds p[A] & p[B] implies q[A, B]; 

See Also  

ex
for
holds



Góra

such

Precedes the conditions clause after given, consider, and let.

Syntax  

"such" conditions

Examples  

given x such that 
  a: A[x] and 
  b: not A[x] by Ax1;

consider y such that a: y = x and b: B[y, y]; 

let x be ANY such that a: x = y and b: A[y]; 

Note  

Linking to statements with a conditions clause is not allowed.

See Also  

and
by
consider
given
let
that



Góra

that

Begins the conditions clause after assume, consider, given, and let.

Syntax  

"that" [ label ":" ] statement 
  { "and" [ label ":" ] statement } [ simple-justification ]

Examples  

assume that a: A[] and b: B[];

given x such that 
  a: A[x] and 
  b: not A[x] by Ax1;

consider y such that a: y = x and b: B[y, y]; 

let x be ANY such that 
  a: x = y and 
  b: A[y]; 

Note  

Linking to statements with a conditions clause is not allowed.

See Also  

:
and
assume
by
consider
given
let
such



Góra

then

Justification of a statement (other than a conclusion) by the previous statement (linking).

Syntax  

"then" statement [ simple-justification ]

Example  

now
  let x;
  assume x in C;
  then x in B by CB, AxSubset;
  hence x in C by AxSubset;
end;

Notes  

For justifying conclusions by linking,
hence may be used.

A link can always be substituted with a simple justification:

p[];
then q[];

is equivalent to

A: p[];
q[] by A;

Linking is forbidden to
assume followed by that, as well as to consider, given, and let.

If a statement is being justified by
proof or now it may not be linked to the previous statement, i.e.

then p[]
proof
  . . .
end;

is incorrect syntactically.

However, a statement justified by
proof or now can be linked to, i.e.

p[]
proof
  . . .
end;
then q[] by Ax1;

See Also  

by
hence



Góra

thesis

thesis means "what remains to be proved". May not be used under a quantifier (for / ex) or outside of a proof.

Examples  

In the examples below, the current
thesis is shown in the comment after each step of the proof.

for A holds p[A] iff q[A]
proof
  :: thesis: for A holds p[A] iff q[A] 
  let A; 
  :: thesis: p[A] iff q[A]
  thus p[A] implies q[A];
  :: thesis: q[A] implies p[A]
  assume q[A];
  :: thesis: p[A]
  thus p[A];
  :: thesis: not contradiction
  thus thesis;
end;

p[] implies q[]
proof
  :: thesis: p[] implies q[]
  assume that 
A:  p[] and
B:  not q[];
  :: thesis: contradiction
  thus contradiction by Axiom;
  :: the above could also read: thus thesis by Axiom;
end;

See Also  

contradiction
proof  
thus  
 


Góra

thus

Conclusion; allowed in proofs and diffuse statements only.

Syntax  

"thus" statement [ simple-justification | complex-justification ]

Examples  

now
  let x;
  thus in[A, x] iff in[B, x] by AB, BA;
end;

thus p[a]; 

thus p[a] by A_label; 

thus p[a]
proof
  . . . 
end;

See Also  

hence 



Góra

Tematy

&

:

::

;

,

[ ]

( )

=

<>

and

assume

be / being

begin

by

consider

contradiction

end

environ

ex

for

given

hence

holds

iff

implies

let

not

now

or

pred

proof

reserve

sort

st

such

that

then

thesis

thus