Start with the propositional variables as atomic symbols and close under the two formation operations
The set of propositional formulas is the smallest set satisfying these conditions: every logical formula has a finite construction from logical variables by negation and logical implication, and no other strings qualify. In particular, parentheses belong to the binary logical implication formation rule; they cannot be added or removed arbitrarily. Each symbol is one token, regardless of how its index is printed.
Use structural induction on the formation of a propositional formula. A propositional variable has no parentheses. Applying negation to a logical formula adds no parentheses, so preserves equality of the two counts. If and each have equally many opening and closing parentheses, the formation of adds one of each to their combined counts. Thus every propositional formula satisfies
This is a necessary condition for being a logical formula; it is not sufficient, since the logical connectives and the placement of symbols must also follow the formation rules.
Not a logical formula. The string has one opening parenthesis and no closing parenthesis, contradicting the parentheses count established above. It also fails the binary logical implication formation rule, whose final symbol must be a closing parenthesis.
Not a logical formula of this language. Logical disjunction is not one of its permitted logical connectives. Even though the displayed expression has an ordinary interpretation in a larger propositional language, membership in the specified formal language is a syntactic question. A logically equivalent logical formula using only negation and logical implication would have to be written with those symbols instead.
A logical formula. Both and are propositional variables, so and are logical formulas. Applying the binary logical implication formation rule to this ordered pair of logical formulas gives the displayed whole expression. This supplies a construction of its formula syntax tree rather than merely checking that its parentheses balance.
The unique readability theorem says that every propositional formula has exactly one of the following forms: a unique propositional variable; for a unique logical formula ; or for a unique ordered pair of logical formulas . These three alternatives are disjoint. Consequently each logical formula has a unique formula syntax tree and a uniquely determined principal logical connective whenever it is not a logical variable.
A propositional variable is a single symbol of the alphabet. Its only nonempty substring is that symbol itself. Every propositional formula is nonempty, so the only substring that is a logical formula is . Therefore
The subscript is part of the name of an atomic token; it does not introduce additional symbol positions inside the logical variable.
A useful consequence of the formation rules is that logical formulas form a prefix-free set of strings. To see this, describe a deterministic parser that reads one logical formula from its starting position. On a logical variable it consumes that one symbol. On a negation symbol it recursively reads one following logical formula. On an opening parenthesis it recursively reads a left logical formula, requires a logical implication symbol, recursively reads a right logical formula, and requires the closing parenthesis. Induction on formation proves that, if a valid logical formula begins at the current position, this procedure consumes exactly that logical formula and stops at its end.
Suppose now that both and are logical formulas and . The same parser, started at their common first symbol, must stop both at the end of and at the end of . Its deterministic stopping position cannot differ, so is empty. Hence
This argument applies to symbol strings; it does not use truth values or logical equivalence.
First note that a substring which is itself a logical formula must coincide with a subtree of the formula syntax tree of the surrounding logical formula. Indeed, a logical formula can begin only at a logical variable, a negation symbol or an opening parenthesis. Every such position in a valid logical formula is the start of one of its parsed subtrees. If is the logical formula at that subtree and is another logical formula starting at the same position, one is an initial segment of the other; prefix-freeness of fully parenthesized formulas from the preceding part forces .
Now consider a final subformula. For a logical variable, it can only be the whole logical formula. For a binary logical implication , every proper subtree is contained in or and finishes before the final closing parenthesis of the whole expression. It therefore cannot be a final substring of the whole. The only remaining possible outer formation is negation. Thus
The second alternative is a necessary possibility, not a claim that every negated logical formula has every one of its subformulas as a suffix.
The whole logical formula is a subformula of itself, and any subformula of remains a contiguous substring after placing a negation symbol in front of .
Conversely, a subformula occurrence starting at the first symbol of is an initial subformula, so equals the whole logical formula by prefix-freeness of fully parenthesized formulas. An occurrence starting later lies wholly inside the following string , and is therefore a subformula of . Consequently
Here records distinct logical formulas; multiple occurrences of the same logical formula do not create different elements of this set.
A subformula beginning at the first opening parenthesis equals the whole logical formula by prefix-freeness of fully parenthesized formulas. Every other subformula is the logical formula of a proper syntax subtree, by the parsing argument in part (iii). The two children of the root are precisely and , so such a subtree lies entirely inside one of those children. In particular no logical formula substring can begin in and cross the principal logical implication symbol into .
Conversely, each subformula of either child is visibly a substring of the whole expression, as is the whole expression itself. Thus
Together these cases identify the substring definition of a subformula with its usual syntax-tree definition.
Fix the particular occurrence of that is being replaced. The subformula analysis above makes it a node of the formula syntax tree of . Proceed by structural induction on the surrounding logical formula.
If this node is the root, the subformula replacement gives , already a logical formula. Otherwise, if , the chosen occurrence lies inside . The induction hypothesis gives a logical formula after the subformula replacement there, and the whole result is the logical formula . If , a proper chosen occurrence lies in exactly one of the two children. Replacing inside that child gives either or , each a logical formula by the formation rule. A logical variable has no proper subformula, so there is no additional base case.
Therefore replacing the designated subformula occurrence by any logical formula preserves well-formedness. The argument concerns one chosen occurrence; it does not require simultaneous subformula replacement of every occurrence of the same string.
Fix any Boolean valuation . Logical equivalence of and means for this Boolean valuation and every other one. Follow the unique path from the replaced node to the root of the formula syntax tree. At a negation node, equal input truth values have equal negations. At a logical implication node, the unaffected child has the same truth value before and after subformula replacement, while the affected child has the same truth value by induction; the resulting logical implications therefore agree as well.
Induction along that finite path yields . Since was arbitrary,
This is the replacement theorem for logical equivalence: the semantics of each logical connective depends only on the truth values of its immediate inputs.

Articles by others on the same topic (0)

There are currently no matching articles.