redux: one premise rules...

[John.H...@utah.edu]

A question was asked here some time ago about logic systems with only
one premiss rules.
For some reason the board software won't let me add on to that
discussion, so I'm starting a new thread.

At that time I pointed out Jean Porte's classic paper.
Well, there is now a newer (and much better) reference...

Lloyd Humberstone just came out with just what was being looked for, I
think.

"Replacing Modus Ponens with One Premiss Rules" in the Logic Journal
of the IGPL.
He covers the procedure for a number of logics, and unlike Jean Porte
he goes into detail on how he got them.

(And it is not an accident that he gets some number of one premiss
rules, and *** only one *** axiom.)

[GrafZahl]

Hi,

Thank you for this interesting reference. It should be pointed out
that the original poster, Jeff, asked for a one-premiss-rules system
which is *equivalent* to the ax-1, ax-2, ax-3, ax-mp based system. If
"equivalent" here means "can prove precisely the same formulas" then
the Humberstone system is a way to go (presumably, haven't read the
paper yet). However, if "equivalent" should mean "can prove precisely
the same formulas *and* rules" then the Humberstone system (and any
one-premiss system) is strictly weaker than ax-{1,2,3,mp} unless I'm
missing something. In each one-premiss system the proof stack grows
monotonically (not counting mandatory variables) since every rule pops
one expression and then adds one again. Since at the end of the proof
there must be exactly one item on the stack, this limits your option
severely: your first proof step must be a (the) axiom, a previously
proven theorem without hypotheses, or a hypothesis. From then on it's
only rules. In particular, you can never prove ax-mp in Humberstone's
system because it needs two premisses and you can use at most one of
them.

[[GrafZahl]]
--
http://wiki.planetmath.org/AsteroidMeta/GrafZahl

[John Halleck]

Re: your discussion of "Equivalent" below.

Yes. Same theorems.
Humberstone's, and Porte's systems prove the same theorems,
but in neither is Modus Ponens a derived rule.

However, I don't understand your "stack" discussion.

You can prove the AXIOM of modus ponens in both Humberstone's
and Porte's systems. You can't prove the RULE in either.
Note that the usual proof in most systems of a given rule
from the axiom "of the same form" depends on the rule of
Modus Ponens if I remember correctly.

That's what I like about these odd systems... they make clear
distinctions that are normally muddled in the "standard" systems.



And, at least in the proof's I've been involved in lately,
one has more than one theorem being proved in the same proof
(which is counter to what I assume you are assuming in your
your stack discussion.)
[For those interested, proving one axiomatic basis for a system
from another is the context of what I've recently been involved
in... Dr. Dolph Ulrich's proof (in 90 steps) of seventy of the
now known shortest single axioms for BCI from the standard basis
is an extreme example.]



P.S. Are you also (implicitly) assuming the deduction theorem
still holds in the One Premiss rule systems?

[GrafZahl]

John Halleck wrote:
> Re: your discussion of "Equivalent" below.
>
> Yes. Same theorems.
> Humberstone's, and Porte's systems prove the same theorems,
> but in neither is Modus Ponens a derived rule.
>
> However, I don't understand your "stack" discussion.

That was metamath parlance. Instead of numbering your deduction steps
and using rules like "(x1), ..., (xn) |- y by rule z", metamath pushes
all deductions on a stack and a rule simply uses the last n elements
pushed on the stack (slight oversimplification but you get the idea).
The stack and numbering systems of writing down a proof are equally
strong though you might have to repeat some steps in the stack system,
where in the numbering system you'd just use the same label more than
once.

> You can prove the AXIOM of modus ponens in both Humberstone's
> and Porte's systems. You can't prove the RULE in either.

By ax-mp I meant the RULE, http://us.metamath.org/mpegif/ax-mp.html

> Note that the usual proof in most systems of a given rule
> from the axiom "of the same form" depends on the rule of
> Modus Ponens if I remember correctly.

Yes, at least in standard propositional logic, modus ponens can
convert anything from rule to axiom form and back again. The latter is
clear, the implementation of the former depends on the axioms at hand.
The standard way appears to be to derive ax-1, ax-2 and id (if you
don't have them already) and then introducing the necessary antecedent
in every step is easy. This is precisely the deduction theorem.

> That's what I like about these odd systems... they make clear
> distinctions that are normally muddled in the "standard" systems.

That's true. In standard propositional logic "muddling" simply means
to make tacit use of the deduction theorem. This can backfire badly
when you switch to some weaker or other system where the deduction
theorem doesn't hold.

> And, at least in the proof's I've been involved in lately,
> one has more than one theorem being proved in the same proof
> (which is counter to what I assume you are assuming in your
> your stack discussion.)

Yes, in my stack discussion I assumed a single theorem was to be
proven. If you prove more than one theorem in a stack system (so you
end up with all your desired results on the stack), the proofs will
simply be the concatenation of the individual proofs. This is of
course not true in a system with numbered deduction steps.

> [For those interested, proving one axiomatic basis for a system
> from another is the context of what I've recently been involved
> in... Dr. Dolph Ulrich's proof (in 90 steps) of seventy of the
> now known shortest single axioms for BCI from the standard basis
> is an extreme example.]
>
>
>
> P.S. Are you also (implicitly) assuming the deduction theorem
> still holds in the One Premiss rule systems?

I don't think I was assuming that. In a system equivalent to ax-
{1,2,3,mp} in the sense that it proves the same theorems but not
rules, the deduction theorem certainly has to hold, though it reduces
to "if p |- q then |- p->q". A more interesting thing would be to
develop a proof for it because the standard proof doesn't work any
more. A one-premiss-rule system whose equivalence to ax-{1,2,3,mp} is
proven must come with some procedure to convert applications of Modus
Ponens to One-Premiss-Deductions. Then it should be possible to
convert the standard derivation to one-premiss form. I wonder what the
effect of such a conversion in action would have on the average
formula length in the proof.

[John Halleck]

Sorry, I'm afraid that I'm not up on "metamath parlance".
(Which is a sorry confession indeed since this is a metamath
discussion group.)
Thank you for the enlightenment.





I question whether or not in propositional calculus MP can
convert things from rule to axiom form and back.

If one has a provability predicate P(x), then
x |- P(x)
holds but
x -> P(x)
does not.

Although I freely admit MP can convert from the axiom form
to the rule form.



I'll have to think on your deduction theorem comments.
It seems to me that if you have the
deduction theorem you can prove multi-premiss rules.
And it is my understanding that in Humberstone's system
you can't prove any multiple premiss rules.

Possibly the comments below are wrong... but I'd welcome
someone pointing out the hole in the logic.

PC has the theorem: (p->((p->q)->q)
if a one-premiss rule version had the deduction theorem, then
we'd have (by the deduction theorem)
p |- (p->q) -> q
and another application of the deduction theorem
p, p->q |- q
which is the rule of Modus Ponens, which Jean Porte
and Lloyd Humberstone state are not derived rules of
their systems.
So at least that half of the deduction theorem isn't
in the systems?

[GrafZahl]

On Jul 1, 4:24 pm, John Halleck <John.Hall...@utah.edu> wrote:
> Sorry, I'm afraid that I'm not up on "metamath parlance".
> (Which is a sorry confession indeed since this is a metamath
> discussion group.)
> Thank you for the enlightenment.
>
> I question whether or not in propositional calculus MP can
> convert things from rule to axiom form and back.
>
> If one has a provability predicate P(x), then
>     x |- P(x)
> holds but
>     x -> P(x)
> does not.

I'm not sure I'm following you here. Wouldn't it require some kind of
incompleteness theorem for this to fail? Or did you mean to say
"predicate calculus" instead of "propositional calculus"?

> Although I freely admit MP can convert from the axiom form
> to the rule form.

And the other way round. Wikipedia even has an example run of the
algorithm: http://en.wikipedia.org/wiki/Deduction_theorem#Example_of_conversion

> I'll have to think on your deduction theorem comments.
> It seems to me that if you have the
> deduction theorem you can prove multi-premiss rules.
> And it is my understanding that in Humberstone's system
> you can't prove any multiple premiss rules.
>
> Possibly the comments below are wrong... but I'd welcome
> someone pointing out the hole in the logic.
>
> PC has the theorem:  (p->((p->q)->q)
> if a one-premiss rule version had the deduction theorem, then
> we'd have (by the deduction theorem)
> p |- (p->q) -> q
> and another application of the deduction theorem
> p, p->q |- q
> which is the rule of Modus Ponens, which Jean Porte
> and Lloyd Humberstone state are not derived rules of
> their systems.
> So at least that half of the deduction theorem isn't
> in the systems?

Sorry, that was bad wording on my part. By "though it reduces to..." I
meant that there should be only a one-premiss version of the deduction
theorem. So you can go from p->(p->q)->q to p |- (p->q)->q but no
further. And yes, I dismissed that half of the deduction theorem
prematurely. See Corollary 3.3 in Humberstone's paper.

[John.H...@utah.edu]

On Wednesday, July 1, 2009 2:10:14 PM UTC-6, GrafZahl wrote:

...

> I question whether or not in propositional calculus MP can
> convert things from rule to axiom form and back.
>
> If one has a provability predicate P(x), then
>     x |- P(x)
> holds but
>     x -> P(x)
> does not.

I'm not sure I'm following you here. Wouldn't it require some kind of
incompleteness theorem for this to fail? Or did you mean to say
"predicate calculus" instead of "propositional calculus"?

...

 
Yes, I did indeed miss-speak.