Natuurlijke deductie, bewijs via Fitch

[pppp]

Ik probeer de volgende opgave op te lossen, maar ik blijf vast zitten. Ik kom of niet uit met m'n permissen of ik kan geen False afleiden. Het systeem dat we gebruiken lijkt op dat van Fitch. Het is afkomstig uit het boek: Logical Reasoning, A first course, van van Nederpelt en is onderdeel van het vak Logica en verzamelingenleer van de TU/E.

Code: Selecteer alles

~P => ~((P = > Q) => P):

Code: Selecteer alles

~P
      (P => Q) => P
{ hier loop ik dus vast, ik zou P => Q aan kunnen nemen, en via =>E op (P => Q) => P
  zou ik P kunnen afleiden. Via de eerste assumptie, ~P, zou ik dan een contradictie kunnen afleiden.
 maar als ik dat doe, kan ik de aanname P = >Q niet sluiten, volgens mij: }
            P => Q
                  P
                  ~P
                  False 
            (P => Q) => False
            ~(P => Q)
{ zoals je ziet lijkt bovenstaande methode niet echt een productieve methode.
  Tips gewenst! }
      False
      (((P => Q) => P) => False          C - 2, =>I Y, X:     
      ~((P => Q) => P                    C - 1, ~ Y, X:     
~P => ~((P => Q) => P)                   C, =>I 1, C-1:

[arie]

Ik ben niet bekend met jullie afleidingssysteem, maar in het algemeen kan je voor natuurlijke deductie van deze stelling het volgende schema gebruiken:

p ⋁ ¬p [uitgesloten derde]
(p ⋁ ¬p) ⋀ (p ⋁ ¬p) [⋀-introductie]
(p ⋁ ¬p ⋁ q) ⋀ (p ⋁ ¬p) [⋁-introductie]
p ⋁ ((¬p ⋁ q) ⋀ ¬p) [distributie]
p ⋁ ((p → q) ⋀ ¬p) [stelling 1]
p ⋁ ¬¬((p → q) ⋀ ¬p) [dubbele negatie]
p ⋁ ¬(¬(p → q) ⋁ ¬¬p) [De Morgan]
p ⋁ ¬(¬(p → q) ⋁ p) [dubbele negatie]
p ⋁ ¬((p → q) → p) [stelling 1]
¬¬p ⋁ ¬((p → q) → p) [dubbele negatie]
¬p → ¬((p → q) → p) [stelling 1]

waarbij [stelling 1] luidt:
(¬p ⋁ q) ↔ (p → q)

Kort samengevat: (p→ q) kan worden verkregen via bovenstaande ⋁-introductie.

Kom je hiermee verder voor jullie afleidingssysteem?