[Skip Navigation] [CSUSB] >> [CNS] >> [Comp Sci ] >> [R J Botting] >> [MATHS] >> intro_logic
[Contents] [Source Text] || [Notation] || [Copyright] || [Contact] [Search ]
Sun May 7 19:53:09 PDT 2006

Contents


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

      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:
      FormulaCase1Case2Case3Case4SyntaxPrecedence
      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 qp \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

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

    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 complete listing of pages by topic see [ home.html ]

End