Beweren en bewijzen/de zuilen/Zekerheid/5. Natuurlijke deductie/propositielogica stellingen

Uit Werkplaats
Ga naar: navigatie, zoeken
de opzet 2017-18    KalenderIcon.gif multimedia kwaliteit commentaren
site map

Beweren en bewijzen
Wijsheid omgaan met onzekerheid: met open blik op wankele ondergrond levenspad bewandelen
Vernuft aanpak van glibberige problemen precies redeneren op het hoogste niveau
vier zuilen → Artefacten Formalisering Taal Zekerheid
1. Rationaliteit Rationaliteitsvierkant 4 werelden Beweren is moeilijk Overtuigen
2. Modellen Focus Precisie Logica Stelling en bewijs
3. Model en realiteit Specificaties Domeinmodel Syntax en semantiek Waarheid
4. Correctheid Structuur Correctheidsstelling Typering Nagaan
5. Methoden Decompositie Systemat. vertalen Definities Natuurl. deductie
6. Theorie Domeintheorie Tijd Tijdslogica Wiskunde
7. Complexiteit Hiërarch. decompositie Vereenvoudigingen Modules Bewijsassistenten
8. Generalisering Standaardisatie Parametrisatie Talen Hulpstellingen
Beweren en bewijzen/de zuilen/Zekerheid/5. Natuurlijke deductie/propositielogica stellingen

Aan deze pagina wordt nog gewerkt. Bedankt voor uw begrip.

literatuur

...

Hier een aantal stellingen in Coq-vorm waarmee je het bewijzen kunt oefenen, zowel met Coq als op papier.

Bedenk, alvorens met het bewijzen te beginnen, voorbeeld-invullingen voor P, Q enz.

<source lang="coq"> Theorem prop_001 : P /\ Q -> P. (*Elementary*) Theorem prop_005 : P /\ Q -> P \/ Q. (*Elementary*) Theorem prop_012 : (P -> Q) -> (P -> P /\ Q). (*Elementary*) Theorem prop_014 : ~(P /\ P) -> ~P \/ ~P. (*Easy*) Theorem prop_017 : P -> ~~P. (*Easy*) Theorem prop_018 : ~~(P -> Q) -> (P -> Q). (*Elementary*) Theorem prop_020 : ~~~P -> ~P. (*Medium*) Theorem prop_023 : ~(P -> Q) /\ Q -> ~P. (*Easy*) Theorem prop_024 : (P \/ Q) /\ ~P -> Q. (*Easy*) Theorem prop_025 : P -> ~Q \/ P /\ Q. (*Easy*) Theorem prop_026 : ~P /\ ~Q -> ~(P \/ ~P /\ Q). (*Medium*) Theorem prop_027 : ~(P \/ ~P /\ Q) -> ~P /\ ~Q. (*Medium*) Theorem prop_028 : ~(P \/ ~Q) \/ (~P /\ ~Q) -> ~P. (*Easy*) Theorem prop_029 : ~P -> ~(P \/ ~Q) \/ (~P /\ ~Q). (* Medium*) Theorem prop_031 : ~(P /\ Q /\ R) -> P -> Q -> ~R. (*Easy*) Theorem prop_032 : (P -> Q -> R) -> (Q /\ ~R -> ~P). (*Easy*) Theorem prop_033 : (P /\ Q -> ~R) -> (P /\ R -> ~Q). (*Easy*) Theorem prop_035 : (P -> Q -> R) /\ (P -> Q) -> (P -> R). (*Easy*) Theorem prop_036 : (P -> R) \/ (Q -> R) -> (P /\ Q -> R). (*Easy*) Theorem prop_037 : (P /\ Q -> R) -> (P -> R) \/ (Q -> R). (*Difficult*) Theorem prop_038 : ~((P /\ (R -> ~Q)) /\ (Q /\ (~R -> ~P))). (*Medium*) Theorem prop_039 : (P -> Q /\ R) /\ (Q \/ R -> ~P) -> ~P. (*Easy*) Theorem prop_040 : (P -> Q) /\ (Q -> R) -> (P -> R). (*Elementary*) Theorem prop_041 : ((P -> Q) /\ (Q -> R)) -> (P -> (Q -> R)). (*Elementary*) Theorem prop_044 : (P -> Q -> R) -> (P -> Q) -> P -> R. (*Easy*) Theorem prop_045 : P -> (Q -> Q). (*Elementary*) Theorem prop_046 : Q -> (P -> Q). (*Elementary*) Theorem prop_047 : P -> (P -> (Q -> P)). (*Elementary*) Theorem prop_048 : (P -> (P -> Q)) -> (P -> Q). (*Elementary*) Theorem prop_049 : (P -> Q -> ~P) -> ~P \/ ~Q. (*Easy*) Theorem prop_051 : P \/ Q -> ((P -> Q) -> Q). (*Easy*) Theorem prop_053 : ((P -> Q) -> Q) -> ~P -> Q. (*Easy*) Theorem prop_054 : ~P \/ ~Q -> (Q -> ~(Q -> P)). (*Medium*) Theorem prop_057 : ~(P -> Q) -> (Q -> P). (*Easy*) Theorem prop_059 : (P \/ Q -> ~R) /\ R -> ~P. (*Easy*) Theorem prop_060 : ~(P \/ Q) /\ (~Q -> R) -> R. (*Easy*) Theorem prop_061 : (P -> Q) /\ ~(P /\ Q) -> ~P. (*Easy*) Theorem prop_062 : (~P -> Q) /\ (~P -> ~Q) -> P. (*Easy*) Theorem prop_065 : P /\ Q \/ ~Q -> Q -> P /\ Q. (*Easy*) Theorem prop_066 : (P -> Q \/ R) -> ((P -> Q) \/ R). (*Medium*) Theorem prop_067 : (P /\ Q -> R) -> P -> (~Q \/ R). (*Easy*) Theorem prop_068 : (P -> R) -> (P /\ Q -> R). (*Elementary*) Theorem prop_069 : (P -> Q /\ R) -> ((R -> ~Q) -> ~P). (*Easy*) Theorem prop_070 : (P /\ Q -> ~R) -> (P /\ R -> ~Q). (*Easy*) Theorem prop_072 : (P -> Q /\ R) /\ (R \/ P) -> R. (*Easy*) Theorem prop_073 : (Q -> ~~R) -> (P -> Q -> P /\ R). (*Easy*) Theorem prop_074 : (P /\ (Q -> R)) -> Q -> (P /\ R). (*Elementary*) Theorem prop_075 : (Q \/ R) /\ (Q -> P) -> (~R -> P). (*Easy*) Theorem prop_076 : ((P -> Q) -> R) /\ (~P \/ Q) -> R. (*Easy*) Theorem prop_077 : ((~P \/ Q) -> (R /\ S)) -> (~S -> P). (*Easy*) Theorem prop_079 : (P \/ Q) -> (P -> R) -> (P -> Q \/ R). (*Elementary*) Theorem prop_080 : (P \/ Q -> (P -> R)) -> P -> (Q \/ R). (*Elementary*) Theorem prop_081 : (P \/ Q -> (P -> R)) -> Q -> (~P \/ R). (*Easy*) Theorem prop_082 : (P -> Q) /\ (R -> S) -> (~Q \/ ~S) -> (~P \/ ~R). (*Medium*) Theorem prop_083 : (P \/ Q -> R) -> (P -> R) \/ (Q -> R). (*Easy*) Theorem prop_084 : ((P \/ Q) -> R) -> (P -> R) /\ (~R -> ~Q). (*Easy*) Theorem prop_086 : (P \/ Q -> R) /\ (P \/ Q) -> (P -> R) \/ (Q -> R). (*Elementary*) Theorem prop_087 : (P -> R) /\ (R -> ~P) /\ (Q -> S) -> (P \/ Q -> S). (*Easy*) Theorem prop_088 : P -> (P /\ R -> Q) -> (((P -> Q) -> Q) -> (P -> R)) -> Q. (*Easy*) Theorem prop_089 : (R -> P \/ S) /\ (E -> Q \/ F) -> (R /\ E) -> (P /\ Q) \/ S \/ F. (*Medium*) Theorem prop_090 : (P -> R) /\ (Q -> S) /\ (P \/ Q) -> (R \/ S). (*Easy*) Theorem prop_092 : (P -> Q) \/ (Q -> P). (*Easy*) Theorem prop_099 : (P -> Q) -> (~Q -> ~P). (*Easy*) Theorem prop_100 : (~P -> ~Q) -> (Q -> P). (*Easy*) Theorem prop_101 : (P -> Q) -> (~~P -> ~~Q). (*Medium*) Theorem prop_102 : (~~P -> ~~Q) -> (P -> Q). (*Easy*) Theorem prop_103 : (~P \/ ~Q) -> ~(P /\ Q). (*Medium*) Theorem prop_104 : (P \/ Q) -> ~(~P /\ ~Q). (*Medium*) Theorem prop_105 : ~(P /\ Q) -> (~P \/ ~Q). (*Easy*) Theorem prop_106 : ~(~P /\ ~Q) -> (P \/ Q). (*Medium*) Theorem prop_107 : ~(P /\ Q) -> ~~ (~P \/ ~Q). (*Difficult*) Theorem prop_108 : ~(P \/ Q) -> (~P /\ ~Q). (*Easy*) Theorem prop_109 : ~(~P \/ ~Q) -> (P /\ Q). (*Medium*) Theorem prop_110 : (~P /\ ~Q) -> ~(P \/ Q). (*Easy*) Theorem prop_111 : (P /\ Q) -> ~(~P \/ ~Q). (*Medium*) Theorem prop_112 : ~(~P \/ ~Q) -> (~~P /\ ~~Q). (*Easy*) Theorem prop_113 : ~(~P \/ ~Q) -> ~~(P /\ Q). (*Difficult*) Theorem prop_119 : ~~P -> ~~(P \/ Q). (*Easy*) Theorem prop_120 : ~~(P /\ Q) -> ~~Q. (*Easy*) Theorem prop_121 : (P -> Q) /\ (P -> ~Q) -> ~P. (*Easy*) Theorem prop_122 : (Q -> R) -> (P \/ Q) -> (P \/ R). (*Easy*) Theorem prop_125 : ((P -> Q) -> P) -> P. (*Easy*) Theorem prop_126 : (~~(((P -> Q) -> P) -> P)). (*Difficult*) Theorem prop_128 : ~((P -> Q) /\ (Q -> ~P) /\ (~P -> ~Q) /\ (~Q -> P)). (*Medium*) </source>

voor de liefhebbers

Hieronder nog een aantal stellingen die voor de verificatie van artefacten niet echt relevant zijn maar inzicht kunnen geven in hoe de logica zelf in elkaar zit.

<source lang="coq"> Theorem prop_002 : (~P -> P) -> P. (*Easy*) (*Een bewering kan alleen uit haar eigen negatie volgen als ze toch al waar was.*) Theorem prop_003 : (~P -> P) \/ ~P. (*Easy*) Theorem prop_016 : ~P \/ P. (*Difficult als LEM niet gebruikt mag worden, Easy als LEM wel gebruikt mag worden*) (*Het Uitgesloten Derde, alleen geldig in de klassieke logica.*) Theorem prop_021 : ~P \/ (Q -> P). (*Easy*) (*Classically, everything is false or implied*) Theorem prop_030 : ~P /\ ~Q -> ~((P -> Q) -> Q). (* Medium*) Theorem prop_034 : R -> ((~P -> ~R) -> ((P -> ~R) -> Q)). (*Easy*) Theorem prop_050 : ((P -> Q) -> P) -> ((Q -> P) -> P). (*Medium*) Theorem prop_055 : (Q -> ~(Q -> P)) -> (~P \/ ~Q). (*Easy*) Theorem prop_056 : (P -> Q) \/ (P /\ ~Q). (*Medium*) Theorem prop_058 : ~P /\ ((Q -> P) -> P) -> Q. (*Easy*) Theorem prop_063 : ~~((~P -> Q) /\ (~P -> ~Q) -> P). (*Difficult*) Theorem prop_085 : ~((P -> (Q \/ ~R)) /\ (Q -> ~P) /\ (P -> R) /\ P). (*Medium*) Theorem prop_117 : (~~P /\ ~~(P -> Q)) -> ~~Q. (*Difficult*) Theorem prop_118 : ~~(P \/ Q) -> (~~P -> ~~R) -> (~~Q -> ~~R) -> ~~R. (*Challenge*) Theorem prop_123 : ((P \/ (P -> Q)) -> Q) -> Q. (*Easy*) Theorem prop_124 : ~~(((P \/ (P -> Q)) -> Q) -> Q). (*Difficult*) Theorem prop_127 : (((((P -> Q) -> P) -> P) -> Q) -> Q). (*Easy*) </source>

Overgenomen van "https://lab.cs.ru.nl/algemeen/index.php?title=Beweren_en_bewijzen/de_zuilen/Zekerheid/5._Natuurlijke_deductie/propositielogica_stellingen&oldid=290711"