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
, i.e. (in Imp's opinion) Imp relates b to x
implies Imp relates a to x
. In particular, since Imp is reflexive, so
relates b to b (so we can take x = b), b implies
x
implies a implies x
(|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 ?
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,
iff (:x←x:Imp&on;{t}) =
(Imp:x←x:), i.e. every statement implies
t;
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:
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.
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:
a or not(a)– does true imply it – if * why *, for either * of
so,
not, ideally for both. Compare and contrast: what's
a and not(a); does it imply false (yes when read as
a and (a⇒false), using modus ponens).
The above correspond to implications:
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.)
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.
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).
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).
Written by Eddy.