[Skip Navigation] [CSUSB] / [CNS] / [CSE] / [R J Botting] / [ MATHS ] / logic_8_Natural_Language
[Contents] [Source Text] || [Notation] || [Copyright] || [Contact] [Search ]
Mon Jul 16 11:18:38 PDT 2012


    Semantics of English

      Be very careful of assuming that the way your language divides up the world is the same as any other language's way of slicing the semantic cake. Terminology varies between countries, regions, companies, and even between parts of a company.

      Also beware the temptation to design a grand hierarchy of all meanings. There have been many attempts in the last 300 years: [Eco95] often as part of the design of a universal or perfect language. None of them have stuck. On the other hand you can use these attempts as a source of ideas to model specific application domains and user concepts. There is a well tested classification system for English called Roget's Thesaurus.

      Each application domain has its own languages and these need to be understood when developing software. There is some evidence that constructing a clear and precise model of such a domain is a step in the direction of better software. Mathematics and logic can be very helpful with eliminating the "goo and dribble" and boiling things down[Asimov].

      What follows here are some examples drawn from the twentieth century. By the end of the twentieth century and start of the twenty-first century there were several logical models of natural language placed on the web in the form of ontologies. Below are some examples of one way the MATHS notation could be used to express these hierarchies but they are not intended to be a complete and finished description. Professionals have been working on these, see [ Ontologies in index ] [ lookup.php?search=ontolog ] for more.

      This page gives examples of how to use the logical fragment of MATHS to construct models of natural world phenomena like dogs, cats, rocks, and parents(STUFF). This is the best approach when we want to express properties of the objects or entities in a domain.

      An alternative would be to use Sets and Relations instead of Nets of variables and axioms. This is close to the way that abstract algebras like groups are modeled in MATHS [ notn_6_Algebra.html ] [ math_43_Algebras.html ] [ notn_7_OO_vs_Algebra.html ] for example. The SUMO ontology is also best modeled this way. See [ Suggested Upper Merged Ontology ] at the end of this page.

      Abbreviation to express subsets

      Natural languages have large numbers of terms indicating objects of different sets and types. This are typically organized in a hierarchy. It is useful to have a simple way of expressing such a hierarchy:
    1. either_or_notation::= See http://cse.csusb.edu/dick/maths/notn_16_Classification.html.

      A statement like

       		either A or B.
      asserts the existence of two Boolean variables A and B and the property that precisely one of them is true. The above is short hand for:
       		|- A or B.
       		|- not(A and B).
       		either A, B, or C.
      asserts the three conditions, but only one is true at a time. If A is true then B and C are false.


      I may be moving the following sample into my directory of samples: [ http://cse.csusb.edu/dick/samples/ ] before September 2004.

      Sampler of Ontologies

        Ontological Categories

        Source: Chi 92, Michelene T H Chi, Figure on page 41 in "The Science & Learning Math and Science", NSF Mosaic V23n2(Summer 92)p37..43

      1. ALL_ENTITIES::=$
        1. material_objects::@,
        2. events::@,
        3. mental_states::@.
        4. |- (ae1): one ( material_objects, events, mental_states).

        5. |- (ae2): if material_objects then either artifacts or natural.
        6. |- (ae3): if events then either intentional or constraint_based.
        7. |- (ae4): if mental_states then either ideas or emotions.


        Mistakes in learning science:

        1. insects not animals - within a category.
        2. heat is material - across a category.


      2. Let{
          August 2004. I'm getting doubts about this approach.


          This section just lays out a logical framework for talking about various meaningful domains. The idea is that the defined terms like STUFF, BEING, etc should be reused in other nets. They are taken from

          Source: Leech, "Semantics", Penguin Books 1974 [Leech 74] however this kind of hierarchy goes back a long way to the Tree of Porphyry [ Tree_of_Porphyry ] (Wikipedia) and [ PorphyryTree.html ] at the University of Washington.

          Leech [Leech74] preents the idea (from anthropology) that terms in natural language can be given meaning in terms of components:

           	man	+HUMAN+ADULT+MALE
           	woman	+HUMAN+ADULT-MALE
           	boy	+HUMAN-ADULT+MALE
           	girl	+HUMAN-ADULT-MALE
          Components match the idea of attributes in a MATHS Net.

          The following Nets translate Leech's diagram on page 121 of his book.

        1. STUFF::=

          1. |-Either countable or mass. So, for instance, "butter" is mass, but "dogs" are countable.
          2. If countable then either singular or plural.
          3. |-if singular or plural then countable.

          4. |-Either concrete or abstract.
          5. If concrete then either solid, liquid, or gas.
          6. |-if solid or liquid or gas then concrete.
          7. (above)|-abstract iff not solid and not liquid and not gas.

          8. If solid then either animate or inanimate.
          9. |-if animate or inanimate then solid.


          The above creates a net with Boolean attributes: countable, mass, concrete, abstract, singular, plural, ... and so on.

        2. CONCRETE::= STUFF and concrete.
        3. SOLID::= CONCRETE and solid.


        4. THING::=SOLID and inanimate.


        5. BEING::=SOLID and animate and following

          1. |-either masculine or feminine.
          2. |-either adult or child.
          3. |-either plant or creature.
          4. |-either living or dead.
          5. age::years.

          (End of Net BEING.)

        6. CREATURE::=BEING and creature and
        7. Net{
            kritters and us.
          1. |-either human or animal.
          2. If animal then ANIMAL


          We can now express Leech's example above:

        8. man::=$ CREATURE and human and adult and masculine.
        9. woman::=$ CREATURE and human and adult and feminine.
        10. boy::=$ CREATURE and human and child and masculine.
        11. girl::=$ CREATURE and human and child and feminine.


        12. ANIMAL::= CREATURE and animal and following,
        13. Net{

          1. |-animal.
          2. Kinds::={bird, fish, insect, mammal,... }.
          3. kind::Kinds.
          4. |-SPECIES.

        14. SPECIES::=
          1. Mammal_Species::={cat, dog, horse, cow, wolf,... }.
          2. If kind=mammal then species::Mammal_Species.
          3. ...
          4. |-BREED.

        15. BREED::=
          1. Dog_Breed::={mixed, alsation,terrier, spanish,... }.
          2. If species=dog then breed::Dog_Breed.
          3. ...


        16. |-Shadow in $ ANIMAL(dead, female, adult, kind=mammal, species=dog, breed=mixed ).

        . . . . . . . . . ( end of section Stuff) <<Contents | End>>

      Spatial Relations

    2. SPATIAL::=
      1. relation:: @($ STUFF and concrete, $ STUFF and concrete).
      2. |-Either normal or converse.
      3. |-Either horizontal or vertical.
      4. If horizontal then either front_to_back or side_to_side.
      5. |-Either close or near or unknown or far.
      6. Directions::={V,F,S}.
      7. direction::Directions=if(vertical, V, if(front_to_back, F, S)).

      8. Distances::={C,N,F,U}.
      9. distance::Distances=if(close,C,if(near,N,if(far,F,U))).


    3. over::= SPATIAL(normal, vertical).
    4. under::= SPATIAL(converse, vertical).
    5. in_front_of::= SPATIAL(normal, front_to_back).
    6. behind::= SPATIAL(converse, front_to_back).
    7. on_the_left::= SPATIAL(normal, side_to_side).
    8. on_the_right::= SPATIAL(converse, side_to_side).

    9. For R,S:$ SPATIAL, R parallel S::@=R (= mod direction)&(= mod distance) S.
    10. |-For R,S:$ SPATIAL, R.normal and S.converse and R parallel S iff R.relation = /(S.relation).

    11. |-For R,S:$ SPATIAL, if R.horizontal and S.vertical then no R.relation & S.relation.

    12. |-For R,S:$ SPATIAL, if R.front_to_back and S.side_to_side then no R.relation & S.relation.

      For more on natural spatial relations see [ math_93_Graphics.html ]


      Source: Leech pp234-237.

    13. colour::British={ white, black, red, green, yellow, blue, brown, purple, pink, orange, grey, ...}.
    14. color::USA=colour.British.


    15. male::=$ BEING and masculine.
    16. female::=$ BEING and feminine.

      Source: Anthropology??

    17. KINSHIP::=
        Includes animal and plant kinship and so ignores marriage.
      1. parent::@($ BEING, $ BEING),
      2. |- (KIN0): parent ==> (<>). can not be ones own parent.

      3. sibling:: @($ BEING,$ BEING).
      4. |-sibling= (/parent;parent) & (<>).

      5. |- (KIN1): no sibling & parent.
      6. (sibling)|- (KIN2): sibling ==> (<>).
      7. (sibling, STANDARD)|- (KIN3): sibling in Symmetric & Irreflexive & Transitive.

      8. child_of::=/parent.

      9. father::= male;parent.
      10. For all x,y:$ BEING, x father y::=x is the father of y.
      11. mother::=female;parent.
      12. For all x,y:$ BEING, x mother y::=x is the mother of y.

      13. |- (KIN4): father and mother ∈ $ BEING(1)-(any)$ BEING.

        For R: {father, mother, son,daughter, child_of, sister, brother, ....}, x R y::=x is a R of y.

      14. son::= male;child_of.
      15. daughter::=female;child_of.

      16. sister::=female;sibling.
      17. brother::=male;sibling.

      18. grandfather::=father;parent.
      19. grandmother::=mother;parent.
      20. grandparent::=parent;parent.
      21. |- (KIN5): grandparent >== {grandfather, grandmother}.

      22. granddaughter::=daughter;child_of.
      23. grandson::=son;child_of.
      24. grandchild::=child_of;child_of.
      25. (above)|- (KIN6): grandchild>=={grandson, granddaughter}.

      26. (above)|- (KIN7): grandparent = /grandchild

      27. uncle::=brother;parent.
      28. aunt::=sister;parent.
      29. nephew::=son;sibling.
      30. niece::=daughter;sibling.

      31. first_cousin::=/parent;sibling;parent.
      32. second_cousin::=/parent;/parent;sibling;parent;parent.
      33. cousin::=first_cousin | /parent;cousin;parent.

      34. first_cousin_once_removed::=/parent;first_cousin | first_cousin;parent.

      35. For x,y:$ BEING, n,m:Positive, (x is the n th_cousin m th_remove of y) ::=child_of^(n+m);sibling;parent^n | child_of^n;sibling;parent^(n+m).

      36. ...


      Structure of Objects

      [ PART_WHOLE in math_21_Order ]


    18. OWNERSHIP::=
        This following is somewhat human-chauvinist.
      1. owner::$ CREATURE(human).
      2. owned:: $ STUFF,
      3. slave::@= owned in $ CREATURE(human).


      ownership:@OWNERSHIP. for x,y:$ STUFF, x owns y ::= x /owner;ownership;owned y.


        The following definition is past tense: shadow = the ($ ANIMAL(female, adult, kind=mammal, species=dog. breed=mixed) & Tricia./owns ).
      1. Slavery::@=some( $ CREATURE(human) & ownership./owned).

      (Close Let )

      Suggested Upper Merged Ontology

    19. SUMO::= See http://icosym-nt.cvut.cz/kifb/en/.
    20. SUMO::acronym="Suggested Upper Merged Ontology".

      Here is my second draft at transmogrifying the top of SUMO into MATHS. Because it is expressed in terms of sets of objects and the properties of the sets (not the properties of the objects in the sets) it best to express it as a net of set definitions and axioms about these sets.

    21. top_of_SUMO_in_MATHS::=
        encoding of a tiny part of the top of the Suggested Upper Merged Ontology...
      1. Entity::Sets.
      2. |- (E1): Some Entity.
      3. |- (E2): Entity >== {Abstract, Physical}.
      4. instance::@( Entity, Set_or_class).
      5. subclass::@( Set_or_class, Set_or_class).
      6. ... about 20 other relations.
      7. |-For all c, if c instance Class then c subclass Entity.

      8. Physical::@Entity.
      9. Object::@Physical.
      10. Process::@Physical.
      11. |-Physical>== {Object, Process}. |- For all p:Entity, p in Physical iff for some t:Entity, l::Entity( p located l and p during t).
      12. (above)|-Physical = |[t:Entity, l:Entity](t./during & l./located).
      13. ...and 9 more...
      14. Abstract::@ Entity.
      15. |-For all a:Entity, a in Abstract iff not for some p:Entity( a located p or a during p).
      16. ... and more...
      17. Set_or_class::@Abstract.
      18. Class::@Set_or_class.


    . . . . . . . . . ( end of section Sampler of Ontologies) <<Contents | End>>

    Tenses, Time, and Temporal modalities

      Natural languages always have ways of talking about events in the past, now, and in the future. It is likely that time is important in many computer systems. And so I decided to document ways to expresses tenses and time in logic. This turns out to be interesting and controversial... well beyond the elementary logic I was planning for these pages.

      First here [ ../samples/tenses.html ] is a list of English tenses with examples of the syntax and Reichenbach's semantics.

      Some developments from this and The classical (2000 year old) approach has beeen reborn in software engineering research. This is the study of temporal logics and can be found in [ logic_9_Modalities.html ] (Modal logic).

      Another direction in MATHS is to use Dynamic Predicates that directly express changes as relations between a past and a future state by putting a prime(') on future variables. For more on this see [ intro_dynamics.html ] and [ math_14_Dynamics.html ] in this set of pages. This is further based on the theory and notation of relationships [ logic_41_HomogenRelations.html#Paths and Trajectories ] and general systems [ maths/math_71_Auto...Systems.html#Discrete_Dynamic_System ] and automata theory.

      Fluents are predicates involving time

      The term fluent was introduced to describe predicates that change. This is a terminolgy from Artificial Intelligence and philosphy.

      A fluent is a predicate that changes value with time. It is quite feasible to express this in first-order logic by adding an extra argument. Thus the proposition "It is raining" might be rendered as

    1. rain(t).


    2. rain : Time -> @.

      Properties of objects -- for example the cat is on the mat -- might be expressed as a predicate with three arguments

    3. on(theCat, theMat, time)


    4. on : @(Object, Object, Time)

      In MATHS we can write something like this

    5. on[t](theCat, theMat)

      So that

    6. on : Time -> @(Object, Object)

      The following "box" is a direct quote from [ #2 ] (Stanford Encyclopedi of Philosophy).

        Donald Davidson (1967). The problem is to give a formal account of the validity of such inferences as
      1. John saw Mary in London on Tuesday.
      2. Therefore, John saw Mary on Tuesday.

        The inference above is cast in logical form as

      3. for some e(See(John,Mary,e) & Place(e,London) & Time(e,Tuesday)),
      4. Therefore, for some e(See(John,Mary,e) & Time(e,Tuesday)).

        Also see the Event Calculus of Kowalski and Sergot (1986).

      Partly Baked Ideas

        May be basis of Jackson's model of time as a series of alternating events and intervals with no events?

        Very flexible -- allows the same logic to handle many different temporal epistimologies by adjusting Time and Place.

        Also... event tokens could act as objects:

      1. Jim saw John seeing Mary in London on Tuesday.
      2. for some e1,e2 (See(Jim, e1, e2) & See(John,Mary,e1) & Place(e1,London) & Time(e1,Tuesday)). Perhaps an axiom
      3. for all e1,e2, p, t, See(Jim, e1, e2), See(John,Mary,e1) & Place(e1,p) & Time(e1,t)(Place(e2,p) & Time(e2,t)).

        Also compare "Babel 17"[Delaney] where events are given a verbal tag for future reference.

        The next level of generality is to reify the verbs:

      4. for some e(Event(e, see, John, Mary) & Place(e, London) & Time(e, Tuesday)).

        This then permits statements at the meta level:

      5. for all x, Event(x, isa, see, verb).

        Perhaps we need to define

      6. EVENT::=Net{identifier, subject, objects, places, times}.

        Even more unbaked ideas on time and events

          We can't assume that time is linear. You find diffferent, parallel, partially synchronized times on computers, in the real world, in data bases, time in a piece of fiction, times of events in history, etc. So merely postulate a partial ordering of times:
        1. TimeBase:: POSET.

          The precise time of an event is never known, but is often known to lie in a range. For example, the 12th of January 1945 is a range of 24 hours. So define,

        2. Time::={ a..b: @TimeBase. for some a,b : TimeBase(a<=b)}. ..., days, weeks, months, years, centuries, millenia, ... : @Time.

        3. ExactTime::={ a..b: @TimeBase. for some a,b : TimeBase(a=b)}.

          Modelling places we need to notice that (1) they are regions (not points) in a space, and (2) they change in time. For example the place Rome has changed its boundaries many time in the last 3 thousand years. So, I start by postulating a Space inwhich we can specify places...

        4. Space::Sets.

          Probably this will have some kind of topology -- which makes the study of events dependent on some deep and abstract mathematics (see Topology below if you want details).

        5. Place::Time->@Space.

          The Events being discussed could be real events or events in a piece of fiction or even might have beens. These are distinguished by the different Spaces -- we can have rain occuring in a real place, like Manchester, England, and in a fictional place like Bree in the Middle Earth.

        6. Situation::= Place><Time, hopefully a convenient abbreviation.

        7. Description::Sets.

          Sample descriptions

           	Jim sees Mary
           	MEB gives birth to RJB

        8. Event::@EVENT, these will be local variables with this structure
        9. EVENT::=following,
          1. description::Description.
          2. place::Place.
          3. time::Time.

          4. situation::Situation= (place, time).

          (End of Net EVENT)

          Example: it is always raining in Manchester (given that manchester isa Place):

        10. For Time t, some Event rm (rm.time=t and rm.place = manchester and rm.description=rain).

        11. event::@( Description, Place, Time)= map[d,p,t](for some Event e ( rm.description=d and e.place=p and e.time=t)).
        12. For Time t, event(rain, manchester(t), t).

          Now an even more speculative development of what a Description moght be:

        13. Description::= O(Subject) Basic_Verb O(Thing) #(N(Basic_Direction) Thing). Subject==>Thing,
        14. for some Time t, Place p, event(MEB gives birth to RJB, p, t) and event(snow, p, t) and past t.
        15. for some Time t, Place p(for some Event b( event(b,MEB gives birth to RJB) and place(b, p) and time(b, t)) and for some Event s( event(s,snow) and place(s, p) and time(s, t)) and past t).

          OR define

        16. POSSIBLE_EVENT::=Net{ Description, Place, Time}, and sets Event, RealEvent, PastEvent(t), ImaginaryEvent, EventInJRRTolkien,... in @$ POSSIBLE_EVENT.

          How to express change?


            journal&blog example motivate Reichenbach E+R+S for utterances & writings.

          (Close But )

        (End of Net)

      (End of Net)

    . . . . . . . . . ( end of section Tenses, Time, and Temporal modalities) <<Contents | End>>

    Systems English

      Systems English is an invented subset of subset of Basic English designed for systems -- collections of parts that pass objects between each other.

    1. SYSTEMS::=
        A Language for Describing Systems.

        The first atteempt below creates a new syntax for facts about systems but leaves the semantics undefined. The second attempt defines a set of natural predicates with MATHS that cover the commonest statements made about systems.

        P3Basic English -- a subset of Basic English that uses the present tense(P) and third person only(3).

      1. Systems_English::semantics=system.
      2. system::Sets.

      3. Systems_English::syntax=
          Use MATHS_Lexemes. [ notn_10_Lexicon.html ]

        1. description::=L(facts, punctuation) period.

        2. fact::=subject verb (object|) #(direction) (target|),
            SASS is a `Simple ASsembler System`
            Pass1 is a process in SASS
            Pass2 is a process in SASS
            Symbols is a store in SASS
            SASS gets input from source_code
            SASS sends output to object_code
            object_code is output from SASS
            Pass1 gets lines from source_code
            Pass1 sends labels and addresses to Symbols
            Pass2 gets instructions from source_code
            Pass2 gets addresses from symbols
            Pass2 gives object_code to output

        3. verb::="does"|"makes"|"puts"|"gets"|"takes"|"gives"|"is"|"has"|"leaves"|"keeps"|"sends", the Basic English verbs in the third person singular.

        4. direction::="in"|"on"|"to"|"from"|"off"|"thru"|"by"|"of"|"after"|"before"| "at"|"with"|"over"|"under"|"up"|"down"|"among"|"about"|"between"|"across"|"out", ripped off from Basic English.

        5. subject::=name,

        6. object::=compound|"input"|"output"|"a process"|"an object"|"data"|"a store"|"an entity".

        7. target::=thing,

        8. compound::=thing #("and" thing),

        9. thing::=("a"|"the") type | name | other_language_string.


      4. Data_Base::= @Systems_English.syntax.facts.
      5. parse::Systems_English.syntax.description->@Systems_English.syntax.facts.
      6. parse("")={},
      7. for f:Systems_English.syntax.facts, parse(f)={f},
      8. for f:Systems_English.syntax.facts, p:punctuation, s:Systems_English.syntax.description, parse(f!p!s)={f} | parse(s).

        Example of a Simple Assembler System

      9. Simple_assembler:: Systems_English.syntax.description= "SASS is a Simple ASsembler System. Pass1 is a process in SASS, Pass2 is a process in SASS. Symbols is a store in SASS. SASS gets input from source_code. SASS sends output to object_code. object_code is output from SASS. Pass1 gets lines from source_code. Pass1 sends labels and addresses to Symbols. Pass2 gets instructions from source_code. Pass2 gets addresses from symbols. Pass2 gives object_code to output." .

      10. Simple_assembler::Data_Base=parse following
        • "SASS is a 'Simple ASsembler System'"
        • "Pass1 is a process in SASS"
        • "Pass2 is a process in SASS"
        • "Symbols is a store in SASS"
        • "SASS gets input from source_code"
        • "SASS sends output to object_code"
        • "object_code is output from SASS"
        • "Pass1 gets lines from source_code"
        • "Pass1 sends labels and addresses to Symbols"
        • "Pass2 gets instructions from source_code"
        • "Pass2 gets addresses from symbols"
        • "Pass2 gives object_code to output" .

        Example Queries

      11. P'!"is a"!T'!"in SASS" in Simple_Assembler; User:!P,T.
      12. "SASS sends"!#char!"to" X' in Simple_Assembler; User!X.

        A semantic approach is to use natural predicates.

      13. FACTS::=
        1. Things::$ THING,
        2. things::Expression(Things).
        3. For x, y:things, (x is a y) ::@.
        4. For x, y, z:things, (x is a y of z) ::@.
        5. For x, y, z, (x gets y from z) ::@.
        6. For x, y, z, (x sends y to z) ::@.
        7. For x, y, (x is output from z) ::@.
        8. For x, y, z, (x gives y to z) ::@. Hence
        9. Example_SASS::=following

          1. |-SASS is a "Simple ASsembler System".
          2. |-Pass1 is a process in SASS.
          3. |-Pass2 is a process in SASS.
          4. |-Symbols is a store in SASS.
          5. |-SASS gets input from source_code.
          6. |-SASS sends output to object_code.
          7. |-object_code is output from SASS.
          8. ...

          (End of Net)


        Or infix operators with structures

      14. Infix_FACTS::=following
        1. isa::@($ THING, $ THING),
        2. isa::@($ THING, $ Net{type:THING, in:$ THING }),
        3. gets::@($ THING, $ Net{it, from:$ THING }),
        4. sends::@($ THING, $ Net{ it, to:$ THING }),
        5. is_output_from::@($ THING, $ THING),
        6. gives::@($ THING, $ Net{ it, to:$ THING }).

          1. |- (example_infix_FACT): SASS gets (it=>input,from=>source_code).

          (End of Net)

        (End of Net)


    . . . . . . . . . ( end of section Systems English -- a subset of Basic English) <<Contents | End>>

. . . . . . . . . ( end of section Semantics of English) <<Contents | End>>


[ math_91_Topology.html ] [ logic_31_Families_of_Sets.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

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


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