How to write a many-one reduction proof

Writing a proof by contradiction is fairly formulaic--first you assume the opposite, then derive a contradiction. I would like to know the steps and conventions for writing a many-one reduction proof. This answer was somewhat helpful, but like other explanations I've heard, it sounds too similar to a proof by contradiction for me to understand the difference.

My specific points of confusion:

• The exact meaning of $A \leq _{m} B$
• Do we reduce an unknown problem to a known problem, or the opposite
• Does the reduction function transform a known problem into an unknown problem, or the opposite
• How a many-one reduction is different from a proof by contradiction. It seems like a simpler version of the same logic; if so, how is the simplification justified

I am only interested in many-one reductions of language/Turing machine problems (in case the term has meaning in other contexts as well). Any help is appreciated, including links and illustrative examples. Thanks.

A many-one reduction is not a "proof-by-contradiction" per se, it is an application of a theorem. The theorem is:

Let $L,L'\subseteq \{0,1\}^*$, and $L \leq_m L'$. Then, it holds that

1. If $L$ is undecidable, then $L'$ is undecidable.
2. if $L'$ is decidable, then $L$ is decidable.

I will omit the proof, there are plenty of resources where you can read up on it. You can view the statement $L \leq_m L'$ intuitively as "The language $L$ is easier to decide than the language $L'$". And that's what a reduction proof does. You show that one language (the hard, known one, like the halting problem $H_0$) is easier to decide than a new, unknown language $L$. By showing $H_0 \leq_m L$ you've essentially shown (by application of the above theorem) that the halting problem is easier than $L$. Thus, $L$ cannot be decided. So, to answer your questions:

1. $A \leq_m B$ means that the language $A$ is easier to decide than the language $B$.
2. To show hardness, you reduce "YOUR_HARD_LANGUAGE $\leq_m$ SOME_NEW_LANGUAGE". To show computability, you can reduce in the other direction, but usually it's simpler to just construct a TM that solves the given problem.
3. A reduction $L \leq_m L'$ takes an instance $x \in \{ 0,1\}^*$ and does the following with it: If $x \in L$, you make sure that the reduction $f(x) \in L'$. If $x \not \in L$, then the reduction maps $f(x) \not \in L'$. So - if you prove hardness, you transform a known hard problem into the unknown problem.
4. It is a contradiction in the sense of "If I could solve the new problem, then I can solve the hard problem, which cannot be, since it is proven to be hard". This contradiction is hidden in the Theorem above and you just slap it (implicitly) on every reduction you do.

I hope that helped. As I said, my main intuitive approach to reductions is "How could I use a new language $L'$ to solve an old, hard language $L$?".

A many-one reduction is not a contradiction and should not be thought of one, even informally. A many-one reduction from problem A to problem B is an efficient translation of instances of problem A into instances of problem B such that "yes" instances are mapped to "yes" instances and "noes" to "noes".

Even when you use many-one reductions to prove NP-completeness, you're not using contradiction. All you're saying is that instances of every problem in NP can be transformed efficiently into instances of some particular problem. It follows that a deterministic polynomial-time algorithm for that problem would give deterministic polynomial-time algorithms for all problems in NP. But, even here, there is no contradiction: we do not know that P $\neq$ NP so there is nothing to contradict.
{"found_math": true, "script_math_tex": 0, "script_math_asciimath": 0, "math_annotations": 0, "math_alttext": 0, "mathml": 0, "mathjax_tag": 0, "mathjax_inline_tex": 1, "mathjax_display_tex": 0, "mathjax_asciimath": 0, "img_math": 0, "codecogs_latex": 0, "wp_latex": 0, "mimetex.cgi": 0, "/images/math/codecogs": 0, "mathtex.cgi": 0, "katex": 0, "math-container": 0, "wp-katex-eq": 0, "align": 0, "equation": 0, "x-ck12": 0, "texerror": 0}