Formal systems or axiomatized formal theories

In chapter 3, Peter Smith defines formal systems or, as he calls them, axiomatized formal theories (I will use AFT as an abbreviation for this phrase).

A theory T is an AFT if...

1. T is couched in an interpreted formal language, that is, a formal language L of well-formed formulas (wff's) that are meaningless sequences of symbols, together with an interpretation I that gives a meaning to the symbols and wff's in L, such that:
• The property of being a wff in L is effectively decidable.
• The function that computes the truth values of wff's is effectively computable.
2. T includes axioms such that whether or not a wff is an axiom is an effectively decidable property.
3. T includes a proof system (or deductive system or inference rules) such that whether or not a sequence of wff's is a valid sequence of applications of inference rules is an effectively decidable property.
4. It is effectively decidable whether or not a sequence of wff's is a proof in T, that is, a valid sequence of applications of inference rules starting from T's axioms. 

A few comments about the interpreted language of T: 

• the language L is made up of a finite alphabet of symbols and syntactic rules for building wff's out of alphabet symbols. 
• The alphabet contains two types of symbols:
• The logical vocabulary contains the symbols for variables, logical connectives (we assume from now on that the logical vocabulary of L contains the negation connective ¬), quantifiers, the identity (or equality) symbol, and parentheses.
• The non-logical vocabulary contains the symbols for constants (e.g., the constant 0), predicates (e.g., the predicate/property of being even) and functions (e.g., the successor function).
• The syntactic rules of L define the "grammar" of the language. For example, ¬ is a unary prefix operator while ∨ and ∧ are binary infix operators.
• The interpretation contains a domain D of objects and a mapping from:
• the constants of L to D, giving meaning to the constants
• the predicate symbols of L to properties and relations in D, giving meaning to the predicates
• the function symbols of L to functions over D, giving meaning to the functions

The middle section of Chapter 3 defines important notation and concepts, some of which we have discussed previously:

1. The notation T ⊦ w means that w is a theorem of T, that is, T proves w.
2. T is sound if every theorem of T is true according to I.
3. T is decidable if the property of being a theorem of T is decidable. Note that decidability (i.e., always being able to tell if any given wff is a theorem) is a stronger property than being able to tell if a given sequence of wff's is a valid proof (see part 4 of the definition of AFT above). The difference is akin to the difference between being able to discover a proof and being able to check a known proof.
4. T decides w if either T ⊦ w or T ⊦ ¬w. 
5. T correctly decides w if T ⊦ w whenever w is true and  T ⊦ ¬w whenever w is false according to I.
6. T is negation-complete if T decides every sentence (i.e., wff with no free variables) in L. Recall the distinction between negation completeness and semantic completeness.
7. T is consistent if there is no sentence w such that T ⊦ w and T ⊦ ¬w.

Let's emphasize the difference between decidability and negation-completeness.

• An AFT is negation-complete if its proof system and axioms are powerful enough to prove or disprove any wff of its language.
• An AFT is decidable if there exists an algorithm that can determine whether any wff is one of its theorems.

So, while all negation-complete AFTs are decidable (see below), a decidable AFT does not have to be negation-complete. For example, a propositional AFT (i.e., without quantifiers) is decidable, since we can use truth tables to determine which propositions follow from the axioms, but the axioms may not be enough to prove or disprove all wff's. For example, if the logical language includes the propositional variables p and q and the AFT contains the single axiom ¬p (that is, p is false), then the AFT cannot prove nor disprove the wff p ∨ q (because T cannot infer the truth value of q). Nevertheless, this AFT is trivially decidable (e.g., a truth table tells us that p ∨ q is not a theorem).

The last part of Chapter 3 proves important properties of AFTs, namely:

1. The set of wff's of any AFT is effectively enumerable.
2. The set of sentences of any AFT is effectively enumerable.
3. The set of proofs of any AFT is effectively enumerable.
4. The set of theorems of any AFT is effectively enumerable.

In general, effective decidability is a stronger property than effective enumerability. Being able to enumerate the theorems of an AFT does NOT imply that the AFT is decidable. Even if we are able to list all of the theorems, determining that a wff is not a theorem may require going through the whole list of theorems, which is often infinite. Therefore, this approach is not an algorithm: it does not always terminate in a finite number of steps. However...

5. All negation-complete theories are decidable.

There are two cases to consider in a proof sketch. If the AFT is consistent, given any wff w, one can simply go through the enumeration of its theorems and stop as soon as either w or ¬w is found (which is guaranteed to happen since the AFT is negation-complete). If the AFT is inconsistent, then its set of theorems is identical to its set of wff's (i.e., in this case, the AFT proves all of its wff's); so the AFT is, by definition, decidable.