.Open Logic
. 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
	If a plant doesn't get enough water it will die.
	This plant hasn't been getting enough water.
	()|- 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
.See http://www/dick/maths/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:
.See http://www.cs.cornell.edu/Info/People/gries/logicthetool.html
. Problems
The key problems of trying to use formal logic real life are:
.Set
 First: the traditional notation is hard to learn and use because it uses special alphabets.
For the traditional notation see
.See http://www.math.csusb.edu/notes/logic/lognot/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:
.See http://www.mcs.net/~jorn/html/ai/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.
.Close.Set
. 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.
.As_is 	x<1 and y>2
.As_is 	not ( x>=1 or y<=2)

The symbol @
represents the type with two values {true, false} and the operators
.As_is 	`not`, `and`, `or`, `iff` `if__then_` `:-`.
A proposition can has two possible meanings - true and false - the Booleans
	Boolean::={true, false}.
	@::shorthand=Boolean.

. Operations
The simplest operator is `not`.  You write it in front
of a proposition.
It changes true to false and vice versa:
.Box
	not:: @->@.   
	|-(neg1): not(true) = false.  
	|-(neg2): not(false)=true.
.Close.Box

The following table summarizes how the other operators work:
.Table Formula	Case1	Case2	Case3	Case4	Syntax	Precedence
.Row P
.Item true
.Item true
.Item false
.Item false
.Row Q
.Item true
.Item false
.Item true
.Item false
.Row P and Q
.Item true
.Item false
.Item false
.Item false
.Item infix(serial)
.Item 2nd (after `not` and `(...)`)
.Row P or Q
.Item true
.Item true
.Item true
.Item false
.Item infix(serial)
.Item 3rd (after `and`)
.Row P iff Q
.Item true
.Item false
.Item false
.Item true
.Item infix(parallel)
.Item 4th
.Row if P then Q
.Item true
.Item false
.Item true
.Item true
.Item natural
.Item 5th
.Row Q:-P
.Item true
.Item false
.Item true
.Item true
.Item infix
.Item See
.See clausal_form
below.
.Close.Table
More formally, the symbols
.As_is  `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:
.Box
 and::@><@->@=`(1st) and (2nd) are both true`,
.As_is 	raining and windy
 or::@><@->@=`at least one of (1st) and (2nd) are true`,
.As_is 	raining or windy
 iff::@><@->@=`(1st) and (2nd) are the same, both true or both false`,
.As_is 	x < y iff y > x
 if_then_::@><@->@=`either (1st)is false or (2nd) is true`,
.As_is 	if raining then I_get_wet.
 :- :: @><@->@=if (2nd) then (1st).
.As_is 	I_get_wet :- raining.
.Close.Box
Sometimes it useful to express an implication in `clausal form`:
(clausal_form): For propositions P,  Q,  
	if P=(P1 or P2 or P3 or,...) and Q =(Q1 and Q2,...) then
		P :- Q ::= if Q then P.

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

Note the similarity of clauses to definitions:
		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
.Set
	x>y
	if P(k) then P(k+1)
	P(1)
.Close.Set

. 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.

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

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

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

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

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

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

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

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

	etc.

It is also OK to write things like this
.As_is 	for all Numbers n,....
as short for
.As_is 	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:
.Table MATHS	\TeX
.Row and	\land
.Row or  	\lor
.Row not	\neg
.Row if p then q	p \to q
.Row iff	\leftrightarrow
.Row for all	\forall
.Row for some	\exists
.Close.Table
. 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:

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

(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.


.Open 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
Boolean_algebra::=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:
.Close Notes
.Close Logic