Object Theory - Expansion of The Notion of Formal System - Well-formed Objects

Well-formed Objects

If a collection of objects (symbols and symbol-sequences) is to be considered "well-formed", an algorithm must exist to determine, by halting with a "yes" or "no" answer, whether or not the object is well-formed (in mathematics a wff abbreviates well-formed formula). This algorithm, in the extreme, might require (or be) a Turing machine or Turing-equivalent machine that "parses" the symbol-string as presented as "data" on its tape; before a universal Turing machine can execute an instruction on its tape, it must parse the symbols to determine the exact nature of the instruction and/or datum encoded there. In simpler cases a finite state machine or a pushdown automaton can do the job. Enderton describes the use of "trees" to determine whether or not a logic formula (in particular a string of symbols with parentheses) is well formed. Alonzo Church 1934 describes the construction of "formulas" (again: sequences of symbols) as written in his λ-calculus by use of a recursive description of how to start a formula and then build on the starting-symbol using concatenation and substitution.

Example: Church specified his λ-calculus as follows (the following is simplified version leaving out notions of free- and bound-variable). This example shows how an object theory begins with a specification of an object system of symbols and relations (in particular by use of concatenation of symbols):

(1) Declare the symbols: {, }, (, ), λ, plus an infinite number of variables a, b, c, ..., x, ...

(2) Define formula: a sequence of symbols

(3) Define the notion of "well-formed formula" (wff) recursively starting with the "basis" (3.i):

• (3.1) (basis) A variable x is a wff
• (3.2) If F and X are wffs, then {F}(X) is a wff; if x occurs in F or X then it is said to be a variable in {F}(X).
• (3.3) If M is well-formed and x occurs in M then λx is a wff.

(4) Define various abbreviations:

• {F} abbreviates to F(X) if F is a single symbol
• abbreviates to {F}(X,Y) or F(X,Y) if F is a single symbol
• λx₁λx₂...] abbreviates to λx₁x₂...x_n•M
• λab•a(b) abbreviates to 1
• λab•a(a(b)) abbreviates to 2, etc.

(5) Define the notion of "substitution" of formula N for variable x throughout M (Church 1936)