Re: Minimal logic valid?

Alan Smaill schrieb:

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.

A similar note can be made for classical logic. Namely
if we have :

T |- exists x A(x)

Then there are some t_1,..,t_n, such that:

T |- A(t_1) v .. v A(t_n)

In some constructive logic we have always n=1, in
classical logic in the general case we cannot
assume that n=1 will hold.

Here is a simple classical example:

p(a) v p(b) |- exists x p(a)
p(a) v p(b) |/- p(a)
p(a) v p(b) |/- p(b)
p(a) v p(b) |- p(a) v p(b)

But although this note is scientifical, it is
not tied to proofs. You dont make a statement
about a proof object. You make a statement about
the implication from a valid statement to another
valid statement.

So the above lemma with the t_1,..,t_n holds
independent what calculus you use. Whether you
use NK or LK, or whatever. It doesnt give you a
property of a calculus.

And the lemma with n=1 holds independentent
what calculus you use. Whether you us Nx or
Lx, or whatever. It doesnt give you a property
of a calculus.

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.

No, the single sukzedent calculus for classical logic will also
produce analytic proofs. It will also have the sub formula
property, eventually prefixed by a negation sign. But this
is enough to be analytical. Calculi are analytical when the
do not force someone in backward search, to invent a formula.
For example modus ponens is not analytical:

A A -> B
-------------- (MP)
B

It forces you to invent A to prove B. There are analytical
calculi for classical and non classical logic. Its not a
domain of classical logic. Gentzen himself shows with LJ
an analytical calculus for a non classical logic.

But value of analytical proofs is very much dimished by the
fact that a proof might force someone to invent terms.
So this is the real show stopper for analytical proofs
when quantifiers are around, that you need to invent terms.

But you are right, "analyticality" is a property of proofs,
and not a property between valid statements. So you are
on the right track.

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.

For me "natural deduction" is an idiomatic phrase, and
it would never ever come to my mind to search some
meaning in it that is related to a notion of "natural".

What makes "natural numbers" natural?

And the paper by Gentzen implies to me, that "natural
deduction" is categorized as "single sukzedent" "sequent
calculus". "single sukzedent" is the least property
for me so that something falls into the category
of "natural deduction".

What concerns "discharging", because it is available
in "sequent calculus", it is also available in "natural
deduction". That the context changes it shape by losing
formulas is not an exclusive property of "natural deduction".
This regularly also happens in multi sukzedent calculi.

Still awaiting a better definition of "natural" from you.




.

Relevant Pages

  • Re: Minimal logic valid?
    ... constructive logics that a proof of some x.Pyields ... independent what calculus you use. ... give you a corresponding natural deduction style calculus, ... But you are right, "analyticality" is a property of proofs, ...
    (sci.logic)
  • Re: Minimal logic valid?
    ... is the minimal logic I found in the textbook 'Propositional Logics' by ... intuitionistisch) und NK wollen wir den so ... Following the lead of G. Gentzen we will formulate now a calculus ... In the calculus of natural deduction one just has to omit the ...
    (sci.logic)
  • Re: Strange models of propositional logic
    ... > in the literature. ... > and most other non-classical logics.* ... Your notion of prepositional calculus is just the turn ... is a finite tree with the axioms in the leafs and the ...
    (sci.logic)