Re: Help with a problem

On Wed, 23 Nov 2005 19:36:23 -0800, William Elliot
<marsh@xxxxxxxxxxxxxxxxxx> wrote:

>
> Here's natural deduction proof with classical negation
> leaving reasons, rules and references for the reader.
>
> assume ~(p v ~p)
> (p v ~p) -> f
> assume p
> p v ~p
> f
> p -> f
> ~p
> p v ~p
> f
> ~(p v ~p) -> f
| ~~(p v ~p)
> p v ~p
>

Proof in Gentzen's system of ND (Lemmon style):

1 (1) ~(P v ~P) A
2 (2) P A
2 (3) P v ~P 2 vI
1,2 (4) _|_ 1,3 ~E
1 (5) ~P 2,4 ~I
1 (6) P v ~P 5 vI
1 (7) _|_ 1,6 ~E
(8) ~~(P v ~P) 1,7 ~I
(9) P v ~P 8 ~~E

The proof in tree form:

(2)
P
(1) ------ vI
~(P v ~P) P v ~P
------------------------ ~E
_|_
----- ~I(2)
~P
(1) ------ vI
~(P v ~P) P v ~P
--------------------- ~E
_|_
--------- ~I(1)
~~(P v ~P)
---------- ~~E
P v ~P

F.


Rules of derivation:

Gentzen W. Elliot Name (Gentzen)
-----------------------------------------------------

A & B A & B
----- ----- same &E
A , B
(&)
A B
----- same &I
A & B

-----------------------------------------------------

A A -> B
----------- same ->E
B
(->)
[A]
: same ->I
B
------
A -> B

-----------------------------------------------------

[A] [B]
: : A -> C
A v B C C B -> C
-------------- ----------- vE
C A v B -> C
(v)
A B
----- ----- same vI
A v B , A v B

-----------------------------------------------------

A ~A ~A
------- ------ ~E
_|_ A -> f
(~)
[A]
:
_|_ A -> f
----- ------ ~I
~A ~A

-----------------------------------------------------

~~A
--- same ~~E
A

--
"I do tend to feel Hughes & Cresswell is a more authoritative
source than you." (D. Ullrich)
.

Relevant Pages

  • Re: Needed to transfer some photos off my camera...
    ... about the price of the reader. ... Will you never check your facts before you post? ... Shipping costs don't change the fact that the *product* only costs ... Insert your references, Edwin! ...
    (comp.sys.mac.advocacy)
  • Re: North South East or West
    ... and allowing the reader to conduct peer review. ... Haphazardly providing opinions without references or citations does not ... get discussions going on the Usenet by being so rigorous. ... I look forward to intelligent questions. ...
    (sci.space.shuttle)
  • Re: When is reader internals garbagecollected?
    ... fields inside the reader, cos the gc knows about them? ... >> recordset then ASP would never the less garbagecollect the ... Then they added managed references from the RCWs ... > of the field values to the RCWs of their owning rows. ...
    (microsoft.public.dotnet.framework.adonet)
  • Re: Clue bats
    ... many writers are tempted to choose a balance which has ... I think the base concept was that the reader had to read and think about what was happening in order to figure out how certain things happen within the given story. ... If you don't know the references at all, you may think the story boring without recognizing that you're missing something, or the writer may have given you enough to enjoy that you don't care about the subtext you're missing. ... there is a free service available. ...
    (rec.arts.sf.composition)
  • Re: North South East or West
    ... In scientific writing the reason for citing sources is to allow the ... stating is only achieved by the author giving credit as to where the ... and allowing the reader to conduct peer review. ... Haphazardly providing opinions without references or citations does not ...
    (sci.space.shuttle)