Formeel bewijs?

[Philip-Voets]

Dag,

Worden binnen propositielogica een bewijs via natuurlijke inductie en een bewijs via logische equivalentie allebei beschouwd als formele bewijzen? D.w.z., als gevraagd wordt een stelling in PL formeel te bewijzen, volstaat het dan logische equivalentie aan te tonen middels de bekende bewerkingen (De Morgan, etc.)?

Gr.

[Professor Puntje]

Er zijn meerdere systemen van propositie logica. Maar in de huis-tuin-en-keuken variant van propositie logica komt natuurlijke inductie als afleidingsregel niet voor. Wat voor boek gebruik je?

[PhilipVoets]

Velleman en syllabus van Klaas Landsman (RU). Voorbeeld uit een opgave; te bewijzen dat modus ponens een tautologie is: (A ∧ (A → B)) → B. Mag ik dat op onderstaande manier doen of "voldoet" dat niet als formeel bewijs van tautologie?

(A ∧ (A → B)) → B
(A ∧ (¬A V B) → B
(A ∧ ¬A) V (A ∧ B)) → B
A ∧ ¬A ≡ F (falsum)
F V (A ∧ B) ≡ A ∧ B
A ∧ B → B
¬(A ∧ B) V B
¬A V ¬B V B (De Morgan)
¬B V B ≡ T (tertium non datur)
¬A V T ≡ T

Gr.,
Philip Voets

[Professor Puntje]

Gebruik je dit boek?: https://www.bol.com/nl/nl/f/how-to-prove-it/30234285/

[Professor Puntje]

En deze lecture notes?: https://www.math.ru.nl/~landsman/Propos ... ca2017.pdf

[Professor Puntje]

Velleman en syllabus van Klaas Landsman (RU). Voorbeeld uit een opgave; te bewijzen dat modus ponens een tautologie is: (A ∧ (A → B)) → B. Mag ik dat op onderstaande manier doen of "voldoet" dat niet als formeel bewijs van tautologie?

(A ∧ (A → B)) → B
(A ∧ (¬A V B) → B
(A ∧ ¬A) V (A ∧ B)) → B
A ∧ ¬A ≡ F (falsum)
F V (A ∧ B) ≡ A ∧ B
A ∧ B → B
¬(A ∧ B) V B
¬A V ¬B V B (De Morgan)
¬B V B ≡ T (tertium non datur)
¬A V T ≡ T

Gr.,
Philip Voets

Om te weten of dat een geldig bewijs is moet je weten van welke axioma's en afleidingsregels je uit mag gaan. En dat hangt er weer vanaf binnen welk formeel systeem je werkt. Hoe dan ook staat je bewijs op zijn kop, want je hoort te beginnen met een axioma (of met een reeds eerder bewezen stelling) en te eindigen met de te bewijzen stelling (en niet omgekeerd).

[Philip-Voets]

En stel dat ik de gedachtengang omdraai, zou het dan geldig zijn?

¬A (startpunt)

¬A V ¬B V B (introductie tautologie en V)

¬(A ∧ B) V B (De Morgan)

A ∧ B → B (implicatie)

(A ∧ ¬A) V (A ∧ B)) → B (introductie V en falsum)

(A ∧ (¬A V B) → B (distributie)

(A ∧ (A → B)) → B (implicatie)

?

[Professor Puntje]

Zoals ik al schreef: ik weet niet binnen welk formeel systeem je wil/mag werken. Als je een formeel bewijs wilt leveren moet je expliciet aangegeven wat binnen je gebruikte formele systeem je axioma's zijn, en welke afleidingsregels ertoe behoren. Als dat niet gegeven is heb je ook geen formeel bewijs.

Maar goed, laten we het informeel bekijken.

¬B V B (is altijd waar)

¬A V (¬B V B) (dus dan is die disjunctie ook altijd waar)

Maar op basis waarvan verplaats je voor de volgende stap dan de haakjes?

[Philip-Voets]

Misschien kun je toelichten wat je bedoelt met “welk systeem”.

De haakjes bij ¬(A ∧ B) meer om aan te geven waar de equivalentie ¬A V ¬B ~ ¬(A ∧ B) volgens De Morgan wordt geïntroduceerd. Dat was de gedachte tenminste, haha

[Professor Puntje]

Misschien kun je toelichten wat je bedoelt met “welk systeem”.

Er zijn verschillende mogelijkheden om je axioma's en toegestane afleidingsregels te kiezen. En dat leidt tot verschillende systemen van (propositie)logica.

De haakjes bij ¬(A ∧ B) meer om aan te geven waar de equivalentie ¬A V ¬B ~ ¬(A ∧ B) volgens De Morgan wordt geïntroduceerd. Dat was de gedachte tenminste, haha

Als je de haakjes verplaatst gaat het wel:

¬A V (¬B V B)

(¬A V ¬B) V B

¬(A ∧ B) V B

Het hele punt is dat je niet aangeeft van welke axioma's en afleidingsregels (en eventueel eerder bewezen stellingen) je uit gaat, zodat ook niet is te zeggen welke stappen (zoals het verplaatsen van de haakjes) in je bewijs wel of niet toelaatbaar zijn.

[PhilipVoets]

Helder. Ik heb in ieder geval gebruik van de gegeven stellingen in de syllabus van Landsma gemaakt. Ik weet niet of dat helpt bij het duiden van het bewijs?

[Professor Puntje]

Ik vind die syllabus van Landsma onnodig ingewikkeld. Of wil je zelf een specialist in moderne logica worden? Dan zou het wel nuttig zijn.

Ik heb zelf vroeger het volgende boekje bestudeerd: https://www.bol.com/nl/nl/p/moderne-log ... 048765394/

Dat is veel eenvoudiger!

[PhilipVoets]

Haha, het is meer uit interesse. Ik overweeg een los bijvak “Inleiding Wiskunde” aan de Radboud-universiteit te volgen vanuit thuis (propositielogica, verzamelingenleer, bewijzen door inductie, etc.). Ik moet zeggen dat het doorakkeren van die reader (2022/2023) zonder illustratieve hoor- of werkcolleges een kluif is, maar de reader lijkt ook wat “convoluut” hier en daar..

[Professor Puntje]

Hebben we het wel over dezelfde reader?

[PhilipVoets]

https://www.math.ru.nl/~landsman/Inleid ... de2022.pdf

Deze bedoel ik.