Assume we have some way of encoding our logical system as a family of texts;
many of these shall describe ways of characterising and manipulating texts; some
of these shall be concerned with identifying which texts are to be understood
as statements
, others with which manipulations can be performed, on
statements, to produce other statements, along with the extent to which
characteristics of the result of manipulation can be inferred from
characteristics of the texts manipulated. One type of text is called
a proof
; charcterising what texts constitute proofs is
ultimately the purpose of all the other texts involved in describing the logical
system. The specification of what constitutes a proof is expressed in terms of
characterising which manipulations of statements constitute valid inferences; a
proof is a sequence of inferences. The texts that state the rules of inference
(possibly along with some others) are given to be true
, as
are all statements that can be reached from true statements by valid
inferences.
In what follows, I'll use common terms
like implies
, and
, not
and or
for logical
operations; I'll be using them in the sense introduced in this discussion. The
logical system hypothetically being discussed may, of course, use the same
terms, possibly with more or less the same meanings; however it's important to
understand that I'm not presuming they do so, or that (if they do) they use
those terms with the same meanings I do; I'm not discussing the logical system's
use of the terms, I'm describing my model of the logical system in terms of its
inference relation, which I name implies
and from which I induce an
equivalence and, modulo this equivalence, a mapping not
and two binary
operators and
and or
. There may be statements that the binary
operators don't know how to combine and there may be statements the function
doesn't accept as inputs; albeit, if the logical system defines analogous binary
operators and function suitably, this may ensure their completeness.
When we encode inference as a relation, which I'll
name implies
, it relates texts to those that can be
inferred from them; all this relation's values are statements. It's reflexive
(every statement does imply itself) and transitive (if A implies B and B implies
C, then A implies C also). Its intersection with its reverse is thus an
equivalence, that identifies two statements precisely if each implies the other;
in equations between statements, I'll use = to denote this equivalence. In
practice, we usually discuss statements (and hence the relation implies
)
modulo this equivalence.
In so far as we have a notion of meaning
to our texts, for which two
statements may be construed as meaning the same thing
, we expect
inference to allow all the same conclusions from each of them, notably including
each other. Thus means the same thing as
is an equivalence subsumed by
inference's equivalence; we can identify each equivalences class of texts as
a meaning
that each text in the equivalence class does indeed mean; we
can then reinterpret our relation on texts as a relation among their meanings.
It may arise that distinct meanings are none the less equivalent under
inference; they imply each other.
Consider the end-relations (|implies:) and (:implies|). The specification implies that: as implies is reflexive, it necessarily subsumes (|implies:) and reverse(:implies|); as implies is transitive, each of (|implies:) and reverse(:implies|) subsumes it; hence it is in fact equal to both. The intersection of (|implies:) with (:implies|) is then our inference-equivalence on statements.
implies
Many of the texts that comprise the statement of the logical system's rules
of inference are values of the implies
relation; and many of these
effectively describe structural properties of that relation. Many of the rules
of inference, indeed, concern themselves with statements about this relation and
how to manipulate such statements to obtain sub-relations of implies.
Given a statement (that is, a text that is a value of implies), there may be
operations I'll refer to as enclosing
, which isolate the text in some way
(e.g. by putting quotes or parentheses at its start and end) that ensure, when
the enclosed text is used as a sub-text, that the part of the text that is a
copy of our given statement will be understood as that statement and not, for
example, split in some way such as having its first part read as the tail of
some earlier text and some tail of the statement read as the beginning of
something later, with the part in between now read as connecting these two
larger things, in the way that the statement we started with only connected the
specified first part and tail. Enclosing a statement produces a statement that
says the same thing but has a textual form that lets us use it as a sub-text of
other texts, such that its meaning as a sub-text is the same as its meaning
taken apart from the text of which it is used as a sub-text.
I suppose that the system has some way to say that one statement does imply
another; and that a text, that says one statement implies another, is itself a
statement (albeit not necessarily a true one). This might be constructed simply
by joining enclosed forms of the two statements with a word, such
as implies
, between them; or it may be expressed in some other way.
Given statements B and C, I'll write B implies C
as my token by which to
refer to the statement, within the system, that declares that B does indeed
imply C. Even when implies
does not relate B to C, this statement may
exist, so be a value of implies
and, indeed, may appear as an enclosed
sub-text of other statements. It's possible the logical system only has a
statement filling this rôle for some pairs of statement, not for all;
there may be a relation, among statements, that we can think of as is
syntactically capable of implying
, that isn't the all-relation on the values
of implies
; however, this relation must subsume implies
.
Note that, in my notation, B←C
is an atomic
relation; when B and C are statements of the logical system, this atom is a
sub-relation of implies
precisely if B implies C; which may also be
written B ⇒ C
; don't let the wrong
direction of the ←
distract you: it's just part of my formal
syntax for denoting relations.
Consider any atom of implies that has, as its right value, a statement of
form B implies C
; if its left value is true, so is this right value (by
transitivity), hence B←C is another atom of implies. One of our rules of
inference might tell us that, whenever implies relates a right value A to a left
value of form B implies C
, it also relates B to A implies C
.
Thus, for any statements A, B, C, the composite statement (A implies (B
implies C)) implies (B implies (A implies C))
is true (i.e. a right value of
implies, to which it relates the given rule of inference) and implies does
subsume the atom A implies (B implies C)
← B implies (A implies
C)
.
and
Given a set S of statements, we can form {statement C: ({C}:implies|S)}, the
collection of statements each of which implies every statement in S; among
these, we can look to see whether there are any that all imply; if there are,
they all imply one another, by construction, so are equivalent; when S is just
{A, B} for some statements A and B, we can think of these statements as
meaning A and B
, with and
serving as a binary
operator; more generally, we can use this to
define a bulk action for and
, which applies
to any collection S of statements for which {statement C: (|implies:{C}) =
intersect(: (|implies:{s}) ←s :S)} is non-empty; the members of this are
all equivalent and may be thought of as bulk(and, S). Because intersectin is
abelian, so is the binary operator and
.
The logical system may provide a construction for combining two texts that,
when applied to two statements, gives one that is implied by exactly every
statement that both implies A and implies B; that statement C would then have
(|implies:C) = (|implies:{A})∩(|implies:{B}), and it would mean A and
B
in the sense just given.
We could equally, given statements A and B, construct {statement C: C
implies exactly those statements X for which A implies (B implies X)}; if it is
non-empty, its members are all equivalent; for now, think of them as
meaning A with B
. If we have the inference rule A implies (B implies
C)
implies B implies (A implies C)
then with
is abelian. If
we have the rule C implies (B implies C)
then A with B
implies A;
and, as implies is reflexive, B implies B
is always true and implies A
implies (B implies B)
; as this is thus also true, we find that A with
B
both implies A and implies B; so the rule C implies (B implies C)
ensures that A with B
implies A and B
. Consider any Z which both
implies A and implies B; A and B
is one such Z; for any C for which A
implies (B implies C), Z implies A hence, transitively, Z implies (B implies C);
if one of our rules of inference is implies subsumes ({U}: |{V, (V implies
W)})
implies U implies W
, then Z both implying B and implying (B
implies C) ensures that Z implies C; in such a case, Z will imply every C for
which A implies (B implies C); thus A and B
implies A with B
. So
we can specify and
and with
generally; they might not always both
have values but, in so far as they do, some fairly reasonable rules of inference
will make them the same binary operator.
In the constructin for and
, I had a set, {statement C: ({C}:implies|)
subsumes {A, B}), in which any statement that implied any in the set was also in
the set; and I selected the members that are implied by all. In the
construction for with
, I had a set, {statement C: A implies (B implies
C)}, in which any statement implied by any member of the set is also a member of
the set; and I selected the members that imply all. Such a selection might, of
course, produce an empty set. I could alternatively look at the intersection of
the two sets, U = {statement C: ({C}:implies|{A, B}) and A implies (B implies
C)}. Again, U might be empty; but, if we have any C in U, any statement
equivalent to it is also in U; if we also have D in U, so A implies (B
implies D)
and ({D}:implies|{A, B}) just as for C; with the rules of
inferences used in the last paragraph, D implies A so, transitively, also
implies B implies C
and D implies B also, hence D implies C; as the same
argument applies with C and D swapped, we infer that all members of U are
equivalent. This, as a result, gives us a third way to define a binary operator
that we might want to think of as and
.
Sticking with the first, let's try to work out what properties and
has and what rules of inference may give it familiar properties. Suppose A
implies B; any statement that implies A does also, transitively, imply B; and
every statement which both implies A and implies B does, in particular, imply A;
so the statements that imply A are exactly the statements that both imply A and
imply B; thus A = (A and B) whenever A implies B. Now, still with A implying B,
consider some statement C for which A and C
and B and C
do
actually exist. Since A and C
does imply A, hence B, and does imply C,
we can infer that it also implies B and C
. In particular, if we have the
rule of inference mentioned above that makes every statement imply every true
statement, (A and T) = A whenever T is true.
We can declare a statement to be false
precisely if it
implies all statements. Any statement that implies a false statement
is, transitively, also false; consequently, for any set S of statements that
includes a false member, bulk(and, S) will also be false. All false statements
are equivalent (they imply each other). I'll say that one statement,
A, complements
another, B, precisely if A and B
is
false. As and
is abelian, complements is a symmetric relation. Any
statement that complements A is known as a complement of A; any statement that
implies a complement of A is itself a complement of A and every false statement
complements all statements. If two statements are equivalent (i.e. each implies
the other) then every complement of either is a complement also of the
other.
If there are any statements that are implied by exactly the complements of
A, since they're implied by themselves they're complements of A and thus each of
them implies all of them, which makes them all equivalent; when such statements
exist, we can understand them as meaning not(A)
. Any attempt to concoct
a statement, from which you can both infer A and infer not(A), actually leads to
a statement from which you can infer all statements. We can thus define a
relation ({statements}: not :{statements}), albeit it might not have all
statements as right values, nor need it have all statements as left values. It
relates B to A precisely if the statements that imply B are the complements of
A. In such a case, it also relates every statement equivalent to B to A; and
every statement it relates to A is indeed equivalent to B; thus not respects
equivalence among its left values and, modulo equivalence, relates only one left
value to any given right value; we can thus understand it as a mapping.
Furthermore, it also relates B to every equivalent of A; albeit there might be some other statements to which it relates B (so it might not be monic, even modulo equivalence). Two statements could complement all the same statements as one another, without either implying the other; in such a case, even if there is a statement C implied by exactly their complements, which not would thus duly relate to both statements, C itself would not be a right value of not unless the two statements both imply (without being implied by) some other complement of exactly the statements that imply C. A rule of inference might provide for equality of sets of complements to imply equivalence, of course, in which case not would be self-inverse; however, such a rule is non-constructive.
For any right value, A, of not we have not(A) which is implied by exactly
those statements, C, for which C and A
is false; in particular, A and
not A
is false. Thus A is a complement of not(A); however, even when not(A)
is a right value of not, I have no guarantee that every complement of not(A)
does imply A. Still, every complement of not(A), including A, does indeed imply
not(not(A)). If C complements A and D complements not(A) then, as C implies
not(A), C and D
implies not(A) and D
which is false, so every
complement of A complements every complement of not(A); in particular, every
complement of A complements not(not(A)), when it exists. Now, any complement of
not(not(A)) complements every complement of not(A), notably including A, so the
complements of not(not(A)) are exactly the complements of A and we can infer
that, whenever A and not(A) are right values of not, so is not(not(A)), with
not(not(not(A))) = not(A). Thus not∘not is a projection; it relates each
left value to itself (and all statements equivalent to it; but possibly also to
some other right values). To summarise:
All statements are complements of any false statement; so not relates,
to each false statement, every statement that all statements imply. Now, a
statement that all statements imply is necessarily implied by the statement of
our rules of inference, hence true. It's possible there are true statements
that not all statements imply, unless of course our logical system has a rule of
inference (as discussed above) which makes all statements imply the statement of
our rules of inference (hence also all true statements). Even without such a
rule, the truths that every statement implies do, necessarily, all imply one
another, so are an equivalence class under inference; and not relates them to
the false statements. In a logical system wherein there are no statements
implied by all statements, not does not even have the false statements as right
values; such a logical system must lack the rule C implies (B implies
C)
.
Nothing actually prevents our logical system's rules of inference from
implying all statements, of course; in such a case, all statements imply one
another and our logical system isn't particularly interesting: both implies and
not relate all statements to each other. However, more usually, one tries to
pick rules of inference that only imply a limited set of statements, that strike
our intuitions as reasonable. In such a case, for any truth T that all
statements imply, i.e. any not(false) statement, each complement C of T implies
T, hence C = C and T
, which is false, hence C is false; so the
complements of T are all false and imply one another, so not(T) is false. If we
have truths that not all statements imply, however, we cannot be sure that all
their complements are false; if any of them aren't, for some such truth T, then
not(T) won't be false; they might even not be right values of T at all.
A logical system's rules may also specify some transformations of text that
turn each (to which the transformations are applicable) into a statement
that contradicts
the original; a rule of inference may then say that
every statement that implies both a statement and its contradiction in fact
implies all statements. For any statement A amenable to the tranformation, its
contradiction would then be one of the texts meaning not(A).
or
Just as we defined and
above, we can define or
: given a set S
of statements, intersect(: ({s}:implies|) ←s :S) is the all-relation on
statements that are implied by every member of S; when it is ({C}:implies|) for
some C, all such C are necessarily equivalent and implied by each member of S.
Thus bulk(or) relates statement C to set S of statements precisely if C implies
exactly those statement that every member of S does imply. There may be some
sets S for which there is no such C. We write bulk(or, {A, B}) as A or B
as usual.
When A implies B, A transitively also implies every statement that B
implies; so the statements that both A and B do imply are precisely the
statements that B implies, hence B = A or B
. Since every false statement
implies all statements, A or F
= A whenever F is false; and, when every
statement implies every true statement, A or T
= T whenever T is
true.
Given statements A, B that are left values of not, consider not(A) or
not(B)
, if it exists; we know it implies not(A) and implies not(B), hence it
complements A and complements B; furthermore, every statement that complements A
and complements B also implies it. Now, as it complements A, it complements
every statement that implies A, notably including (A and B); we can reach the
same conclusion also by observing that it complements B. So, as long as A
and B
also exists and is a right value of not, not(A) or not(B)
implies not(A and B). Now, not(A and B) is implied by exactly those statements
that complement (A and B), i.e. those statements C for which (A and B and C)
implies all statements. For each such C, (B and C) implies not(A) while (A and
C) implies not(B).
Written by Eddy.