There is no bijection (one to one mapping) between E and P(E), where P(E) stands for the set of E subsets.
Goal- Formalize the above statement and prove it;
- Learn how to represent sets using types or predicates;
- Learn how to turn a hand made proof into a PVS proof scenario.
Formalization process - PVS prelude contains many mathematical definitions: check it out (Meta-x view-prelude-file) for the notion of bijection (bijective? predicate);
- Sets may be represented in two ways, depending on the context: types or predicates (functions of type [T -> bool], where T is a type). Here are some hints on set representation related to this statement:
| Mathematical set | PVS representation | {0, 1, 2, 3, ...}
the set of natural numbers | nat
% one of basic types introduced in PVS prelude |
{5, 7, 11} | (LAMBDA(n: nat): n=5 OR n=7 OR n=11)
{n: nat | n=5 OR n=7 OR n=11} % syntactic variant of above expression
The type of these equivalent expressions is [nat -> bool]. | |
P({0, 1, 2, 3, ...})
the set of subsets of {0, 1, 2, 3, ...} |
[nat -> bool] % This is a type. |
E | E % as a type
E may be introduced through the declaration E: TYPE (for instance, as a theory parameter). | P(E)
the set of E subsets |
[E -> bool] % This is a type. |
- This should allow you specify your statement as a PVS theorem.
Proving the statement - Start the PVS proof, and quickly get stuck with a strange sequent with one consequent and no antecedent (no hypothesis)!
- You need to think ... maybe with a piece of paper and a pen (or digital tablet).
Look for your own manual proof, before looking at this manual proof |
 Updating... Paul Y Gloess, 23 sept. 2013, 08:43 Paul Y Gloess, 23 sept. 2013, 08:42 Paul Y Gloess, 23 sept. 2013, 07:14
|
