[Skip Navigation] [CSUSB] / [CNS] / [CSE] / [R J Botting] / [ MATHS ] / logic_10_PC_LPC
[Contents] [Source Text] || [Notation] || [Copyright] || [Contact] [Search ]
Tue Oct 11 10:33:38 PDT 2011


    Lower Predicate Calculus

      The lower predicate calculus (LPC) with equality is a standard logic that can be applied to a wide range of situations where we have objects or individuals to talk about.

      Michael Jackson argues strongly that LPC is clearest language for stating and clarifying:

      For an extended and readable discussion see [Jackson95] and the following references Jackson.*9

      In MATHS (the logic I developed to help get programs that work well) we describe LPC in terms of a generic type of object. We assume that the rules can then be used any type of object at all. Further we identify the type with the set of all objects of that type (a universe of discourse). To put this another way - a type is a collection of things to which LPC with equality applies.

      In practice, there is evidence that it pays to divide up the universe of discourse into objects of different types. This idea needs further work but fits with the simple model proposed here if we assume a set of predicates setting up the ontology of the domain or universe of discourse. For example we may want to distinguish animals from rocks for example, or numbers from teachers.

      In essence, MATHS can talk about an infinite array of different universes. A natural name would be a multiverse perhaps. Each universe has its own type of object, its own axioms, formulae, theorems etc. This includes objects with complex internal structures like lists and sets. MATHS dare not talk about all of these without getting into paradoxes. But it assumes the
      (principle_of_genericity): The lower predicate calculus with equality is a generic logic that applies to all types of objects.

      In other parts of the MATHS system we make the assumption that the collection of all subsets of a type will have a similar logic. We assume that structured objects will be a type to which LPC will apply. We assume that certain families of functions and relations form a types.

      The logic is based on expressing the properties of individuals of a given type. We use the term predicate for a property -- the term ultimately comes from natural language grammar and Greek philosophy. An example might be the classic argument:

      1. All humans are Mortal.
      2. Socrates is a human.
      3. Therefore:
      4. Socrates is mortal.

      In the MATHS notation and assuming a domain of discourse or type symbolized by Being, then LPC is input like this:
       	|- for x:Beings, if human (x) then mortal(x).
       	|- human(socrates).
      It is rendered to look like this:
         	|- for x:Beings, if human (x) then mortal(x).
         	|- human(socrates).

      Lewis Carroll gives us an example of a plausible but wrong argument:

      1. Alice saw nobody on the road.
      2. The mad hatter arrived before nobody did.
      3. Therefore
      4. Nobody is slower than the mad hatter.

      In LPC the error is exposed:
      1. for no x:Beings ( saw(alice, x) ).
      2. for no x:Beings ( before(the_mad_hatter, x) ).
      3. slower(nobody, the_mad_hatter)

      Statements involving people's knowledge and desires (optative logic) do not always follow the generic LPC rules. They may look like predicates, but they fail to follow the rules that predicates follow. People commonly assert both that I want A(x) for all x and also `I don't want A(a)' . Logic texts use Hamlet killing Polonius as an example. In software engineering this means that a statement of requirements (What the user wants") is likely to contain inconsistencies which must be detected and removed.

      Propositions are statements that are either true or false. Propositions have type @ (In script a curly P or the ΤΕΧ \pw symbol). Predicates map elements of various types into propositions. The are constructed using "and", "or", "not", "if_then_" and so on. These are the operators in the propositional calculus or PC. Phrases like "for all", "for one", "for some", "for no" etc are also used. These are quantifiers in the LPC. A typical logical text will provide one quantifier. MATHS has a great many more.

      Identity and equality are two fundamental binary relations which relate expressions of a given type. Identity (==) means that the two expressions are identical in everything except their lexical layout. Identity should be treated as a meta-linguistic idea... used for discussing the logic of the type, rather than used inside the type itself.

      Equality (=) is an equivalence relation that holds between two elements that can be, for this logical system, treated the same way. Two expressions of a given type are equal if and only if one can be substituted for each other, in all circumstances, without changing the meaning of the result. Each type has it's own equality relationship. It in many ways defines the properties of the type.

      After this see [ logic_11_Equality_etc.html ] or return to the introduction: [ logic_0_Intro.html ] or list of logical items [ home.html#Logic ]


    1. |- (basis): PROPOSITIONS.
    2. |-LPC.

    3. PROPOSITIONS::=following,
      1. simple_proposition::@#lexemes, given.
      2. formula_in_a_different_language::@#char, given.
      3. proposition::= equivalences |implication,
      4. equivalences::= implication #( "iff" implication),
      5. implication::= disjunction |"if" proposition "then" disjunction O("else" implication)|clausal_form,
      6. clausal_form::=disjunction ":-" conjunction | conjunction "-:" disjunction,
      7. |- (dis_syn): SERIAL(disjunction, conjunction, "or", or, @),
      8. ()|-disjunction = conjunction #("or" conjunction)
      9. |- (con_syn): SERIAL(conjunction, elementary_proposition, "and", and, @),
      10. ()|-conjunction = elementary_proposition #("or" elementary_proposition)
      11. elementary_proposition::= O("not")( "(" proposition ")" | simple_proposition | formula_in_a_different_language),

      (End of Net)

    4. PC::=Propositional_Calculus.
    5. Propositional_calculus::= PROPOSITIONS( simple_proposition= propositional_variable, formula_in_a_different_language=>{}).

    6. LPC::=Lower_Predicate_Calculus_with_equality.
    7. Lower_Predicate_Calculus_with_equality::=following,

      1. |- (LPC1): PROPOSITIONS(simple_proposition=>predicate).

      2. predicate::= propositional_function | equality | parallel_form | set_theoretical_proposition | relational_proposition | quantified_proposition |...,

      3. propositional_function::= expression(@) | natural_predicate | formula_in_a_different_language,

      4. natural_predicate::=#(word_in_dictionary | expression) & fits_template.

      5. equality::= expression "=" expression #("=" expression) & correct_types, Equality is only defined between objects of the same type:
      6. correct_types::= |[T:Types] (expression(T) "=" expression(T) #("=" expression(T))).
      7. |- (LPC2): PARALLEL(expression,"=").


        The alternative of defining x=y to be false unless they have the same type leads to a paradox:
      8. PARADOX::=

        1. |-For T1,T2:Types, x:T1, y:T2, if T1<>T2 then (x=y)=false.
        2. T1,T2:Types, t:T1,
        3. |-T1<>T2.
        4. F::@^T2=not((_)=t).
        5. G::@^T1=not((_)=t).
        6. F has type @^T2 and G type @^T1 and so not(F=G) and yet they have the same expression.
        7. (F)|-For all x:T2 ( F(x) ).
        8. (G)|-For all x:T1( G(x) iff x<>t ).


      9. parallel_form::= (expression relation expression #(relation expression) ) & correct_typed_relations,

      10. |-For e:#(relation expression), R, S:relation, x, y:expression, x R y S e in correct_typed_relations iff x in dom(R) and y in cod(R)=dom(S) and e in cod(S),
      11. |-For e:#(relation expression), R, S:relation, x, y:expression, if x R y S e in correct_typed_relation then x R y S e = (x R y) and (y S e).

      12. quantified_proposition::= ("for"|"For") quantified_variable #( "," quantified_variable) ( "(" proposition ")" | implication ).

      13. quantified_variable::= quantifier binding, [ notn_12_Expressions.html#binding ]

      14. quantifier::= ((|"all") |"some" |"no" |"one" | number |set_of_numbers |"abf" |"most" | "(" expression "%)" | "generic" ,

      15. number::= digit #digit | "("expression(Nat0)")",

      16. set_of_numbers::= "("expression(@Nat0)")" |number ".." | ".." number |number"..*" | "*.." number | number".."number | "any",

      17. definite_description::= "the" set_expression | "the" structured_class_name "(" ( expression(@) | L(key_component"=>"value") ")" |"the" "(" loose_binding "||" proposition")"|"the" loose_binding "(" proposition")".

      18. loose_biding::= See http://cse.csusb.edu/dick/maths/notn_12_Expressions.html#loose_binding.

        More on equality quantifiers descriptions

        [ logic_11_Equality_etc.html ]


      19. all::lexeme= "all", universal quantifier.
      20. some::lexeme= "some", existential quantifier.
      21. no::lexeme= "no", negative universal quantifier.
      22. one::lexeme= "one", unique quantifier.
      23. most::lexeme= "most", mathematical quantifier.
      24. generic::lexeme= "generic", mathematical quantifier.
      25. the::lexeme= "the", definite article, only used when a unique object fits.

      (End of Net)


      The following are meta-linguistic ideas. They are used, privately, to discuss the properties of equality:
    8. META_LPC::= LPC with (predicate:=definition(predicate) | identity, identity ::= expression "==" expression).


    9. |-LPC. Propositions have two possible meanings - true and false. The following tables summarizes how these values combine with respect to the operators of 'not' 'and', 'or' 'iff' 'if__then_'.

       P               true            false
       not P           false           true
       P               true    true    false   false
       Q               true    false   true    false
       P and Q         true    false   false   false
       P or Q          true    true    true    false
       P iff Q         true    false   false   true
       if P then Q     true    false   true    false
    10. (above)|-(@,or,false,and,true,not) in Boolean_algebra.

      Equivalences are PARALLEL operators,

    11. (above) |- P iff Q iff R ...::= (P iff Q) and (Q iff R) and...

    12. |-(if P then Q else R) = (if P then Q) and (if not P then R)

    13. (previous, boolean algebra)|-if P then Q else R = (P and Q) or ((not P) and R).

      The clausal_form P:-Q is used in Prolog and some other systems:

    14. For P:disjunction, Q:conjunction, (P:-Q) ::= if Q then P.

      For the lazy, Q-:P can be used for if Q then P as well. If an arrow is available then write (P->Q) but beware confusion with the notation for maps between two sets: (A->B).

      Equality of propositions

    15. LPCe::= See http://cse.csusb.edu/dick/maths/logic_11_Equality_etc.html
    16. (LPCe)|-if (P=Q) then (P iff Q).

    17. |- (PC_equal): if (P iff Q) then (P=Q).

    18. (-1)|-(P iff Q) iff (P=Q).
    19. (-1)|-(P iff Q) = (P=Q).
    20. So equivalent propositions can be substituted for each other. (This rule is listed separately in the section on proofs).

      Further, Since '<>' indicates the negation of '=' (in LPCe) it follows that

    21. (-1, LPCe)|-(P<>Q) = not(P iff Q).

      Since many call this the "exclusive or" operator we can define

    22. P xor Q::@= (P<>Q).

      Summary of Logical operators

      PQP=QP<>QP and QP or Q

      (Close Table)


      Informally a predicate is a proposition with zero or more variables in it. These variables can be be of different types. To be able to determine whether or not a predicate is true or false all its variables must be given values. Associated with any predicate is function of type @^(T1><T2><T3...T[n]) and so a set of n-tpls. Some predicates remain true for all values of a variable, others are true for only one value, some are true for at least one value some are true for no value. This leads to the theory of quantification - "for all", "for one", "for some", "for no", etc..

      Two predicates are equal when one can be written for the other in any context. This would hold when they have the same free variables and if they are true when the same values are substituted for their variables.

      Notation for a Predicate

      MATHS allows prefix, postfix and infix (Loglan like) notations:
       		x older y

    23. For all e:L(expression), F:propositional_function, F(e) = (e).F = e1 F (e2,e3,e4,...).

      It would be nice to allow more complex and natural syntax:

       		`RJBotting` has degree `Ph.D.` from `Brunel University`
      in place of
       		`RJBotting` has_degree_from( `Ph.D.` ,`Brunel University`)
      See [ Natural, distfix, or mixfix predicates ] below.

      Definitions of Quantifiers

        All, some, and none

      1. For X:Sets, x:variables, W: predicates, (for all x:X(W)) ::predicates= For all x of type X , W is true.

        We can define for all as applying and:

      2. For X:Sets, x:variables, W: predicates, (for all x:X(W))= and[x:X](W).

        We define no and some in terms of all

      3. For X, x, W, (for no x:X(W)) ::= for all x:X(not W).

      4. For X, x, W, (for some x:X(W)) ::= not for no x:X(W).

        Notation for TeXies

        The following can also be used:
        not not
        if p then qp → q
        for all
        for some

        (Close Table)

        Abbreviated forms

        We can omit all:
      5. For X, x, W, (for x:X(W)) ::= for all x:X(W).

        We can run a series of quantifiers together:

         		for all x, some y, no z(F(x,y,z)) = for all x(for some y(for no z(F(x,y,z)))).
      6. For Q1,Q2:quantifiers, x, x1, x2:variables, W: propositions, (for Q1 x1:X1, Q2 x2:X2(W)) ::= for Q1 x1:X1(for Q2 x2:X2(W)).

      7. For Q1,Q2, x, x1, x2:, W, (for Q1 x1:X1, x2:X2(W)) ::= for Q1 x1:X1, Q1 x2:X2(W).

      8. For Q1,Q2, x, x1, x2:, W, (for Q1 x1, x2:X1(W)) ::= for Q1 x1:X1, x2:X1(W).

        Here are a couple of classic quantified (and abbreviated) propositions taken from automata theory:

        1. Pumping lemma examples for quantifiers
        2. For all Regular L, some n, all w:L, if |w| >=n then for some x, y, z(w=x y z and y<>"" and |x y| <=n and for all k:0..* (x y^k z in L))
        3. For all CFL L, some n, all z:L, if |z| >=n then for some u, v, w, x, y (z=u v w x y and v x<>"" and |v w x| <=n and for all i:0..* (u v^i w x^i y in L))

        (End of Net)

      9. Definition of the big O asymptotic notation for functions.
        1. For f,g:Nat0->Positive & Nat0, f is_big_O g::= for some c:Nat0,n0:Nat0, all n > n0 ( f(n) <= c* g(n) ).
        2. For f:Nat0->Positive & Nat0, bigO(f)::= {g:f:Nat0->Positive & Nat0. for some c:Nat0,n0:Nat0, all n > n0 ( f(n) <= c* g(n) )}.

        (End of Net)

        Tight bindings

        A tight binding introduces a variable with a fixed values. They are an abbreviation:
      10. For x:variables, W : propositions, e:expressions, (for x:=e (W)) ::= (e.[x]W), (e.[x]W) extracts the free 'x's in W and replaces them by 'e's.

      11. |-(example) for x:=2(x*x=4) = (2*2=4) = true.

      12. (def)|-For x:variable,W:propositions, e, (for x:=e(W)) = e.[x](W).

      13. For Q1,Q2:quantifiers, x, x1, x2:variables, W: propositions, e:expressions, (for x1:=e, Q2 x2:X2 (W)) ::= for x1:=e ( for Q2 x2:X2(W)),

      14. For Q1,Q2, x, x1, x2, W, e, (for Q1 x1:X1, x2:=e (W)) ::= for Q1 x1:X1 (for x2:=e (W)).

      15. For x:variables, W1(x),W2(x) : propositions, (for x:X, if W1(x) then W2(x)) ::= for all x:X(if W1(x) then W2(x)).

        Natural Abuses of Notation

      16. For x:variables, W1(x),W2(x) : propositions, (for x:X, W1(x)(W2(x))) ::= for all x:X(if W1(x) then W2(x)).

        The following idiom is both common and natural:

      17. For all Real x, some Real ε where ε>0, all Real δ where δ<ε....

        This is taken to be an abbreviation for

      18. For all x:Real, some ε:{ x:Real || ε>0}, all δ:{ x:Real ||δ< ε},...

        Note: an abuse of notation follows. The word macro in a definition indicates an abbreviation that can be used anywhere and is always removed before any meaning or parsing etc. is applied to the formula:

      19. For Q:quantifiers, x: variables, W: propositions, S: name_of_set, (Q S x where W) ::macro= Q x:{x:S|| W},

      20. For Q:quantifiers, x: variables, S: name_of_set, (Q S x) ::macro= Q x:S.

      . . . . . . . . . ( end of section Definitions of Quantifiers) <<Contents | End>>

      Very abreviated quantifiers

      I'm not sure whether the following is wise or not.

        Suppose that we have a Quantifier Q, a predicate (P(x)) with free variables x plus some other bound variables. The bound variables could have been bound in the context of the quantification or inside P(x). Assume that other rules also assign default types T to these free variables:

        (Q P(x))::macro = (Q x:T( P(x) ).

        (Q P(x) (W))::macro = (Q x:T, P(x) (W)).

        For example,

      1. for all 2*i=j, one 4*k=2*j.

        Supposing further R(x,y) is another proposition with with some extra free variables y (disjoint to x!) with default types U then

        P(x) ==> R(x, y) ::macro= for all x:T( if P(x) then for some y:U ( R(x, y))).

      (End of Net)

    24. Roadworks::=following,
        This is experimental: If you have any better ideas about ways to make formal the way we normally write things I would be interested in hearing about them.

        Natural, distfix, or mixfix predicates

        Idea a definition like this

         		For x:Person, y:Degree, z:College, (x has degree y from z) ::@.
        defines a "mixfix" or "distfix" expression. It describes a template into which expressions can be placed to create predicates:
         		`RJBotting` has degree `Ph.D.` from `Brunel University`

        template:@TEMPLATE, for all s:#char, 0..1 template t ( s in syntax(t) ).

      1. fits_template::= |[t:template](syntax(t)).

      2. TEMPLATE::=
          A template is a sequence of delimeters and arguments.

        1. delimiters::%delimiter.
        2. d:=delimiters.
        3. delimiter::=%( word_in_dictionary ~ ("and" | "or" | "not" | "if" | "then" | "else" | "the" |"a" | "for" |"For" | "set" | "map" | "Net" | "Let" ) ).

          For example

           		`RJBotting` has degree `Ph.D.` from `Brunel University`
          has delimiters ("", "has degree", "from", "").

        4. example0::=sort (2,1,4,3) into (1,2,3,4).
        5. example1::=Net{ delimiters=("sort", "into", ""). ...}.

        6. types::%(Types~{@}). --to avoid ambiguities no Boolean arguments.
        7. example2::=
            delimiters=("sort", "into", "").
          1. types=(%Nat, %Nat).
          2. ...


        8. arity::0..* = |types|, -- the term arity comes from Prolog.
        9. a:=arity.

          For example

           		`RJBotting` has degree `Ph.D.` from `Brunel University`
          has 4 delimiters (the first and last are "" null) and so a, the arity, is 3.

        10. (nbr_of_delimiters): |d|=a+1. -- d for number of delimiters
        11. (no_empty_delimiters): not ( "" in d(2..a) ) -- only the first and last delimiters can be null.
        12. example3::=
          1. delimiters=("sort", "into", ""). types=(%Nat, %Nat).
          2. a=2, |d|=3, ""=delimiters(3).
          3. ...


        13. D::1..a+1->@#lexeme=map[i:1..a+1] (! [w:pre(d(i))](d(i)(w) ) ).

          For example

           		`RJBotting` has degree `Ph.D.` from `Brunel University`
          has delimiters D(1)="", D(2)="has degree", D(3)="from", and D(4)="".

        14. example4::=
          1. D(1)={"sort"}, D(2)={"into"}, D(3)={""}.
          2. ...


        15. form::(1..a->@#lexeme)->@#lexeme= fun[v](D(1) ! v(1) ! ![i:2..a](D(i) v(i)) ! D(a+1) ) ).

          For example

           		`RJBotting` has degree `Ph.D.` from `Brunel University`
          has form(RJBotting, Ph.D., Brunel University).

        16. example5::=
          1. form( e1, e2 )={"sort"} e1 {"into"} e2 {""}.
          2. ...


        17. syntax::@#lexeme= form(expression o types).
        18. example6::=
          1. syntax={"sort"} expression(%Nat) {"into"}expression(%Nat) {""}.
          2. ...


          For example

           		`RJBotting` has degree `Ph.D.` from `Brunel University`
          has syntax= expression(BEING) "has degree" expression(qualification) "from" expression(institution).

        19. meaning::><types->@.
        20. |-for v1:types(1),v2:types(2),...v(a) :types(a), meaning(v1, v2,...v(a)) in @.
        21. example7::=
          1. meaning::(%Nat)><(%Nat) -> @. meaning( (2,3,4,1), (1,2,3,4) ) :@.
          2. ...


        22. definitions::@#lexeme= | [v:(1..a-->variable), p:1..a---1..a]( "For" v(p(1)) ":" representation(t(p(1))) ! ![i:1..a]("," v(p(i)) ":" representation(t(p(i))) "," ! form(v) ":"":""=" representation(meaning(v)) ).

          End of road works.


      (End of Net Roadworks)

    . . . . . . . . . ( end of section Lower Predicate Calculus(LPC)) <<Contents | End>>

    Operations on Predicates

      These ideas are new and untried but seem to be natural and sanctioned by a long tradition in formal logic going back to Aristotle. Indeed Fred Sommers and others have been championing TFL:
    1. TFL::="Term Functor Logic".

      Two predicates are said to be of the same type if they are defined on the same types of variables -- on the same universe of discourse. For example the predicates: even, odd, prime, composite, etc. are all of the same type because they apply to the natural numbers. Similarly: <, >, <=, >=, etc can be thought to be predicates of the same type because they apply to pairs of objects in a common domain.

      On predicates of the [ same type ] we can define operations that take two predicates and generate a new predicate.

    2. For T:Types, F,G: @^T.
    3. F & G::= map[x:T](F(x) and G(x)).
    4. F | G::= map[x:T](F(x) or G(x)).
    5. ~F::= map[x:T](not F(x)).
    6. F ~ G::= F & (~G).

      We can easily show that (&) and (|) on predicates of the same type are associative:

    7. F & (G & H) = (F & G) & H.
    8. F | (G | H) = (F | G) | H.

      We can assume that (&) and (|) are serial and omit parentheses.

      In fact all the properties of a Boolean Algebra will hold:

    9. (above)|-BOOLEAN_ALGEBRA(@^T, &, |, ~, ...).

      The result is suspiciously like Set Theory.

      It is also a term logic. In term logic you get expressions like:

    10. [R+B-L]
      	Red Boxes that are not Large
       	Small Red Boxes
      and in MATS we might have
    11. R & B ~ L.

      To complete Aristotlean logic we need the following predicates that operate on predicates!

      Here are some predicates that operate of predicates:

    12. no F::@ = for no x(F(x)).
    13. all F::@ = for all x(F(x)).
    14. some F::@ = for some x(F(x)).
    15. F==>G::@= for all x(if F(x) then G(x)).

    16. F overlaps G::@= some(F&G).

      We are now ready to express (and prove) the classic medieval syllogisms [ ../samples/syllogisms.html ] in MATHS.

    . . . . . . . . . ( end of section Operations on Predicates) <<Contents | End>>

    See Also

  1. O::=optional
  2. SERIAL::= See http://cse.csusb.edu/dick/maths/math_11_STANDARD.html#SERIAL
  3. PARALLEL::= See http://cse.csusb.edu/dick/maths/math_11_STANDARD.html#PARALLEL

    Introduction to Logic: [ logic_0_Intro.html ]

    Properties of Equality: [ logic_11_Equality_etc.html ]

    Proofs: [ logic_2_Proofs.html ]

    Sets: [ logic_30_Sets.html ]

    Relations: [ logic_40_Relations.html ]

    Maps and Functions: [ logic_5_Maps.html ]

    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

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


  5. 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).
  6. given::reason="I've been told that...", used to describe a problem.
  7. given::variable="I'll be given a value or object like this...", used to describe a problem.
  8. goal::theorem="The result I'm trying to prove right now".
  9. goal::variable="The value or object I'm trying to find or construct".
  10. 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.
  11. hyp::reason="I assumed this in my last Let/Case/Po/...".
  12. QED::conclusion="Quite Easily Done" or "Quod Erat Demonstrandum", indicates that you have proved what you wanted to prove.
  13. QEF::conclusion="Quite Easily Faked", -- indicate that you have proved that the object you constructed fitted the goal you were given.
  14. RAA::conclusion="Reducto Ad Absurdum". This allows you to discard the last assumption (let) that you introduced.