Formalizing logic

One may characterize a logical system in terms of implication; the obvious way to do so is as a relation – I'll call it Imp, to avoid having its name get mixed up with this discourse's discussion of its own processes of inference. Imp's left and right values are called statements; if Imp relates a to b, then its logical system considers a to imply b. Implication is transitive: a implies b and b implies c guarantees us a implies c; and reflexive – i.e. it subsumes the identity on statements; a implies b guarantees us both a implies a and b implies b; thus every statement is a fixed point of Imp (and every fixed point of Imp is a statement). Thus Imp∘Imp = Imp and Imp subsumes {statements}.

Now, (|Imp:) relates a to b iff Imp relates b to x implies Imp relates a to x, i.e. (in Imp's opinion) b implies x implies a implies x. In particular, since Imp is reflexive, so relates b to b (so we can take x = b), (|Imp:) relates a to b implies Imp relates a to b; so Imp subsumes (|Imp:). Since Imp is transitive, Imp relates a to b and b to x implies Imp relates a to x, hence Imp relates a to b implies (|Imp:) relates a to b, so (|Imp:) subsumes Imp; hence (|Imp:) = Imp. By a similar argument, reverse(Imp) = (:Imp|). The intersection of Imp with its reverse is just the equivalence of mutual implication; for all practical purposes, Imp's logical system considers this equality among statements.

The classic ab falso quod libet specification of false (false statements imply everything) and its dual can be encoded as

being the collections of statements which Imp considers, respectively, true and false. Imp is consistent iff T∩F = {}; Imp is complete iff T∪F = {statements}.

Consider any x in (T:Imp|). There's some y in T for which Imp relates y to x; and (Imp|Imp:{y}), so (Imp|Imp∘Imp:{x}), but Imp∘Imp = Imp, whence we infer x in T. Thus T subsumes (T∘Imp:x←x:) – anything a true statement implies is, itself, true. Since Imp is reflexive, this collection also subsumes T, so we infer (T∘Imp:x←x:) = T; likewise, F = (:x←x:Imp∘F).

Notice that, thanks to this last, T and F are trivially equivalence classes of Imp; it may thus be more useful to deal with the all-equivalences on T and F in place of the collections; these are (T:Imp|) and (|Imp:F), each of which is an equivalence that Imp subsumes. Even a single t in T and f in F will yield ({t}:Imp|) = (|Imp:{f}) as an equivalence – however, I shall not assume that T and F are non-empty.

Since Imp = Imp∘Imp, any X = (Y∘Imp:x←x:) satisfies (X∘Imp:x←x:) = X and any (:x←x:Imp∘Y) = X satisfies X = (:x←x:Imp∘X). [If you can get there from X, via Imp, then you can get there from Y via Imp∘Imp = Imp, but then you can get there from Y via only Imp, so there is in X to begin with.] Furthermore, any such X (of either kind) is trivially a union of equivalence classes of Imp.

The classic set of axioms becomes a collection, Axi, of statements; then V = (Axi∘Imp|x←x:) is the collection of statements one may infer from Axi; as long as T subsumes Axi, and Axi is non-empty, we have V = T. We can also introduce A = (V:Imp:), the sub-relation of Imp containing all inferences one may obtain in Imp starting from Axi. As Imp is reflexive, so (:A|) must subsume V; and, as Imp is transitive, x in (:A|) implies x in (Axi:Imp|) implies x in V; so V = (A:x←x:) and A = (V:Imp|V), whence we can infer A = A∘A, so A looks like Imp.

The complication with axioms is that we only know as much about Imp as is encoded in the statements in Axi; while (Axi:Imp|) may be (T:Imp|), we need to ensure Axi contains enough information to tell us this. So now we must address the issue of how statements, Imp's values, encode information about Imp itself. How do we pull ourselves up by our own boot-straps ?

Thoughts and Asides Concerning Logic

We'll generally include, in Axi, some statements about Imp: we'd better make these true (i.e. we, externally, can see they're true: A is going to presume they're true regardless, along with anything it can infer from them) if we want A to be a faithful description of itself. Those statements about Imp will encode information like: for all a, b in {statements}, Imp relates (a and b) both to a and to b, for each statement a, Imp relates a to not(not(a)). We shall, thus, need to find ways of encoding such statements – in particular the operations and, or and not – as statements about structural properties of Imp.

I'll define: a statement,

t, is true

iff (:x←x:Imp&on;{t}) = (Imp:x←x:), i.e. every statement implies t;

f, is false

iff ({f}&onn;Imp:x←x:) = (:x←x:Imp), i.e. (ab falso quod libet) f implies every statement.

Along with these I can define two sub-relations of Imp:

True = ({true statements}:Imp:)

so True relates t to z iff t is true and Imp relates t to z; Imp relates any statement to itself, so we instantly know that True subsumes {true statements} = (|True:); whence so does (:True|). Next, consider any z in (:True|), whence, for some true t, Imp relates t to z; for any statement a, we know Imp relates a to t; so Imp∘Imp = Imp relates a (via t) to z; thus z in (:True|) implies z is true, so {true statements} subsumes (:True|) and we infer that True subsumes (|True:) = (:True|).

Thus, as for Imp, we can write t is true as t in True. Imp relates every statement to each t in True; in particular, it relates every a in True to every t in True; so True = (True: All :True) is a restriction of the all-relation, which relates anything to anything.

False = (:Imp:{false statements})

which relates a to f iff f is false and Imp relates a to f; whence, for any statement z, Imp∘Imp = Imp relates a (via false f) to z; so a is False. Thus {false statements} = (:False|) subsumes (|False:). We know Imp subsumes {false statements} = (:False|) whence so does False; whence (as before) so does (|False:) which we've just seen subsumed by (:False|) so we find that False subsumes (|False:) = (:False|) and can write a in False for a is false. Again, False relates every false statement to every false statement, False = (False:All:False).

Since Imp∘Imp = Imp, we readily obtain: False∘Imp = Imp and Imp∘True = True. To go the other way, consider True∘Imp: this relates a to z iff; Imp relates a to some t and True relates t to z iff; t is true and Imp relates a to some t and t to z iff; a is true and Imp∘Imp = Imp relates a to z iff; True relates a to z

Now consider any statement, z, in (:True|); there is some true t for which, True (hence Imp) relates t to z; for any statement a, Imp relates a to t since t is true; so Imp = Imp∘Imp relates a (via t) to z. Thus z in (:True|) implies every statement implies z, which is to say: z is true; thus (:True|) = {true statements} = (|True:); furthermore, Imp relates every true statement to itself, so True subsumes {true statements} and (as for Imp) I can write t in True for t is true.

Likewise, a in (|False:) implies some false f for which Imp relates a to f; then, for any statement z, Imp relates f to z

then observe at least one of each pair in: False∘Imp = False = Imp∘False and Imp∘True = True = True∘Imp. Now, I (or indeed A) considers a statement to be true iff it's in (:I|), i.e. it can be inferred from the axioms, A. In these terms, the notion true is going to be somewhat dependent on A and I. These are classical logic's characterization: of course, Imp may not be a classical logic, so either True or False might be empty; but we can, at least, define them and describe statements as true and false in terms of them. We can safely assert that (:I|) will subsume (:True|), but we need to take care to avoid having (|I:) and (|False:) overlap.

Two combinators from the lambda calculus:

Some more burbles:

The above correspond to implications:

Let us begin

Logic's utility lies in its ability to give me definite answers; but it also has to give me right answers. I may have difficulty in determining what are right answers (after all, why would I delegate to a formalization if I knew already ?), but I can at least stop to check whether a logical system ever gives an answer which even it agrees is wrong: a logical system which proves two contradictory things isn't much use !

Kurt Gödel's great triumph (in about 1930) was to find a way to twist around the notion of counting far enough to ensure that, if a logical system were capable both of describing counting and of deciding every statement in its remit, it would have to entertain (an encoding of) Gödel's fork as being within its remit; which would oblige it to either prove or disprove it. The fork in question may informally be expressed, in a logical system called L, as: Gödel's fork in L asserts that there is no proof, in L, of Gödel's fork in L. A logical system which makes up its mind for or against this is in deep trouble, since a proof yields a disproof and vice versa, so either way the logical system disagrees with itself: after that, how shall I know when to trust its answers ?

Even inconsistency needn't be utterly lethal in a logical system: if it only disagrees with itself about things about which we don't care, we may tolerate it. Of course, if the logical system contains apparatus for inferring disagreements we do care about, our tolerance is going to evaporate: in particular, being able to make up its mind about every statement within its remit would make inconsistency this infectious. So, even if we accepted an inconsistent system, we'd have to regard completeness (the ability to decide everything) untenable.

Logic is thus freed from any obligation to claim that it can make up its mind about every question we know how to ask it: and we are freed to choose logical systems which at least yield intelligible and convincing reasoning and answers, without having to try to so construct them as to give them a good chance of attaining completeness – the unattainable.


So what can I say in total generality about a logical system that I'm interested in being able to use ? It doesn't disagree with itself about anything important, but that notion important is a bit nebulous. Still, any logical system which disagrees with itself about everything is clearly a waste of space: if nothing at all is important, we won't have much need for the logical system; otherwise, it's going to disagree with itself about something important. I also want to be able to use the logical system in my analysis of itself, partly as a sanity check but also because (if it's worth using) it should be quite a good tool for describing itself …

So, at least implicitly, every logical system of interest is capable of talking about the question do I disagree with myself about everything ?. This statement may quite sensibly be given the name false: in classic ab falso quad libet style, this statement implies everything (by modus ponens); so we'd far sooner have it answer I do not know than Yes. (Some more advanced work from Gödel discourages one from being so pushy as to demand the answer No. Ignorance may not be bliss, but there are worse fates.)

Quod Libet (Twelfth Night; or, What You Will)

So we know at least one statement in our logical system. For it to warrant the title logical system it must resemble reason at least enough to provide a characterization of how, given some of its statements, we may discover which other statements. That will oblige it to discuss both statements and relationships among statements; in particular, some of its statements will thus be about such relationships.

One pretty prominent characteristic of reason, known to some as modus ponens, is that statements mean what they say; we're not really going to be interested in a logical system which says that some logical system it subsumes can prove itself inconsistent, but can't show you such a proof (for instance).

… and we presume that, within our logical system, we can describe (potentially via some layer(s) of interpretation) at least some of its mechanics. So, for all practical purposes, it includes the means to describe how it goes about reasoning: which lets us move on to introducing statements it is implicitly able to make.

To systematize reason, logic proceeds from given truths to answers to interesting questions. We introduce the givens from our own knowledge of the domain to which we're applying logic; we select questions in the light of what seems to us to matter in each domain; we interpret the answers, likewise, in that domain. For us to be able to do this with our logical system, and for it to be able to describe the part of the process which it contributes, it must be able to discuss things we think of as statements (in that logical system). One of those statements is false, just introduced; some of the others must be intelligible to us as rules of inference which say what we would be able to infer if we were given assorted forms of statement as prior truths.

Logic as category theory

Associate any statement with the collection of proofs of that statement. A proof of A ⇒ B is a function from proofs of A to proofs of B: thus the collection of proofs of A ⇒ B is the homset from the collection of proofs of A to that of B.

A statement is false if one may deduce False from it: i.e. there is a functions from its set of proofs to the (empty) set of proofs of False. A statement is true if one can exhibit a proof of it, in which case one may prove it from anything (for, given a proof P of A: from any set of proofs, we may define the constant function, whose value, when taken, is P, to the proofs of A; thus A may be proved from anywhere).

In some sense, we here equate A and hom(True, A). In Set, this makes sense as True is the terminal 1 and any hom(True, A) is described exactly by the value, in A, it gives to True's one member: there is such a hom(True, A) for each member of A and the relation is 1-to-1, so A and hom(True, A) are, indeed, isomorphic.

The statement not A is A ⇒ False. If we know that not A is false, what can we say about A ? Not A is false is equivalent to there is a function Proofs(not A) → {}, which is, in turn, equivalent to Proofs(not A) is empty or {} = hom(A, False). In Set, this says A is non-empty: however, we may have no exhibitable proof of A, since exhibiting a function Proofs(not A) → {} need not involve exhibiting a proof of A.

Crucially, this assumes the absence of any morphism from any terminal identity (True) to our initial identity (False). Any such morphism would (via the uniquenesses implied by the definitions of initial and terminal) convert the (unique) morphism from initial to terminal into an isomorphism between the two, which is a proof of inconsistency.

Gödel's fork on a logical system L corresponds to an identity morphism, G, on the set of proofs of Gödel's fork in L: this says there is no morphism from True to G. In some sense, G may be read as hom(hom(True, G), False). A morphism in here identifies hom(True, G) as empty, in which case G has no members, so there are no morphisms in here. But if G is empty, then hom(True, G) is empty, whence there are morphisms from it to False, whence G is non-empty. Thus it is not possible to decide whether G = hom(hom(True, G), False) is empty.

Consider a category in which there is an initial identity, False, with hom(False, False) terminal. Now, False being initial, there is precisely one morphism from False to False, and that is False. So our terminal hom(False, False) has precisely one member: call it True. Then hom(True, True), by virtue of True being terminal, has precisely one member and so is isomorphic to hom(False, False) = True.

With not(A) defined as hom(A, False), this gives us not(False) = True, but tells us nothing about not(True). We tend to assume that not(True), i.e. hom(True, False), is isomorphic to False: but Gödel's fork teaches us not to make that assumption formal – for it is the assumption of consistency. We also have, for any A, both hom(A, True) and hom(False, A) isomorphic to True, by virtue of the terminal and initial properties of True and False, respectively. Our attention is then focused on hom(True, A) and hom(A, False).

First, examine hom(hom(A, False), False), i.e. not(not(A)), and its relationship with A and hom(True, A).

Peano's successor functor

Cantor's diagonal argument is closely related to this.

Peano's successor functor 1+ (aka. suc) on the category Set takes any morphism (A|f:B) to (1+A|1+f:1+B) with

There is a natural transformation between this functor and the identity, (identity|T:1+): given (A|f:B) in Set, T(f) takes A under f to B and embeds this in 1+B, or equivalently takes A under its natural embedding and follows 1+f thereafter.

In a category in which a functor, F, may be found to fill the rôle 1+ fills for Set, if we have an initial identity, then the associated natural transform, T, yields T(initial identity) as the unique successor of the initial identity which has, as a successor, F(initial identity).

Valid CSSValid HTML 4.01 Written by Eddy.