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.
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.
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.
Written by Eddy.