Undecidable Tao

Proposition VI: To every ω-consistent recursive class c of formulae there correspond
recursive class-signs r, such that neither v Gen r nor Neg(v Gen r) belongs to Flg (c) (where v is the free variable of r).

or:

All coherent axiomatizations of arithmetic contains undecidable propositions.

In one of the most important works of logic of all time Kurt Gödel in 1931 proved two theorems limiting based on Principia Mathematica, but in fact valid (...and related systems) for every formal system powerful enough.

The first incompleteness theorem states that:

In every mathematical theory T expressive enough to contain arithmetic, there is a formula φ such that if T is consistent, then neither φ nor its negation Neg(φ) are provable in T.

with some simplification:

In any consistent formalization of mathematics that is sufficiently powerful to axiomatize the elementary theory of natural numbers - that is, powerful enough to define the structure of natural numbers with the operations of sum and product - it is possible to construct a proposition that is syntactically correct which can be neither proved nor disproved within the system itself.

The second incompleteness theorem of Gödel, already quoted, obtained, essentially, by formalizing the proof of the first incompleteness theorem within the theory itself, states:

For any formal effectively generated theory T including basic arithmetical truths and also certain truths about formal provability, T includes a statement of its own consistency if and only if T is inconsistent.

with some simplification:

No consistent system can be used to prove its own consistency.