A Note about Theories
Most of the interesting results that we are going to consider later in the course require that a theory be a clearly defined kind of object. For that reason, we need to assume the following. Whenever we refer to a "theory" we will mean a thing that has the following features:

1. A finite number of basic elements (an alphabet)

2. Finite set of formation rules that tell us which combinations of these elements are well-formed formulas (this is like the most basic level of the grammar, and includes statements which are obviously not true -- just as it is grammatical in English to say false things like "Lake Ontario contains no water," and also weird things like "The color Nixon is taller than Smith winks," it is grammatical though false to say in a standard axiomatization of arithmetic something that means "1 is not equal to 1").

3. A finite set of axioms or axiom schemas (these are assumed statements, or schemas out of which you can derive assumed statements)

4. A finite set of inference rules.

We call anything provable in a theory (without using extra assumptions or premises) a theorem of that theory. (Things are proved using the application of rules to the axioms to produce new sentences that are not axioms.)

Sometimes, we will call a language the total set of theorems of the theory (this is common in computer science, not so much in logic). Thus, the language is all the statements that can be derived from a theory. All of the theorems of arithmetic is all of the statements of arithmetic you can derive from basic arithmetic theory, and we can call this the "language of arithmetic."

Here is an example of most of a theory for arithmetic (I follow Smullyan and Mendelson); this kind of theory is sometimes called Peano Arithmetic, after a mathematician who first proposed a similar list of axioms:

1. Elements. We'll hide these for now, since we are later going to rephrase them in a different way. But these include: ', 0, +, v, (, and ). More on this later.
2. Formation rules: here I'll just give some examples. Any two terms flanking a "+" yields a new term; any two terms flanking a "=" makes a sentence; any sentence with a "¬" in front of it is a sentence; any two sentences flanking a "→" form a sentence; etc.
3. Axioms (the first 5 constitute standard first order logic, and the rest are a version of Dedekind's axiomatization of arithmetic; assume P, Q, R are any sentences or predicates, so that P(x) is a well formed formula in which at least x appears as a free term). v₁ is short for v_*, and v₂ is short for v_**, and etc.

   A1: (P → (Q → P))
   A2: ((P → (Q → R)) → ((P → Q) → (P → R))
   A3: ((¬Q→¬P) → ((¬Q → P) → Q))
   A4: (Av₁)P(v₁) → P(t), where t is any term that replaces the free occurences of v₁ in P.
   A5: (∀v₁)(P → Q) → (P → (∀v₁)Q) if P contains no free occurences of v₁.
   A6: (v₁=v₂ → (v₁=v₃ → v₂=v₃))
   A7: (v₁=v₂ → v₁'=v₂')
   A8: ¬(0=v₁')
   A9: (v₁'=v₂' → v₁=v₂)
   A10: (v₁+0) = v₁
   A11: (v₁+v₂') = (v₁ + v₂)'
   A12: (v₁ * 0) = 0
   A13: (v₁ * v₂') = ((v₁ * v₂) + v₁)
   A14: For any well formed formula P(x) of the theory, P(0) → (∀v(P(v) → P(v')) → ∀v(P(v)))

   
   For A6-A13, one might expect a quantifier, but that is usually implicit in the metalanguage. We are used to that: it means think of v₁ as any arbitrary number.
   
   
4. Rules: modus ponens, and universal instantiation.

Think now of Hilbert's two questions, to which we will add a third:

• Decidability: can we prove this theory is decidable? A theory is decidable if there is some mechanical method that will tell us, for any sentence (formed using the symbols of this theory) whether that sentence is a theorem of this theory. (A theorem of the theory is a sentence provable from the theory alone, without adding premises to your argument/proof.)
• Consistency: can we prove that this theory is consistent? Note then that if we accept that this theory is arithmetic, then if we prove this is consistent we have proven that arithmetic is consistent. Recall that consistency means that for no statement P can we prove both P and ¬P. In this system, and in any standard implementation of first order logic, from P and ¬P we can prove any sentence Q -- so, if your system is inconsistent, it is useless because it will allow you to prove all falsehoods. (To convince yourself, prove (¬P → (P → Q)) using the above axioms!) But, conversely, that means if we can show that you cannot prove just any old sentence (such as, say, the claim that ¬(1=1)) then we would know that this system was consistent.
• Completeness: can we prove this theory is complete? A theory is complete if all the truths of the theory are provable with the theory.

---

The axiomatization used above follows that in Mendelson, Introduction to Mathemetical Logic, 3rd Edition, 1987. The elements of the language are from Smullyan Godel's Incompleteness Theorems.