One may characterise a logical system as a relation, called `implication'. Its initial and final values are called `statements'. Implication is transitive: `a implies b' and `b implies c' guarantees us `a implies c'; and subsumes the identity on statements, so `a implies b' guarantees us both `a implies a' and `b implies b'. Thus implies&on;implies = implies as a relation.
We shall be standing outside this relation to study it. While I am describe it as `implication', it hijacks the words I would be using in the present discourse to explain how I infer truths about the relation under study. So, from here, I'll just call the relation Imp and revert to using the language of implication in its natural sense within this discourse.
I'll continue referring to Imp's initial and final values (each of which is, indeed, a fixed point) as statements. Note, in particular, that any collection of statements is a sub-collection of (|Imp:) = {statements} = (:Imp|) and that, since every statement is a fixed point of Imp (i.e. implies itself), {statements} is a sub-relation of Imp; so any collection of statements is a sub-relation of Imp.
Further, since I define `a in B' to mean `B relates a to a', I can use Imp in place of {statements}: `a in Imp' iff `Imp relates a to a' iff `a is a statement'. In general, if a relation, r, subsumes (:r|), `r relates a to z' implies `r relates z to z' implies z in (|r:) so (|r:) subsumes (:r|); likewise, if r subsumes (|r:) then so does (:r|); so, if r subsumes (|r:) and (:r|) then each subsumes the other and (|r:) = (:r|) = {fixed points of r}, and we can describe the values (initial and final) of r as being `in r'.
We have Imp&on;Imp = Imp, and we can examine sub-relations of Imp. The classic `set of axioms' becomes a collection, A, of statements; then (A:Imp|) is the collection of statements one may infer from A; and I = ((A:Imp|):Imp:) is the sub-relation of Imp containing all inferences one may obtain in Imp starting from A. As specified, I is Imp&on;(A:Imp|) and we obtain I = Imp&on;I. Further, since Imp subsumes {statements}, (:I|) = (|I:) = (A:Imp|), I = (I:Imp:) and I&on;I = I.
We'll generally include, in A, some statements about Imp: we'd better make these true (i.e. we, externally, can see they're true: I is going to presume they're true regardless, along with anything it can infer from them) if we want I 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. We'll also need some characterisation the notions `true' and `false'.
I'll define: a statement,
iff (|Imp:{t}) = (:Imp|), i.e. every statement `implies' t - or {true statements} = intersect({({a}:Imp|): a in (|Imp:)});
iff ({f}:Imp|) = (|Imp:), i.e. (ab falso quod libet) f implies every statement - or {false statements} = intersect({(|Imp:{z}): z in (:Imp|)}).
Along with these I can define two sub-relations of 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&on;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.
which relates a to f iff f is false and Imp relates a to f; whence, for any statement z, Imp&on;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&on;Imp = Imp, we readily obtain: False&on;Imp = Imp and Imp&on;True = True. To go the other way, consider True&on;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&on;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&on;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&on;Imp = False = Imp&on;False and Imp&on;True = True = True&on;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 characterisation: 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:
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 formalisation 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 aparatus for infering 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 sytem, 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 chose logical systems which at least yield ingelligible 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.)
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 characterisation 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 systematise 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.
Associate any statement with the collection of proofs of that statement. A proof of A &implies; B is a function from proofs of A to proofs of B: thus the collection of proofs of A &implies; 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: ie 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 &implies; 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), ie 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 focussed on hom(True, A) and hom(A, False).
First, examine hom(hom(A, False), False), ie not(not(A)), and its relationship with A and hom(True, A).
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).
Written by Eddy.