Hi Kori,
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
http://iridia.ulb.ac.be/~marchal/
Received on Wed Apr 28 2004 - 12:05:04 PDT