Editing Propositional formula (section)

=== IDENTITY and evaluation ===

The first table of this section stars *** the entry logical equivalence to note the fact that "[[Logical equivalence]]" is not the same thing as "identity". For example, most would agree that the assertion "That cow is blue" is identical to the assertion "That cow is blue". On the other hand, ''logical'' equivalence sometimes appears in speech as in this example: " 'The sun is shining' means 'I'm biking' " Translated into a propositional formula the words become: "IF 'the sun is shining' THEN 'I'm biking', AND IF 'I'm biking' THEN 'the sun is shining'":<ref>The use of quote marks around the expressions is not accidental. Tarski comments on the use of quotes in his "18. Identity of things and identity of their designations; use of quotation marks" p. 58ff.</ref>
: "IF 's' THEN 'b' AND IF 'b' THEN 's' " is written as ((s → b) & (b → s)) or in an abbreviated form as (s ↔ b). As the rightmost symbol string is a '''definition''' for a new symbol in terms of the symbols on the left, the use of the IDENTITY sign = is appropriate:
:: ((s → b) & (b → s)) = (s ↔ b)

Different authors use different signs for logical equivalence: ↔ (e.g. Suppes, Goodstein, Hamilton), ≡ (e.g. Robbin), ⇔ (e.g. Bender and Williamson). Typically identity is written as the equals sign =. One exception to this rule is found in ''Principia Mathematica''. For more about the philosophy of the notion of IDENTITY see [[Identity of indiscernibles|Leibniz's law]].

As noted above, Tarski considers IDENTITY to lie outside the propositional calculus, but he asserts that without the notion, "logic" is insufficient for mathematics and the deductive sciences. In fact the sign comes into the propositional calculus when a formula is to be evaluated.<ref>Hamilton p. 37. Bender and Williamson p. 29 state "In what follows, we'll replace "equals" with the symbol " ⇔ " (equivalence) which is usually used in logic. We use the more familiar " = " for assigning meaning and values."</ref>

In some systems there are no truth tables, but rather just formal axioms (e.g. strings of symbols from a set { ~, →, (, ), variables p<sub>1</sub>, p<sub>2</sub>, p<sub>3</sub>, ... } and formula-formation rules (rules about how to make more symbol strings from previous strings by use of e.g. substitution and [[modus ponens]]). the result of such a calculus will be another formula (i.e. a well-formed symbol string). Eventually, however, if one wants to use the calculus to study notions of validity and truth, one must add axioms that define the behavior of the symbols called "the truth values" {T, F} ( or {1, 0}, etc.) relative to the other symbols.

For example, Hamilton uses two symbols = and ≠ when he defines the notion of a '''valuation v''' of any [[well-formed formula]]s (wffs) ''A'' and ''B'' in his "formal statement calculus" L. A valuation '''v''' is a ''[[Function (mathematics)|function]]'' from the wffs of his system L to the range (output) { T, F }, given that each variable  p<sub>1</sub>, p<sub>2</sub>, p<sub>3</sub> in a wff is assigned an arbitrary truth value { T, F }.
{{NumBlk|*|  '''v'''(''A'') ≠ '''v'''(~''A'')|{{EquationRef|i}}}}
{{NumBlk|*|  '''v'''(''A'' → ''B'') {{=}} F if and only if '''v'''(''A'') {{=}} T and '''v'''(''B'') {{=}} F|{{EquationRef|ii}}}}

The two definitions ({{EquationNote|i}}) and ({{EquationNote|ii}}) define the equivalent of the truth tables for the ~ (NOT) and → (IMPLICATION) connectives of his system. The first one derives F ≠ T and T ≠ F, in other words " '''v'''(''A'') does not '''mean''' '''v'''(~''A'')". Definition ({{EquationNote|ii}}) specifies the third row in the truth table, and the other three rows then come from an application of definition ({{EquationNote|i}}). In particular ({{EquationNote|ii}}) '''assigns''' the value F (or a meaning of "F") to the entire expression. The definitions also serve as formation rules that allow substitution of a value previously derived into a formula:
{|
|- style="font-size:9pt" align="center"
| width="8.25" Height="12" | 
| width="25.5" | 
|style="background-color:#E5E0EC" width="50" | v(A→B)
| width="29.25" | 
| width="6.75" | 
|- style="font-size:9pt" align="center"
| Height="12" | (
| v(A)
|style="background-color:#E5E0EC" |  →
| v(B)
| )
|- style="font-size:9pt" align="center"
| Height="12" | 
| F
|style="background-color:#E5E0EC" | T
| F
| 
|- style="font-size:9pt" align="center"
| Height="12" | 
| F
|style="background-color:#E5E0EC" | T
| T
| 
|- style="font-size:9pt" align="center"
| Height="12" | 
| T
|style="background-color:#CCC0DA" | F
| F
| 
|- style="font-size:9pt" align="center"
| Height="12" | 
| T
|style="background-color:#E5E0EC" | T
| T
| 
|}

Some [[formal system]]s specify these valuation axioms at the outset in the form of certain formulas such as the [[law of contradiction]] or laws of identity and nullity. The choice of which ones to use, together with laws such as commutation and distribution, is up to the system's designer as long as the set of axioms is '''complete''' (i.e. sufficient to form and to evaluate any well-formed formula created in the system).