.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