ABSTRACT
A formal system consists of a set of symbols called an alphabet and a set of rules describing the way in which these symbols may be joined together to form strings of symbols. Our initial formal system is built from the following alphabet: https://www.w3.org/1998/Math/MathML"> p , q , r , s , … , ⊥ ¬ ∧ , ∨ , → , ↔ ( , ) , , , https://s3-euw1-ap-pe-df-pch-content-public-p.s3.eu-west-1.amazonaws.com/9780203211991/94c3b92a-0a16-4a4e-9014-02b93290d004/content/math_4_B.tif" xmlns:xlink="https://www.w3.org/1999/xlink"/> Symbols p, q, r, s, … represent an infinite number of atomic statements in the alphabet and may be seen as the building blocks of propositions. Three rows of symbols then show logical connectives that bind these atomic elements together according to the following rules:
Symbols ⊥, p, q, r, s, … are themselves propositions.
If A is a proposition then ¬A is also a proposition.
If A and B are both propositions then A ∧ B, A ∨ B, A → B, and A ↔ B are also propositions.
Strings of symbols not built up according to these rules are not propositions.
Unlike the atomic statement symbols p, q, r, …, symbols A and B represent any proposition and are not themselves part of the formal system being described. Symbols of this kind are often called metasymbols. The rules above define the number of arguments that each logical connective requires to produce a correctly formed proposition, producing a form of valency called the arity. Statement symbols p, q, r, … and the connective ⊥ are themselves propositions and thus have an arity of zero. A zero-arity connective might at this point seem a little fraudulent, but later we shall see that it does have properties in common with the other connectives. Only one connective symbol is defined with an arity of one, limiting the form of propositions that might be constructed from this symbol and atomic statement symbols. Increasingly large propositions may be constructed by the repeated attachment of this connective to a simple atomic statement as follows: https://www.w3.org/1998/Math/MathML"> ¬ ( ¬ p ) ¬ ( ¬ ( ¬ p ) ) ¬ ( ¬ ( ¬ ( ¬ p ) ) ) https://s3-euw1-ap-pe-df-pch-content-public-p.s3.eu-west-1.amazonaws.com/9780203211991/94c3b92a-0a16-4a4e-9014-02b93290d004/content/math_5_B.tif" xmlns:xlink="https://www.w3.org/1999/xlink"/> or to the special connective ⊥, e.g. ¬⊥, ¬(¬(⊥)). All remaining connectives are defined to be of arity two, giving propositions of the form https://www.w3.org/1998/Math/MathML"> p ∧ q r ∨ ( ¬ p ) ¬ ( ¬ ( ¬ p ) ) → ¬ q ⊥ ↔ ( ¬ p ) https://s3-euw1-ap-pe-df-pch-content-public-p.s3.eu-west-1.amazonaws.com/9780203211991/94c3b92a-0a16-4a4e-9014-02b93290d004/content/math_6_B.tif" xmlns:xlink="https://www.w3.org/1999/xlink"/> with simple or negated atomic statements. Such connectives may take arguments that are themselves formed from arity-two connectives, creating propositions such as https://www.w3.org/1998/Math/MathML"> ( ¬ ( ¬ p ) ) → ( r ∨ ( ¬ p ) ) ( ¬ p ) ∧ ( r ∨ ( ¬ p ) ) https://s3-euw1-ap-pe-df-pch-content-public-p.s3.eu-west-1.amazonaws.com/9780203211991/94c3b92a-0a16-4a4e-9014-02b93290d004/content/math_7_B.tif" xmlns:xlink="https://www.w3.org/1999/xlink"/> Parentheses are defined as part of the formal system to record the order in which a proposition is constructed from its atomic symbols. A proposition might be built from atomic statements p and q as follows: https://www.w3.org/1998/Math/MathML"> p ¬ q ¬ p q ( p ∧ ( ¬ q ) ) ( ( ¬ p ) ∧ q ) ( p ∧ ( ¬ q ) ) ∨ ( ( ¬ p ) ∧ q ) https://s3-euw1-ap-pe-df-pch-content-public-p.s3.eu-west-1.amazonaws.com/9780203211991/94c3b92a-0a16-4a4e-9014-02b93290d004/content/math_8_B.tif" xmlns:xlink="https://www.w3.org/1999/xlink"/> but if the same starting propositions are combined in a different order, a different proposition is obtained: https://www.w3.org/1998/Math/MathML"> p ¬ q ¬ p q p ( ( ¬ q ) ∨ ( ¬ p ) ) q p ∧ ( ( ¬ q ) ∨ ( ¬ p ) ) ∧ q https://s3-euw1-ap-pe-df-pch-content-public-p.s3.eu-west-1.amazonaws.com/9780203211991/94c3b92a-0a16-4a4e-9014-02b93290d004/content/math_9_B.tif" xmlns:xlink="https://www.w3.org/1999/xlink"/> In order to reduce the number of brackets used in formulas a precedence order for arity one and two connectives is defined as follows: https://www.w3.org/1998/Math/MathML"> low precedence ↔ → ∨ ∧ ¬ high precedence https://s3-euw1-ap-pe-df-pch-content-public-p.s3.eu-west-1.amazonaws.com/9780203211991/94c3b92a-0a16-4a4e-9014-02b93290d004/content/math_10_B.tif" xmlns:xlink="https://www.w3.org/1999/xlink"/> Connectives with the highest precedence bind most tightly to the objects that they connect. Thus ¬p ∧ q is understood to mean (¬p) ∧ q because a ¬ symbol has greater precedence than a ∧ symbol. Explicit bracketing would have to be included if the alternative proposition, ¬(p ∧ q), were intended. Similarly, proposition p ∧¬q ∨ ¬p ∧ q represents the first of the two examples constructed above and brackets would have to be retained to represent the second possibility. Symbol ∧ has a higher precedence than →, so the formula p ∧ q → r is assumed to represent (p ∧ q) → r, a formula in which connective ∧ is first applied to statements p and q then this proposition itself becomes an argument. The alternative proposition, p ∧(q → r) requires brackets to overide the precedence rule.