How are proof techniques formulated in mathematical logic?

How are proof techniques formulated in mathematical logic, for example:

• direct proof,
• proof by contrapositive,

Are the following some possible ways?

1. This Wikipedia article formulates them as some logical equivalence identities. How are the identities used in proofs as proof techniques? Is it by "if $$\phi$$ and $$\psi$$ are logically equivalent, then $$\Phi \models \phi$$ iff $$\Phi \models \psi$$ for any set $$\Phi$$ of formulas" and "if $$\Phi$$ and $$\Psi$$ are logically equivalent, then $$\Phi \models \phi$$ iff $$\Psi \models \phi$$ for any formula $$\phi$$"?

2. Does p35 of Ebbinghaus' Mathematical Logic formulate proof by contraction at some metalanguage level using "iff" to connect two instances of $$\models$$?

4.4 Lemma. For all $$\Phi$$ and all $$\phi$$, $$\Phi \models \phi$$ iff not Sat $$\Phi \cup \{ \neg \phi \}$$.

How are other proof techniques formulated at some metalanguage level using "iff" to connect two instances of $$\models$$?

3. Ebbinghaus' Mathematical Logic formulates proof by contradiction and proof by contrapositive, as some inference rules in the sequent calculus, e.g. IV.2.4 Contradiction Rule (Ctr) on p63 for proof by contradiction, and IV.3.3 Contrapositon Rules (Cp) on p64 for proof by contrapositive. Notice that the inference rules are one-directional, while proof techniques are bi-directional by nature, which the other possible ways of formulations have shown. So how can inference rules be used for representing bi-directionalness of proof techniques?

4. What are other ways for formulating proof techniques, if any?

Thanks.

• There seems to be a negation sign missing in the quote. – tomasz Sep 6 '20 at 15:54
• Usual rules of inference of propositional and predicate logic formalize the "basic" proof technique. See Natural Deduction – Mauro ALLEGRANZA Sep 7 '20 at 14:28
• See e.g. the rule of Negation Introduction: "if $\Phi, \varphi \vdash \bot$, then $\Phi \vdash \lnot \varphi$". Lemma 4.4. above is the semantical counterpart of the rule. – Mauro ALLEGRANZA Sep 7 '20 at 14:30
• @MauroALLEGRANZA What is the semantical counterpart for proof by contrapositive? – Tim Sep 8 '20 at 12:22
• What does it mean? Please, be precise with references... In Ebbinghaus, page 64, there are four Contraposition rules: each one “implement” a valid argument. Example: if $\Gamma \varphi \vDash \psi$, then $\Gamma \lnot \psi \vDash \lnot \varphi$” – Mauro ALLEGRANZA Sep 8 '20 at 12:27

If $$P$$ is a proposition, then $$P$$ is equivalent to $$\neg P\Rightarrow false$$.