[FOM] SOL vs. ZFC

[Joe Shipman]

The set of validities in Second Order Logic with standard semantics is Pi^1_2 complete, so we can't give a complete axiomatization. My question has two parts:
1) is there any commonly used system of axioms for second order logic that includes sentences which ZFC does not prove are validities?
2) is there any sentence which ZFC proves is a validity of second order logic, but which is not a consequence of any commonly used system of axioms for second order logic other than the system "enumerate sentences with ZFC-proofs of their validity"?

-- JS


Sent from my iPhone