Editing Propositional formula (section)

== Parsing formulas ==
The following "laws" of the propositional calculus are used to "reduce" complex formulas. The "laws" can be verified easily with truth tables. For each law, the principal (outermost) connective is associated with logical equivalence ≡ or identity =. A complete analysis of all 2<sup>n</sup> combinations of truth-values for its ''n'' distinct variables will result in a column of 1's (T's) underneath this connective. This finding makes each law, by definition, a tautology. And, for a given law, because its formula on the left and right are equivalent (or identical) they can be substituted for one another.
* Example: The following truth table is De Morgan's law for the behavior of NOT over OR: ~(a &or; b) ≡ (~a & ~b). To the left of the principal connective ≡ (yellow column labelled "taut") the formula ~(b &or; a) evaluates to (1, 0, 0, 0) under the label "P". On the right of "taut" the formula (~(b) &or; ~(a)) also evaluates to (1, 0, 0, 0) under the label "Q". As the two columns have equivalent evaluations, the logical equivalence ≡ under "taut" evaluates to (1, 1, 1, 1), i.e. P ≡ Q. Thus either formula can be substituted for the other if it appears in a larger formula.
{| style="margin-left: auto; margin-right: auto; border: none;"
|- style="font-size:9pt; text-align:center"
| width="18.75" Height="12" | 
| width="18.75" | 
| width="4.5" | 
| width="10.5" | 
|style="background-color:#D7E4BC" width="10.5" | P
| width="10.5" | 
| width="10.5" | 
| width="10.5" | 
| width="10.5" | 
| width="11.25" | 
|style="background-color:#FFFF99" width="21.75" | taut
| width="10.5" | 
| width="10.5" | 
| width="10.5" | 
| width="10.5" | 
| width="12" | 
|style="background-color:#DBE5F1" width="12.75" | Q
| width="10.5" | 
| width="10.5" | 
| width="10.5" | 
| width="10.5" | 
| width="10.5" | 
| width="10.5" | 
|- style="font-weight:bold" align="center"
|style="font-size:9pt" Height="15" | b
|style="font-size:9pt" | a
|style="background-color:#A5A5A5;font-size:9pt" | 
|style="font-size:9pt" | (
|style="background-color:#D7E4BC;font-size:9pt" | ~
|style="font-size:9pt" | (
|style="font-size:9pt" | b
|style="background-color:#FDE9D9;font-size:9pt" | V
|style="font-size:9pt" | a
|style="font-size:9pt" | )
|style="background-color:#FFFF99" | ≡
|style="font-size:9pt" | (
|style="background-color:#EAF1DD;font-size:9pt" | ~
|style="font-size:9pt" | (
|style="font-size:9pt" | b
|style="font-size:9pt" | )
|style="background-color:#DBE5F1;font-size:9pt" | &
|style="background-color:#EAF1DD;font-size:9pt" | ~
|style="font-size:9pt" | (
|style="font-size:9pt" | a
|style="font-size:9pt" | )
|style="font-size:9pt" | )
|style="font-size:9pt" | )
|- style="font-size:9pt" align="center"
| Height="12" | 0
| 0
|style="background-color:#A5A5A5" | 
| 
|style="background-color:#D7E4BC" | 1
| 
| 0
|style="background-color:#FDE9D9" | 0
| 0
| 
|style="background-color:#FFFF99" | 1
| 
|style="background-color:#EAF1DD" | 1
| 
| 0
| 
|style="background-color:#DBE5F1" | 1
|style="background-color:#EAF1DD" | 1
| 
| 0
| 
| 
| 
|- style="font-size:9pt" align="center"
| Height="12" | 0
| 1
|style="background-color:#A5A5A5" | 
| 
|style="background-color:#D7E4BC" | 0
| 
| 0
|style="background-color:#FDE9D9" | 1
| 1
| 
|style="background-color:#FFFF99" | 1
| 
|style="background-color:#EAF1DD" | 1
| 
| 0
| 
|style="background-color:#DBE5F1" | 0
|style="background-color:#EAF1DD" | 0
| 
| 1
| 
| 
| 
|- style="font-size:9pt" align="center"
| Height="12" | 1
| 0
|style="background-color:#A5A5A5" | 
| 
|style="background-color:#D7E4BC" | 0
| 
| 1
|style="background-color:#FDE9D9" | 1
| 0
| 
|style="background-color:#FFFF99" | 1
| 
|style="background-color:#EAF1DD" | 0
| 
| 1
| 
|style="background-color:#DBE5F1" | 0
|style="background-color:#EAF1DD" | 1
| 
| 0
| 
| 
| 
|- style="font-size:9pt" align="center"
| Height="12" | 1
| 1
|style="background-color:#A5A5A5" | 
| 
|style="background-color:#D7E4BC" | 0
| 
| 1
|style="background-color:#FDE9D9" | 1
| 1
| 
|style="background-color:#FFFF99" | 1
| 
|style="background-color:#EAF1DD" | 0
| 
| 1
| 
|style="background-color:#DBE5F1" | 0
|style="background-color:#EAF1DD" | 0
| 
| 1
| 
| 
| 
|}

Enterprising readers might challenge themselves to invent an "axiomatic system" that uses the symbols { &or;, &, ~, (, ), variables a, b, c }, the formation rules specified above, and as few as possible of the laws listed below, and then derive as theorems the others as well as the truth-table valuations for &or;, &, and ~. One set attributed to Huntington (1904) (Suppes:204) uses eight of the laws defined below.

If used in an axiomatic system, the symbols 1 and 0 (or T and F) are considered to be well-formed formulas and thus obey all the same rules as the variables. Thus the laws listed below are actually [[axiom schema]]s, that is, they stand in place of an infinite number of instances. Thus ( x &or; y ) ≡ ( y &or; x ) might be used in one instance, ( p &or; 0 ) ≡ ( 0 &or; p ) and in another instance ( 1 &or; q ) ≡ ( q &or; 1 ), etc.

=== 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)) ) )

=== Commutative and associative laws ===

Both AND and OR obey the [[commutative law]] and [[associative law]]:
* Commutative law for OR: ( a &or; b ) ≡ ( b &or; a )
* Commutative law for AND: ( a & b ) ≡ ( b & a )
* Associative law for OR: (( a &or; b ) &or; c ) ≡ ( a &or; (b &or; c) )
* Associative law for AND: (( a & b ) & c ) ≡ ( a & (b & c) )

'''Omitting parentheses in strings of AND and OR''': The connectives are considered to be unary (one-variable, e.g. NOT) and binary (i.e. two-variable AND, OR, IMPLIES). For example:
: ( (c & d) &or; (p & c) &or; (p & ~d) ) above should be written ( ((c & d) &or; (p & c)) &or; (p & ~(d) ) ) or possibly ( (c & d) &or; ( (p & c) &or; (p & ~(d)) ) )
However, a truth-table demonstration shows that the form without the extra parentheses is perfectly adequate.

'''Omitting parentheses with regards to a single-variable NOT''': While ~(a) where a is a single variable is perfectly clear, ~a is adequate and is the usual way this [[literal (mathematical logic)|literal]] would appear. When the NOT is over a formula with more than one symbol, then the parentheses are mandatory, e.g. ~(a &or; b).

=== Distributive laws ===
OR distributes over AND and AND distributes over OR. NOT does not distribute over AND or OR. See below about De Morgan's law:
* Distributive law for OR: ( c &or; ( a & b) ) ≡ ( (c &or; a) & (c &or; b) )
* Distributive law for AND: ( c & ( a &or; b) ) ≡ ( (c & a) &or; (c & b) )

=== De Morgan's laws ===
NOT, when distributed over OR or AND, does something peculiar (again, these can be verified with a truth-table):
* De Morgan's law for OR: ¬(a &or; b) ≡ (¬a ^ ¬b)
* De Morgan's law for AND: ¬(a ^ b) ≡ (¬a &or; ¬b)

=== Laws of absorption ===
Absorption, in particular the first one, causes the "laws" of logic to differ from the "laws" of arithmetic:
* Absorption (idempotency) for OR: (a &or; a) ≡ a
* Absorption (idempotency) for AND: (a & a) ≡ a

=== Laws of evaluation: Identity, nullity, and complement ===
The sign " = " (as distinguished from logical equivalence ≡, alternately ↔ or ⇔) symbolizes the assignment of value or meaning. Thus the string (a & ~(a)) symbolizes "0", i.e. it means the same thing as symbol "0" ". In some "systems" this will be an axiom (definition) perhaps shown as ( (a & ~(a)) =<sub>Df</sub> 0 ); in other systems, it may be derived in the truth table below:
{| style="margin-left: auto; margin-right: auto; border: none;"
|- style="font-size:9pt; text-align:center"
| width="18.75" Height="12" | 
| width="4.5" | 
| width="9" | 
| width="9" | 
| width="10.5" | 
|style="background-color:#C5D9F1" width="10.5" | c
| width="9.75" | 
| width="9.75" | 
| width="15.75" | 
| width="8.25" | 
| width="8.25" | 
|style="background-color:#FFFF99" width="18" | taut
| width="13.5" | c
| width="11.25" | 
|- style="font-weight:bold" align="center"
|style="font-size:9pt" Height="15" | a
|style="font-size:9pt" | 
|style="font-size:9pt" | (
|style="font-size:9pt" | (
|style="font-size:9pt" | a
|style="background-color:#C5D9F1;font-size:9pt" | &
|style="background-color:#EAF1DD;font-size:9pt" | ~
|style="font-size:9pt" | (
|style="font-size:9pt" | a
|style="font-size:9pt" | )
|style="font-size:9pt" | )
|style="background-color:#FFFF99" | ≡
|style="font-size:9pt" | 0
|style="font-size:9pt" | )
|- style="font-size:9pt" align="center"
| Height="12" | 0
| 
| 
| 
| 0
|style="background-color:#C5D9F1" | 0
|style="background-color:#EAF1DD" | 1
| 
| 0
| 
| 
|style="background-color:#FFFF99" | 1
| 0
| 
|- style="font-size:9pt" align="center"
| Height="12" | 1
| 
| 
| 
| 1
|style="background-color:#C5D9F1" | 0
|style="background-color:#EAF1DD" | 0
| 
| 1
| 
| 
|style="background-color:#FFFF99" | 1
| 0
| 
|}

* Commutation of equality: (a = b) ≡ (b = a)
* Identity for OR: (a &or; 0) = a or (a &or; F) = a
* Identity for AND: (a & 1) = a or (a & T) = a
* Nullity for OR: (a &or; 1) = 1  or (a &or; T) = T
* Nullity for AND: (a & 0) = 0  or (a & F) = F
* Complement for OR: (a &or; ~a) = 1 or (a &or; ~a) = T, [[law of excluded middle]]
* Complement for AND: (a & ~a) = 0 or (a & ~a) = F, [[law of contradiction]]

=== Double negative (involution) ===
* ¬(¬a) ≡ a