I'm really interested by questions like:
Why is second order logic irreducible to first order logic if I could use first order logic to reason about the behavior of a turing machine running a second order logic theorem prover with whatever inputs I like?
How do I get something that can do what I can do, which is to say take any formal system and prove theorems with it? How do you determine what formal systems are "valid" logics? (Leading to sensible conclusions rather than nonsense like A & ~A)