1. ## 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
$\displaystyle \forall$ CPlusPlus program C$\displaystyle \exists$ Turning Machine Mc$\displaystyle \forall$ Instance I Mc(I)=C(I)

sentence 2
$\displaystyle \forall$ Problem P [
$\displaystyle \exists$ CPlusPlus program Cp$\displaystyle \forall$ Instance I Cp(I)=P(I)
$\displaystyle \implies$
$\displaystyle \exists$ Turning Machine Mp$\displaystyle \forall$ 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
$\displaystyle \exists$ CPlusPlus program Cp$\displaystyle \forall$ Instance I Cp(I)=P(I)

and prove
$\displaystyle \exists$ Turning Machine Mp$\displaystyle \forall$ 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

2. ## Re: Formal proof

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.