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 Don't immediately look at the solutions |