Metalogical results

It is a corollary of Godel’s incompleteness theorem that there is no deductive system (that is, no notion of provability) for second-order formulas that simultaneously satisfies these three desired attributes:

• (Soundness) Every provable second-order sentence is universally valid, i.e., true in all domains under standard semantics.
• (Completeness) Every universally valid second-order formula, under standard semantics, is provable.
• (Effectiveness) There is a proof-checking algorithm that can correctly decide whether a given sequence of symbols is a valid proof or not.

— Wikipedia on Second-order logic

2013.10.14 Monday ACHK