Explanation of Proof-of-Encryption Regarding the question  Provable Encryption,
I'm trying to understand how a 'proof of encryption' might actually work.

What I can deduce from the answers is this: we need a cryptographic scheme that is somewhat homomorphic, in the sense that some algebraic structure on the set of plaintext is respected by the encryption transformation (like RSA and Rabin (plain $x^2$ version) respect multiplication in the underlying finite rings).

Can someone explain this in more detail? How can it be used to decide whether or not a given string is actually the ciphertext of something w.r.t. to a given public key?

I mean, in a sense all elements of the underlying finite field (or lattice or whatever algebraic structure the scheme is based on) are ciphertexts of something, right?
Not all encryption schemes have the property that all strings are ciphertexts of something. For instance, if you created a version of RSA where you added an extra 0 at the end of every ciphertext, this would still be a valid encryption scheme, but any ciphertext with a 1 at the end would not be an encryption of anything.

In a public-key cryptosystem, to prove that a ciphertext is an encryption of something, you can prove that you have some plaintext $x$ such that $Enc_k(x)=y$ where $k$ is the public key and $y$ is the ciphertext.

There are generic techniques which allow you to create proofs of arbitrary computable statements, namely that you know some value $x$ such that $f(x) = y$. There are also generic techniques that allow you to do this in a non-interactive way. By definition, these techniques reveal nothing about $x$ except that it satisfies the given statement.

Note: For certain functions, we know of more efficient ways to do zero knowledge proofs. Some answers in the question you posted refer to some more efficient ways of doing this in the case of public key cryptosystems. But for any computable function there is always some way of making a zero-knowledge proof using generic techniques.



EDIT

I don't really understand how the generic protocols work under the hood, but I do understand the following:


First, you can represent the function as a circuit. As long as you have bounds on how long a function will take to do this (e.g. the max number of iterations of a for loop), you can always represent a function this way. (May not be very efficient though.)
Then you convert the circuit into a list of constraints that need to be satisfied. This article by Vitalik Buterin has, among other things, a good explanation of how this step is done.
Finally, there are tools such as libsnark that, given a set of constraints and a correct input provide a way to generate a Short Non-Interactive Argument of Knowledge (SNARK) that the constraints were satisfied. This is the part where I don't understand how it works.


By Non-interactive, it means that once the person encrypting has generated a SNARK, $\pi$ that they know the plaintext to a ciphertext $y$ and has sent this proof to the verifier, no more interaction is needed. Since no interaction is needed, anyone who gets access to $\pi$ and $y$ can verify that $y$ is an encryption of something.