Si esto vale como definición:
Definición 3
is
subformula of

if:
1-

, or
2-

and

is a subformula of

or of

, or
3-

and

is a subformula of

.
Entonces esto también vale:

,
puesto que "ser subfórmula de" ya está definido previamente. Otra cosa es que este ejercicio se entienda como justificación de que la definición precedente es correcta, pero si es así, tendría que ser previo a cualquier teorema sobre subfórmulas.
Tienes razón. Tu definición de la función

es igualmente válida.
No veo por qué la concatenación de las dos sucesiones de formación tiene que ser una sucesión de formación de longitud mínima.
No estoy seguro de si es cierto o no. Pero hago dos observaciones:
1-No son dos secuencias de formación cualesquiera. Tienen
largo mínimo, una para

y otra para

.
2-No las concatené una seguida de la otra, sino que concatené un pedazo de una a continuación de la otra. Si te fijas en los subíndices, es la primer secuencia de formación, o sea, la de

, a la que le anexé el trozo

. Es más, mi intuición me dice que toda la primer secuencia

es la misma que

a no ser, quizás, por el orden de alguna de las fórmulas. Me baso en la creencia de que si dos secuencias de formación tienen largo mínimo, entonces han de ser la misma (a no ser, quizás, como dije antes, por reordenación de alguna fórmula).
Entonces
debiera poderse probar que

es una secuencia de formación para

de largo mínimo en la que ocurre

. Por el ejercicio
B) apartado ii)

es subfórmula de

.
Ese "debiera poderse" en la demostración debiera cambiarse por "aquí está la prueba". Pero no sé como hacerla. En realidad (en caso de ser secuencia de formación), que es de largo mínimo es bastante inmediato. Porque si suponemos que no es de largo mínimo, hay una fórmula que se puede eliminar. Si eliminas una antes de la ocurrencia de

, tienes que la primer secuencia (o sea la de

, no sería de largo mínimo, lo cual es una contradicción). De la misma manera, si puedes eliminar una fórmula de la tira

también la podrías eliminar de

, ¿o no? Y ésa se supone que es de largo mínimo, por lo que también se llegaría a una contradicción.
Por el contrario, si las fórmulas

y

tienen subfórmulas en común, sus sucesiones de definición tendrán fórmulas en común, por lo que al concatenarlas habrá fórmulas repetidas que se podrán eliminar, luego la concatenación no será de longitud mínima.
Claro, pero ese problema no ocurre (creo) porque lo que se concatenan no son las secuencias enteras, sino que a una se le añade un pedazo de otra.
Por otra parte, en la demostración que yo te he dado del ejercicio B), he usado la transitividad de las subfórmulas, si pretendes usar ese ejercicio para probar la transitividad, necesitarás dar una prueba de B) que no dependa de ella, si no, el argumento sería circular.
Esto sí es incuestionable. Tienes toda la razón, tendría que buscar otra prueba para el ejercicio
B) i). Pero en el hipotético caso que encuentre otra demostración, me gustaría saber si hay fallo en la mía y cómo se puede completar.
Muchísimas gracias por todo lo que me estás ayudando en estos temas, Carlos.
Saludos