A question in substitution in logic.

[MathematicalPhysicist]

i need to prove that if x is the first of sub($$\phi$$;a,$$\psi$$) then there exists 1<=i<=n and there exist firsts $$\phi' of \phi_i and \psi' for \psi$$ such that x=sub($$\phi';a,\psi$$)$$\psi'$$

where sub(t;a,b) is defined as follows:
let a1,..,an be n signs and b1,..,bn expressions.
a=(a1,...,an)
b=(b1,..,bn)
the substitution sub(t;a,b) is defined as:
if t is t1,...,tk then sub(t;a,b)=x1x2...xk
when 1<=i<=k xi is bj if ti=aj and xi is ti when ti isn't in {a1,...,an}.

what i did is as follows:
x is the first of sub(t;a,b) then there exists y such that sub(t;a,b)=xy
and let t' be the first of t, then t=t'z and thuse we can deduce that:
sub(t;a,b)=sub(t';a,b)sub(z;a,b)=xy
but i don't know how to procceed from here.
thanks in davance.

 

[MathematicalPhysicist]

i have another question:
let a|=a' and b|=b' then prove that a'->b|=a->b' without using ~a'|=~a and metrial conditional, i.e without using ~PvQ=P->Q.

 

[tacman]

To prove this statement, we can use mathematical induction on the length of the expression t.

Base case: If t is a single sign, then the statement is trivially true.

Inductive step: Assume the statement is true for an expression t of length k. We will prove it for an expression t' of length k+1.

Let x be the first of sub(t';a,b). By the definition of sub, we know that t' is a concatenation of expressions t_1, ..., t_n, where each t_i is either a sign from a or an expression not in {a1,...,an}.

So, we can write t' as t_1t_2...t_n. Since x is the first of sub(t';a,b), we know that x is either a sign from a or an expression not in {a1,...,an}.

If x is a sign from a, then by the definition of sub, there exists 1<=i<=n such that t_1 = a_i.

Now, let t_1' be the first of t_1. Since t_1 = a_i, we know that t_1' is also a_i. Similarly, let t_2' be the first of t_2, and so on.

So, we have t_1' = a_i, t_2' = t_2, ..., t_n' = t_n.

Now, by the inductive hypothesis, we know that there exist firsts \phi' of \phi_i and \psi' for \psi such that t_2 = sub(\phi';a,\psi) and t_n = sub(\psi';a,\psi).

Therefore, we can write t' as t_1't_2'...t_n' = a_it_2'...t_n'.

So, by the definition of sub, we have sub(t';a,b) = a_i sub(t_2';a,b) sub(t_n';a,b) = x sub(\phi';a,\psi) sub(\psi';a,\psi).

Similarly, if x is an expression not in {a1,...,an}, we can use the same argument to prove that there exist firsts \phi' of \phi_i and \psi' for \psi such that t_2 = sub(\phi';a,\psi) and