- Logic
- : Introduction
- : Using Logic
- : Problems
- : Solutions
- : Propositions
- : Operations
- : Predicates
- : Quantifiers
- : Logical Notation for TeXies
- : Axioms
- : Types
- : Notes
- : : Jevons
- : : Boolean Algebra
- Notes on MATHS Notation
- Notes on the Underlying Logic of MATHS

- If a plant doesn't get enough water it will die.
- This plant hasn't been getting enough water.
- (above) |-This plant will die
- 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. - 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:

The following table summarizes how the other operators work:

More formally, the symbolsFormula 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. `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:- and::@><@->@=
*(1st) and (2nd) are both true*,raining and windy

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

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

- if_then_::@><@->@=
*either (1st)is false or (2nd) is true*,if raining then I_get_wet.

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

Sometimes it useful to express an implication in*clausal form*: - and::@><@->@=
- (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- 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. - 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

for all Numbers n,....

as short forfor 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: - |- (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.

## Notes

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

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

*. . . . . . . . . ( end of section Notes)*<<Contents | End>> - 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

Let

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

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 ]

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.

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

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

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.

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