The Laws of Thought in Formal Calculi
In philosophical discussions with laypersons I often encounter references to three so-called "laws of logic." Although they may take any of a wide range of different expressions which convey an arguably greater diversity of meaning, I shall adopt for the purposes of this document a simple and specific set of formulations, given thusly:
I wish briefly observe the role and expression of these laws in certain formal logical systems, namely that of the statement and first-order predicate calculi. As we shall shortly see, the laws of noncontradiction and of excluded middle appear as theorem schemas but not axiom schemas of the statement calculus, given an appropriate overlaying theory and interpretation thereof. The law of identity, in contrast, is not a theorem schema of the statement calculus, nor any pure predicate calculus. However, it is an axiom schema of equality, the results of which are commonly absorbed into first-order formal theories.
Before we begin our outline, I should say a few words regarding our motivation: For mathematicians and logicians usually perceive nothing special about these laws, and in the context of formal logic we have little reason to pay them any great attention relative to other theorem and axiom schemas. However, they are well-known in certain circles as Aristotelian "laws of thought"[1] which, according to certain philosophy enthusiasts I've encountered, lie at the root foundation of our ability to think and reason. This view has become especially popular among what are called "presuppositionalist" Christian apologists, who argue that the God Yahweh is the only possible explanation for the existence, as they describe it, of these laws. Needless to say, such arguments have failed to convince most academic philosophers, and this author, although not a philosopher himself, follows in their skepticism. Let us now explicitly clarify that our discussion shall not further involve those arguments. Neither will our outline deal with the possible role which some versions of the Aristotelian laws may play in understanding our ability to reason. Instead, we will restrict our attention to the appearance, or lack thereof, of the laws strictly within the context of axiom and theorem schemas of formal statement and first-order predicate calculi, with the hope that it will spark the interest of those who are involved in some manner or another with apologetics.
We do not intend it to be necessary to have any knowledge of formal logic in order to appreciate our forthcoming observations. Instead, we will introduce the reader presently to formal systems by providing an example of a very basic formal logical calculus. To that end, the following is Jan Łukasiewicz's refinement of Gottlob Frege's statement calculus, as reorganized by Robert Stoll:[2]
As we can plainly see, none of the three laws of thought make an appearance in the axiom schemas of the statement calculus, nor in its essential definitions, that is, the definitions of formula, proof and theorem. The same goes for at least one if not all first-order predicate calculi, namely that of Alonzo Church, as presented by Robert Stoll (which we shall not reproduce here).[3] However, something like the law of noncontradiction we incorporate into the definition of consistency of formula sets:
Although not quite the same as the law of noncontradiction, we can see the parallel. Every consistent set of assumptions, for example the axioms of a first-order theory, over the framework of the given statement calculus (and indeed Church's predicate calculus), upholds the principle that for no formula A do we have both A and ¬A as theorems. Nevertheless, the definition of consistency is an identifier, not a rule, and as such does not behave as a "law" in the sense we have in mind.
Therefore we may consider presently how to state the law of noncontradiction as such a theorem schema. Now, the concepts of true and false do not automatically accompany the statement calculus. However, the concept of a theorem schema is usually intended as the formal analog of a tautology, that is, a statement form which is always true, regardless of its interpretation. Meanwhile, the logical connectives ∧ and ∨ are usually associated with the concepts of and and or, respectively, whereas ¬ we read as not, or, more explicitly, it is not the case that. Furthermore, the concept of a law we take as analogous to a theorem or axiom schema in formal calculi, that is, a theorem or axiom for which we may substitute any individual or predicate constant for all instances of any free or predicate variable, respectively. To this end, we offer the following formulations of the laws of noncontradiction and of excluded middle as possible theorem schemas of the statement calculus:
By definition of the ∧ and ∨ symbols, we write these theorems using formal notation as A → A and ¬A → ¬A, respectively. Each are theorems, regardless of our choice of A. The proof of the former is quite straightforward:
We obtain the result ¬A → ¬A by substituting all occurrences of A with ¬A in the preceding proof.
On the other hand, the law of identity makes no obvious appearance among the axiom schemas of the statement calculus which we have stipulated, and indeed the same goes for Church's predicate calculus. This may seem surprising to those with only knowledge of semiformal mathematics, since the = symbol is employed in just about every informal system of note. However, in a formal system, the = operator must be explicitly defined into existence, which is not the case in either Łukasiewicz's or Church's calculi. We describe such predicate calculi as without equality, to distinguish them from those calculi for which we wish to explicitly define = as a logical symbol.
We shall presently begin a discussion of predicate calculi with equality. However, in order to do so, some general understanding of predicate calculus notation is required. Readers lacking a familiarity with this notation may refer to wikipedia's page describing the formulation rules of first-order logic.
With predicate calculus notation in mind, we describe the constant = as a special kind of two-place predicate symbol, such that we may construct the formula (x=y) for any individuals x,y. As a predicate, then, it is absent from the statement calculus regardless of its specific formulation. In order to incorporate it into a predicate logic, we append to the initial set of predicate logic axiom schemas the following two additional schemas:
Axiom schemas (E1) and (E2) are absent from what we call a "pure" predicate calculus, which, among other characteristics, excludes by definition all constants. Since = is a logical constant, then it cannot appear in a pure predicate calculus. Informally, we may expound axiom schema (E2) as follows: If A is a 1-place predicate, then (x=y) → (A(x) → A(y)), if A is a 2-place predicate, then (x=y) → (A(x,z) → A(y,z)) and (x=y) → (A(z,x) → A(z,y)), and so on for all n-place predicates A. Similar implications hold for formulas which are not precisely of the n-place form, but rather incorporate a subformula, so to speak, which is an n-place predicate. Needless to say, this informal description is inadequate for a precise understanding of (E2), but we offer it for the benefit of those lacking familiarity with formal predicate calculus.
Plainly, the statement schema x=x has a striking interpretive similarity to the law of identity as we stated it in English: every entity is the same as itself we may read as every entity x is the same as x, or, in the context of predicate calculus, for every individual x we have x=x. It seems clear, then, that (E1) best represents the law of identity in predicate calculus with equality. Axiom schema (E2), meanwhile, describes the intuitive consequences of the law of identity.
Now that we have identified the laws of thought in the axiom and theorem schemas of predicate calculus with equality, we may turn to address their spirit. In our formal system of predicate calculus these schemas establish the mechanical rules for the organization of symbols. For example, axiom schemas (E1) and (E2) govern the behavior of the = symbol. This is all any such axiom or theorem schema could ever do in systems such as the statement and predicate calculi, which have been stripped of meaning by logicians, and act as self-contained mechanisms.
Finally, we may observe that second-order logical calculi may offer a method of formalizing the laws of thought, so that we may state them as theorems rather than theorem schemas. However, we shall not pursue that avenue here.
To summarize, we have observed that certain formulations of the laws of noncontradiction and excluded middle appear as theorem but not axiom schemas of the statement calculus and of the first-order predicate calculus, and we have presented the single proof schema sufficient for both. They are therefore theorem schemas of any expansion on the statement calculus, including any first-order theory which uses it. Since it would therefore be redundant to include them as axiom schemas of any theory overlaying the statement calculus, we can expect them never to appear as such. On the other hand, although the law of identity is absent in any natural form from the statement calculus and from the pure predicate calculus, it appears as axiom schema (E1) of the predicate calculus with equality, and therefore as an axiom schema of any associated formal first-order theory, for example certain common formulations of set theory. Since any axiom is also a theorem, we therefore acknowledge that all three laws are theorem schemas of any formal theory overlaying first-order predicate calculus with equality.
Notes:
[1] We may wish to note that some have questioned whether the law of identity authentically originates with Aristotle, but for our purposes we will ignore that somewhat arcane controversy in favor of popular convention.
[2] Stoll, Robert. Set Theory and Logic (originally published 1963, this edition 1979), ISBN 0-486-63829-4. The statement calculus is described on pp375-377. According to Stoll, the system of Frege was published (not necessarily originally) in Die Grundlagen der Arithmetik, Eine logischmathematische Untersuchung Über der Begriff der Zahl (1934); Łukasiewicz is credited without citation as having contributed to Stoll's formulation.
[3] Stoll, pp388-390, citing Church, Alonzo, Introduction to Mathematical Logic, Vol. I (1956).
The law of identity: Every entity is the same as itself.
The law of noncontradiction: No proposition is both true and false.
The law of excluded middle: Every proposition is either true or false.
I wish briefly observe the role and expression of these laws in certain formal logical systems, namely that of the statement and first-order predicate calculi. As we shall shortly see, the laws of noncontradiction and of excluded middle appear as theorem schemas but not axiom schemas of the statement calculus, given an appropriate overlaying theory and interpretation thereof. The law of identity, in contrast, is not a theorem schema of the statement calculus, nor any pure predicate calculus. However, it is an axiom schema of equality, the results of which are commonly absorbed into first-order formal theories.
Before we begin our outline, I should say a few words regarding our motivation: For mathematicians and logicians usually perceive nothing special about these laws, and in the context of formal logic we have little reason to pay them any great attention relative to other theorem and axiom schemas. However, they are well-known in certain circles as Aristotelian "laws of thought"[1] which, according to certain philosophy enthusiasts I've encountered, lie at the root foundation of our ability to think and reason. This view has become especially popular among what are called "presuppositionalist" Christian apologists, who argue that the God Yahweh is the only possible explanation for the existence, as they describe it, of these laws. Needless to say, such arguments have failed to convince most academic philosophers, and this author, although not a philosopher himself, follows in their skepticism. Let us now explicitly clarify that our discussion shall not further involve those arguments. Neither will our outline deal with the possible role which some versions of the Aristotelian laws may play in understanding our ability to reason. Instead, we will restrict our attention to the appearance, or lack thereof, of the laws strictly within the context of axiom and theorem schemas of formal statement and first-order predicate calculi, with the hope that it will spark the interest of those who are involved in some manner or another with apologetics.
We do not intend it to be necessary to have any knowledge of formal logic in order to appreciate our forthcoming observations. Instead, we will introduce the reader presently to formal systems by providing an example of a very basic formal logical calculus. To that end, the following is Jan Łukasiewicz's refinement of Gottlob Frege's statement calculus, as reorganized by Robert Stoll:[2]
We define a string of the primitive symbols ¬, →, (, ), A, B, C, A1, B1, C1, ..., as a formula if it meets the following inductively-applied criteria:
(F1) Each statement variable (a primitive symbol of the form Xi) is a formula.
If A and B are formulas, then
(F2) (A) → (B) is a formula, and
(F3) ¬(A) is a formula.
(F4) A string is a formula only if it is the last in a column of strings, each of which is a statement variable, or which is obtained from strings appearing earlier in the column by the application of (F2) or (F3).
Regarding (F2) and (F3), we almost always abbreviate formulas by omitting parentheses where their place is otherwise unambiguous.
Given the above definition, we present the axiom schemas for the statement calculus: If A,B,C are formulas, then
(S1) A → (B → A),
(S2) (C → (A→B)) → ((C→A) → (C → B)), and
(S3) (¬A → ¬B) → (B → A).
A proof is a finite column of formulas, each of which is either an axiom or else inferred by modus ponens (B if A and A → B) from two (not necessarily immediately) preceding formulas in the column. A theorem is the last formula in such a column.
As we can plainly see, none of the three laws of thought make an appearance in the axiom schemas of the statement calculus, nor in its essential definitions, that is, the definitions of formula, proof and theorem. The same goes for at least one if not all first-order predicate calculi, namely that of Alonzo Church, as presented by Robert Stoll (which we shall not reproduce here).[3] However, something like the law of noncontradiction we incorporate into the definition of consistency of formula sets:
A formula A is deducible from a set Γ of formulas iff it is possible to construct a column of formulas such that the last formula in the column is A, and each formula in the column (including A) is either an axiom, a member of Γ, or else inferred by modus ponens from two preceding formulas in the column. Γ is consistent iff for no formula B can we deduce from Γ both B and ¬B; otherwise Γ is said to be inconsistent.
Although not quite the same as the law of noncontradiction, we can see the parallel. Every consistent set of assumptions, for example the axioms of a first-order theory, over the framework of the given statement calculus (and indeed Church's predicate calculus), upholds the principle that for no formula A do we have both A and ¬A as theorems. Nevertheless, the definition of consistency is an identifier, not a rule, and as such does not behave as a "law" in the sense we have in mind.
Therefore we may consider presently how to state the law of noncontradiction as such a theorem schema. Now, the concepts of true and false do not automatically accompany the statement calculus. However, the concept of a theorem schema is usually intended as the formal analog of a tautology, that is, a statement form which is always true, regardless of its interpretation. Meanwhile, the logical connectives ∧ and ∨ are usually associated with the concepts of and and or, respectively, whereas ¬ we read as not, or, more explicitly, it is not the case that. Furthermore, the concept of a law we take as analogous to a theorem or axiom schema in formal calculi, that is, a theorem or axiom for which we may substitute any individual or predicate constant for all instances of any free or predicate variable, respectively. To this end, we offer the following formulations of the laws of noncontradiction and of excluded middle as possible theorem schemas of the statement calculus:
The law of noncontradiction: For any formula A, we have ¬(A ∧ ¬A) as a theorem.
The law of excluded middle: For any formula A, we have A ∨ ¬A as a theorem.
By definition of the ∧ and ∨ symbols, we write these theorems using formal notation as A → A and ¬A → ¬A, respectively. Each are theorems, regardless of our choice of A. The proof of the former is quite straightforward:
(1) A → ((B → A) → A) (S1)
(2) A → (B → A) (S1)
(3) (A → ((B → A) → A)) → ((A → (B → A)) → (A → A)) (S2)
(4) (A → (B → A)) → (A → A) (1,3,MP)
(5) A → A (2,4,MP)
We obtain the result ¬A → ¬A by substituting all occurrences of A with ¬A in the preceding proof.
On the other hand, the law of identity makes no obvious appearance among the axiom schemas of the statement calculus which we have stipulated, and indeed the same goes for Church's predicate calculus. This may seem surprising to those with only knowledge of semiformal mathematics, since the = symbol is employed in just about every informal system of note. However, in a formal system, the = operator must be explicitly defined into existence, which is not the case in either Łukasiewicz's or Church's calculi. We describe such predicate calculi as without equality, to distinguish them from those calculi for which we wish to explicitly define = as a logical symbol.
We shall presently begin a discussion of predicate calculi with equality. However, in order to do so, some general understanding of predicate calculus notation is required. Readers lacking a familiarity with this notation may refer to wikipedia's page describing the formulation rules of first-order logic.
With predicate calculus notation in mind, we describe the constant = as a special kind of two-place predicate symbol, such that we may construct the formula (x=y) for any individuals x,y. As a predicate, then, it is absent from the statement calculus regardless of its specific formulation. In order to incorporate it into a predicate logic, we append to the initial set of predicate logic axiom schemas the following two additional schemas:
(E1) x=x, where x is any individual symbol.
(E2) (x=y) → (A → B), where B is obtained by substituting y for all free occurrences of x in A.
Axiom schemas (E1) and (E2) are absent from what we call a "pure" predicate calculus, which, among other characteristics, excludes by definition all constants. Since = is a logical constant, then it cannot appear in a pure predicate calculus. Informally, we may expound axiom schema (E2) as follows: If A is a 1-place predicate, then (x=y) → (A(x) → A(y)), if A is a 2-place predicate, then (x=y) → (A(x,z) → A(y,z)) and (x=y) → (A(z,x) → A(z,y)), and so on for all n-place predicates A. Similar implications hold for formulas which are not precisely of the n-place form, but rather incorporate a subformula, so to speak, which is an n-place predicate. Needless to say, this informal description is inadequate for a precise understanding of (E2), but we offer it for the benefit of those lacking familiarity with formal predicate calculus.
Plainly, the statement schema x=x has a striking interpretive similarity to the law of identity as we stated it in English: every entity is the same as itself we may read as every entity x is the same as x, or, in the context of predicate calculus, for every individual x we have x=x. It seems clear, then, that (E1) best represents the law of identity in predicate calculus with equality. Axiom schema (E2), meanwhile, describes the intuitive consequences of the law of identity.
Now that we have identified the laws of thought in the axiom and theorem schemas of predicate calculus with equality, we may turn to address their spirit. In our formal system of predicate calculus these schemas establish the mechanical rules for the organization of symbols. For example, axiom schemas (E1) and (E2) govern the behavior of the = symbol. This is all any such axiom or theorem schema could ever do in systems such as the statement and predicate calculi, which have been stripped of meaning by logicians, and act as self-contained mechanisms.
Finally, we may observe that second-order logical calculi may offer a method of formalizing the laws of thought, so that we may state them as theorems rather than theorem schemas. However, we shall not pursue that avenue here.
To summarize, we have observed that certain formulations of the laws of noncontradiction and excluded middle appear as theorem but not axiom schemas of the statement calculus and of the first-order predicate calculus, and we have presented the single proof schema sufficient for both. They are therefore theorem schemas of any expansion on the statement calculus, including any first-order theory which uses it. Since it would therefore be redundant to include them as axiom schemas of any theory overlaying the statement calculus, we can expect them never to appear as such. On the other hand, although the law of identity is absent in any natural form from the statement calculus and from the pure predicate calculus, it appears as axiom schema (E1) of the predicate calculus with equality, and therefore as an axiom schema of any associated formal first-order theory, for example certain common formulations of set theory. Since any axiom is also a theorem, we therefore acknowledge that all three laws are theorem schemas of any formal theory overlaying first-order predicate calculus with equality.
Notes:
[1] We may wish to note that some have questioned whether the law of identity authentically originates with Aristotle, but for our purposes we will ignore that somewhat arcane controversy in favor of popular convention.
[2] Stoll, Robert. Set Theory and Logic (originally published 1963, this edition 1979), ISBN 0-486-63829-4. The statement calculus is described on pp375-377. According to Stoll, the system of Frege was published (not necessarily originally) in Die Grundlagen der Arithmetik, Eine logischmathematische Untersuchung Über der Begriff der Zahl (1934); Łukasiewicz is credited without citation as having contributed to Stoll's formulation.
[3] Stoll, pp388-390, citing Church, Alonzo, Introduction to Mathematical Logic, Vol. I (1956).
Comments