This is perhaps closer to computational complexity than to logic, but there are many open problems in propositional proof complexity that are analogous to, and have close connections to, well-known open problems in computational complexity.  For example, it is widely believed that there are tautologies whose proof in a <a href="https://en.wikipedia.org/wiki/Frege_system">Frege system</a> is necessarily exponential in size; however, so far, no superpolynomial lower bounds have been proven.