Wikipedia:Reference desk/Archives/Mathematics/2022 August 14

Welcome to the Wikipedia Mathematics Reference Desk Archives
The page you are currently viewing is a transcluded archive page. While you can leave answers for any questions shown below, please ask new questions on one of the current reference desk pages.

August 14

Defining new rules of inference and making use of them in formal proofs?

According to converse property and transitivity property of inequalities:

$a<b$ and $b>a$ are equivalent for any real numbers $a$ and $b$.

If $a<b$ and $b<c$, then $a<c$ for any real numbers $a$, $b$, $c$.

May I interpret the above descriptions as the following 2 rules of inference

${\begin{array}{l}a\!\in \!\mathbb {R} \\b\!\in \!\mathbb {R} \\\hline \therefore (a<b)\leftrightarrow (b>a)\end{array}}$ (Rule A)

 

${\begin{array}{l}a\!\in \!\mathbb {R} \\b\!\in \!\mathbb {R} \\c\!\in \!\mathbb {R} \\a<b\\b<c\\\hline \therefore a<c\end{array}}$ (Rule B)

so that I could use them in, for example, the following proof?

Prove that $x<z$ if $z>y$ and $x<y$ for real numbers $x$, $y$, $z$.

Step	Proposition	Derivation
1	$(z>y)\land (x<y)$	premise
2	$x\!\in \!\mathbb {R}$	premise
3	$y\!\in \!\mathbb {R}$	premise
4	$z\!\in \!\mathbb {R}$	premise
5	$(y<z)\leftrightarrow (z>y)$	Rule A (3, 4)
6	$(y<z)\land (x<y)$	Material equivalence (1, 5)
7	$x<y$	Conjunction elimination (6)
8	$y<z$	Conjunction elimination (6)
9	$x<z$	Rule B (2, 3, 4, 7, 8)

I guess that we should define some rules of inference for inequalities before we can incorporate them in a formal proof, right?

(I don't know if the proof is valid or not because I'm not able to find similar examples on the internet.) -- Justin545 (talk) 07:13, 14 August 2022 (UTC)

I think your thinking of something like Natural deduction. There are many different notations and sets of axioms and rules of inference, so a lot depends on personal preference. But any reasonable system can be proven equivalent to classical deductive logic, making allowances of course for the law of excluded middle and other variations. There has always been a "gap" between formal logic and the way mathematicians actually use logic in proofs. There have been many attempts to bridge that gap, some quite successful, but I don't think a "standard" has really emerged. There are many computer proof assistants that fill in proof details automatically, and they use this type of formalized reasoning. --RDBury (talk) 23:22, 14 August 2022 (UTC)

Thanks for the reply. I have tried to read Natural deduction, but it seems to be obscure to me. For example, I failed to understand the following inference rule in Hypothetical derivations:

${\cfrac {\begin{matrix}{\cfrac {}{A{\hbox{ true}}}}\ u\\\vdots \\p{\hbox{ true}}\end{matrix}}{\lnot A{\hbox{ true}}}}\ \lnot _{I^{u,p}}$

Therefore, I think I am more used to formal proofs in tabular notation or tabular form which also appear in "Proof" section of Destructive dilemma and Negation introduction. The main problem would be the lack of concrete example of formal proofs which have connections with mathematical formula (equations, identities, inequalities, etc.). Computer proof assistants would be a direction to find the connections. Hopefully I can find more examples of formal proofs in tabular form there. -- Justin545 (talk) 20:21, 15 August 2022 (UTC)

The following is a justification of the negation rule $\neg _{I^{u,p}}.$ Using instead the implication rule $\supset _{I^{u}},$ the conclusion of the derivation would have been $A\supset p~{\hbox{true}}.$ Since $p$ could have been any proposition not occurring in $A,$ we could have made the same derivation using $\neg A$ instead of $p,$ leading to the conclusion $A\supset \neg A~{\hbox{true}}.$ Since Aristotle, this has been understood to be equivalent to $\neg A~{\hbox{true}}.$  --Lambiam 05:24, 16 August 2022 (UTC)

Is inference rule $\neg _{I^{u,p}}$ equivalent to modus tollens ${\frac {A\to p,\neg p}{\therefore \neg A}}$? It seems that $p$ must not occur in the conclusion $A$ is due to "The introduction rule DISCHARGES both the name of the hypothesis u, and the succedent p" but I'm not able to confirm that. I'm not sure what "discharge" mean because I didn't see explicit explanation for "discharge" in Natural deduction... -- Justin545 (talk) 08:24, 16 August 2022 (UTC)

A very simple case of $p$ occurring in $A$ is when $A$ is identical to $p.$ Clearly, having successfully derived $p\supset p~{\hbox{true}},$ one should not infer from this conclusion that $\neg p~{\hbox{true}}.$ So there has to be be some restriction on $A$ with regard to $p.$ The simplest restriction that does the job is that $p$ must not occur in $A.$ Forget for a moment all formality, and think of how a working mathematician works on a proof. She may be heard mumbling, "Assume $m$ is even. Then ... Therefore $m\equiv 0~{\hbox{(mod 4)}}.$" She then jots down, "$m\equiv 0~{\hbox{(mod 2)}}~\supset ~m\equiv 0~{\hbox{(mod 4)}}$" and starts to examine the case that $m$ is odd. At this point, the earlier assumption that $m$ is even is no longer in play – it has served its purpose and has been honourably discharged.  --Lambiam 14:55, 16 August 2022 (UTC)

The sentence "one should not infer from this conclusion that $\neg p~{\hbox{true}}.$" reminds me that I noticed both ${\cfrac {}{A{\hbox{ true}}}}\ u$ and $\lnot A{\hbox{ true}}$ appearing in $\neg _{I^{u,p}}$. It looks like the presence of ${\cfrac {}{A{\hbox{ true}}}}\ u$ and $\lnot A{\hbox{ true}}$ in $\neg _{I^{u,p}}$ is equivalent to $A\land \neg A{\hbox{ true}}$ which seems that there is a contradiction between ${\cfrac {}{A{\hbox{ true}}}}\ u$ and $\lnot A{\hbox{ true}}$. I think it was the possible contradiction in $\neg _{I^{u,p}}$ confused me so badly and stopped me from going ahead... -- Justin545 (talk) 06:44, 17 August 2022 (UTC)

I may need to reconsider it to know it better. Thank you for patiently answering my questions. -- Justin545 (talk) 08:52, 17 August 2022 (UTC)