As the main text of 'An approach...' is rather long and makes use of a notation
which will be strange to most readers, and will take quite a bit of getting used to, I have cooked up this
introductory example or 'prospectus' with the aim of enticing the unwary general reader into the main text. Some
of course will be unenticed  there is nothing I can do about that. I am only interested in the person who feels
that there could be something here that is worth looking into. To this person I tender my apologies that I cannot
explain the whole thing better, and make it easier to assimilate. I feel sure that sooner or later others will follow and
make a better job of it.
So let's jump in and see what we can do with a typical problem of predicate logic. This one is taken from the online text
'for all x: An Introduction to Formal Logic'
by P.D.Magnus, page 138. (You will also find relevant material on
pages 67 and 155.)
Problem
Suppose we are given the following (the premise):
There is someone who likes everyone that likes everyone that he or she likes
Prove that we may legitimately draw the following conclusion from the premise:
There is someone who likes him or herself.
Before embarking on our quest for a proof, let us clarify the premise. It is meant that there is someone (let's
call them A) who likes everyone that likes everyone that A likes. Otherwise, it is not quite clear
who the he or she is that is mentioned near the end of the statement.
Stage 1
Transcription of premise and conclusion into the notation of the conventional predicate calculus
As the premise
is somewhat convoluted, we break down the transcription into several stages.
(i) The statement
'y is someone who likes everyone that x likes'
may be rephrased as follows:
for all z, (x likes z) implies (y likes z)
which can be written in abbreviated formulaic form as
∀z ((xLz)→(yLz))
(ii) Building on this, the statement
if y is someone who likes everyone that x likes, then x likes y
may be transcribed as
(∀y (∀z((xLz)→(yLz)))) → xLy
(iii) Finally, the premise as a whole can be rephrased as
there exists an x, such that the statement in paragraph (ii) is true
leading to the formula
∃x ( ∀y ( ((∀z((xLz)→(yLz))) → xLy ) ) ).
(iv) The conclusion is relatively easy to transcribe:
∃x xLx
Stage 2
Transcription into the CLScalculus
(This stands for 'the calculus of Circles, Letters and Subscripts'.) We transcribe our formulae
using the following rules[1]:
 the twoplace predicate 'x likes y' or xLy is written as L_{xy} (in general: a subscripted uppercase letter).
 'A and B' or A∧B is written simply as AB
 'not A' or ¬A is written as A enclosed in a circle
 'A or B' or A∨B is written as
 'if A then B' or 'A implies B' or A→B is written as
By i and ii this means the same as 'not (A and notB)'
Alternatively, by i and iv, it means the same as 'either B or notA'
Following these prescriptions, (xLz)→(yLz) becomes
We deal with the quantifier ∀z by writing it beside the expression:
(∀z((xLz)→(yLz))) → xLy becomes
Again, we deal with the quantifiers ∃ and x.∀y by writing them beside the expression:
We write the dot between ∃x and ∀y to indicate that the quantifier ∀y
is 'inside' the ∃x; we're saying 'there exists an x such that for all y...'.
If they were the other way round, like so
∀y.∃x ...
the meaning would be different; it would be saying 'for all y there is an x such that...'
Stage 3
Get rid of the quantifiers [2]
We start at the outside of our expression and work inwards. The first quantifier we come across is ∃x. Our attitude is this.
We're told, there is an x such that blah blah. Well let's call that x (or one of those x's,
if there is more than one of them) x. Then we rewrite the expression, leaving out the ∃x and replacing each occurrence of
x by x, thus:
The outermost remaining quantifier is ∀y. We deal with it by leaving it as it is, for the time being.
Next outermost is ∀z. However, ∀z is not on the outside of our expression.
To get to the outside, it would have to cross a boundary.
Well, that's OK, except there is just one little extra rule that we haven't mentioned yet. When an ∀ crosses a boundary, it
becomes an ∃; and when an ∃ crosses a boundary, it becomes an ∀.
(You can see that this is perfectly reasonable, as follows. To say 'it is not the case that for all x, P is true of x' is the same
as saying 'there is an x such that P is not true of x'. Similarly, to say 'it is not the case that there exists an x such that P is true of x'
is the same as saying 'for all x, P is not true of x'.)
So now we have:
OK, now the quantifier ∃z is on the outside, saying there is a z such that blah blah; so why don't we just call
that z that does the trick, z ?
There's just one little snag: that particular z called z is allowed to depend on y.
'For each y, there is a z such that...' The point is, there doesn't have to be a universal z that does the trick for
every possible choice of y:
z can be tailored to y. We indicate this by writing z with a subscript y, thus:
z_{y}
We then proceed to rub out ∃z, and replace each occurrence of z in the expression by a subscripted, bold z:
Finally, we erase the ∀y. Any lowercase letter that has not been emboldened by this late stage
we assume to be a 'for all' type of letter.
The final result of Stage 3:
Stage 4
The Process of Deduction
The above expression transcribes our premise, 'There is someone (call them A) who likes everyone that likes everyone that A likes'.
Our task now is to draw inferences from it. The challenge is to do this not by thinking but by blindly calculating. In the calculation
we are allowed to transform
the premiseexpression according to certain rules. (Think of these as analogous to the rules of algebra
e.g. you can multiply top and bottom by the same thing.)
1. You can perform any of the allowed moves of the CircleandLetter Calculus (CLcalculus for short), treating any subscripted
uppercase letter (what we will call an 'atom' for short) just as if it were an ordinary letter
in the CLcalculus. To fully understand what this
means you will have to study the main part of
The Markable Mark. For now, we'll just say that any legal CLmove
can be built up by combining instances of the following six primitive moves, or replacements.
They are grouped into three pairs:

These moves are called 'wrap' and 'unwrap' respectively

These moves are called 'delete' and 'undelete' respectively

These moves are called 'copy' and 'uncopy' respectively
2. You can perform a new kind of move, exclusive to the CircleLetterandSubscript Calculus (CLScalculus)
called thetacopy. Given an expression, you can take any of its factors[3], make a copy of it in the space
beside the original expression, then subject this copy to
a substitution. Neglecting certain subtleties (which are covered in the main text of 'An approach...'),
a substitution fixes its attention on an unbold or still variable lowercase letter, which we
will call the replacee;
selects a replacement letter (which can be either another variable letter, or a bold letter, or a subscripted bold letter);
then goes through the factor replacing each occurrence of the replacee by the replacement. The result of doing two
substitutions in succession is also regarded as a substitution.
So let's have another look at our expression, but now bearing these possible moves in mind:
If we restrict attention to CLmoves there is nothing useful to be done because no two 'atoms' (i.e. subscripted uppercase
letters) are the same.
We need to get to work on the expression with thetacopy.
We note that there are no factors other than the whole expression, so the whole expression needs to be copied, then the copy
subjected to a substitution.
y is the only letter that is still variable (the others are 'fixed' i.e. bold)
so we select y as replacee.
As replacement we could choose anything; but as our aim is to cause some atoms to become identical,
the obvious choice is x. Replacing, in the copy, each occurrence of y by x, we obtain:
Two of the atoms in the second factor have indeed become identical. This second factor now has the form
(where A stands for L_{xzx}, B for L_{xx}). Now, it is a theorem of the CLcalculus that
in other words, any expression having the form of the expression on the left is equivalent to the void expression.
(The theorem may be proved by performing the moves uncopy, delete, unwrap in succession.)
So, substituting the void,
where the second equivalence is an application of 'unwrap'. Thus our whole initial expression (the premise) is equivalent
to
Now the second factor of the expression, namely, the atom L_{xx}, is a transcription of the statement
x likes him or herself.
Thus the premise by itself is equivalent  algebraically  to
the premise and x likes x.
Stage 5
Appeal to a General Theorem
We're nearly there, but we haven't yet got a proof that the conclusion follows logically
from the premise. For this we need to appeal to a general theorem that says that if two expressions
are algebraically equivalent (as defined by the CLS rules of equivalence) then they are
necessarily logically equivalent  meaning that one is true, in any particular set of circumstances,
if and only if the other is true.
Such a theorem exists (for this see the main text), but requires quite a lot of machinery to prove it.
For present purposes, we will take it as given.
Now, if the premise is logically equivalent to the premise and x likes x, then there
can be no circumstances in which the premise is
true but 'x likes x' is false. In other words, the statement 'x likes x' is implicated
in  or deducible from  the premise.
Finally, given that x likes x, the soughtfor conclusion ('there exists an a, such that a likes a') follows.
Now, you may well feel that all the above is a prime example of using a sledgehammer to crack a nut. To
which my reply is (i) you are quite right: general methods are indeed sledgehammers; however (ii) once
you have got the sledgehammer up and running, you can use it to crack any nut.
With a little
practice stages 1, 2 and 3 become automatic and the work of moments. Stage 4 can be trickier, but this is where
the real magic is: the reduction of 'reasoning' to 'calculation'. There are quite a few other wellestablished systems for
accomplishing this. My claim for the Laws of Form approach is simply that it is the most economical in symbols, and
therefore the most elegant, and ultimately the most beautiful.
If you want to know more, read on...
Notes
[1] For completeness, although we don't need it here, we should add that the zeroplace predication
'YES!!!' which is always true in all circumstances, is transcribed as the empty expression:
Thus the silence of the infinite spaces, rightly heard, connotes a resounding 'YES!!!'.
As a corollary, we note that the opposite predication 'no' (unconditional)
must be transcribed as an empty circle:
O
Nyet!
[2]Those familiar with predicate logic will recognize this as the process of
'Skolemization'.
[3]Factor: if an expression can be seen as arising out of the juxtaposition of subexpressions E,F,G... ,
in other words, can be seen as their 'product', then any of E,F,G... is a 'factor' of the whole expression.
Main text 'An Approach from Laws of Form to the Predicate Calculus'
Home page of The Markable Mark
Definition of the CLcalculus
© George BurnettStuart 2016
