Introduction

Jevons (See Jevons below) remarks that just as everybody speaks "prose", everyone is a logician. We often use logic with out noticing it. For example:
Let
1. If a plant doesn't get enough water it will die.
2. This plant hasn't been getting enough water.
   
3. (above) |-This plant will die

(Close Let )
He says that just as we are all to some extent athletes we are also to some extent logicians.

Logic has a long history [ logic_history.html ] but it changed more in the 19th and 20th centuries than it did in the previous 2000 years!

My focus in this page is using modern, formal, and symbolic logic in a simple and practical way. I'm not so concerned with the philosophical issues.

Using Logic

Logic can be a useful tool - when combined with normal human creativity. It is a means to avoid making mistakes. It is a way to clarify confusion -- it nails the jelly to the tree. Symbolic logic boils out the "goo and dribble"("Foundation" by Isaac Asimov). Symbols give a short-hand notation and so a key to faster thinking. I have used symbolic logic for note taking for many years.

Within software development it can be used to express domain knowledge (what is known or assumed about the world in which software exists), requirements (the way we wish the world was), and specifications ( how the software must behave to satisfy the requirements). It can also be used to find logic errors in programs ( situations where the program does not fit the specification). Unlike testing logic permits a systematic search for errors can end up showing that a piece of software has no bugs. I've used logic like this ( when I've had the time) since the late 1960s.

Unlike creativity, logic can be taught. I've done this. So have many others in computer science degrees: [ logicthetool.html ]

Problems

The key problems of trying to use formal logic real life are:
• First: the traditional notation is hard to learn and use because it uses special alphabets. For the traditional notation see [ lognot.html ]
• Second: practical reasoning has to be done at a higher level than found in the research and in most text-books - there is no point in proving that a wheel must be round every time we design a cart!
• Third: good software has to fit into a world that is described by a large number of more or less trivial facts. Traditional symbolic logic is designed to fit in to a world with few assumptions but many deep theorems. The Cyc project has studied these problems: [ cyc.html ]
• Fourth: You need to experience the state of flow that comes after mastering a symbolic or formal language before one understands that it is a powerful tool for a creative mind.

Solutions

Programming languages have taken the ideas of symbolic and formal logic ( Booleans, Theory of types, etc. ) and made them a part of the every day work for large numbers of people. They did this by encoding them in ASCII. The notation here applies the same idea to non-executable logic and mathematics.

The notation described here tries to answer the first two problems by having a fairly intuitive ASCII coding of logical concepts plus a way of packaging up logical systems for future Internet reuse. The third problem can be handled by people putting logical systems for the vital trivia of everyday life on the World wide web. They can then be reused via a hypertext link.

Here is an quick introduction to the notation used to express logic in MATHS.

Propositions

Propositions are statements that can only have one of have two possible meanings - true and false. There are operators that combine two propositions into a single more complex ones. The operators are those found in programming language (and, or, not) plus some more theoretical ones.

 	x<1 and y>2

 	not ( x>=1 or y<=2)

The symbol @ represents the type with two values {true, false} and the operators

 	`not`, `and`, `or`, `iff` `if__then_` `:-`.

A proposition can has two possible meanings - true and false - the Booleans
1. Boolean::={true, false}.
2. @::shorthand=Boolean.

   Operations

   The simplest operator is not. You write it in front of a proposition. It changes true to false and vice versa:

   ---

   1. not:: @->@.
      
   2. |- (neg1): not(true) = false.
      
   3. |- (neg2): not(false)=true.

   ---

   The following table summarizes how the other operators work:

   Formula	Case1	Case2	Case3	Case4	Syntax	Precedence
   P	true	true	false	false
   Q	true	false	true	false
   P and Q	true	false	false	false	infix(serial)	2nd (after not and (...))
   P or Q	true	true	true	false	infix(serial)	3rd (after and)
   P iff Q	true	false	false	true	infix(parallel)	4th
   if P then Q	true	false	true	true	natural	5th
   Q:-P	true	false	true	true	infix	See [ clausal_form ] below.

   More formally, the symbols

     `and`, `or`, `iff` `:-`.

   are infix operators turning two Booleans into a Boolean, and 'if__then__' is a distfix operator . They each take two Booleans (@><@) and return a Boolean (->@) as shown below:

   ---

   1. and::@><@->@=(1st) and (2nd) are both true,

       	raining and windy

   2. or::@><@->@=at least one of (1st) and (2nd) are true,

       	raining or windy

   3. iff::@><@->@=(1st) and (2nd) are the same, both true or both false,

       	x < y iff y > x

   4. if_then_::@><@->@=either (1st)is false or (2nd) is true,

       	if raining then I_get_wet.

   5. :- :: @><@->@=if (2nd) then (1st).

       	I_get_wet :- raining.

   ---

   Sometimes it useful to express an implication in clausal form:
3. (clausal_form): For propositions P, Q,
4. if P=(P1 or P2 or P3 or,...) and Q =(Q1 and Q2,...) then
5. P :- Q ::= if Q then P.

   For instance

6. x>y:-x=y+1,
7. x>y:-for some z ( x=z+1 and z>y).

   Note the similarity of clauses to definitions:

8. x>y::=x=y+1 or for some z(x=z+1 and z>y).

   Definitions imply the equality of two expressions. Clauses allow partial definition in the listed cases...

   Predicates

   A predicate is a proposition that has one or more variables or constants that represent objects other than the values true and false. For example
   • x>y
   • if P(k) then P(k+1)
   • P(1)

   Quantifiers

   In the following X stands for a name of a type, x is a variable and W(x) a predicate containing x in a number of places.

9. for all x:X(W(x)) ::=For all x of type X , W(x) is true,

10. for x:X(W(x)) ::= for all x:X(W(x)),

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

12. for some x:X(W(x)) ::=not for no x:X(W(x)).

13. for 0..1 x:X(W(x)) ::=for all y,z:X(if W(y) and W(z) then y=z),

14. for 1 x:X(W(x)) ::= for some x:X(W(x)) and for 0..1 x:X(W(x)),

15. for 2 x:X(W(x)) ::= for some x:X(W(x)) and for 1 y:X(x<>y and W(y)).

16. for 3 x:X(W(x)) ::= for some x:X(W(x)) and for 2 y:X(x<>y and W(y)).

17. etc.

    It is also OK to write things like this

     	for all Numbers n,....

    as short for

     	for all n:Numbers.

    However the type of the variable (Number above) must indicated by a name, not a formula to avoid ambiguities.

    Logical Notation for TeXies

    The following (from Knuth's typesetting program) can also be used:

    MATHS	\TeX
    and	\land
    or	\lor
    not	\neg
    if p then q	p \to q
    iff	\leftrightarrow
    for all	\forall
    for some	\exists

    Axioms

    The set of values {true, false} are the original Boolean Algebra. They and all predicates, variables etc follow axioms like these: For all propositions and predicates, P, Q, & R:

    
    

18. |- (Commutivity): P and Q = Q and P, P or Q = Q or P.
    
19. |- (Associativity): P and (Q and R) = (P and Q) and R, ...
    
20. |- (Absorbative): P and (P or Q) = (P or Q),...
    
21. |- (Units): P and true= P, Q or false = Q.
    
22. |- (Zeroes): P or true = true, Q and false = false.

    
    

23. (above) |-(@,or,false,and,true,not) in Boolean_algebra.

    Types

    In programming language we have data types. In modern logic we have types. Most practical programmers do not know that the idea of type and much of the type systems that they use were invented to resolve paradoxes in logic in the late 1800s and early 1900s.

    In MATHS variables are always attached to a type and this type determines the values it may have and the operations and functions that can be applied to it. This turns out to be very useful for writing programs. It also allows the economy of overloaded operator and function symbols.

    Much of the logic is defined using generic types with symbolic names (usually T). These are very like templates in C++ or generic packages in Ada. An actual type is substituted when the logic is put to use.

    We can define the predicate calculus as the logic of objects of a given (generic) type.

    Notes

    Jevons

    Prof. W Stanley Jevons, MA, LLD, FRS. Logic, A Science Primer published by Macmillan 1906.

    Also created an early logic machine -- a kind of piano for playing syllogisms, if I recall correctly.

    Boolean Algebra

    1. Boolean_algebra::= See http://www.csci.csusb.edu/dick/maths/math_41_Two_Operators.html#Boolean Algebra, George Boole was another Victorian mathematician who worked out a set of Laws of Thought. These laws for what we call Boolean Algebra:

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

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

Notes on MATHS Notation

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, and give them a name. 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.

Notes on the Underlying Logic of MATHS

For a complete listing of pages by topic see [ home.html ]