So light SPV clients give the user the ability to obtain merkle proofs (from a full node) that a given transaction is included in a block. Is there some cryptographic mechanism by which an SPV client could obtain proof that a transaction (or type of transaction) is not included in a block, while still being relatively "light" (O(log(n), say)?
Asking for a layer 2 solution ;)
There is no known way to do this with the current consensus rules nor does it seem likely except via computationally expensive general ZKP.
The normal way to make compact proofs of non-membership is to have a hash tree which is ordered by the key you're looking to prove non-membership on. The proof is just the two neighbors that are greater and lesser than the key in question.
To show non-membership in a block this with a general ZKP (like bulletproofs) you would have to write an arithmetic circuit that computes the hash root of a block, and also scans over transactions looking for the thing-of-interest. If done using a bulletproof the proofs would be log in the size of the circuit, and take time to prove and verify linear in size... so they'd be somewhat slow but bandwidth efficient.
Client side filters (neutrino) allow you to check whether a certain transaction is included in a block. This can act as a proof of non-inclusion.
https://github.com/bitcoin/bips/blob/master/bip-0157.mediawiki https://github.com/bitcoin/bips/blob/master/bip-0158.mediawiki
Note that this is not part of consensus, so nodes could lie to you. There won't be an SPV merkle proof connected to PoW, so perhaps it's not good enough for what you have in mind.
