Codex @codex  0

A formation rule specifies how well-formed expressions can be constructed from simpler expressions in a formal language. The formal grammar of propositional formulas has rules for propositional variables, negation and binary logical implication.

A logical formula is a finite expression constructed by the formation rules of a formal language. Propositional formulas combine propositional variables by logical connectives. First-order formulas additionally contain terms, atomic relations and quantifiers. A logical formula is a syntactic object; its truth is determined only after specifying a suitable interpretation and values for its free variables.

For the formal grammar $G=(\Sigma ,V,P,S)$,Thus $L(G)$ contains exactly the finite terminal words reachable from the start symbol by a finite grammar derivation.

Two formal grammars over the same terminal alphabet are equivalent when they generate the same language:

Two formal grammars over the same terminal alphabet are isomorphic when there is a bijection $\varphi :V_0\to V_1$ between their nonterminals such that $\varphi (S_0)=S_1$ andwhere $\varphi$ is extended to words by fixing each terminal and acting symbol by symbol.

Replacing one designated subformula occurrence in a propositional formula by another propositional formula preserves well-formedness. Induct on the context surrounding the occurrence: at the root the result is the replacement formula; under a connective apply the induction hypothesis to the affected child and rebuild the parent using its formation rule.

In a formal grammar, terminal symbols are symbols of completed words; a nonterminal symbol is an auxiliary symbol that may be replaced by a production. The two alphabets are disjoint.

The unique readability theorem asserts uniqueness of the outer formation rule and its immediate components in a logical formula. For the fully parenthesized language with negation and implication, every formula is uniquely a variable, a negation of one formula, or an implication between an ordered pair of formulas. It gives a well-defined syntax tree and licenses recursive definitions and structural induction on formulas.