Theories and Proofs

A theory (in a given formal language) is a combination of sentences (formulas) in that language. This is certainly different from the every day understanding. A theory in this sense is more like a collection of axioms formed without any regard for independence - just a set of formulas in a formal language.

A proof in a formal language is a finite sequence of formulas in which subsequent members are logically obtained (or derived) from any of the preceding ones. For example, let φ and ψ be formulas, x a variable, while a a constant - one possible value of variable x. The following sequences are proofs:

φ, ψ, φ ∨ ψ
φ(a), ∃x φ(x),
φ, φ→ψ, ψ,
∀x φ(x), φ(a).

Proofs may be long, but what is important is that they are finite. In fact, a proof is a proof of its last formula. If the formulas in the proof that were not derived from others come from a certain theory, the last formula in the proof is said to be deducible in that theory.

More accurately, if T is a theory in a formal language L and φ a formula in L, we say that φ is deducible from T if there is a proof ψ₁, ψ₂, ..., ψ_n, in which ψ_n = φ and any formula ψ_i in the proof either belongs to T, or is derived from the formulas preceding it in the proof. We write T ⊢ φ if φ is deducible from T.

Truth be told, not all proofs in mathematics are in the form just described. For example, proofs by contradictions start with assuming the opposite of what is supposed to be proved and shows by a sequence of logical derivations that such an assumptions leads to a contradiction. Often, after a statement such as ∃x φ(x) has been proven, a mathematician would say "Let a be such that φ(a)." This method of proof is also outside the limited scope of the above Description. For a more inclusive definition of proof see, for example [Smullyan] or [Robinson]. The essential point regardless of a definition is the finiteness requirement: a proof is a finite sequence of either axioms, assumptions or deductions from the previous terms.

Observe that the symbol ' ⊢' does not belong to language L, although, it is used as a shorthand to describe a relation between a theory and a sentence, both of which expressed in terms of L. Symbols like ' ⊢' that are used in a discourse about mathematics are said to be metamathematical, or to belong to metamathematics.

As an example, consider a theory that consists of the three group axioms:

∀x {[x • e = x] ∧ [e • x = x]},
∀x∀y∀z {(x • y) • z = x • (y • z)},
∀x∃y {[x • y = e] ∧ [y • x = e]}.

The following is a proof that the unity element is unique:

∀x {[x • e = x] ∧ [e • x = x]},
let there be f such that ∀x {[x • f = x] ∧ [f • x = x]},
e = f • e = f,
e = f.

Not all statements in language L may be proved in theory T. For example, the statement ∀x∀y (x • y = y • x) could not be proved in the group theory. The statement claims the commutativity of the group operation &bull. But as we know, the are groups that are not commutative. In this sense, the group theory is incomplete: there are sentences in the language of the group theory that are not logical consequences of the theory. Incidentally, ∃x∃y (x • y ≠ y • x) is another such sentence because there are commutative groups. This shows that there are sentences that could not be proved nor disproved in the group theory. This is because (logically)

¬ ∀x∀y (x • y = y • x) = ∃x∃y (x • y ≠ y • x).

Gödel's (first) incompleteness theorem states more generally that in the language of any sufficiently powerful formal theory there are undecidable sentences, i.e., sentences that can't be either proved or disproved from the theory's axioms.

Back to What Is Infinity?

References

D. Marker, Logic and Model Theory, in T. Gowers (ed.), The Princeton Companion to Mathematics, Princeton University Press, 2008, pp. 635-646
A. Robinson, Non-standard Analysis, Princeton University Press (Rev Sub edition), 1996
R. M. Smullyan, First-Order Logic, Dover, 1995

71930170