🚀 go-pugleaf

I'm reading "Mathematical Logic" by S.W.P. Steen and I don't get
the proof (if it is a proof) on how the composition building
scheme on p. 42 is reversible. Can anyone tell me what's going on?

I'm looking at a section on the classical propositional calculus,
called Pc. There's a negation symbol (Noo of type oo), a disjunction
symbol (Dooo), a variable (po), a generating sign (apostrophe), and
the parentheses. One of the proof rules is the composition building
rule:

 DNaw  DNbw
 ----------
   DNDabw

The rest of the proof rules:

                               DDDxaby
There is a remodelling rule:   -------
                               DDDxbay

There are 2 other building rules:

            x
dilution:  ---
           Dax
                   Daw
double negation:  -----
                  DNNaw

Steen says one of the properties of the composition rule is
reversibility. That is, from DNDabw constructive proofs can be
found for DNaw and DNbw. The justification given for finding a
constructive proof of DNaw is to rebuild the proof for DNDabw.
I'm not sure, but it seems that Steen is telling how to prove
DNaw, and there's only an indirect relation to DNDabw.

--

Henry Choy
choy@cs.usask.ca

What rolls down stairs alone or in pairs            This has been brought to 
Rolls over your neighbor's dog?                     you by the numbers 4
What's great for a snack and fits on your back?     and 9 and the letter P.
It's Log, Log, Log!  -- "The Log Song", from            -- Big Bird
                         Ren & Stimpy

Math is tough!       -- Barbie