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.

  • 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 

     % 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         % as a type
     E may be introduced through the declaration E: TYPE (for instance, as a theory parameter).
    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
Not E<-->P(E) - thumb

Do not immediately click on thumb for enlarged image.
Don't immediately look at the solutions
Paul Y Gloess,
23 sept. 2013 à 08:43
Paul Y Gloess,
23 sept. 2013 à 08:42
Paul Y Gloess,
23 sept. 2013 à 07:14