The Curry-Howard correspondence suggests the analogy of computation with lambda calculus and logical proof systems. As a non-expert it seems that same analogy extends roughly to lambda calculus and a lisp system
For that reason, only _typed_ lambda calculi have any hope of corresponding to a proof system. You could rephrase Lisp as a Unityped system, but I seriously doubt it would be consistent.
Perhaps a para-consistent logic might work, but we're getting very exotic here.
It's not. (x -> x) is always inhabited, so if you have a fixed point combinator (x -> x) -> x then every theorem is true.