[FOM] Additional expressiveness of free logic

[Mario Carneiro]

On Tue, Oct 27, 2015 at 6:58 AM, Anthony Coulter <fom at anthonycoulter.name>
wrote:

> The gist of the problem is that if you wanted to formalize Errett
> Bishop's book "Constructive Analysis," you would run into a problem
> because these two sentences are NOT intuitionistically equivalent:
>
>    all real a,b: b != 0 -> exists c: a = b*c   -- Weaker (and true)
>    all real a,b: exists c: b != 0 -> a = b*c   -- Stronger (and false)
>
> The trouble is that if (a/b) always exists (even in places where it is
> undefined), then the stronger sentence is an immediate consequence of:
>
>    all real a,b: b != 0 -> a = b*(a/b)
>
> This is the reason I was finally won over by free logic.


I work with a formal system based on ZFC with classes, and although we
don't usually pursue intuitionistic logic it is formalizable and some work
has been done in this direction. In this case we can define iota x: P[x] =
union {y| {x|P[x]} = {y}}, in which case we can prove that if {x|P[x]} is a
set, then (iota x: P[x]) c= union {x|P[x]} and hence iota x: P[x] is
unconditionally a set by separation. (This is not a free logic - if NOT(Exu
x: P[x]) then iota x: P[x] = emptyset. In classical logic we can prove that
iota x: P[x] is a set under no assumptions, because it is either empty or
the union of a singleton, but this requires Exu x: P[x] to be decidable.)
Therefore we also have the bare statement

all a,b in R: exists c: b != 0 -> a = b*c

being true. However, this is not a very useful statement because it is
missing a type annotation for c; the actual set in which c lives here is

all a,b in R: exists c in pow(union R): b != 0 -> a = b*c

which is not strong enough to even show that the multiplication at the end
is well-defined. Of course it is well-defined, but we can only prove that c
has the correct type after the b != 0 assumption:

all a,b in R: exists c in pow(union R): b != 0 -> (c in R /\ a = b*c)

so in particular we have

   all real a,b: b != 0 -> exists real c: a = b*c   -- provable
   all real a,b: exists real c: b != 0 -> a = b*c   -- unprovable

I don't see how this state of affairs is in violation of other tenets of
intuitionistic logic.

Mario
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20151027/4781ae5b/attachment.html>