In PDF of lecture 8, slide 78, it is shown a way of proving that ALLcfg is undecidable, by using computational histories. Specifically - it is a proof by contradiction: buiding a reduction from ALLtm to ALLcfg, thus showing that ALLtm is decidable, and hence the contradiction.
My question is - as far as I understand it (and I probably don't understand it correctly), the same thing could be done with EMPTYcfg, which is known to be decidable.
We just replace the word "not" in the slide. With little more details: given <M,w>, we construct a PDA that accepts only accepting computational of M on w.
Result: if M accepts w —> the PDA will not be empty. Else —> the PDA will be empty.
Isn't this a plausible iff connection ?