The Theory pf
First we introduce for these definitions the new theory "pf", a child of zfc.
xlsml
open_theory "zfc";
set_pc "basic_hol";
delete_theory"pf" handle _ => ();
new_theory"pf";


hereditary properties
A property of sets is "pf_hered" if a function inherits this property from the sets in its field.
i.e. if all functions over a field of pf_hered sets are themselves pf_hered.


pf_hereditary
A pure function is a function which has all the pf_hereditary properties.
This is an oblique way of saying that the function can be constructed from the empty set by a process which involves only the formation of functions from functions already constructed.

consistency proof
We now prove that there exists a pure function.

