Formation sequences for propositional formulas.
Martin M. Zuckerman · Notre Dame Journal of Formal Logic · 1973
Formation sequences play a central role in Smullyan's elegant development of the propositional calculus, given in [1] and [2].In the following, we modify the treatment of [1] in that we take only ~ and v as our undefined logical connectives; the definitions given in [1] are altered accordingly.*Let ^0 be a denumerable collection of symbols, called propositional variables.Let the four symbols ~,v,(,) be distinct from each other and from the propositional variables.A formation sequence is defined, recursively, to be a finite sequence each of whose terms is either (i) a propositional variable, (ii) of the form ~P, where P is an earlier term of the sequence, or (iii) of the form (PvQ), where P and Q are earlier terms of the sequence.P is called a formula if there is a formation sequence, (P o , P l5 . . ., P N ) in which P N = P; (P o , p u . . ., P N ) is then called a formation sequence for P. It follows directly from this definition that if (P o , P u . . ., P N ) is a formation sequence, then for each K ^ N, (P o , Pi, . . ., P κ ) is a formation sequence for P κ .As the name suggests, formation sequences yield information concerning the manner in which formulas are constructed from propositional variables by means of connectives.Clearly, a formation sequence for a formula, P, is not unique.Formulas of type (ii) are called negations; those of type (iii) are called disjunctions.It is well-known that for every formula P, exactly one of the following holds: