snd Dominik: (p ⇒ r) ∧ (q ⇒ s) ∧ (~p ∨ ~s) ⇒ (~p ∨ ~q) (1) zalozmy (p ⇒ r) ∧ (q ⇒ s) ∧ (~p ∨ ~s) (cel ~p ∨ ~q) (2) zatem ~p ∨ ~s (elim koniunkcji 1) (3) zalozmy ~p (cel elim ~p ∨ ~s) (4) zatem ~p ∨ ~q (wprowadzenie alternatywy 3) (5) zalozmy ~s (cel elim ~p ∨ ~s) (6) zalozmy q (cel sprzecznosc) (7) zatem q ⇒ s (elim koniunkcji 1) (8) zatem s (regula odrywania 7, 6) (9) zatem sprzecznosc (eliminacja negacji 5, 8) (10) zatem ~q (wnioskowanie przez zaprzeczenie) (11) zatem ~p ∨ ~q (wprowadzenie alternatywy 10) (12) zatem ~p ∨ ~q (eliminacja alternatywy 4, 11) (13) zatem (p ⇒ r) ∧ (q ⇒ s) ∧ (~p ∨ ~s) ⇒ (~p ∨ ~q) ok?

Dominik: podbijam

Dominik: podbijam.

Dominik: podbijam.

Dominik: czyzby nikt na forum nie znal systemu naturalnej dedukcji?

ciuchcia: Jadę teraz do Szczecina, sprawdzę potem . Nawet nie zauważyłem, że założyłeś taki temat.