How are proof techniques formulated in mathematical logic?

Question

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

Are the following some possible ways?

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$"?
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$?
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?
What are other ways for formulating proof techniques, if any?

Thanks.

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

Wuestenfux · Accepted Answer · 2020-09-06 15:42:11Z

1

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

answered Sep 6 '20 at 15:42

Wuestenfux

16.2k2 gold badges8 silver badges21 bronze badges

add a comment |

1 Answer 1