At 10:55 27/04/04 -0400, Kory Heath wrote:

At 10:17 AM 4/27/04, Bruno Marchal wrote:

Don't worry, I will try NOT to give a 120h course in

mathematical logic which is just impossible without chalk &

black board. But I will try to give some insights. I must think

how to do it. It will help me, btw, to prepare my talk in Paris

and Amsterdam so that any critics is welcome.

Ok! I'm very interested to hear it, and I'll let you know where I'm confused, and where I'm bored. :)

Yes but I must go now. Mmmh... I should definitely connect myself at home.

I will do asap.

Here is a beginning.

1)we will interview a simple machine which has very basic beliefs in number theory.

The most well know "Escherichia Coli"-machine of that

sort is know as PEANO ARITHMETIC PA.

It is an extension of classical logic CL. Originally Godel worked with

the PRINCIPIA MATHEMATICA machine instead, but the proof will work

for a *very vast* class of machines (and even more).

2) Godel showed how to translate metaproposition (talk on proposition) into

the language of arithmetic used by PA (talk on numbers), and this by

coding the alphabet by numbers, formula by suitable sequence of numbers,

proof by sequences of sequences of numbers.

He got an arithmetical formula B(x,y) such that PA proves B(n,m) if and

only if m is a code of a proof of a formula coded by n.

And so he got easily from that a formula Bew(x) (for beweisbar = provable

in German), which means intuitively that x represents a provable formula.

Obviously (?) Bew(x) can be defined by EyB(y,x). OK?

Note that B(x,y) is decidable. Do you understand that any one patient

enough can verify if B(n, m) is the case or not, in finite time.

Do you intuit this is no more obvious for Bew(n)?

I surely should say a little more about what is a proof in or by PA, and

more about what is PA for those who never did heard about her before.

Here is an attemp of a cut and paste from chapter 2 of Conscience et

Mecanisme (+ minor translation in english...)

http://iridia.ulb.ac.be/~marchal/bxlthesis/Volume1CC/4z1_2sansp.pdf

giving you an explicit presentation of PA.

Axioms

1) A->(B->A) (a posteriori principle)

2) (A->B)->((A->(B->C))->(A->C))

3) A->(B->A&B)

4) (A->C)->((B->C)->(AvB->C))

5) A->AvB

6) B->AvB

7) A&B->A

8) A&B->B

9) (A->B)->((A-> B)-> A)

10) Av A (exclude middle principe)

Inference Rules:

MP) A, A->B => B (I will say more about that)

Quantifiers rules:

QE1) A(t)->.xA(x)

QE2) A(x)->B => .xA(x)->B

QU1) .xA(x)->A(t)

QU2) B->A(x) => B->.xA(x)

**PA non logical axiom:**

1) (0 = SUC(x))

2) (SUC(x) = SUC(y)) -> x = y

3) x+0 = x

4) x+SUC(y) = SUC(x+y) ; recursive definition of addition

5) xx0 = 0

6) xxSUC(y) = (xxy) + x ; recursive definition of multiplication

And the the following infinite set of induction formula (one

for each formula A you can express in PA language).

A(0) & .x{A(x) -> A(SUC(x))} -> .xA(x)

Comments? Questions? I surely need to explain

what is an inference rule for the non logician.

-Bruno