Denoting $ac=bc$ by $p,\quad$ $a=b$ by $q\quad$ and $c=0$ by $r,$
$\text{If }ac=bc \text{ and if } c\neq 0 \text{ then }a=b\tag I$
$p\wedge\neg r\to q\tag1$
Correction: $$∀a\,∀b\,∀c\;(Pabc\wedge\neg Rc\to Qab)\tag A$$
$\neg p\to \neg q\vee\neg r\tag2$
$\text{If }ac\neq bc \text{ then }a\neq b \text { or }c\neq 0\tag{II}$
Correction: $$∀a\,∀b\,∀c\;(\neg Pabc\to \neg Qab\vee\neg Rc)\tag B$$
Question: Which of the formal statements $(1),(2)$ correctly formalises the statement $\textrm{(I)}$?
$(\mathrm I)$ is implicitly universally quantified, and is formalised by $(\mathrm A),$ but not $(\mathrm B)$ or $(1)$ or $(2).$
Similarly, $(\mathrm {II})$ is formalised by $(\mathrm B),$ but not $(\mathrm A)$ or $(1)$ or $(2).$
$(\mathrm I),$ i.e., $(\mathrm A),$ is mathematically equivalent, but not logically equivalent, to $(\mathrm {II}),$ i.e., $(\mathrm B).$
in the given
context, where $a,b,c$ are real numbers (or elements of any field for
that matter),
Given a propositional-logic sentence, each interpretation specifies exactly one row of its truth table.
Regarding your propositional-logic sentences $(1)$ and $(2),$ the triples $(1,1,0)$ and $(3,7,1),$ which specify the first and eighth row, respectively, of your truth table, are two interpretations/scenarios. In these contexts, the two sentences are equivalent.
Does the fact that the fourth
and fifth lines are impossible imply that both statements $(1),(2)$
are correct formalisations of $\textrm{(I)}\,?$
No. For a simpler and sillier example, let $A$ and $B$ formalise $\sqrt4=2$ and $\sqrt9=3,$ respectively. Then $A$ and $B$ are both true, yet only $A$ is a formalisation of $\sqrt4=2.$
So, two formalisations being true in a set of contexts/interpretations does not imply that some natural-language sentence that is true in this set is formalised by both of them. What is implied, however, is that in this set of interpretations, their natural-language counterparts are equivalent to each other (that is, have the same truth value).
It is indeed true the falsehood of $p \to q$ implies $p$ is true and $q$ is false. In other words, it is indeed true $\neg (p \to q)$ imples $p \wedge \neg q$. You have presented a semantic proof of a valid argument form that doesn't have a name (that I'm aware of). This should not be suprising because there are many, many valid argument forms that can be constructed in a given system.
From a syntactic point of view, every natural deduction system has a "starting" set of inference rules that contains the primitive inference rules of the system, which you can think of as inference rules we simply take for granted to be true. You can use the primitive inference rules to derive other inference rules, but derived inference rules do not allow you to prove anything new that you could not prove apart from the primitive rules. This is because anything proven with a derived rule can be proven by applying some sequence of primitive rules.
For example, suppose a system defined Modus Ponens (MP), Conjunction Introduction ($\wedge$I), and Reductio ad Absurdum (RAA) as primitive rules. Then, one could derive Modus Tollens $p \to q, \neg q \vdash \neg p$ as follows
$
\begin{array}{llll}
\{1\} & 1. & p \to q & \text{premise} \\
\{2\} & 2. & \neg q & \text{premise} \\
\{3\} & 3. & p & \text{Assumption for RAA} \\
\{1,3\} & 4. & q & \text{1,3 MP} \\
\{1,2,3\} & 5. & q \wedge \neg q & \text{2,4 $\wedge$I} \\
\{1,2\} & 6. & \neg p & \text{3,5 RAA} & \square \\
\end{array}
$
Thus, in such a system Modus Tollens is a derived rule, proven by the primitive rules MP, $\wedge$I, and RAA.
So, if we wish, we could take the valid form of inference you mentioned
$\neg (p \to q) \vdash p \wedge \neg q$
and give it a name like "toliveira's rule," but in most natural deduction systems (that I'm aware of) this would be one of many derived inference rules that do not have a name. Some derived inference rules are given names because they are used often, provide useful shortcuts in proofs, or capture our intuition well; others are more obscure. So, in summary I think you're simply observing a valid argument form that doesn't have a flashy name like "Modus Tollens" or "Constructive Dilemma."
Best Answer
You need to have many more implications.
Note that $p\lor q=(\lnot q\Rightarrow p)$ and so $p\land q=\lnot(q\Rightarrow \lnot p)$ in the Lindenbaum algebra of our Boolean algebra. So I'll leave you to build $((A\land B)\lor (B\land C))\lor (C\land A)$.