[Skip Navigation] [CSUSB] / [CNS] / [CSE] / [R J Botting] / [ MATHS ] / logic_11_Equality_etc
[Contents] [Source Text] || [Notation] || [Copyright] || [Contact] [Search ]
Tue Oct 11 11:03:22 PDT 2011

Contents


    Equality, Uniqueness, etc

      Introduction

      In MATHS equality has properties that are different to those proposed by logicians like Whitehead and Russell(1920s) or Kleene 1967. The logician's equality is a given property of given objects which is true when and only when the objects are identical. In MATHS identity is used in a meta-linguistic way. Each network of assumptions defines a set of objects and can redefine when they are to be considered equal. Equality in MATHS is more useful and looser relationship between expressions.

      In logic where expressions can be evaluated to expressions are equal when they have the same value. One can also argue that the natural values in a logic with equality are essentially the sets of equivalent elements under equality.

      In MATHS, as in an algebra, we get different types by assuming different forms of equality. Items are equal, not when they are identical but when we wish to confuse them! We are permitted to create new types of object by ignoring differences. For example the strings "1+2" and "2+1" are different but 1+2 and 2+1 are expressions of an numeric type and so will be assumed equal.

      When an axiom of the form

    1. for all x,y: T, if W(x,y) then x=y

      is added to the other axioms and variables that define a type, a new type is generated. The new type is called a quotient type and can be thought of as being a collection of sets of elements of the original type. The elements in the new set are treated as single objects however.

      Example


        An example of this is the construction of the rational numbers by
      1. Pairs::=$ following.
        Net
        1. numerator::Integer,
        2. denominator::Natural.

        (End of Net)

      2. Rational_Numbers::=Pairs / cross_ratio. [ logic_41_HomogenRelations#Equivalence Relations ]
      3. cross_ratio::=rel[x,y:Pairs](numerator(x)*denominator(y)=numerator(y)*denominator(x)).

        In MATHS we can write

      4. RATIONAL::=
        Net{
        1. Rational::=Pairs.
        2. For all x,y:Pairs, if (numerator(x)*denominator(y)=numerator(y)*denominator(x)) then x=y.
        3. ...

        }=::RATIONAL.
      5. Rational::= $ RATIONAL

      For each type of object a rule needs to be given specifying when two objects are to be assumed equal. In many ways the conditions under which two expressions are considered to be equal define the mathematical properties of a type. In may ways algebra is the study of the effect of various equalities - commutativity, associativity, cancellation and so on. In practice there are three distinct ways an equality is asserted: (1) By a simple definition of a new term,(2) As an axiom making certain simple expressions equal, and (3) By a recursive definition. Take these in turn:


        [1] A simple definition of a new term:
        	t ::= e
        or
        	t::T=e
        where e does not contain t and t is free prior to the definition.

        These definitions declare the term t and also add the axiom

        	t=e.

        Such a definition does not change the logic of the type very much because such terms can always be removed from any expression by substituting their expression. This does not constrain the type: if there were objects of the type without the definition then there will be similar objects existing afterward. These are essentially notational conveniences.

        Compare with [Jackson95c] where terms are attached to real world designations. The syntax of a definition is used in MATHS also to designate a term:

         	t::T=`string in some other language`.
        is semantically equivalent to
         	t::T.
        This is therefore a declaration of a new term and can not constrain the type.

        [2] An axiom making certain simple expressions equal:

         	For all .....  , e1=e2.
        The result is a different type of object called a quotient type because the the original objects are now divided up into class of equivalent objects that are treated as equal. [ logic_41_HomogenRelations#Equivalence Relations ]

        [3] By a recursive definition:

         		t ::= e
        or
         	t::T=e
        where e does contain t, or t has been used in an earlier definition. These add a new axiom:
         	t=e,
        These may or may not invalidate the type. It is wise to demonstrate that there is a set of objects that satisfy the axioms when there is a recursive definition in the axiom system.

      Mathematically such formulas look very like equations: Such equations can often be solved.
      1. For example:
      2. x = 2*x

        This equality is satisfied by exactly one value of x, x=0. So sometimes an axiom like this leads to defining a particular value for a term.

        However consider this equation:

      3. x = x^2+2*x

        This is satisfied by x=0 or x=-2, for example. This shows that a recursive definition may not define a unique value. We have an under-defined term.

        Considering:

      4. x = 2^x

        we are forced to realize that there is no value of x that satisfies some definitions. Here x is over-defined.

        All we can say when we know that x should satisfy some property P then one of these cases will hold:

        1. for no x(P)
        2. for one x(P)
        3. for 2..* x(P)


      Equality has attracted the attention of both computer scientists and software engineers. Here are some notes:

        Substituting one expression for an equal one is the heart of Gries approach to logic and programming[Gries 91, Gries & Schnieder 93). From this rules of symmetry, transitivity, ... can be deduced [Kalish & Montague 64].

        Substitution of equals does not always work inside character strings and quotations. It can also fail in statements involving beliefs, desires, and knowledge. The MATHS assumption (as in Cyc [Lenat et al 90]) is that such statements can be handled by placing the beliefs, knowledge, etc in a string. Just because two expressions have the same informal description we can not conclude that they are equal.

        Parnas has pointed out that when expressions in an equality contain partial functions then it is simplest to assume that the equality is false whenever either or both expressions are undefined[Parnas 93].

      Syntax

      The full syntax is integrated into the predicate calculus, see [ logic_10_PC_LPC.html#equality ] for the full syntax.

      For any two expressions x and y of the same type x=y and x<>y are predicates. Thus x=y and x<>y have type @ if and only if x and y have the same type.

    2. For T:Type, x,y:T, (x=y) ::@=x and y are defined and are identical.
    3. For T:Type, x,y:T, (x!=y) ::@= not(x=y).
    4. For T:Type, x,y:T, (x<>y) ::@= (x!=y).

      The "!=" notation comes from the C family of languages and has infected just about every programmer by now. The abbreviation representing inequality (<>), comes from BASIC and Pascal, but this should be shown (if possible) as the conventional mathematical symbol ≠ when a document is typeset or displayed.

      Equality and inequality are both parallel operators so expressions of form x = y = z, w = x = y = z, and so on are valid when x, y, and z are expressions of the same type. For example x = y = z means x=y and y=z.

      Semantics of equality

    5. For x,y:T, (x=y) ::= y can be substituted for x in all logical contexts.

      The exceptional non-logical contexts are: character strings, quotations, and statements involving beliefs, desires, and knowledge. These will not in general keep the same value when equals replace equals.

      Note that if x or y are expressions with free variables then one needs to be careful to not substitute one for the other in a context where the free variables are bound. The bound variables need to be changed to other variables. Similarly, if x is a variable then only free occurrences of it can be replaced in an expression by y.

      Equality is used via Euclid's Axiom - Equals can be substituted for equals:

    6. |- (euclid): For expressions x and y of type T, x=y iff for all e(x):expression_containing_x, e(x) = e(y)

      and

    7. |- (euclid): For expressions x and y of type T, x=y iff for all W(x):predicate_containing_x, W(x) iff W(y).

      Liebnitz's Axiom is similar: Two expressions are equal if and only if they remain equal when any and/all values of variables they are equal:

    8. |- (liebnitz): For variables x with type T1 and e1(x), e2(x):expression_containing_x of type T2, e1(x)=e2(x) iff for all x:T ( e1(x)=e2(x) ).

      So x+1 = 1+x in any traditional numeric type because 0+1=1=1+0, 1+1=1+1, 2+1=1+2, 3+1=1+3, ....

      Similarly for predicates, two predicates are equal exactly when they have the same truth value when the same values are substituted for the same variables in each predicate. The iff is the same as = between predicates.

      In [ maths/logic_25_Proofs.html ] the following rules are claimed to be derived from the above about equality



      1. (above)|- (eqid): for all e ( e=e ).
      2. (above)|- (eqcomm): for all e1,e2 ( (e1=e2) iff (e2=e1).
      3. (above)|- (eqtrans): if (e1=e2 and e2=e3) then e1=e3).

      Notice -- for this rules to be applicable then the expressions on both sides of the equals sign should define a single object, and they must be both of the same type. The chief risk is using the definite description operator ("the") when there is more than one object described.

      Uniqueness and Definite Descriptions

        These two techniques are vital for describing programs and data. For example we nearly always want aprogram to produce a particular output for the given inputs. The whole theory of normalized data depends on the concept of a key attribute... and each value of a key attribute defines at most one object.

        Expressing Uniqueness

        Recall that for a propert W(x) there can be no object x, one object x or many objects x.

        In MATHS use the quantifier one: (uniqueness): (for one x:X(W(x))) ::= for some x:X( W(x) and for all y:X(if W(y) then x=y)).

      1. one::quantifier="one". We can abbreviate "one" to the digit "1" if we wish.

        You can easily demonstrate results like the following:

      2. (above)|- (one_exists): if (for one x:X(W(x)) then for some x:X(W(x)).
      3. (above)|- (only_one): if (for one x:X(W(x)) then for all u,v:X (if W(u) and W(v) then u=v).
      4. (above)|- (one_eq): for all x:T, one y:T (x=y).

        Proving Uniqueness

        The following paterns are common when you need to prove that one and only one x satifies property W(x). First we can, conside the three possibilities and eliminate two of them
         	.Case for no x(W(x)).
         	...
         	Reduce to absurdity.
         	.Else x1,x2, W(x1), W(x2).
         	...
         	   x1=x2
         	.Else for one x(W(x)).
         	...
         	.Close.Case

        Another common form is when we can find an x that satisfies W(x) but need to establish that it is the only possible x. Here we might use this pattern:

         	.Let x2, W(x2).
         	...
         		x2=x.
         	.Close.Let

        Definite descriptions and articles

        If we know that there is only one object satisfying a property, then we can define the object that satisfies that property. We borrow the definite article symbol the from English:
         	the (object:Type || Property).
         	the (x:Real || 2*x = 1 ).

        A more writable alternative is:

         		the(object:Type . Property).

        The standard binding form is:

         		the[object:Type] (Property).
        which suggests using the with a subscript when type set.

        Note. Later we can also define,

      5. the [ x:T1, y:T2, ...] (W(x, y,...) = the [v:T1><T2><T3...] (W(v.1st, v.2nd,...)) and
      6. for all S:Sets, the S = the [x:S](true).

      7. For N:structure, S:@$ N, P:proposition(variables(N)), the N(P)::=the unique $(N) in S and satisfying P.

        Syntax of definite descriptions

        [ logic_10_PC_LPC.html#definite_description ]

      8. definite_description::= the variable ":" type "(" predicate ")" | the "(" variable ":" type "||" proposition")" | the "[" loose_bindings"]" "(" predicate")" | the set_expression | the structure "(" proposition")".

      9. the::lexeme= "the", see definite_description. In handwriting I use an upside down capital "T".

        Derivation Rules for definite descriptions

        You have to be careful with definite descriptions when they do not describe a unique item.
      10. the(x:X||W(x)) exists if and only if
      11. for one x:X (W(x)).

        The Wikipedia [ Definite_description ] has an introduction to Russell's approach to this.

        In normal MATHS, derivation rules that work on "the" all require uniqueness.

      12. |- (the1): if for one x:X (W(x)) then the(x:X||W(x)) is in X.
      13. |- (the2): if for one x:X (W(x)) then W( the(x:X||W(x) )).
      14. (the2, only_one)|- (the3): if for one x:X (W(x)) then for all y:X (if W(y) then the(x:X||W(x) ) = y).

        However, the rules for equality can be used, [ Proving Uniqueness ] abov.

        Undefined Definite Descriptions

          Occasionally we need the idea of `the x satisfying P, iff its unique, else some other value`
        1. For W:@^T, a:T, the(z:T||W(z)||a)=if(for one (z:T||W(z)),the(z:T||W(z)),a).

          Kalish and Montague go further and effectively introduce the idea that all non-unique descriptions define the same value the(x:X || false). This is reminiscent of the null pointer in many languages and the Smalltalk Class of Undefined Objects. This lets them derive three useful inference rules:

        2. You can change all occurrence of a bound variable to a different (unused) one.
        3. If two predicates are equivalent then one can be substituted for the other.
        4. If two expressions are equal then one can be substituted for the other.

          However MATHS takes these inferences for granted. Now we can show that, if no object of the relevant set(X say) fits the definition then, the description formula is equal to the(x:X || x<>x):

        5. |-if for no x:X(W(x)) then the(x:X|| W(x) ) = the(x:X || false).
          Let

          1. |- (1): for no x:X(W(x)),
          2. (1)|- (2): for all x:X(not W(x)),
          3. (2)|- (3): for all x (W(x) iff false),
          4. (subs iff):|-(4) the(x:X|| W(x) ) = the(x:X || x<>x).

          (Close Let )
          However if two or more objects can fit a property W then it is not obvious that the(x:X||W(x))=the(x:X||W(x)).

          At this time ( Tue Oct 11 10:59:10 PDT 2011 ) MATHS still treats definite descriptions as syntactically correct expressions even if uniqueness has not been proven.

          But before they can be used in arguments uniqueness must be established. For example, (inspired by [BergmanMoorNelson90] and presuming a net of definitions for Roman Empire )
          Let


          1. |- (RH): ROMAN_HISTORY.
          2. (RH)|-cesar, pompey in Roman_generals,
          3. (RH)|-cesar = the( r: Roman_generals. r conquered_gaul ).
          4. (RH)|-the( r: Roman_general. r conquered_gaul ) defeated pompey.
          5. (RH)|-for one r: Roman_generals ( r conquered_gaul )
          6. (-1, -2, -3, euclid)|-cesar defeated pompey.

          (Close Let )

          I recall a paradox in Euclidean Geometry that depends on a particular construction defining a point ... when in fact it can not do so.... thus MATHS does not allow algebra on undefined or over-defined objects.

          Further a recent "proof", discovered by a computer [ http://mally.stanford.edu/cm/ontological-argument/ ] (refered to by [Krakovsky11] ) clearly breaches these rules... and, further, will also prove some clearly false results, for example that the numbers have a unique largest number, or that this graph has a single node that has no other node coming from it [Kuratowski(3,3) has 3 maxima and 3 minima]

          Dana Scott's Domains are sets of objects which are more or less defined and contain both an undefined object (⊥) and the overdefined object(top) - one that can not exist because its specification is contradictory [ACM87]. So we do not assume this as an axiom but name the proposition encoding the inference as "Improper descriptions".

        6. Improper_descriptions::@. Improper_descriptions iff if for no x:X, some y:X (W(x) iff x=y ) then the(x:X|| W(x) ) = the(x:X || false).

          If you want impropper descriptions in your logic, you must link to the definition above and then assert it -- as an assumption.

          Top and Bottom

          Taking this a step further, we can associate with each type a domain - this has, in addition to the usual values, two extra ones - the undefined value(bottom) and the over-defined value(top) with the following properties
        7. DOMAIN::=following,
          Net
          1. bot::T.
          2. ::T=bot. A common symbol for the bottom of a lattice.

          3. top::T. The ΤΕΧ upside down ⊥ does not render in HTML.

          4. For all W:predicate, if for 0 x(W(x)) then the(x:X||W(x))=top.
          5. For all W:predicate, if for 1 x(W(x)) then W(the(x:X||W(x)).
          6. For all W:predicate, if for 1 x(W(x)) then for all y(if W(y) then y=the(x:X||W(x)).
          7. For all W:predicate, if for (2..) x(W(x)) then the(x:X||W(x))=⊥.

          (End of Net)

          If you need these formulas then you must link to DOMAIN and assert it in your document.

        If-then-else

        This is used a lot in functional programming. It dates back to LISP.
         		if( even n, n/2, 3*n+1)


      15. (above)|- (ite1): For all p:@, x:T, y:T, one z:T, (if p then z=x else z=y).
      16. For p:@, x:T, y:T, if(p,x,y)::= the(z:T||if p then z=x else z=y).
      17. (above)|- (ite2): For p:@, x:T, y:T, if p then if(p,x,y)= x.
      18. (above)|- (ite3): For p:@, x:T, y:T, if p then if(p,x,y)= y.

        Cans of Worms

        Adding definite descriptions into a logic opens a can of worms. We have the problem of handling expressions that have no valid value or no defined value. For example: mathematicians regularly solve equations under the assumption that a solution exists. But the value they find is only a solution if there is a solution - see section 7 below. Kalish and Montague assume that if there is no unique x that satisfies W(x) then
      19. the(x:T||W(x)) = the(x:T|| x<>x). Parnas argues out that this is not just a theoretical problem but one that arises in software specifications:
      20. For all Real x, sqrt(abs(x))=if(x>=0, sqrt(x), sqrt(-x)),

        but y'=sqrt(x) or y'=sqrt(-x) in normal logic is undefined because one part is undefined.

        This question has also been debated on Usenet: comp.specification.z

        Mathematicians assumed that there was an "imaginary" sqrt(-1) and developed complex numbers. LISP, Algol 60, C, Smalltalk, etc all delay the evaluation of all the arguments in condition expressions until after the condition is evaluated. Dijkstra introduces a special operator cand that is the logical equivalent of Ada's short circuited "and then" or UNIX's "&&".

        Parnas notes that in software engineering it is simpler to assume that certain primitive predicates (like equality) are false when their parts are undefined[Parnas93]. In MATHS the predicate e1=e2 is assumed false if either e1 or e2 are undefined. This is quite different to Kalish and Montague's assumption, but is, apparently consistent[Parnas 93]. We can say that '=' is Parnasian predicate. It follows that e1<>e2 must be true if either e1 or e2 are undefined. We might call this an anti-Parnasian predicate.
        Net

          Parnas gives the general rules but does not specify what the primitive predicates would be in practice. So if "=" and "<>" are taken as primitive then both are true if they applied to an undefined term. Thus we could no longer assume that for all terms x and y:
        1. x=y iff not(x<>y).

          Parnas does not discuss the question of whether a recursive definition of a predicate creates a primitive or non-primitive predicate. This may be because recursion opens the question of predicates being undefined -- something that Parnas is trying to avoid.


        (End of Net)

        Adding '=' to a logic opens another can of theoretical worms if we then ask which universes of discourse fit the logic - the different semantic models of the logic. The work on Universal Algebra and Category Theory shows that there are several ways to define these models[Wechler 92, Cramer et al 94]. In the strictest of these (initial semantics) all the models are similar except for relabeling the objects systematically - here two objects in the universe are taken to be equal if and only if they can be proved equal in the logic. The loosest form - final or terminal semantics - two objects can be the same(confused) unless they can be proved different. In practice these distinctions don't seem to be particularly important.

      . . . . . . . . . ( end of section Uniqueness and Definite Descriptions) <<Contents | End>>

    . . . . . . . . . ( end of section Equality, Uniqueness, etc) <<Contents | End>>

    Numerical quantifiers

  1. An example is for all x, 2 y(y^2=x). To define these completely we have to use both set and number theory - which comes later - Maths.Numbers.

  2. For n:Nat0, for n x:X(W(x)) ::= if n=0 then for no x:X(W(x)) else if n=1 then for one x:X(W(x)) else for some x:X( W(x) and for (n-1) y:T( W(y) and not x=y) ).


  3. |-for 1 x:X(W(x)) iff for some x:X(W(x)) and for 0..1 x:X(W(x)).

  4. For N:@Nat0,x,X,W, (for N x:X(W)) ::= (|{x:X||W}| in N).

  5. For n:Nat0, (..n) ::= { i:Nat0 || i<=n},
  6. For n:Nat0, n..::= { i || i >=n}
  7. For n,m:Nat0, n..m::= n.. & ..m.

  8. any::quantifiers= Nat0. This is used mainly in quantifying relationships - for example X(any)-(1)Y says that for each X there is one Y but there can be any number of X's (including none) for a given y.


  9. |-for 0..1 x:X(W(x)) iff for all x,y(if W(x) and W(y) then x=y).


  10. |-not for 0..1 x:X(W(x)) iff for all x,y (W(x) and W(y) not x=y).


  11. |-for ..n-1 x:X(W) = not for n.. x:X(W).


  12. |-for n+1.. x:X(W) = not for ..n x:X(W).

  13. For A: Finite(T),..., (for most a:A(W(a)) ) ::= |{ a:A||W(a)}| > 0.5 * |A|,
  14. For A, (for (p%) a:A(W(a)) ) ::= |{ a:A||W(a)}|*100=|A|*p.

    Advanced Quantifiers

  15. abf::= all but a finite number of.
  16. finite::=only a finite number of, well defined on natural numbers.
  17. infinite::=infinite number of, well defined on netural numbers.

  18. For a:variables, W:integer_proposition, for abf a(W(a))=for some n:Nat0, all m:Nat0( if m>n then W(m)).
  19. For a:variables, W:integer_proposition, for finite a(W(a))=for some n:Nat0, all m:Nat0( if m>n then not W(m)).
  20. For a:variables, W:integer_proposition, for infinite a(W(a))=for all n:Nat0, ssome m:Nat0( m>n and W(m)).

    In general, For T:Types,... (for abf x:T(W(x)) ) ::= {x:T||not W(x)} in finite(T).

  21. generic::=in the general case excluding a highly unlikely class of special cases. This is rather an advanced idea and only has meaning when the type of the variable is some kind of continuum or space, and the excluded cases form a continuum or space of lower dimension or of measure zero.

    Do not confuse this the idea of generic properties that apply to any type of objects.

  22. For T:Type, m:measure(T), W:predicate(T), (for generic x:T(W(x)) ) ::= m({x:T||not W(x)} = 0.
  23. For T:Type, dim:@T->Nat0, if T in space(dim=>dim(T)) then W:predicate(T), (for generic x:T(W(x)) ) ::= dim{x:T|| not W(x)} < dim(T).

    For example, in normal 3D space, two 2D objects generically intersect in a 1D object. The chances of the just touching is mathematically 0. Or, generically two lines are never parallel, ...

    Either_or

    The following are useful abbreviations for documenting systems that have internal classifications:
  24. PET1::=Net{ ... Either cat, dog, gopher, or peculiar. ... }.

  25. For A,B:identifier, Either A or B::=Net{ A,B:@. one(A,B). },
  26. For A,B,C:identifier, Either A, B, or C::=Net{ A,B,C:@. one(A, B, C). },
  27. For A:L(identifier), B:identifier, Either A, or B::=Net{ A,B:@. one(A,B). }.

  28. For P, Q:@, one(P,Q)::@=P iff not Q,
  29. For P, Q, R:@, one(P,Q,R)::@=if not P then one(Q,R) else not P and not Q,
  30. For P:#@, one(P)::=if not 1st(P) then one(rest(P)) else no(rest(P)),
  31. For P:#@, no(P) ::=not 1st(P) and no(rest(P)), no()::=true,
  32. For p:#@, two(p)::=if 1st(p) then one(rest(p) else two(rest(p)).

  33. For p:#@, n:Nat0, (n)(p) ::= if 1st(p) then (n-1)(rest(p)) else (n)(rest(p)).

    Existence Dependency

    Partly Baked Idea!

    Here is an abbreviation that may be useful for discovering databases and class hierarchies and ontologies. Suppose that we have a predicate F on type X and predicate G on objects of type Y then define:

  34. F >-> G::@=for all x:X(if F(x) then for 1 y:Y( G(y))). The idea is that a good data base design can be based on the predicates describing the situation/state of the world and connected by the existence dependencies. These lead to the functional dependencies used in data base normalization etc.

    Notes on MATHS Notation

    Special characters are defined in [ intro_characters.html ] that also outlines the syntax of expressions and a document.

    Proofs follow a natural deduction style that start with assumptions ("Let") and continue to a consequence ("Close Let") and then discard the assumptions and deduce a conclusion. Look here [ Block Structure in logic_25_Proofs ] for more on the structure and rules.

    The notation also allows you to create a new network of variables and constraints. A "Net" has a number of variables (including none) and a number of properties (including none) that connect variables. You can give them a name and then reuse them. The schema, formal system, or an elementary piece of documentation starts with "Net" and finishes "End of Net". For more, see [ notn_13_Docn_Syntax.html ] for these ways of defining and reusing pieces of logic and algebra in your documents. A quick example: a circle might be described by Net{radius:Positive Real, center:Point, area:=π*radius^2, ...}.

    For a complete listing of pages in this part of my site by topic see [ home.html ]

    Notes on the Underlying Logic of MATHS

    The notation used here is a formal language with syntax and a semantics described using traditional formal logic [ logic_0_Intro.html ] plus sets, functions, relations, and other mathematical extensions.

    For a more rigorous description of the standard notations see

  35. STANDARD::= See http://www.csci.csusb.edu/dick/maths/math_11_STANDARD.html

    Glossary

  36. above::reason="I'm too lazy to work out which of the above statements I need here", often the last 3 or 4 statements. The previous and previous but one statments are shown as (-1) and (-2).
  37. given::reason="I've been told that...", used to describe a problem.
  38. given::variable="I'll be given a value or object like this...", used to describe a problem.
  39. goal::theorem="The result I'm trying to prove right now".
  40. goal::variable="The value or object I'm trying to find or construct".
  41. let::reason="For the sake of argument let...", introduces a temporary hypothesis that survives until the end of the surrounding "Let...Close.Let" block or Case.
  42. hyp::reason="I assumed this in my last Let/Case/Po/...".
  43. QED::conclusion="Quite Easily Done" or "Quod Erat Demonstrandum", indicates that you have proved what you wanted to prove.
  44. QEF::conclusion="Quite Easily Faked", -- indicate that you have proved that the object you constructed fitted the goal you were given.
  45. RAA::conclusion="Reducto Ad Absurdum". This allows you to discard the last assumption (let) that you introduced.

End