Editing Propositional calculus (section)

=== Syntax ===
Given a set of atomic propositional variables <math>p_1</math>, <math>p_2</math>, <math>p_3</math>, ..., and a set of propositional connectives <math>c_1^1</math>, <math>c_2^1</math>, <math>c_3^1</math>, ..., <math>c_1^2</math>, <math>c_2^2</math>, <math>c_3^2</math>, ..., <math>c_1^3</math>, <math>c_2^3</math>, <math>c_3^3</math>, ..., a formula of propositional logic is [[Recursive definition|defined recursively]] by these definitions:<ref name=":2" /><ref name=":0" /><ref name=":33"/>{{refn|group=lower-alpha|A very general and abstract syntax is given here, following the notation in the SEP,<ref name=":2" /> but including the third definition, which is very commonly given explicitly by other sources, such as Gillon,<ref name=":0" /> Bostock,<ref name="BostockIntermediate" /> Allen & Hand,<ref name=":35" /> and many others. As noted elsewhere in the article, languages variously compose their set of atomic propositional variables from uppercase or lowercase letters (often focusing on P/p, Q/q, and R/r), with or without subscript numerals; and in their set of connectives, they may include either the full set of five typical connectives, <math>\{ \neg, \land, \lor, \to, \leftrightarrow \}</math>, or any of the truth-functionally complete subsets of it. (And, of course, they may also use any of the notational variants of these connectives.)}}

:'''Definition 1''': Atomic propositional variables are formulas.

:'''Definition 2''': If <math>c_n^m</math> is a propositional connective, and <math>\langle</math>A, B, C, …<math>\rangle</math> is a sequence of m, possibly but not necessarily atomic, possibly but not necessarily distinct, formulas, then the result of applying <math>c_n^m</math> to <math>\langle</math>A, B, C, …<math>\rangle</math> is a formula.
:'''Definition 3:''' Nothing else is a formula.

Writing the result of applying <math>c_n^m</math> to <math>\langle</math>A, B, C, …<math>\rangle</math> in functional notation, as <math>c_n^m</math>(A, B, C, …), we have the following as examples of well-formed formulas:

* <math>p_5</math>
* <math>c_3^2(p_2, p_9)</math>
* <math>c_3^2(p_1, c_2^1(p_3))</math>
* <math>c_1^3(p_4, p_6, c_2^2(p_1, p_2))</math>
* <math>c_4^2(c_1^1(p_7), c_3^1(p_8))</math>
* <math>c_2^3(c_1^2(p_3, p_4), c_2^1(p_5), c_3^2(p_6, p_7))</math>
* <math>c_3^1(c_1^3(p_2, p_3, c_2^2(p_4, p_5)))</math>

What was given as ''Definition 2'' above, which is responsible for the composition of formulas, is referred to by [[Colin Howson]] as the ''principle of composition''.<ref name=":13" />{{refn|group=lower-alpha|Note that the phrase "principle of composition" has referred to other things in other contexts, and even in the context of logic, since [[Bertrand Russell]] used it to refer to the principle that "a proposition which implies each of two propositions implies them both."<ref name="ms17"/>}} It is this [[recursion]] [[recursive definition|in the definition]] of a language's syntax which justifies the use of the word "atomic" to refer to propositional variables, since all formulas in the language <math>\mathcal{L}</math> are built up from the atoms as ultimate building blocks.<ref name=":2" /> Composite formulas (all formulas besides atoms) are called ''molecules'',<ref name=":8" /> or ''molecular sentences''.<ref name=":21" /> (This is an imperfect analogy with [[chemistry]], since a chemical molecule may sometimes have only one atom, as in [[monatomic gas]]es.)<ref name=":8" />

The definition that "nothing else is a formula", given above as ''Definition 3'', excludes any formula from the language which is not specifically required by the other definitions in the syntax.<ref name="BostockIntermediate" /> In particular, it excludes ''infinitely long'' formulas from being [[Well-formed formula|well-formed]].<ref name="BostockIntermediate" /> It is sometimes called the ''Closure Clause''.<ref>{{Cite journal |last=Makridis |first=Odysseus |date=2022 |title=Symbolic Logic |url=https://link.springer.com/book/10.1007/978-3-030-67396-3 |journal=Palgrave Philosophy Today |language=en |pages=87 |doi=10.1007/978-3-030-67396-3 |isbn=978-3-030-67395-6 |issn=2947-9339}}</ref>

==== CF grammar in BNF ====
An alternative to the syntax definitions given above is to write a [[Context-free grammar|context-free (CF) grammar]] for the language <math>\mathcal{L}</math> in [[Backus–Naur form|Backus-Naur form]] (BNF).<ref name=":41"/><ref name=":42"/> This is more common in [[computer science]] than in [[philosophy]].<ref name=":42" /> It can be done in many ways,<ref name=":41" /> of which a particularly brief one, for the common set of five connectives, is this single clause:<ref name=":42" /><ref name=":02"/>
:<math>\phi ::= a_1, a_2, \ldots  ~ | ~  \neg\phi  ~ | ~  \phi ~ \& ~ \psi  ~ | ~  \phi \vee \psi  ~ | ~  \phi \rightarrow \psi  ~ | ~  \phi \leftrightarrow \psi</math>
This clause, due to its [[Self-reference|self-referential]] nature (since <math>\phi</math> is in some branches of the definition of <math>\phi</math>), also acts as a [[recursive definition]], and therefore specifies the entire language. To expand it to add [[modal operator]]s, one need only add … <math>| ~ \Box\phi ~ | ~ \Diamond\phi</math> to the end of the clause.<ref name=":42" />