**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