Re: Minimal logic valid?

translogi schrieb:
This is NOT natural deduction, you are using
This is sequent calculus (schluszweisenkalkul), something different
all together

You see the text of gentzen is very easy to
obtain. You can find it here:
http://gdz.sub.uni-goettingen.de/dms/load/img/?IDDOC=17178

Gentzen introduces two calculi:

NJ, NK: "Natürliches Schliessen"
= translates to "Natural Deduction"
LJ, LK: "Schlussweisen Kalküle"
= translates to Sequent Calculus"

I will now show you that my calculus is among NJ, NK
and not among LJ, LK.

The only difference between Gentzens presentation
and my presentation is that Gentzen uses a graphic
representation with detachment indicated specially.
Whereas I am using a more flat representation.

That both representations amount to the same system
is a well known fact, and there are even papers about
it. Its even part of the results of Gentzens original
paper itself.

I will try to give a rough intuitive explanation
why both representation yield the same system.
We have the following graphic rules:
(Page 186 of the above paper)


[A] A A -> B
B ---------
------ B
A -> B


These graphics rules are steps in a proof tree.
The [A] indicates that this A is a detached
assumption. So when something is a detached
assumption, it will only temporarily used,
and then later in the proof tree not anymore
referenced (the position of it).

What my flat representation makes explicit,
is what can be referenced, what is available
as an assumption. In my flat representation
we have the following corresponding rules:

G |- B G |- A D |- A -> B
------------- ---------------------- ---------
G\A |- A -> B GuD |- B A |- A

This is in accordance with what Gentzen about
the transition from NJ, NK to LJ, LK:
(Page 190 of the above paper, towards the bottom)

"Das naheliegendste Verfahren, um aus einer NJ
Herleitung eine logistische Herleitung zu machen,
ist dieses: Man ersetzt eine H Formel B
welche avon den Annahmeformeln A1,..,An abhängt
durch die neue Formel A1,..,An |- B."

So when a formula B depends on the assumption A1,..,An
in the graphic representation, then we write for
it A1,..,An |- B.

So my system is natural deduction.
.