[FOM] 618: Adventures in Formalization 4

[Anthony Coulter]

Freek mentions the impossibility of setting 1/0 = 0 in Bishop-style 
constructivism because computable functions must be continuous. In fact, 
the problem is more general than that (though it's contained to 
intuitionistic logic).

In intuitionistic logic, the following two schemes are NOT equivalent:
   All x: D[x] -> Exi y: P[x,y]     --- Weaker
   All x: Exi y: D[x] -> P[x,y]     --- Stronger

As it applies to division by zero, we would have that the weak sentence
   All a,b: b != 0 -> Exi c: b*c = a
does NOT imply its intuitionistically-stronger counterpart:
   All a,b: Exi c: b != 0 -> b*c = a

If this doesn't make sense, think about the Dialectica interpretation: 
the first sentence says, "If you give me a pair of numbers a and b, and 
also show me a proof that b != 0, then I can construct a number c which 
satisfies b*c = a." The second sentence says, "Give me the numbers a and 
b and I will construct the desired c *before* you show me a proof that b 
is nonzero."

The two schemes can be proven equivalent from the assumption that
   All x: D[x] or ~D[x]
or in our specific example, that
   All b: b != 0 or b = 0
But in intuitionistic logic this is often not possible. (In the case of 
Bishop-style constructivism, checking whether a real number is zero is 
distinctly *not* decidable.)

Now, most reasonable definitions of division will make it possible to 
prove that
   All a,b: b != 0 -> b*(a/b) = a
 From this it's child's play to prove
   All a,b: Exi c: b != 0 -> b*c = a
by taking c = (a/b). But this isn't an intuitionistically valid 
sentence, so we have to block the existential-introduction rule. That 
means using free logic (also called a logic partial terms) with an 
explicit existence predicate. Then you can require a proof that a/b 
exists before you are allowed to replace it with an 
existentially-quantified variable; this extra rule is enough to block 
the invalid derivation.

So our general rule is: If membership in a function's domain is not 
intuitionistically decidable, then you pretty much have to use free 
logic with an explicit existence predicate. A definition by cases is not 
possible if you cannot determine, intuitionistically, which case applies.