Editing Well-formed formula (section)

==Propositional calculus==
{{Main|Propositional calculus}}
The formulas of [[propositional calculus]], also called [[propositional formula]]s,<ref>First-order logic and automated theorem proving, Melvin Fitting, Springer, 1996 [https://books.google.com/books?id=T8OMqvXvWWQC&dq=%22propositional+formula%22&pg=PA11]</ref> are expressions such as <math>(A \land (B \lor C))</math>. Their definition begins with the arbitrary choice of a set ''V'' of  [[propositional variable]]s. The alphabet consists of the letters in ''V'' along with the symbols for the [[logical connective|propositional connective]]s and parentheses "(" and ")", all of which are assumed to not be in ''V''.  The formulas will be certain expressions (that is, strings of symbols) over this alphabet.

The formulas are [[inductive definition|inductively]] defined as follows:
* Each propositional variable is, on its own, a formula.
* If φ is a formula, then &not;φ is a formula.
* If φ and ψ are formulas, and • is any binary connective, then ( φ • ψ) is a formula. Here • could be (but is not limited to) the usual operators ∨, ∧, →, or ↔.

This definition can also be written as a [[formal grammar]] in [[Backus–Naur form]], provided the set of variables is finite:
{{#tag:syntaxhighlight|<alpha set> ::= p {{!}} q {{!}} r {{!}} s {{!}} t {{!}} u {{!}} ... (the arbitrary finite set of propositional variables)
<form> ::= <alpha set> {{!}} ¬<form> {{!}} (<form>∧<form>) {{!}} (<form>∨<form>) {{!}} (<form>→<form>) {{!}} (<form>↔<form>)|lang="bnf"}}
Using this grammar, the sequence of symbols
:(((''p'' &rarr; ''q'') &and; (''r'' &rarr; ''s'')) &or; (&not;''q'' &and; &not;''s''))
is a formula, because it is grammatically correct. The sequence of symbols
:((''p'' &rarr; ''q'')&rarr;(''qq''))''p''))
is not a formula, because it does not conform to the grammar.

A complex formula may be difficult to read, owing to, for example, the proliferation of parentheses. To alleviate this last phenomenon, precedence rules (akin to the [[standard mathematical order of operations]]) are assumed among the operators, making some operators more binding than others. For example, assuming the precedence (from most binding to least binding) 1. &not; &nbsp; 2. &rarr;&nbsp; 3. &and;&nbsp; 4. &or;. Then the formula
:(((''p'' &rarr; ''q'') &and; (''r'' &rarr; ''s'')) &or; (&not;''q'' &and; &not;''s''))
may be abbreviated as
:''p'' &rarr; ''q'' &and; ''r'' &rarr; ''s'' &or; &not;''q'' &and; &not;''s''
This is, however, only a convention used to simplify the written representation of a formula. If the precedence was assumed, for example, to be left-right associative, in following order: 1. &not; &nbsp; 2. &and;&nbsp; 3. &or;&nbsp; 4. &rarr;, then the same formula above (without parentheses) would be rewritten as
:(''p'' &rarr; (''q'' &and; ''r'')) &rarr; (''s'' &or; (&not;''q'' &and; &not;''s''))