]> A categoric formalization of logic

I've mumbled, about assorted things not covered here, in an older page whose content I intend to eventually migrate to here, after some cleaning up.

A categoric formalization of logic

Classical boolean logic (and its constructivist restriction, Heyting algebra) manipulates statements using a unary operator, two symmetric binary operators and a relation:


Negation: for any given statement A, the statement ¬A is true (false) precisely according as A is false (true): negating a false statement produces a true statement and vice versa. Classically, ¬ was supposed to be self-inverse – i.e. it was supposed that ¬¬A = A for all A – but Gödel obliges us to allow that, while every A does indeed imply ¬¬A, the converse need not hold (because A might be undecidable).

Or (a.k.a. disjunction; its symbol resembles the letter v because the Latin for or is vel): given two statements A and B, the statement A∨B is true precisely if at least one of A and B is true. More generally, we can construct a bulk action, bulk(∨) which combines arbitrarily many statements and yields one which is true precisely if any of the statements combined is true; it is false precisely if all are false.

And (a.k.a. conjunction; its symbol is just ∨ upside-down): given two statements A and B, the statement A∧B is true precisely if both A and B are true. Its bulk action, bulk(∧), combines arbitrarily many statements and yields one which is true precisely if all of the statement combined are true; it is false precisely if any of them is false.


Implies: this relates A to B, written A&implies;B, precisely if, whenever A is true, B is necessarily also true. This relation is transitive (A&implies;B and B&implies;C does indeed imply A&implies;C) and reflexive (every statement does indeed imply itself).

The attentive reader shall have noticed that my informal explanations presumed meanings for false and true; one's axioms are taken to be true and a broad class of absurd and nonsensical statements is taken as false; any statement which is implied by true ones is accepted as also true; any statement which, in conjunction with true statements, implies a false one is deemed to be false. I shall not, here, attempt to formalise that.

As binary operators, both ∧ and ∨ are associative; each distributes over the other (that is: A∧(B∨C) = (A∧B)∨(A∧C) and likewise with ∧ and ∨ swapped); they have identities – any true statement is an identity for ∧ while any false statement is an identity for ∨ – and an identity of each overwhelms the other (just as the identity of addition, in a ring, overwhelms multiplication: zero times anything is zero); false and anything is false, true or anything is true. Combining them with ¬, we find that ¬(A∨B) = (¬A)∧(¬B) and likewise with ∨ and ∧ swapped. The attentive reader shall have noticed a strong degree of symmetry between ∧ and ∨.

The statement A&implies;B can be construed as (¬A)∨B. Taken together with the results of combining ¬ with ∧ and ∨ we see that, among our four operations, there is enough redundancy that we should be able to get rid of at least two: it turns out, indeed, that we can reduce to only one, from which the others are all derived.

If we interpret each statement as an object and each truth of form A&implies;B as a morphism from A to B, we can cast formal logic into the framework of category theory. We get an initial object, False, which implies everything, and a final object, True, which everything implies; and we can formalise ¬A as the statement A&implies;False. Given a collection of statements, we can construct a cone to the left or right factorizing via the bulk(∧) or bulk(∨) of the statements – given just two statements, A and B, we construct A∧B and A∨B as cartesian product and disjoint sum: A∧B is the statement implied by every statement which implies both A and B; while A∨B is the statement which implies every statement which is implied by both A and B.

I intend, below, to explore the form this last takes when we work directly with the relation &implies; rather than construing it as a category.

Categoric logic as inference relation

We have a relation, &implies;, whose values are statements. Since it is transitive and reflexive, its intersection with its reverse is necessarily an equivalence; &implies;&intersect;reverse(&implies;) is written ⇔. I shall interpret this equivalence as equality for the rest of this discussion; i.e. the following should be read modulo ⇔.

Define relations And and Or (which shall serve as bulk(∧) and bulk(∨) in due course) as follows. Given any relation S whose left values are statements (they're all I'll be referring to of S; it can be replaced by (:x←x:S), but I define bulk actions in terms of the left values of a relation so that they work nicely with the outputs of a function): we can express A implies every left value of S as ({A}:&implies;|S); and every left value of S implies A by ((|S:)|&implies;:{A}); so let And relate D to S precisely if ({D}:&implies;|S) and ({A:({A}:&implies;|S)}|&implies;:{D}), i.e. D implies every left value of S and is implied by every statement which implies every left value of S; and let Or relate C to S precisely if ((|S:)|&implies;:{C}) and ({C}:&implies;|{A:((|S:)|&implies;:{A})}). That is, define

Now suppose And relates both D and E to S; we have ({D}:&implies;|S), whence D in {A:({A}:&implies;|S)}; and ({A:({A}:&implies;|S)}|&implies;:{E}), so we can infer D&implies;E; equally, E&implies;D so we have D⇔E. Thus, modulo ⇔, And's left values are unique, so And is a mapping; likewise, Or is a mapping (modulo ⇔). That each non-empty ({statements}:S:) yields non-empty (|And:{S}) and (|Or:{S}) must be taken as an axiom of logic. For the case S = {B}, we find And relates D to S precisely if D⇔B: ({D}:&implies;|S) says D&implies;B; ({A: A&implies;B}|&implies;:{D}) implies B&implies;D (since B is in {A: A&implies;B}); and B&implies;D implies ({A: A&implies;B}|&implies;:{D}) by transitivity of &implies;. For similar reasons, Or relates C to {B} precisely if C⇔B.

In the special case where S is a list, its left values are just the entries in the list; so we can define ∧ and ∨ by A∧B = And([A,B]) and A∨B = Or([A,B]).

Now, ({statements}|&implies;:) is itself a relation; every statement is a left value of it, so define False = And(&implies;), which implies every statement, and True = Or(&implies;), which is implied by every statement.

Valid CSSValid XHTML 1.1 Written by Eddy.