[FOM] free logic

[Harvey Friedman]

On Tue, Oct 27, 2015 at 6:11 PM, Joe Shipman <joeshipman at aol.com> wrote:
> Has inadequate attention to these issues ever resulted in failure to prove a mathematical theorem that was proved after more care had been taken?
>
> Has inadequate attention to these issues ever resulted in a proof of a false mathematical proposition being published?
>
> I think not, and that these issues are important only for mechanizing proof assistants (which is indeed valuable), but I'd be interested to be shown to be mistaken about this.
>
> -- JS

Probably no for the first two. However, the third statement, the
conclusion, is not warranted.

Just an example (the main one I am thinking of): I have pushed a
program over the years of analyzing the structure and complexity of
mathematical definitions and mathematical statements, as a subject in
and of itself, not involving proofs. For this, you really want to have
a hard nosed rigorous formalization of mathematics - even without
proofs. Otherwise, the project is not suitably well defined.

Harvey Friedman