Matroids Matheplanet Forum Index
Moderiert von mire2 StrgAltEntf
Mathematik » Logik, Mengen & Beweistechnik » Sind folgende Formeln logisch beweisbar?
Autor
Universität/Hochschule Sind folgende Formeln logisch beweisbar?
carlox
Aktiv Letzter Besuch: in der letzten Woche
Dabei seit: 22.02.2007
Mitteilungen: 1249
  Themenstart: 2021-09-14

Hallo allerseits, I) Sind folgende 2 Formeln logisch beweisbar in der Prädikatenlogik 1. Stufe (PL1)? Behauptung 1 (B1): $\vdash \exists x (\alpha \rightarrow \beta) \quad .\rightarrow. \quad \forall x \alpha \rightarrow\exists x \beta$ Behauptung 2 (B2) $\vdash \exists x (Px \rightarrow \forall y Py$) Bei B1 bin ich mir ziemlich sicher. Bei B2 nicht (habe dafür einen möglicherweise aber falschen Beweis). II) Kennt ihr ein Programm, wo man eine Fomel eingeben kann und als Ergebnis dann geliefert wird: logisch beweisbar / nicht bweisbar. Ich weiß, das Problem ist unentscheidbar. Könnte aber sein, dass es ein Programm für "kleinere" Formeln gibt. mfg cx


   Profil
tactac
Senior Letzter Besuch: in der letzten Woche
Dabei seit: 15.10.2014
Mitteilungen: 2185
  Beitrag No.1, eingetragen 2021-09-14

I B1 ist mit Minimallogik beweisbar. B2 ist mit klassischer Logik beweisbar, wenn es in jeder Struktur Individuen der Sorte geben muss, über die da quantifiziert wird. Das kann der Fall sein, oder auch nicht — machen manche so, andere anders. II Ich kenne keins konkret. Aber so berühmte und kleine Beispiele wie B2 (das Trinkerparadoxon) sollten die meisten automatischen Beweiser hinkriegen, auch wenn die einfachsten Beweise wohl recht komplex sind im Vergleich mit der Komplexität der Formel. Alternativ kannst du deinen Beweis (einer ggf. angepassten Variante) ja auch in so etwas wie Lean eingeben zumindest prüfen lassen. (Oder hier vorstellen, und ich übersetze den vielleicht.)


   Profil
carlox
Aktiv Letzter Besuch: in der letzten Woche
Dabei seit: 22.02.2007
Mitteilungen: 1249
  Beitrag No.2, vom Themenstarter, eingetragen 2021-09-15

\quoteon(2021-09-14 20:36 - tactac in Beitrag No. 1) I B1 ist mit Minimallogik beweisbar. B2 ist mit klassischer Logik beweisbar, wenn es in jeder Struktur Individuen der Sorte geben muss, über die da quantifiziert wird. Das kann der Fall sein, oder auch nicht — machen manche so, andere anders. \quoteoff Danke für dein Feedback. B1 konnte ich jetzt mit meinem Beweiskalkül ableiten. mfg cx


   Profil
tactac
Senior Letzter Besuch: in der letzten Woche
Dabei seit: 15.10.2014
Mitteilungen: 2185
  Beitrag No.3, eingetragen 2021-09-16

Okay. Hier mal ein Beweis von B2 mit Taktiken in Lean: \sourceon Lean import tactic theorem Drinker(U : Type)(inh : U)(P : U → Prop): ∃ x : U, P x → ∀ y : U, P y := begin cases em (∀ y, P y), { existsi inh, intro j, assumption }, { push_neg at h, cases h with x i, existsi x, intro j, contradiction } end \sourceoff Und ein Link auf eine JavaScript-Implementierung mit diesem Code zum Rumspielen. Man könnte auch direkt einen Beweisterm schreiben, was dann in etwa eine Kurznotation einer Ableitung in einem Kalkül natürlichen Schließens wäre.


   Profil
carlox
Aktiv Letzter Besuch: in der letzten Woche
Dabei seit: 22.02.2007
Mitteilungen: 1249
  Beitrag No.4, vom Themenstarter, eingetragen 2021-09-17

Hallo tactac, Danke für dein Feedback. Habe auf: https://matheplanet.com/matheplanet/nuke/html/printtopic.php?topic=255286&load_mathjax=1 noch in meinem letzten Posting dort eine Frage (betrifft auch Lean). Ich bitte dich, diese zu beantworten. mfg cx


   Profil
carlox hat die Antworten auf ihre/seine Frage gesehen.
carlox wird per Mail über neue Antworten informiert.

Wechsel in ein anderes Forum:
 Suchen    
 
All logos and trademarks in this site are property of their respective owner. The comments are property of their posters, all the rest © 2001-2021 by Matroids Matheplanet
This web site was originally made with PHP-Nuke, a former web portal system written in PHP that seems no longer to be maintained nor supported. PHP-Nuke is Free Software released under the GNU/GPL license.
Ich distanziere mich von rechtswidrigen oder anstößigen Inhalten, die sich trotz aufmerksamer Prüfung hinter hier verwendeten Links verbergen mögen.
Lesen Sie die Nutzungsbedingungen, die Distanzierung, die Datenschutzerklärung und das Impressum.
[Seitenanfang]