Re: Minimal logic valid?

translogi schrieb:

The main difference is that natural deduction uses lots of inference
rules and no axioms.
while the axiomatic method uses axioms(chemata) and only detachment /
modus ponens

Hilbert style calculi usually have no detachment rule.
Natural deduction has it. What are you talking
about?

In natural deduction you have a context G, and
you can formulate a rule as such:

G |- A
-----------
G\B |- B->A

Or graphically:

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

Hilbert style calculi dont have this context.
They have just rules over a single sukzedent
sequents with zero context.

But a hilbert style calculi might make use
of axioms G, and then we write also:

G |- A

And we might have the meta result, that when
G |- A is valid, that G\B |- B->A is also
valid. That is called the deduction theorem.

The deduction theorem states that when there
is a hilbert style proof G |- A, then
there is "another" hilbert style proof of
G\B |- B->A.

That hilbert style methods need more axiom schemas,
I agree. Namely to be classical, because things
go rather into the axioms than into the rules.

But that hilbert style is an axiomatic method,
while natural deduction is not, I wouldn't
agree. For example as soon as one has the
classical apparatus in both system, one can
work the same way with axiom systems.

Also an axiom schema is a degenerated instance
of the following pattern of a rule:

Template_1 .... Template_n
--------------------------
Template

An axiom schema has just n=0, i.e. no precluding
patterns. So we can compare hilbert style and
natural deductions:

System Templateform n
---------------------------------------------
Hilbert style |- A =0 for the logic axioms
=0 for the axioms
=2 for MP
Natural deduction G |- A =1, 2, 3 for the logic rules
=0 for axioms and assumptions
=1 for detachment
=2 for MP

I think both systems belong to the axiomatic method
as there are some principles (the rules with n=0
or n<>0) layed down, and we try to work from these
principles.

Bye
.

Relevant Pages

  • Re: Proof of a certain theorem in =?windows-1252?Q?=93G=F6del=27?= =?windows-1252?Q?s_Proof=
    ... "Each of these axioms may seem "obvious" and trivial. ... I am trying to get a grip why these Hilbert Style ... Now natural deduction has additional rules. ... Premisses as Types: ...
    (sci.logic)
  • Re: Prove axiom in S5
    ... >Does anybody know how to prove the following using Natural Deduction ... follows from two of the axioms, I mentioned, and not all three? ... > Posted Via Usenet.com Premium Usenet Newsgroup Services ...
    (sci.logic)
  • Re: Logarithm of transfinite numbers
    ... An axiomless system of natural deduction does not have ... True, because without axioms, you cannot generate a theorem. ... axiomatized with all true statements trivially being true... ...
    (sci.math)
  • Re: Why will Cantor be a target for cranks?
    ... Has to have an axiomatic system infinite many axioms to be definite? ... My point is that, at least in in pure mathematics, one cannot conclude ... The axiomatic method does not in any way dispute what you have just ...
    (sci.math)
  • Re: Defining things in Mathematics and in Scheme
    ... For instance group theory benefited when it was put on axiomatic basis. ... Accept my axioms and investigate the consequences. ... So the axiomatic method does help to clarify things and facilitates the ... work of one researcher to build upon work of other researchers. ...
    (comp.lang.scheme)