In this paper we ask the question whether the extended Frege proof
system EF satisfies a weak version of the deduction theorem. We
prove that if this is the case, then complete disjoint NP-pairs
exist. On the other hand, if EF is an optimal proof system, then
the weak deduction theorem holds for EF.
Hence the weak deduction property for EF is a natural intermediate
condition between the optimality of EF and the completeness of its
canonical pair.
We also exhibit two conditions that imply the completeness of the
canonical pair of Frege systems.