Formal systems in which $\forall x \in \mathbb{R}(x \neq 0 \rightarrow x^{-1} \neq 0)$ is true, but the contrapositive is disallowed.

Question

Question. Are there any formal systems out there for which $$\forall x \in \mathbb{R}(x \neq 0 \rightarrow x^{-1} \neq 0)$$

is true, but the contrapositive

$$\forall x \in \mathbb{R}(x^{-1} = 0 \rightarrow x = 0)$$

is "ill-formed" or "ill-typed" (or whatever)?

Motivation 0. This seems to accord well with mathematical practice; in the sense that if you asked a typical mathematician whether or not the first statement was true, they'd probably say 'yes', but if you asked them whether the second statement was true, they'd probably start feeling uncomfortable, and probably suggest adjoining an $x \neq 0$ premise.

Motivation 1. I'm interested in whether there's formal systems out there that provide convenient ways of reasoning about functions whose domain isn't exactly what you wish it were.

Also, please, no answers of the form "this makes no sense because..." I think that, as a general rule, jumping to these kinds of conclusions too quickly is stifling and just an all-round bad idea.

Answer 1

I addressed this in a comment on some SE answer I can no longer find. One way is to adopt guarded conditionals like the ternary operator in programming language, which allows us to enforce syntactic type-checking restrictions. In general one would probably like to have at least: $\def\imp{\rightarrow}$ $\def\cand{\mathbin{?\land}}$ $\def\cimp{\mathbin{?{\rightarrow}}}$ $\def\then{\mathbin{?}}$

$A \cand B = ( A \then B : \bot )$.

$A \cimp B = ( A \then B : \top )$.

Then in the context where $x$ is real, "$x \ne 0 \cimp x^{-1} \ne 0$" is syntactically valid and true, because "$x^{-1}$" is valid in the subcontext where $x \ne 0$. In contrast "$x^{-1} = 0 \imp x = 0$" is syntactically invalid and hence meaningless since $^{-1}$ is a function that only accepts nonzero reals.

Division by zero is just one example, but it is not a very good one because some people would just force $0^{-1} = 0$ in the formal system so that they can get away with not solving the problem. However, there are many other instances of such things which are not so easily solved. For example, one instance of Bolzano-Weierstrass theorem is: $\def\nn{\mathbb{N}}$ $\def\rr{\mathbb{R}}$

Given any function $f : \nn \to [0,1]$, there is some $c \in [0,1]$ such that, for any $k \in \nn$, there is some $n \in \nn$ such that $f(n) \in [c-\frac1k,c+\frac1k]$.

But "$f(n)$" is syntactically valid only if $f$ is a function! We have two options:

1. Use guarded conditionals in the same way as for the real inverse, namely as in the sentence "$\forall f\ ( f \in Func(\nn,[0,1]) \cimp \cdots )$".

2. Allow restricted quantifiers such as "$\forall f \in Func(\nn,[0,1])$" and therefore we can allow the use of $f$ under the scope of quantification as a function.

The division example could be stated using the second option as in "$\forall x \in \rr_{\ne 0} ( x^{-1} \ne 0 )$", but to define "$\rr_{\ne 0}$" probably still needs the first option as in "$\{ r : r \in \rr \cand r \ne 0 \}$". The 'converse' that is as you say ill-formed would indeed be syntactically invalid, because "$\{ r : r \in \rr \cand r^{-1} \ne 0 \}$" is invalid.

Anyway I prefer having both options. Unfortunately, I don't know enough about existing computer proof assistants to tell you whether any of them support this. Probably any system that has a strict type system will support this, but potentially not allow you to do mathematics as freely as you might want. (Coq does not allow subtyping. Mizar does but its types are only in the sense of abbreviation power.)

Answer 2

To my knowledge, there are no very well-known systems that handle this sort of thing. "Real" natural-language mathematics is done in a kind of free logic where particular terms (such as $0^{-1}$ and $0/0$) are undefined.

Ordinary first-order logic does not handle undefined terms at all. There are "free logics" which do allow for undefined terms, but they do not match all the subtleties of natural-language mathematics. In particular, both of the formulas in the question are well-formed in free logics - these logics do not try to modify which formulas are well-formed, they only try to handle reasoning with formulas that may involve undefined terms.

Part of the challenge is that natural-language mathematics does not separate the syntax from meaning in the same way that formal systems do. Formal logic tends to begin by defining a class of uninterpreted formulas, and then assigning them a meaning. Mathematicians tend to treat a natural-language statement as mathematical (that is, as a "proposition") exactly when it has an unambiguous meaning. So the directions are reversed.

Of course, there is a standard way to handle these things in first-order logic, which is replace all function symbols that might be interpreted as partial functions with relation symbols, and then rewrite formulas accordingly. Then the only terms are constants and variables, so the issue of undefined terms goes away. A prototype of this is seen, for example, in the usual language for fields, which is $(+, \times, 0, 1)$ and not $(+, \times, {}^{-1}, 0, 1)$, and $y = x^{-1}$ is treated as a binary relation $I(x,y) \equiv xy = 1$. So $(\forall x)(x \not = 0 \to x^{-1} \not = 0)$ becomes either $$ (\forall x)(x \not = 0 \to (\forall y)[I(x,y) \to y \not = 0]) $$ or $$ (\forall x)(x \not = 0 \to (\exists y)[I(x,y) \land y \not = 0]) $$ which are equivalent over the axioms for a field.