I understand that second order logic does not have a sound and complete proof system but I was wondering, how this lack of sound and complete proof system affects the usefulness of the SoL.
As far as I understand SoL is a very strong logic that allows us to pin down the structure of Natural numbers. However, not having a sound and complete proof system means that there will be statements in the language that cannot be proved using finite steps via computers as opposed to FoL. Is my understanding correct?
My question is that how not being able to prove things using finite steps affect the usage of SoL? Is it deemed useless because proofs cannot be checked by computers or is it still useful and popular among mathematicians?