rev. Sept 5, 2007
A calculus is a game--that is, a set of symbols together with a set of rules about the symbols. Let's say we make a calculus.
For this game, as for any other formal system, we will need some agreements on making rules. We'll review the main rules that are already in use for building formal systems, and then build a simple calculus using them.
Formal systems are built on the axiom principle. A small number of things said make up the foundation of the system. We call them axioms. No proof is required for axioms; they are just accepted for the sake of the game. If someone refuses to accept one of the axioms, he simply can't play the game.
Definitions are like axioms. That's because they too are accepted for the sake of the game, without proof.
In this presentation, we'll signal axioms with the phrase, "let's say ..." Definitions will often start with "let's say ..." or "let's call ..."
There are other things said which we call propositions. Propositions may be true or false. Proving a proposition in a formal system is just a matter of discovering a chain of reasoning that ultimately harks back all the way to axioms or definitions (maybe just one) of the system.
Some propositions will be of continuing importance as we proceed; these we call theorems. Before we have proven a theorem we might call it a conjecture. This is math-speak for "a really good guess which we hope we can prove."
Just two axioms and a few definitions are needed for building this calculus. First, there is the definition of a region-delimiting symbol, which we call a pancake here. Other authors have different names and ways of symbolizing it.Then, two axioms called primitives of the primary arithmetic, along with with some definitions for talking with precision about pancake arrangements, make it possible to do useful things with the region-delimiting symbol. The primitives are the first wands (EVglax and SSglax) we shall wave at pancake arrangements to make changes to them.
All other propositions in the game are required to be proven from these axioms and definitions. Those which are generally important to developing the game we'll call theorems. Some which are used in applying the game to problems we'll call algebraic identities, such as the blabber identity, which says "two identical appearances of an arrangement on a showdown plaza are interchangeable with just one of them standing on the same plaza:"
a a = a
The pancake's boundary may be marked by paired parentheses, which we think of together as one symbol.
We shall often say "plaza" instead of "showdown plaza" and mean the same. Everything a pancake contains is on its input plaza.
Let's call the region in which a pancake arrangement sits --the region outside the outermost pancakes of the arrangement, if any-- a showdown plaza as well, namely the unrepresented showdown plaza.
Let's call the plaza on which a pancake
directly sits --the region
it immediately occupies--
its ambient plaza.
Let's say that it is not legal for a
pancake to have more than one ambient plaza
in a given arrangement.
Here is an arrangement of three pancakes. One of them is inside another pancake, and one sits apparently empty:(( )) ( )
Here is a different arrangement of three pancakes. No one contains another; all are apparently empty:( ) ( ) ( )
An example (--there really is an example just below:)
The unrepresented showdown plaza above, with no pancakes indicated, is a legal pancake arrangement, called invisible symbol. This is due to the any number (possibly none) in PA1. In all of your math reading, be ready to suspect that "any number of" may well be saying "none" is a possibility.
Another example:
((( ) ( ) ( ))
(( ) ( ))
( )
(( )))
( )
In the arrangement above, just two of the pancakes are sitting directly on the unrepresented plaza. One has several visible arrangements inside it, and the other is seemingly empty. All the seemingly empty pancakes, however, have the invisible symbol arrangement inside them. This we shall prove later.
Same example, analyzed on separate lines:
( ) ( ) ( )
( ) ( )
( )
(
)
( )
( )
( )
(
) ( )
The exact nesting --what is inside what-- can be easier to see when an expression is presented on multiple lines, with inner pancakes appearing on higher lines. However, this is at least inconvenient and often a royal pain in most editing tools. Better to get used to reading pancake arrangements on a single line.
PA2)
Let's say every pancake of an arrangement
must have both its parens showing, not hidden under other
pancakes. That is, parens must always be paired.
Bad Example 1: An illegal pancake arrangement:
( ))))) ((( )
Let's call pancake arrangements which do not violate these two rules (PA1, PA2), legal arrangements.
Here is another pancake arrangement -- the Short Stack:
(( )) Short Stack
This is the easy way to find the invisible symbol: as a pancake arrangement on the outermost plaza.
But the invisible symbol is hiding elsewhere also, waiting to turn this rather boring arithmetic into an elegant, powerful algebra for logic. It is the "yin within the yang," always there, making life possible.
You'll see the outermost plaza's invisible symbol indicated indirectly, usually with as much blank space as can be managed, often following an "=" sign, perhaps followed by a semicolon or a comma. (Semicolons, commas, dots and such like are not part of this calculus.)
Watch for it. Will you be the first to see the invisible symbol? I seen it, I seen it! You seen it? I seen it!
Proof of the invisible symbol's everywhereness, however, will depend on an axiom called Short Stack Good Luck. I am introducing everywhereness prematurely so that you can become accustomed to seeing the invisible symbol on every plaza.
In related mathematics the word empty symbol
is used to denote some invisible symbol.
Here, however, we require the
word empty for a different purpose,
namely to talk about empty-looking pancakes,
which are visible.
"Ahhh! So you have 'Expressions' in your formal system! Well, now, Maestro, what do these 'Expressions' of yours express?"
Not much, directly. At this point we can only say a pancake expresses its own inside-outside boundary and the possibility of participating in arrangements or containing arrangements.
Soon, however, we will start interpreting expressions in our formal system as not, yes, no, true, false, and, or, valid, fallaceous, implies, depends, undecided, all, some, there is, there exists, and other concepts that have wide application in practical life, in thinking, and in other mathematics.
Other formal systems which are capable of being modeled in pancake calculus (certain logics such as classical syllogisms, Boolean B2 calculus, propositional calculus, predicate calculus), have richer symbol sets, making them more expressive.
When we get to know how pancake notation relates to those more directly expressive, richer notations, our expressions will express all that can be expressed in those notations. Then our payback begins, for calculation in this calculus is easier, quicker and more powerful than in the more expressive calculi. It even makes available a proof technique that goes beyond what the more expressive systems offer: imaginary truth values.
In short, we give up expressiveness for elegance.
In return we get algebraic power.
We intend to use this power in proofs, both
within pancake and in other areas of math.
Let's say that an "=" sign between expressions means they are interchangeable.
In Greek, "arithmee" are "numbers." What is a number, anyway, before someone says what it is?
Let's say that ( ) ( ) is interchangeable with ( ), that is,
( ) ( ) = ( )
We can put this axiom to use in practice --apply it, that is-- in either provoking or revoking sense. In provoking sense, we may read it thus:
Let's say it's good luck to find find a single vizzo, for then we may write another vizzo in the same plaza.1.8.1 Spells, Quasi-spells (definition)
Let us call the act of applying an axiom or definition in a proof, using a spell.Let us call the act of applying a principle not directly based on an axiom or definition in a proof, using a quasi-spell (rhymes with "Fozzy's Well").
1.8.2 provoco spell sense
If we prefer to wave a wand to apply the Extra Vizzo axiom in its provoking sense, we use the wand EVglax with the provoco spell ("I call forth," Latin).
I build EVglax wands from CPVC plumbing pipe, with an elbow at one end. It does the provoco spell when you touch the elbow to a vizzo.
1.8.3 revoco spell sense
In revoking sense, we can read the Extra Vizzo Good Luck axiom thus:
Let's say it's good luck to find find two vizzos in a plaza, for then we may make one of them disappear with the revoco spell ("I call back," Latin).You can use the wand EVglax for doing revoco spells by holding the elbow end and indicating a vizzo, ( ) with the other end. You must be careful, though! If the vizzo you indicate is not Extra in its ambient plaza, the spell backfires and makes you, the wandholder, disappear instead.
You are not forever lost if this happens. Since in disappearing, you become the Invisible Symbol, there is a counter-spell, coming up in the next section.If your wand-waving partner notices you are gone, she can make you appear again, as a Short Stack, wherever she chooses to see the Invisible Symbol --that is, if she can see Invisible Symbols.
Being a Short Stack is not so bad. You have to wear a double-decker "pancake" hat. Makes you look like a mutated mushroom. What else can you expect from thirty thousand genes?
By what has been said so far, would it always be possible to rid a plaza of all the empty-looking pancakes there by calling on the Extra Vizzo axiom in revoco spells?
(thinkety-think-think, thinkety-think-think, thinkety-think-think, ---)
No, not always. Consider an expression on
the unrepresented plaza such as
( )( )( )( )( )( )
, a given expression
Say we do the EVglax revoco spell
successively, one at a time, and track the
results:
( )( )( )( )( )( )
, the given expression
( )( )( )( )( )
, EVglax "Revoco!" spell
( )( )( )( )
, EVglax "Revoco!" spell
( )( )( )
, EVglax "Revoco!" spell
( )( )
, EVglax "Revoco!" spell
( )
, EVglax "Revoco!" spell
Once we have revoked
them down to a single empty-looking pancake
there is no longer an Extra Vizzo
(Lhs --left-hand side)
on the unrepresented plaza to point to
for a revoco spell.
1.8.4 cognosco quasi-spell
When your proof has progressed to where something is now obvious if only someone would look, you can invoke the cognosco quasi-spell. This saves you from saying things like "Guk' nur, Dummklotz," or "Ta' a wee look, ya grea' loomp! ha'e ye no been payin' attention?" or "Du-uhh!"
"By inspection" is another way to invoke the cognosco quasi-spell.
1.8.8 QED quasi-spell, []
If someone does not accept our proof, the best we can do is try another -- so says G.Spencer-Brown in Laws of Form.One way of helping people accept our proof is to present it in a traditional style. A reliable traditional style is the "rewrite at left, justification at right" style. Many proofs can be done almost completely in this style, with just a few opening and closing remarks.
Traditional final closings to a proof are:
Q.E.D. ("which was to be shown." --quod erat demonstrandum, Latin)
"This completes the proof."
a square block glyphHere, we use [] as our Q.E.D. quasi-spell.
When you see the QED quasi-spell, you might read it as "something is finally obvious if we know where to look, and it can't be too far away. Maybe it's two things that are identical."
1.8.8.2 nauseando spell
What kind of spell could you use to make someone seasick? Alright, Hermione, what is it? "A queasy spell!" "Ba-dump bump." That will do, Malfoy.
1.8.9 Proofs using EVglax
Here is a proposition that two expressions are interchangeable, and a proof by the Extra Vizzo Good Luck axiom. We present the proof in the traditional "rewrite and justification" style. We shall use Rhs and Lhs to say right-hand side and left-hand-side, referring to the respective sides of a given formal interchangeability proposition --a given Fi.
We are to show
( )( )( )( )( ) = ( )( ), a given Fi
Rhs = ( )( )( ) , EVglax "Provoco!" spell, ( )=( )( )( )( )( )( ), EVglax "Provoco!" spell
( )( )( )( )( ), EVglax "Provoco!" spell
identical to Lhs, "Cognosco!" quasi-spell
and so, perforce, interchangeable. []How is this a proof? It presents successive rewrites of the Lhs of the proposed formal interchangeability. At each rewrite it presents a note about why we can be sure that the rewritten expression is interchangeble with the one just above. The succession arrives at a situation where we can note that the rewritten Rhs is interchangeable with the Lhs by virtue of being identical to it.
We are to show
( ) ( )( )( )( ) = ( )( ), a given Fi
Lhs = ( )( )( )( ) , EVglax "Revoco!" spell( )( )( ) , EVglax "Revoco!" spell
( )( ) , EVglax "Revoco!" spell
identical to Rhs, "Cognosco!" quasi-spell
and so, perforce, interchangeable. []1.9 SSglax, the Short Stack Good Luck Axiom Wand
Let's say (( )) is interchangeable with the invisible symbol:
(( )) = ; SSglaxLet's call the arrangement consisting of a vizzo, ( ), together with a pancake that contains it as the sole visible content, a short stack: (( )).
Then we may give the revoking sense of this axiom thus:
Let's say it's good luck to find a Short Stack anywhere, for then we may eat both the pancakes of the Short Stack at a single gulp, simultaneously and without a trace. No fair eating one at a time. That could be confusing if we got distracted halfway through. Both together or not at all! Clean getaway! Revoco!(( )) = ; SSglax "Revoco!" spell
I make Short Stack Good Luck wands out of PVC plumbing pipe. At one end I affix a tee. This way, I can tell the wand SSglax from the wand EVglax in the dark. This is important for nighttime operations, since these wands have no "lux" spell for making light.
1.10 The Arithmetic Primitives (definition)
1.10.1 Primitives of the Pancake Arithmetic
Let's call the Short Stack Good Luck axiom, SSglax, a primitive of the pancake arithmetic.Let's call the Extra Vizzo Good Luck axiom, EVglax, a primitive of the pancake arithmetic.
Let SSglax and EVglax be the only primitives of the pancake arithmetic.
1.10.1.1 The Only Arithmetic Primitives
The arithmetic primitives are (and shall remain) the only ways of making arithmetic changes to a pancake expression. We'll be referring to them over and over in the further development, as you might guess from their having magic names.Later we'll note that Boolean B2 calculus (used heavily in digital circuit design) is built on a larger number of arithmetic primitives, making it more expressive than pancake calculus. In boolean you can say AND, OR, NOT, TRUE, FALSE directly.
However, boolean suffers for that expressiveness in being poorer in calculation resources (algebra) than pancake calculus.
The biggest weakness in boolean is the difficulty of disclosing irrelevant input variables, and irrelevant appearances of relevant variables. We will have several easy-to-use tools for these problems among the algebraic identities to come: outfect, blabber, red herring and occultation.
1.11 The Invisible Symbol is Everywhere (Theorem)
Everywhereness Theorem:
The invisible symbol is everywhere --that is, we may consider it present on any plaza we might choose in any expression whatsoever.We have not yet given a provoking-sense reading of SSglax, the arithmetic primitive that says
(( )) = ; SSglaxWhat would the provoco spell of SSglax say?
Let's say it's good luck to find the invisible symbol on a plaza, for it would let us make a short stack, (( )), appear on that plaza.It would be distressing to discover that not every plaza contains an invisible symbol. (How would we know when it failed to be there?) We had better be quite sure we can rely on it.
1.11.1 The Invisible Symbol is Everywhere (Proof)
Probeamus theorem igitur: Well then, let's prove this theorem now. If you don't accept this proof, you'll have to consider everywhereness an axiom instead, for it is central to the next big step in the axiomatic development of this calculus, where value and an operator come alive.
Everywhereness Theorem:The invisible symbol is everywhere --that is, we may consider it present on any plaza we might choose in any expression whatsoever.
To prove this, it is enough to show that acting as if it were so cannot lead to a contradiction of anything we have already said.
Since the theme of the arithmetic primitive axioms is interchangeability of pancake arrangements, the formal system's self-consistency is completely evidenced by whether any alteration of an expression is reversible under these axioms.
The only way to alter an expression in its appearance by relying on the everywhereness conjecture would be to invoke Short Stack Good Luck in its provoking sense somewhere in or about the expression, because SSglax alone among the interchangeability axioms and their sense readings presupposes the presence of the invisible symbol.
Procedure, Phase One
Say we choose an arbitrary plaza within or ambient to an arbitrary pancake arrangement. Say we consider the invisible symbol to be present there and provoke a short stack, (( )), from it by SSglax.
Observe that, since we did this on an arbitrary arrangement, this procedure fairly typifies the most drastic change that can be made to any arrangement by relying on the everywhereness conjecture, for an arrangement results which could be likewise altered by the same procedure.
But say we continue in this manner making just such drastic changes to the successive arrangements, recording the steps we take somehow so that we can later tell which was the last plaza altered at each step.
Procedure, Phase Two
Having proceeded thus, say we now revisit every altered plaza in reverse order to Phase One and repeatedly invoke SSglax but in revoking sense now, producing the invisible symbol from every new short stack provoked in Phase One.
It is evident that Phase One of the procedure above fairly typifies the most that can be done to alter the appearance of an arbitrary expression by acting on the everywhereness conjecture. It is also evident that Phase Two of the procedure specifies a sure way of restoring the expression to its original appearance.
This shows that using the everywhereness conjecture cannot lead to a contradiction of the formal system as developed thus far.
We conclude the invisible symbol is everywhere. []
1.13 Can you get There from Here?
1.13.1 Proofs with SSglax
We are to show
(( )) = (( )) (( )).
Lhs = (( )) (( )), SSglax "Provoco!" spell;
identical to Rhs, "Cognosco!" quasi-spell []
We are to show
(( )) = (( )) (( )).
Rhs = (( )), SSglax "Revoco!" spell;
identical to Lhs, "Cognosco!" quasi-spell []
We are to show
( ) (( )) = (( )) (( )) ( ).
Rhs = ( ), SSglax "Revoco!" spell twice;
Lhs = ( ), SSglax "Revoco!" spell once;
Lhs = Rhs, "Cognosco!" quasi-spell []
We are to show
(( (( ) (( )))) (( ))) = .
Lhs = (( (( ) )) (( ))) , SSglax "Revoco!" spell;(( (( ) )) ) , SSglax "Revoco!" spell;Lhs = Rhs, "Cognosco!" quasi-spell []
(( ) ) , SSglax "Revoco!" spell;
, SSglax "Revoco!" spell;
With the invisible symbol as your starting expression, can you specify a sequence of spells that ends with the expression consisting of just vizzo, ( ), the empty-looking pancake?
Another way of asking this is:
We are to prove that = ( ).
We are to prove that ( ) = .
But I won't show you how. This is extra credit for the suckup student who is trying to do this without thinking.
1.13.2.1 This can't actually be done. [* side-trip]: a note on why that's important, with thanks to a correspondent.
1.14.1.a ordinem ignoramus Experiment 1a
I choose as my seed expression,( )
I take the wand SSglax and do a provoco spell two times: first I touch the plaza within the empty-looking pancake, calling forth a short stack there:((( )))
I then do a second provoco spell, this time designating the unrepresented plaza.(( )) ((( )))Note that this is identical to the Lhs of the proposed formal interchangeability.
1.14.1.b ordinem ignoramus Experiment 1b
I choose again the same seed expression,( )
Once again I take the wand SSglax and do a provoco spell two times. As before, I touch the plaza within the empty-looking pancake first, calling forth a short stack there:((( )))
And once again I do a second provoco spell, designating the unrepresented plaza essentially as before. This time, however, I happen to do this to the right of the arrangement-in-progress:((( ))) (( ))Now note that this is identical to the Rhs of the proposed formal interchangeability.
Note that I did nothing arithmetically different in the two experiments. I chose the same plazas both times, carefully distinguishing, as the arithmetic axioms require, what is inside, and what is outside, each pancake. In other words, I did the same arithmetic both times. That means, there can be no arithmetic change in the Rhs as compared to the Lhs.
What, then? Have we proven anything? Have we made a new theorem? a new definition?
No. All we have done is demonstrate that the calculus we are building says nothing about the serial order of anything. Indeed, nothing to come will do so, either. We are through building the arithmetic, as we intended to say, above, with "let EVglax and SSglax be the only arithmetic primitives."
Let us entertain the objection that the serial order of the complementary components of the paren-style pancake is crucially important. For instance, the symbol ")(" would be illegal.
Okay, you got me there. But I point out that this is not of interest to the arithmetic axioms and how to use them, since they speak only of legally contructed pancakes. Once we are above the level of how to write a pancake, serial order is not of interest to the arithmetic, nor perforce of the algebra which we are shortly to build from it.
We have taken this trouble for the sake of having some official-sounding spell for those occasions, when doing some proof or other, when we want to do a rewrite of an expression to make it obvious it is interchangeable with another by showing it literally identical.
So we root around in our English-Latin dictionary for "we ignore" and find "ignoramus." We now have a wandless spell, dependent on no definitions, nor any axioms, for justifying a non-arithmetic rewrite --a rewrite, that is, where only the serial order changes: ordinem ignoramus!
Smile when you call me that, Pardner.
((( ) ( )) ( ) ( )) = .
Lhs = ((( )) ( ) ( )), EVglax "Revoco!"(( ) ( )), SSglax "Revoco!"identical to Rhs, "Cognosco!" []
(( )), EVglax "Revoco!"
, SSglax "Revoco!"
((( ) ( )) ( )) = .
Lhs = ( (( )) ( )) , EVglax "Revoco!"( ( )) , SSglax "Revoco!"identical to Rhs, "Cognosco!" []
, SSglax "Revoco!"
(( ) ( )) ( ) = ( ) (( ) ( )).
Lhs = ( ) (( ) ( )), "Ordinem ignoramus!"identical to Rhs, "Cognosco!" []
((( ) ( )) ( )) = (( ) (( ) ( ))).
Lhs = (( ) (( ) ( ))) , "Ordinem ignoramus!"
identical to Rhs, "Cognosco!" []
( ) (( (( ) ( )) ( ) )) = ( ).
Lhs = ( ) (( (( )) ( ) )) , EVglax "Revoco!"( ) (( ( ) )) , SSglax "Revoco!"identical to Rhs, "Cognosco!" []
( ) (( )( )) ((( ))) = (( )( )) ((( ))) ( ).
Lhs = Rhs , "Ordinem ignoramus!", "Cognosco!" []
( ) ( (( (( (( )) )) )) ) = ( ).
Lhs = ( ) ( ) , SSglax "Revoco!" 3 times( ) , EVglax "Revoco!"identical to Rhs, "Cognosco!" []