# 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 ψ_{1}, ψ_{2}, ..., ψ_{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

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 *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 *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 *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) = ∃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.

- Infinitesimals. Non-standard Analysis
- Formal Languages
- Theories and Proofs
- Models and Metamathematics
- Hyperintegers and Hyperreal Numbers
- Structure of Hyperreal Numbers
- The Transfer Principle
- Common Concepts - A Non-standard View
- Is .999... = 1? A Non-standard View

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

|Contact| |Front page| |Contents| |Up| |Algebra|

Copyright © 1996-2018 Alexander Bogomolny70519672