[FOM] The unbearable ghastliness of EFQ, and Tim Chow's focusing question

[Harvey Friedman]

On Sat, Sep 5, 2015 at 1:09 PM, Tennant, Neil <tennant.9 at osu.edu> wrote:
> Tim Chow has focused on the critical issue:
>
.....
......

> Counterexample:
>
> ~A |- A->B  but not ~A,A |- B.
>
> The Core Logician countenances such failures with equanimity, resorting as
> usual to the upbeat observation that the failure of yet another cherished
> but over-valued 'general principle' can be turned into potential epistemic
> gain.

So let me summarize my position more clearly than I have previously.
And the research that this interchange has suggested for me - research
that of course can be viewed as tangential to the interchange.

1. Mathematicians, including myself, actually write down proofs whose
obvious formalization involves reasoning from contradictions to
arbitrary assertions. This is done at various levels in proofs -
sometimes deep inside, sometimes not. Often when case splitting. It is
very convenient and considered legal.

2. Any formalization of mathematical proofs that does not allow 1
explicitly, without modification, is not an adequate formalization for
mathematics, for the purpose of investigating actual mathematical
proofs.

3. Generally, results to the effect that restricted systems - perhaps
not reflecting important features of existing mathematical proofs -
are strong enough to derive all statements, or all statements of a
certain form, even with or without turnstiles, can definitely be of
interest.

4. With regard to Tennant's system Core Logic. We have been talking
about it for propositional logic only. And the basic result is that a
sentence of propositional logic is provable in classical CL if an only
if it is provable in classical propositional logic. Also is provable
in intuitionistic CL if and only if it is an intuitionistic
propositional logic.

5. However, as the above Tennant Counterexample illustrates, the
turnstile derivability's in classical CL are NOT the same as the
turnstile derivabilities in classical propositional logic. QUESTION:
Is there a completeness theorem for the turnstiles that are derivable
in classical CL? Putting it differently, can we characterize the
turnstiles that are derivable in classical CL? In particular, is there
an interesting large class of turnstiles such that if they represent
tautologies then they are derivable in classical CL?

6. I look for new restrictions on reasoning that do make a difference,
rather than restrictions that are shown to not make a difference. The
idea of totally removing negation is a rather intriguing idea. I know
it has been around. I remember seeing something very classical about
this when I was a student in the mid 1960s, and being totally
fascinated by it. But I don't think it was carried too far way back
then, and I quickly went on to some other things.

7. So after some initial results on negation free arithmetic, I am
planning to move this topic onto my numbered postings. But let me ask
the readership what they have seen of interest about negation free
formalizations for mathematics?

Harvey