Thread: Formal proof

Hi guys

I am a beginner at FOL, trying to prove sentence1 implies sentence 2. I have followed some steps, but I am not able to formally write a proof. Please see and correct.

sentence 1
CPlusPlus program C Turning Machine Mc Instance I Mc(I)=C(I)

sentence 2
Problem P [
CPlusPlus program Cp Instance I Cp(I)=P(I)

Turning Machine Mp Instance I Mp(I)=P(I) ]


So first I assume sentence 1 is right. My first question is what should I note after this assumption? How to state the facts?


Now I say
for arbitrary problem P, it is true that
CPlusPlus program Cp Instance I Cp(I)=P(I)

and prove
Turning Machine Mp Instance I Mp(I)=P(I)


So I say something like
Let Mp1 be a Turning machine for arbitrary instance I. then we have assumed Cp(I)=P(I) from sentence 2 part 1, and from sentence 1 I know Cp(I)=Mp1(I) therefore we have Mp1(I)=P(I)


Could you help me write this formally?

Thank you so mcuh.
Jungar








Thanks
Jungar

First, Cp is a function in the expression Cp(I) since it is applied to an argument. First-order logic does not allow quantifying over functions. You can replace Cp(I) by R(Cp, I) where R (for "result") is a predicate symbol, and similarly for Turing machines (TMs) and problems.

Second, since you mention TMs and C++ programs, you should appreciate the fact that they are syntactic objects constructed using specific rules. A TM is not a C++ program, which is not a Java program, even if all three solve the same problem. So, if you need a formal proof, please specify the proof calculus, which is also a requirement is this sticky thread. Without it, you can only write an informal proof, which is similar to a description of an algorithm in English.