Peano arithmetic is a formal axiomatic system. Infinitely many axioms can be built by replacing with formulas in the language of PA. In PA a theorem is a formula that is either an axiom or can be derived from finitely many axioms with finitely many rules of inference.

Inference Scheme

1. from and , infer
2. from , infer
3. from , infer

can be any formula obtained by renaming variables in .

ZFC is a pure set theory meaning that every object is a set. It uses the same logical axiom scheme and inference scheme as PA - but the resulting axioms are different.

The Zermelo-Fraenkel axioms are (TODO: write them out).

1. Extensionality
2. Pairing
3. Union
4. Power set
5. Infinity
6. Foundation
7. Choice
8. Separation scheme
9. Replacement schme

A statement is consitent with a familily of axioms if it cannot be disproven based on these axioms.

A statement is independent of a family of axioms if it can neither be proven nor disproven based on these axioms.

TODO

TODO

TODO

Let be a formula in ZFC. We define

ZFC+ is obtained from ZFC by taking

• symbols from ZFC, and a new symbol
• formulas of ZFC with one unquantified variable replaced by

and the following axioms

• Equality axioms and logical axiom schemes of ZFC
• non-logical axioms of ZFC
• is countable and transitive
• with any non-logical axiom of ZFC.

A forcing notion for a set is a any non-empty set .

Two elements are compatible if they have a common extension in

Let be a set. If and then is an extension of .

An ideal of a forcing notion is a subset satisfiying

1. and then (downward stability)
2. then there exists with (directedness)

A subset is dense if every has an extension in .

It is dense above if every extension of has an extension in .

An ideal of a forcing notion for is generic relative to if it intersects every dense subset that lies in .