[FOM] Additional expressiveness of free logic

[Harvey Friedman]

On Tue, Oct 27, 2015 at 6:58 AM, Anthony Coulter
<fom at anthonycoulter.name> wrote:
>> Advocates of free logics really have to prove that they can deliver
>> useful additional expressiveness without imposing unreasonable costs.
........

I am only replying to this opening statement.

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.

Free logic is one of many essential components needed for a really
good clean completely rigorous formalization of mathematics.

NOTE: I have always emphasized that mathematicians generally don't
care at all about this, and don't need this, but a growing number are
starting to care some, as they begin to appreciate what can and might
be accomplished by Provers, which still have a long way to go to be
sufficiently friendly for (regular use by) substantial groups of
mathematicians.

I am simply interested in absolutely rigorous formalization of
mathematics in a way that reasonably optimizes friendliness and
faithfulness. As Arnon Avron has pointed out so well, substantial
modifications of what mathematicians actually write and teach needs to
be made (even though mathematicians have learned to get along just
fine with their business as usual and don't need to make these changes
for their practical reasons).

Free logic is but one of dozens of devices needed to accomplish this.
There are no substantial intellectual costs - and far less than
alternatives. Yes, I am aware that with Provers, there are going to be
costs, and the Prover community generally isn't going to adopt free
logic because of this cost, unless they "know" in advance that there
are big benefits. I am not in a position to argue at this point what
those big benefits are, without the development of a proper body of
examples - except to say that I have the genuine feeling that ANY even
small flaw at the foundations of Provers is likely (in my opinion) to
exponentiate wildly out of control when it comes time for industrial
strength Provers. This is at the crux of my interest in starting on
paper at square one (or square zero).

Harvey Friedman