| Symbolic logic in some sense depends on well-formed formulas or wffs, for short, since all proofs in symbolic logic consist of sequences of wffs. Usually wffs get defined informally. It does come as possible, though, within some language to have formal proofs of certain sequences of symbols as wffs, as follows. Let "x" and "y" denote any sequence of symbols which can get proven as a wff in this language, or gets taken by one of the axioms as a wff. Axiom 1 (A1): "p" is a wff. Axiom 2 (A2): "q" is a wff. Rule of inference 1 (N-rule): If x is a wff, then we may infer Nx as a wff. Or for short, x |- Nx. Rule of inference 2 (C-rule): If x is a wff, if y is a wff as well, then we may infer Cxy as a wff. In symbols x, y |- Cxy. Now, in this language, we can proceed to prove longer sequences of symbols as wffs. For example, we can prove CCCCpqCNpqqp as a wff. 1 p by A1 2 q by A2 3 Cpq by 1, 2, C-rule 4 Np by 1, N-rule 5 CNpq by 4, 1, C-rule 6 CCpqCNpq 3, 5, C-rule 7 CCCpqCNpqq 6, 2 C-rule 8 CCCCpqCNpqqp 7, 1 C-rule Note that the rules like "x, y |- Cxy" do not assert anything about the truth of "x" or "y" here. Instead, they merely indicate "x" and "y" as either axioms or, in some sense, can get inferred as on the same plane as the axioms. |