A finite model property for fully complete denotational models of propositional logics is investigated using fully complete translations to compare programming languages and logics. The main result is that there can be no finite and fully complete models of linear or affine propositional logic. This is shown to be a consequence of Loader's result that contextual equivalence for finitary PCF is not decidable by giving a fully complete translation from finitary PCF into a lambda-calculus for a dual affine/non-linear logic. This extends conservatively to a fully complete cps translation from finitary PCF with control (mu PCF) into the simply-typed lambda calculus, showing that a fully complete model of the latter yields a fully abstract model of the former.
