   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.

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.

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;

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[];

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.

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.

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[];

&

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

assume is not allowed if followed by conditions.

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).

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.

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).

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

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];

Góra

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

Examples

p[] implies q[]
proof
:: thesis: p[] implies q[]
assume that
A:  p[] and
B:  not q[];
:: 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;

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.

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:
 ·
 ·
 ·
 · 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

. . .

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;

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];

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;

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];

given is not allowed.

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;

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;

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;

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[]);

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];

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

let is not allowed.

Góra

 not

Negation of a statement.

Syntax

"not" statement

Examples

not p[];

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

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
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;
end;

now to the previous statement is not allowed.

Góra

 or

Disjunction of statements.

Syntax

statement { "or" statement }

Examples

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

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

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.

[ ]
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;
end;

Notes

The example above is equivalent to the following diffuse statement:

now
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

proof to the previous statement is not allowed.

Simple justifications can be expressed with the
by reserved word.

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.

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.

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 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];

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.

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.

:

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

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;

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;

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];
thus thesis;
end;

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

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; 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  