]> Representing Formal Logic

Representing Formal Logic

Assume we have some way of encoding our logical system as a family of texts; many of these shall describe ways of characterising and manipulating texts; some of these shall be concerned with identifying which texts are to be understood as statements, others with which manipulations can be performed, on statements, to produce other statements, along with the extent to which characteristics of the result of manipulation can be inferred from characteristics of the texts manipulated. One type of text is called a proof; charcterising what texts constitute proofs is ultimately the purpose of all the other texts involved in describing the logical system. The specification of what constitutes a proof is expressed in terms of characterising which manipulations of statements constitute valid inferences; a proof is a sequence of inferences. The texts that state the rules of inference (possibly along with some others) are given to be true, as are all statements that can be reached from true statements by valid inferences.

In what follows, I'll use common terms like implies, and, not and or for logical operations; I'll be using them in the sense introduced in this discussion. The logical system hypothetically being discussed may, of course, use the same terms, possibly with more or less the same meanings; however it's important to understand that I'm not presuming they do so, or that (if they do) they use those terms with the same meanings I do; I'm not discussing the logical system's use of the terms, I'm describing my model of the logical system in terms of its inference relation, which I name implies and from which I induce an equivalence and, modulo this equivalence, a mapping not and two binary operators and and or. There may be statements that the binary operators don't know how to combine and there may be statements the function doesn't accept as inputs; albeit, if the logical system defines analogous binary operators and function suitably, this may ensure their completeness.

Encoding inference by a relation

When we encode inference as a relation, which I'll name implies, it relates texts to those that can be inferred from them; all this relation's values are statements. It's reflexive (every statement does imply itself) and transitive (if A implies B and B implies C, then A implies C also). Its intersection with its reverse is thus an equivalence, that identifies two statements precisely if each implies the other; in equations between statements, I'll use = to denote this equivalence. In practice, we usually discuss statements (and hence the relation implies) modulo this equivalence.

In so far as we have a notion of meaning to our texts, for which two statements may be construed as meaning the same thing, we expect inference to allow all the same conclusions from each of them, notably including each other. Thus means the same thing as is an equivalence subsumed by inference's equivalence; we can identify each equivalences class of texts as a meaning that each text in the equivalence class does indeed mean; we can then reinterpret our relation on texts as a relation among their meanings. It may arise that distinct meanings are none the less equivalent under inference; they imply each other.

Consider the end-relations (|implies:) and (:implies|). The specification implies that: as implies is reflexive, it necessarily subsumes (|implies:) and reverse(:implies|); as implies is transitive, each of (|implies:) and reverse(:implies|) subsumes it; hence it is in fact equal to both. The intersection of (|implies:) with (:implies|) is then our inference-equivalence on statements.

Texts discussing implies

Many of the texts that comprise the statement of the logical system's rules of inference are values of the implies relation; and many of these effectively describe structural properties of that relation. Many of the rules of inference, indeed, concern themselves with statements about this relation and how to manipulate such statements to obtain sub-relations of implies.

Given a statement (that is, a text that is a value of implies), there may be operations I'll refer to as enclosing, which isolate the text in some way (e.g. by putting quotes or parentheses at its start and end) that ensure, when the enclosed text is used as a sub-text, that the part of the text that is a copy of our given statement will be understood as that statement and not, for example, split in some way such as having its first part read as the tail of some earlier text and some tail of the statement read as the beginning of something later, with the part in between now read as connecting these two larger things, in the way that the statement we started with only connected the specified first part and tail. Enclosing a statement produces a statement that says the same thing but has a textual form that lets us use it as a sub-text of other texts, such that its meaning as a sub-text is the same as its meaning taken apart from the text of which it is used as a sub-text.

I suppose that the system has some way to say that one statement does imply another; and that a text, that says one statement implies another, is itself a statement (albeit not necessarily a true one). This might be constructed simply by joining enclosed forms of the two statements with a word, such as implies, between them; or it may be expressed in some other way. Given statements B and C, I'll write B implies C as my token by which to refer to the statement, within the system, that declares that B does indeed imply C. Even when implies does not relate B to C, this statement may exist, so be a value of implies and, indeed, may appear as an enclosed sub-text of other statements. It's possible the logical system only has a statement filling this rôle for some pairs of statement, not for all; there may be a relation, among statements, that we can think of as is syntactically capable of implying, that isn't the all-relation on the values of implies; however, this relation must subsume implies.

Note that, in my notation, B←C is an atomic relation; when B and C are statements of the logical system, this atom is a sub-relation of implies precisely if B implies C; which may also be written B ⇒ C; don't let the wrong direction of the ← distract you: it's just part of my formal syntax for denoting relations.

Consider any atom of implies that has, as its right value, a statement of form B implies C; if its left value is true, so is this right value (by transitivity), hence B←C is another atom of implies. One of our rules of inference might tell us that, whenever implies relates a right value A to a left value of form B implies C, it also relates B to A implies C. Thus, for any statements A, B, C, the composite statement (A implies (B implies C)) implies (B implies (A implies C)) is true (i.e. a right value of implies, to which it relates the given rule of inference) and implies does subsume the atom A implies (B implies C)B implies (A implies C).

Conjunction: combining statements with and

Given a set S of statements, we can form {statement C: ({C}:implies|S)}, the collection of statements each of which implies every statement in S; among these, we can look to see whether there are any that all imply; if there are, they all imply one another, by construction, so are equivalent; when S is just {A, B} for some statements A and B, we can think of these statements as meaning A and B, with and serving as a binary operator; more generally, we can use this to define a bulk action for and, which applies to any collection S of statements for which {statement C: (|implies:{C}) = intersect(: (|implies:{s}) ←s :S)} is non-empty; the members of this are all equivalent and may be thought of as bulk(and, S). Because intersectin is abelian, so is the binary operator and.

The logical system may provide a construction for combining two texts that, when applied to two statements, gives one that is implied by exactly every statement that both implies A and implies B; that statement C would then have (|implies:C) = (|implies:{A})∩(|implies:{B}), and it would mean A and B in the sense just given.

We could equally, given statements A and B, construct {statement C: C implies exactly those statements X for which A implies (B implies X)}; if it is non-empty, its members are all equivalent; for now, think of them as meaning A with B. If we have the inference rule A implies (B implies C) implies B implies (A implies C) then with is abelian. If we have the rule C implies (B implies C) then A with B implies A; and, as implies is reflexive, B implies B is always true and implies A implies (B implies B); as this is thus also true, we find that A with B both implies A and implies B; so the rule C implies (B implies C) ensures that A with B implies A and B. Consider any Z which both implies A and implies B; A and B is one such Z; for any C for which A implies (B implies C), Z implies A hence, transitively, Z implies (B implies C); if one of our rules of inference is implies subsumes ({U}: |{V, (V implies W)}) implies U implies W, then Z both implying B and implying (B implies C) ensures that Z implies C; in such a case, Z will imply every C for which A implies (B implies C); thus A and B implies A with B. So we can specify and and with generally; they might not always both have values but, in so far as they do, some fairly reasonable rules of inference will make them the same binary operator.

In the constructin for and, I had a set, {statement C: ({C}:implies|) subsumes {A, B}), in which any statement that implied any in the set was also in the set; and I selected the members that are implied by all. In the construction for with, I had a set, {statement C: A implies (B implies C)}, in which any statement implied by any member of the set is also a member of the set; and I selected the members that imply all. Such a selection might, of course, produce an empty set. I could alternatively look at the intersection of the two sets, U = {statement C: ({C}:implies|{A, B}) and A implies (B implies C)}. Again, U might be empty; but, if we have any C in U, any statement equivalent to it is also in U; if we also have D in U, so A implies (B implies D) and ({D}:implies|{A, B}) just as for C; with the rules of inferences used in the last paragraph, D implies A so, transitively, also implies B implies C and D implies B also, hence D implies C; as the same argument applies with C and D swapped, we infer that all members of U are equivalent. This, as a result, gives us a third way to define a binary operator that we might want to think of as and.

Sticking with the first, let's try to work out what properties and has and what rules of inference may give it familiar properties. Suppose A implies B; any statement that implies A does also, transitively, imply B; and every statement which both implies A and implies B does, in particular, imply A; so the statements that imply A are exactly the statements that both imply A and imply B; thus A = (A and B) whenever A implies B. Now, still with A implying B, consider some statement C for which A and C and B and C do actually exist. Since A and C does imply A, hence B, and does imply C, we can infer that it also implies B and C. In particular, if we have the rule of inference mentioned above that makes every statement imply every true statement, (A and T) = A whenever T is true.


We can declare a statement to be false precisely if it implies all statements. Any statement that implies a false statement is, transitively, also false; consequently, for any set S of statements that includes a false member, bulk(and, S) will also be false. All false statements are equivalent (they imply each other). I'll say that one statement, A, complements another, B, precisely if A and B is false. As and is abelian, complements is a symmetric relation. Any statement that complements A is known as a complement of A; any statement that implies a complement of A is itself a complement of A and every false statement complements all statements. If two statements are equivalent (i.e. each implies the other) then every complement of either is a complement also of the other.

If there are any statements that are implied by exactly the complements of A, since they're implied by themselves they're complements of A and thus each of them implies all of them, which makes them all equivalent; when such statements exist, we can understand them as meaning not(A). Any attempt to concoct a statement, from which you can both infer A and infer not(A), actually leads to a statement from which you can infer all statements. We can thus define a relation ({statements}: not :{statements}), albeit it might not have all statements as right values, nor need it have all statements as left values. It relates B to A precisely if the statements that imply B are the complements of A. In such a case, it also relates every statement equivalent to B to A; and every statement it relates to A is indeed equivalent to B; thus not respects equivalence among its left values and, modulo equivalence, relates only one left value to any given right value; we can thus understand it as a mapping.

Furthermore, it also relates B to every equivalent of A; albeit there might be some other statements to which it relates B (so it might not be monic, even modulo equivalence). Two statements could complement all the same statements as one another, without either implying the other; in such a case, even if there is a statement C implied by exactly their complements, which not would thus duly relate to both statements, C itself would not be a right value of not unless the two statements both imply (without being implied by) some other complement of exactly the statements that imply C. A rule of inference might provide for equality of sets of complements to imply equivalence, of course, in which case not would be self-inverse; however, such a rule is non-constructive.

For any right value, A, of not we have not(A) which is implied by exactly those statements, C, for which C and A is false; in particular, A and not A is false. Thus A is a complement of not(A); however, even when not(A) is a right value of not, I have no guarantee that every complement of not(A) does imply A. Still, every complement of not(A), including A, does indeed imply not(not(A)). If C complements A and D complements not(A) then, as C implies not(A), C and D implies not(A) and D which is false, so every complement of A complements every complement of not(A); in particular, every complement of A complements not(not(A)), when it exists. Now, any complement of not(not(A)) complements every complement of not(A), notably including A, so the complements of not(not(A)) are exactly the complements of A and we can infer that, whenever A and not(A) are right values of not, so is not(not(A)), with not(not(not(A))) = not(A). Thus not∘not is a projection; it relates each left value to itself (and all statements equivalent to it; but possibly also to some other right values). To summarise:

All statements are complements of any false statement; so not relates, to each false statement, every statement that all statements imply. Now, a statement that all statements imply is necessarily implied by the statement of our rules of inference, hence true. It's possible there are true statements that not all statements imply, unless of course our logical system has a rule of inference (as discussed above) which makes all statements imply the statement of our rules of inference (hence also all true statements). Even without such a rule, the truths that every statement implies do, necessarily, all imply one another, so are an equivalence class under inference; and not relates them to the false statements. In a logical system wherein there are no statements implied by all statements, not does not even have the false statements as right values; such a logical system must lack the rule C implies (B implies C).

Nothing actually prevents our logical system's rules of inference from implying all statements, of course; in such a case, all statements imply one another and our logical system isn't particularly interesting: both implies and not relate all statements to each other. However, more usually, one tries to pick rules of inference that only imply a limited set of statements, that strike our intuitions as reasonable. In such a case, for any truth T that all statements imply, i.e. any not(false) statement, each complement C of T implies T, hence C = C and T, which is false, hence C is false; so the complements of T are all false and imply one another, so not(T) is false. If we have truths that not all statements imply, however, we cannot be sure that all their complements are false; if any of them aren't, for some such truth T, then not(T) won't be false; they might even not be right values of T at all.

A logical system's rules may also specify some transformations of text that turn each (to which the transformations are applicable) into a statement that contradicts the original; a rule of inference may then say that every statement that implies both a statement and its contradiction in fact implies all statements. For any statement A amenable to the tranformation, its contradiction would then be one of the texts meaning not(A).

Disjunction: combining with or

Just as we defined and above, we can define or: given a set S of statements, intersect(: ({s}:implies|) ←s :S) is the all-relation on statements that are implied by every member of S; when it is ({C}:implies|) for some C, all such C are necessarily equivalent and implied by each member of S. Thus bulk(or) relates statement C to set S of statements precisely if C implies exactly those statement that every member of S does imply. There may be some sets S for which there is no such C. We write bulk(or, {A, B}) as A or B as usual.

When A implies B, A transitively also implies every statement that B implies; so the statements that both A and B do imply are precisely the statements that B implies, hence B = A or B. Since every false statement implies all statements, A or F = A whenever F is false; and, when every statement implies every true statement, A or T = T whenever T is true.

Given statements A, B that are left values of not, consider not(A) or not(B), if it exists; we know it implies not(A) and implies not(B), hence it complements A and complements B; furthermore, every statement that complements A and complements B also implies it. Now, as it complements A, it complements every statement that implies A, notably including (A and B); we can reach the same conclusion also by observing that it complements B. So, as long as A and B also exists and is a right value of not, not(A) or not(B) implies not(A and B). Now, not(A and B) is implied by exactly those statements that complement (A and B), i.e. those statements C for which (A and B and C) implies all statements. For each such C, (B and C) implies not(A) while (A and C) implies not(B).

Valid CSSValid XHTML 1.1 Written by Eddy.