proving bicondtionals without cases?

From: futurist (adamgolding_at_adamgolding.com)
Date: 02/27/05 

Date: 26 Feb 2005 16:15:31 -0800

Ok, so the standard technique for proving statements of the form P<=>Q
is to prove P=>Q and Q=>P separately. However, doesn't this seem like
an inelegant proof strategy? after all, when we prove another
symmetrical relation, numerical equality, we don't first prove 7<_5+2
and then 5+2<_7. And, for very simple proofs and corrolaries, i know i
can usually achieve a shorter proof by using a string of reversible
steps leading from p to q. It will often look like this:

    P
<=> R
<=> S
<=> Q

and cearly, this proof would be *twice as long* if we used the standard
strategy. However, i have found in more advanced proofs that i can
find no clear way to proceed by this method...

to take one example: the proof that the union of subspaces is a
subspace iff one contains the other. I can prove it by separating it
into cases, but i would still like to this that i can find a better
proof that proceeds using <=>.

however, it is clear that in some systems, this would be impossible,
for instance, say we have a system with only 3 expressible
propositions, P, Q, and R, and only three primitive rules: P|-R R|-Q,
and Q|-P. in this case proof by cases is really the only way, although
whenever we have rules like tautology laws etc. we can probably
construct a bidirectional proof OUT of the case-by-case proof, but then
the resulting bidirectional proof would be even *longer*

so, i'm wondering if conventional mathematical inference is in this
situation--where sometimes the shortest reversible proof is longer than
the shortest case-by-case proof--or if i simply need to try harder to
find the 'better' proofs i'm dreaming about..

so, I was hoping group memebers could share their experience regarding
the two different techniques--do you think that with some effort it
will be easy enough to always use the reversible approach, or is using
<=>-strings impossible, or at least impracticable in some cases? Is
there a clear metatheorical reason for this?

Also, if common systems of inference have this 'limitation' that
iff strings are sometimes impossible, does anyone think it might be
fruitful to define a new property of systems, in addition to
'soundness' and 'completeness' called something like
'bidirectional completeness' ? the definition would run something
like:

P=|=Q => P-|-R1-|-R2-|- ... -|-RN-|-Q

For some finite string of R's connected by biconditional primitive
rules in each case?

To make an analogy, if your proof system is a city, and propositions
are intersections, this property would ensure that your city has no
unnecessary one-way streets. Making it easier to get around? what do
you think?

Relevant Pages

  • proving bicondtionals without cases?
    ... so the standard technique for proving statements of the form PQ ... I can prove it by separating it ... construct a bidirectional proof OUT of the case-by-case proof, ... For some finite string of R's connected by biconditional primitive ...
    (sci.math)
  • Re: from array of ints to string and vice versa
    ... I want to convert this string to an array, ... other to generate it, separating them with ", ". ... takes a buffer and returns a size, which you first call with a NULL pointer ...
    (comp.programming)
  • How to Export as text file with NO delimiters or modifications?
    ... contents saved as a simple long string of data, regardless of content. ... tab's separating the original cell contents. ...
    (microsoft.public.excel.misc)
  • Re: String manipulation
    ... > since that is what is separating the fields in your text string. ... > Dim Number As Long ... > Here I've used Print to display the separate fields because your example ...
    (microsoft.public.vb.general.discussion)