[FOM] Additional expressiveness of free logic

[Lawrence Paulson]

> On 28 Oct 2015, at 02:37, Harvey Friedman <hmflogic at gmail.com> wrote:
> 
> If "Advocate" is meant in the general sense, I don't agree. If
> "Advocate" means "Advocate for Provers" then I agree with some form of
> this.

It looks like I need to clarify my remark about “imposing unreasonable costs”. Under this I do not include the difficulty of implementing a proof assistant, because our job is to build things and let the computer do the work. The costs rather are those imposed on users who have to work within the free logic. I often compare theorem proving in a formal logic to building a ship in a bottle, and nobody wants to make the bottle any smaller, or the ship any bigger. To be more precise, I have seen proof-theoretic work showing that very small changes to a proof calculus can increase the length of a formal proof, in the worst case, by a non-elementary factor. It isn’t obvious that the use of a free logic would be as costly as that, but I get the impression that users who have tried such systems have not been happy with the effort involved. I don’t believe that good automation could entirely eliminate this effort.

> On 27 Oct 2015, at 10:58, Anthony Coulter <fom at anthonycoulter.name> wrote:
> 
> Free logic is required if you want to support partial functions on
> undecideable domains in intuitionistic logic. See:
>  http://cs.nyu.edu/pipermail/fom/2015-September/019169.html
> 
> 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:

By referring to intuitionistic logic, you are moving the goalposts by light years. Most of us are working in classical logic, where the situation is much more straightforward. I would hardly want to judge the competing claims to be the right calculus for intuitionistic logic, as proposed by people such as Martin-Löf or Feferman or as implemented in systems such as Coq or Agda. And we have this key paper on free logic:

	Dana Scott. Identity and existence in intuitionistic logic. In: Applications of Sheaves
	Springer LNM 753 (1979) pp 660-696.

Coq users would probably say that their calculus prevents the introduction of undefined expressions (as type checking will reject them).

The discussion of various fine points concerned with free logic only compounds my concerns. I’m particularly concerned by the suggestion that { 1/0 } could denote the empty set. Let’s instead consider 0^0: once it was undefined, but later, Donald Knuth decided to put 0^0 = 1. If we regard an undefined expression as something that we don’t know much about, then it’s natural to see { 0^0 } as a singleton set about which we know little, and later we might learn that this set is in fact equal to {1}.

As another example, suppose we define \alpha = 1 provided the continuum hypothesis is true and \alpha = 2 otherwise. Given that the continuum hypothesis appears to be completely unknowable, such a definition looks absurd. But it is absolutely normal to define \alpha to be that ordinal such that \aleph_\alpha equals the cardinality of the continuum. One can go on to prove various things about \alpha. But this definition is just as contingent as the previous one.

Ultimately it’s a personal judgement, but I’m perfectly content with the idea that we know more about some things than we do about others, at least in the context of reasoning within a formal calculus, where proofs are difficult enough already.

Larry Paulson