A Brief History of Formality

 

 

 

George Boole (1815-1864) developed an algebra for logic, which is still in use today : ANDs, ORs, NOTs, EXORs, etc.

 

 

 

 

Giuseppe Peano (1858-1932) developed a formalization of arithmetic consisting of:

1.    an alphabet (symbols)

2.    a grammar (rules that describe which sequence of symbols are valid)

3.    axioms (sequence of symbols assumed to be true)

4.    rules of inference (how one sequence may be converted to another)

 

 

 

David Hilbert (1862-1943) influenced mathematics the early part of the 20th century as many graduate students tried to solve his list of 23 problems (1900). In particular, the last problem, known as “Hilbert’s Tenth Problem,” had a great impact. It asks if a computational procedure (algorithm) exists to determine whether a set of Diophantine (Diophantos of Alexandria, 3rd century, AD) equations has a solution.

 

 

 

 

 

 

Meanwhile, the work of Bertrand Russell (1872-1970) and Alfred North Whitehead (1861-1947) , Principia Mathematica (1910-1913), attempted to totally formalize all mathematical thinking.

 

 

 

Kurt Godel (1906-1978) proved that there would always be statements of a formal system that cannot be determined to be true or false by the axioms of the formal system alone. This is known as the “incompleteness theorem.”

 

 

Alan Mathison Turing (1912-1954) presented a rigorous definition of the term “computation.” All digital computers of today are manifestations of his “Universal Turing Machine” (or UTM). The UTM consists of a tape containing data and instructions, which are written using symbols of an alphabet, according to a grammar. It operates according to the instructions, finally producing a result – or perhaps never stopping. This is what Hilbert was asking: how do we know that the computation will halt? (known as the halting problem).

 

The Millennium Project of the Center for Cognitive Sciences at the University of Minnesota asked for nominations for the top 100 works in cognitive science. The quote below is from the person nominating Turing’s work:

Principia Mathematica begat Godel, and Godel begat Turing, and Turing of course begat all manner of things important to cognitive science...

 

More Recently...

 

Roger Penrose (born 1931) argued why computational approaches alone can never duplicate mathematical thinking – quantum consciousness!

 

 

 

Program a Turing Machine

 

This site http:

 

http://wap03.informatik.fh-wiesbaden.de/weber1/turing/

 

has a TM simulator. Try the following programs:

 

Alternating sequence. Use tape data 1000..01

 

1,1,1,1,>

1,0,2,0,>

2,0,2,0,>

2,1,3,1,<

3,0,3,0,<

3,1,2,1,>

 

Add two numbers. Use tape data 11..1011..10

 

1,1,1,1,>

1,0,2,1,>

2,1,2,1,>

2,0,3,_,<

3,1,H,0

 

Building a Computing Machine...

 

Computing machines may be built around mechanical or electro-mechanical devices (see Zuse).  Turing worked on the Colossus during WW-II.

 


Simple power supply, switch, load circuit.

 

 

 


Control input (switch) is now 'relayed' to the load circuit.

 

 


Load is energized when the switch is not pressed. Implements the logical "NOT" operation.

 

 


The basic building block can be used as a non-inverting buffer, or an inverter (logical NOT operator).

 

 


Many different types of switches may be activated by the relay.

 

 


A two-stage relay circuit. Works but logically not very useful. (Sometimes used to activate a larger relay from a smaller one.)

 

 


Circuit implements combinatorial logic...

 

 


...that could have been implemented also by simple switches.

 

 


A sequential logic circuit that cannot be implemented by simple switches. This is called a "latch" circuit, because the output latches on to the input. Once activated, the output cannot be turned off (pull the plug?).

 

 

 


The electrical circuit diagram readily translates into an equivalent "ladder logic" schematic. Ladder logic is used by industry to describe control operations. It is a visual description of both the hook up diagram and the control task it performs.

 

 


Common gates.

 

 

 


Schematic of a latched "ON" button.

 

 

 

 


A Set-Reset (SR) flip-flop is a bi-stable device. If both buttons are pressed, the output is on. It is said that the "on button dominates."

 

 

 


The inverter (NOT) is used so that when both buttons are pressed, the output is off. Now the off button dominates – useful if the off button is an emergency stop!

 

 

 

 

 

 

Sequential logic circuits that rely on a “clock” signal play a central role in contemporary machine computing.

 

 

Use the Boolean Expression Evaluator to study the behavior of this circuit.

 

Sequential logic outputs are a function of not only the current inputs, but also of the past inputs. In certain cases, the outputs may also be a function of initial conditions. This implies that the system as a whole “remembers” the sequence of states visited. Hence, sequential logic is said to have memory. Obviously, the past inputs are not explicitly presented to the system. This would require an external memory, defeating the entire purpose. Rather, some of the outputs are redirected as inputs. Since the outputs were functions of previous inputs, so are the current outputs dependent on the previous inputs. Think about it -- ingenious, eh?

 

 

Tidbits...

 

Turing also worked at Bletchley Park during WW-II to break the German Enigma cipher. The Colossus, the then-top-secret first electronic computers were scrapped and burnt in the mid 70s.

Hilbert’s Tenth Problem was finally resolved in 1970 by Yuri Matiyasevich: there can be no algorithm that would systematically determine if a system of Diophantine equations has a solution.

Penrose worked on the tiling problem, which is often used as an example for non-computability.

A few links

 

Diophantos

http://www-history.mcs.st-andrews.ac.uk/history/Mathematicians/Diophantus.html

 

Boole

http://www-groups.mcs.st-and.ac.uk/~history/Mathematicians/Boole.html

 

Peano

http://www-groups.mcs.st-and.ac.uk/~history/Mathematicians/Peano.html

 

Hilbert

http://www.phy.bg.ac.yu/web_projects/giants/hilbert.html

 

Russell

http://www.mcmaster.ca/russdocs/russell1.htm

 

Whitehead

http://alfred.north.whitehead.com/

http://alfred.north.whitehead.com/wwanw_exam.htm

Godel

http://www.logic.at/kgs/home.html

http://www-groups.dcs.st-and.ac.uk/~history/Mathematicians/Godel.html

A nice summary of the proof may be found at the web site http://www.miskatonic.org/godel.html

 

Turing

http://www.turing.org.uk/turing/scrapbook/machine.html

http://www.turing.net/Alan.Turing.html

http://pass.maths.org.uk/issue5/turing/

http://wap03.informatik.fh-wiesbaden.de/weber1/turing/

http://www-lns.mit.edu/~dsw/turing/turing.html

 

Penrose

http://en.wikipedia.org/wiki/Roger_Penrose

http://dhushara.tripod.com/book/quantcos/penrose/penr.htm

 

Principia Mathematica

Still on sale!

http://www.amazon.com/exec/obidos/ASIN/0521626064/jonradel/002-7938526-8278462

http://plato.stanford.edu/entries/whitehead/

 

On Formally Undecidable Propositions of Principia Mathematica and Related Systems (Godel's proof)

http://www.amazon.com/exec/obidos/ASIN/0486669807/jonradel/002-7938526-8278462

http://www.chaos.org.uk/~eddy/math/Godel.html

http://www.math.hawaii.edu/~dale/godel/godel.html