Re: Minimal logic valid?

Jan Burse <janburse@xxxxxxxxxxx> writes:

Alan Smaill schrieb:
You did suggest that single succedent sequent calculus corresponds to
natural deduction, yet the most natural system obtained from classical

There is something to multi sukzedent calculi and classicality.
Because to be able to move things in multiple to the left side,
needs some form of negation:

G, ~A |- D
----------
G |- A, D

So in a minimal logic, which has no double negation elimination
we will have problems in pursuing a multi sequent calculi.

But because multi sukzedent calculi allow classicality, but do
not allow non classical logic, does not imply that single
sukzedent calculi are not ammeneable to classical logic.

I agree to that (and have already agreed this point earlier
in the thread).

You are subject to the simple fallacy of uniqueness of
examples:

P(a) -> forall x(P(x) -> x=a)

P(x) : calculus x can do classical logic
a : multi sukzedent calculi

You can replace P also by "can do classical logic naturally",
"can do classical logic ....", put your favorite adjective
"..." here.

How do you measure these adjectives, natural, etc.. They are
not logical notions. But to be a little scientifc you need
measurable conditions.

More scientifically, I note that it is the case in most
constructive logics that a proof of some x.P(x) yields
a term in the language such that P(t) is provable;
in corresponding classical cases this is not the case.


If you give me a classical multi sequent calculus, I will
give you a corresponding natural deduction style calculus,
with the same order of proof depth.

The reason is that we instead of a rule:

G |- A, B
----------
G |- A v B

We could also use a rule:

G, ~A |- B
----------
G |- A v B

BECAUSE we are classical. And we will thus stay as a natural
deduction style calculus. And guess the proofs will have
the same shape.

I find this unsatisfactory as an argument, because the proof system
you end up with loses a basic property of sequent calculi which
makes them well suited for proof search, as Gentzen already noted,
namely producing analytic proofs -- proofs where all the formulas
appearing in the proof are subformulas of the original formula.
The notion of analytic proof is scientific.

Do you find anything in the comparison between Gentzen's
sequent and ND calculi for intuitionist logic that suggests
another, more scientific, criterion for distinguishing
between the ND and sequent formulations? From what you have said
so far, there seems no grounds for making a distinction ND/sequent
in this case at all. For me, the discharging of hypotheses
in the ND case is what makes the difference.


Bye

--
Alan Smaill
.