Questions

Should all theorem provers be based on type theory?
- Apparently not, ZFC could work too, but it is more difficult to have constructive proofs in ZFC?
Why only till second order logic? After that we just say higher order logic. Why not 3rd, 4th, etc?