Re: Modus Ponens Is Unprovable?

Hi

The Deduction theorem is the other
direction, i.e. from

Z, C |- D (2)

to

Z |- C -> D

But we discussed from

Z |- C -> D (1)

to

Z, C |- D

What concerns the deduction theorem,
as can be readily seen, the transition
(2) is not archivable via modus ponens.
How do you remove the C?

So the usual transformation, maybe the same
as in the frege reference, uses a proof
transformation, that rewrites the proof
from the bottom up.

Bye

translogi@xxxxxxxxxxxxxx wrote:

Thanks for your reply

I found a reference ( not followed itr up yet) that Frege proved it in
1921
It is called the deduction theorem.

Maybe you are right.

I will look in to it.
Sorry for letting you wait so long


Jan Burse wrote:

The equivalence is not obvious.

Normaly the transition from:

Z |- C -> D

to

Z, C |- D

Is itself an application of modus
ponens. Namely:

------ (A)
Z |- C -> D C |- C
---------------------- (MP)
Z, C |- D

Also the transition yields not
a complete system . How
would you proof:

Z, T |- B

From

Z |- A

And

T |- A->B

You see modus ponens has two
antecedents and not only one.
But your transition rule has
only one antecendent.

Also in modus ponens the implication
is on the right side, and you
have the implication on the left
side.

But the left side/right side is
not so much an obstacle. Because
there are complete rules with
implication on the left side.
Namely:

Z, ~C |- A T, B |- C
-----------------------
Z, T, A->B |- C

is a pretty complete rule(*), and
has a single formula on the
right side and two antecedents!

Bye

(*) Proof: Forthcoming.

translogi@xxxxxxxxxxxxxx wrote:

No i meant
As third step
Z |- C -> D
is equivalent with
Z, C |- D


so

A -> B |- A -> B
is equivalent with
A -> B , A |- B
and that is a representation of Modus Ponens
So it has nothing to do with other translations of P -> Q in Q v ~P


Frederick Williams wrote:


"translogi@xxxxxxxxxxxxxx" wrote:


Another interesting way of "proving" MP

=> stand for turnstile

P => P priniple of equality
A->B => A-> B UF uniform substitution forom P to A->B

Let the A jump to the left

A -> B, A => B and there you have Modus Ponens

...

A -> B |- A -> B

A -> B |- ~A v B

A -> B |- ~A, B

A -> B, A |- B

is valid in multiple conclusion logic if A -> B and ~A v B are
interdefinable. Is that what you meant?

--
Remove "antispam" and ".invalid" for e-mail address.



.

Relevant Pages

  • Re: Modus Ponens Is Unprovable?
    ... Also the transition yields not ... antecedents and not only one. ... Also in modus ponens the implication ...
    (sci.logic)
  • Re: Proof without deduction theorem
    ... With the derived rules ... And that in turn means that the deduction theorem will hold in our system! ... "...the deduction theorem holds for any propositional calculus ... which has only the rule _modus ponens_ and which contains ...
    (sci.logic)