|
|
Mizar-MSE Syntax |
|
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
Top
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
Top
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;
Top
Ends all statements in Mizar-MSE. The use of ; is forbidden after proof, now, environ, and begin.
Example
thus thesis by Ax1;
Top
Separates elements in lists of identifiers:
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;
Top
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
Top
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
Top
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
Top
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
Top
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
Top
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
Top
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 L 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
Top
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
Top
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
Top
Used for introduction of local constants.
Syntax
"consider" qualified-list "such" conditions [ 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
Top
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
Top
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
Top
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:
· | axioms (statements preceded by labels that are assumed to be true)
|
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
Top
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
Top
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
Top
Introduction of global constants (when in the environment) or an existential assumption (when in proof, instead of assume, then consider).
Syntax
"given" qualified-list [ "such" conditions ]
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
Top
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
Top
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
Top
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
Top
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
Top
Used for generalization of variables when proving general sentences.
Syntax
"let" qualified-list [ "such" conditions ]
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
Top
Negation of a statement.
Syntax
"not" statement
Examples
not p[];
not (p[] or q[]) iff not p[] & not q[];
See Also
&
( )
iff
implies
or
Top
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
Top
Disjunction of statements.
Syntax
statement { "or" statement }
Examples
p[] or q[] implies r[];
p[] or q[] or r[];
See Also
&
( )
iff
implies
not
Top
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
Top
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
Top
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 "for" sort
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
Top
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
Top
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
Top
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
Top
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
Top
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
Top
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
Top
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
Top
|
|
|
|