PVS‎ > ‎exercises‎ > ‎

### no bijection

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

Do not immediately click on thumb for enlarged image.
Don't immediately look at the solutions
• (one proof);
• (three proof variants, more elegant than above proof).
ċ
Paul Y Gloess,
23 sept. 2013, 08:43
ċ
Paul Y Gloess,
23 sept. 2013, 08:42
ą
Paul Y Gloess,
23 sept. 2013, 07:14