Editing Propositional formula (section)

=== Connective seniority (symbol rank) ===
In general, to avoid confusion during analysis and evaluation of propositional formulas, one can make liberal use of parentheses. However, quite often authors leave them out. To parse a complicated formula one first needs to know the seniority, or rank, that each of the connectives (excepting *) has over the other connectives. To "well-form" a formula, start with the connective with the highest rank and add parentheses around its components, then move down in rank (paying close attention to the connective's scope over which it is working). From most- to least-senior, with the predicate signs ∀x and ∃x, the IDENTITY = and arithmetic signs added for completeness:{{efn|Rosenbloom{{sfn|Rosenbloom|1950|p=32}} and Kleene 1952:73-74 ranks all 11 symbols.}}
:; ≡: (LOGICAL EQUIVALENCE)
:; →: (IMPLICATION)
:; &: (AND)
:; &or;: (OR)
:; ~: (NOT)
:; ∀x: (FOR ALL x)
:; ∃x: (THERE EXISTS AN x)
:; =: (IDENTITY)
:; +: (arithmetic sum)
:;<nowiki>*</nowiki>: (arithmetic multiply)
:; ' : (s, arithmetic successor).

Thus the formula can be parsed—but because NOT does not obey the distributive law, the parentheses around the inner formula (~c & ~d) is mandatory:
: Example: " d & c &or; w " rewritten is ( (d & c) &or; w )
: Example: " a & a → b ≡ a & ~a &or; b " rewritten (rigorously) is
::* ≡ has seniority: ( ( a & a → b ) ≡ ( a & ~a &or; b ) )
::* → has seniority: ( ( a & (a → b) ) ≡ ( a & ~a &or; b ) )
::* & has seniority both sides: ( ( ( (a) & (a → b) ) ) ≡ ( ( (a) & (~a &or; b) ) )
::* ~ has seniority: ( ( ( (a) & (a → b) ) ) ≡ ( ( (a) & (~(a) &or; b) ) )
::* check 9 ( -parenthesis and 9 ) -parenthesis: ( ( ( (a) & (a → b) ) ) ≡ ( ( (a) & (~(a) &or; b) ) )
: Example:
:: d & c &or; p & ~(c & ~d) ≡ c & d &or; p & c &or; p & ~d rewritten is ( ( (d & c) &or; ( p & ~((c & ~(d)) ) ) ) ≡ ( (c & d) &or; (p & c) &or; (p & ~(d)) ) )