Are Multiple Substitutions Allowed in Proofs?

[Alternamaton]

I'm reading Introduction to Mathematical Logic gy by Vilnis Detlovs and Karlis Podnieks, and I'm confused about proofs.

In the book, it says that to prove directly you should find ways to substitute the hypoethesis formula(s) into one of the axiom schemas so that other formulas will be implied, with the goal of ultimately leading to the conclusion which one wishes to prove.

However, I'm a bit unsure about what types of substitutions are allowed. For instance, take the following axiom schema, "L2":

A -> (B -> C) -> (A -> B) -> (A -> C)

Can I substitute the same letter in a hypoethesis formula for more than one letter in the schema? For instance:

Hypothesis: A -> (A -> C)

Conclusion: (A -> A) -> (A -> C) (L2)

Where the A from the hypothesis is substituted for A and B (consistently) in the axiom schema.

Is this "valid" (to use the word imprecisely)?

Thanks.

 

[AKG]

Does it say anywhere that A and B have to be different?

 

[Alternamaton]

No, and I assumed that I could substitute a single letter twice. It phrases the axioms, as "[some formula including A B and C] for any formulas A, B, and C." It doesn't say anything like "for any unique formulas...".

If you have any experience with formal languages, do you think it would be paranoid to assume that I'm doing my proofs incorrectly because I'm substituting the same letter twice?

 

[AKG]

If it says "for any formulas A, B, and C" then A and B can indeed be the same. So yes, you are being paranoid ;).

 

[Alternamaton]

Heh, thanks. :)