| |
| Autor |
 Sind folgende Formeln logisch beweisbar? |
|
carlox
Aktiv 
Dabei seit: 22.02.2007
Mitteilungen: 1528
 |  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 
Dabei seit: 15.10.2014
Mitteilungen: 2796
 | 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
Dabei seit: 22.02.2007
Mitteilungen: 1528
| 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
Dabei seit: 15.10.2014
Mitteilungen: 2796
| 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
Dabei seit: 22.02.2007
Mitteilungen: 1528
| 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. |
|
All logos and trademarks in this site are property of their respective owner. The comments are property of their posters, all the rest © 2001-2023 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]
|
Home / Seite ohne Frame
Wie unterstütze ich den Matheplaneten mit Geld?
