Re: Minimal logic valid?

On Jun 18, 3:32 pm, Jan Burse <janbu...@xxxxxxxxxxx> wrote:
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    

Hilbert style proof that p ->p

This is the simplest proof of something 'obvious', It can get much
worse
axioms

C1 (p->(q->p))
C2 ((p->(q->r))->((p->q) -> (p->r)))

rules
Detachment
given (or proved) A->B and A B is proved

substitution
any variable may be replaced by any other variable or formula.
(But all variables need to be replaced)


Theorem D1 is axiom C2 with p replaced by r
((p->(q->p))->((p->q) -> (p->p)))

Theorem D2 is the detachment from theorem D1 given axiom C1
((p->q) -> (p->p)))

Theorem D3 is theorem D2 with q replaced with (q->p)
((p->(q-> p)) -> (p->p)))

Theorem D4 is the detachment from D1 given C1
(p->p)))

Probably more in line with Hilberts thinking is:

Theorem E1 is axiom C2 with
p replaced by r
q replaced by (q->p)
E1 = ((p->((q->p)->p))->((p->(q->p)) -> (p->p))))


Theorem E2 is axiom C1 with
q replaced by (q->p)
E2 = (p->((q->p)->p))


E3 is the detachment from theorem E1 given theorem E2
E3 = ((p->(q->p)) -> (p->p)))

E4 is the detachment from theorem E3 given axiom C1
E4 = (p -> p)

You can from these two axioms and rules prove

(p->((p->q) ->p))
((p -> q) -> ((q->r) -> (p->r)))
((p->(q->r)) -> (q->(p->r)))
and so on
But it is hard work (as shown above)

in lemmon style natural deductiom

in lemmon style natural deductiom

1 1 p Assumption
- 2 p-> p 1,1 ->I
is just so much more easier.

although proving
((p->(q->r))->((p->q) -> (p->r)))
is done this way

1 1 (p->(q->r) A
2 2 (p-q) A
3 3 p A
2,3 4 q 2,3 ->E
1,3 5 (q->r) 1,3 ->E
1,2,3 6 r 4,5 ->E
1,2 7 (p->r) 3-6 ->I
1 8 ((p->q) -> (p->r)) 2-7 ->I
- 9 ((p->(q->r))->((p->q) -> (p->r))) 1-8 ->I
.

.

Relevant Pages

  • Re: how to prove ~(P <--> Q) |- ~P <-->Q
    ... or the philosopher (those non descript symbol will not ... When you add A v ~A as an axiom to the rules for the ... intuitionistic calculus you get the classical calculus. ... In Gentzen's original systemof natural deduction, ...
    (sci.logic)
  • Re: Contradiction or paradox
    ... You'll have to do better than that, Frege. ... proof must be justified as being an axiom, ... See one of the many books on natural deduction. ...
    (sci.logic)
Loading