| |
| Autor |
 Ist diese Formel beweisbar in Prädikatenlogik 1. Stufe? |
|
carlox
Aktiv 
Dabei seit: 22.02.2007
Mitteilungen: 1504
 |  Themenstart: 2023-01-21
|
Hallo allerseits,
ich probiere schon einige Zeit folgende Formel innerhalb der Prädikatenlogik 1. Stufe zu beweisen:
$\forall y (A \rightarrow B) \land \exists yA \rightarrow \exists y (A \land B)$
Als Schlussregeln habe ich zur Verfügung:
Modus Ponens
Substitution
Gv (vordere Generalisierung),
Ph (hintere Generalisierung),
Gh (falls „keine freie Variable“),
Pv (falls „keine freie Variable“)
und einige Axiome.
Ich komme leider nicht weiter.
Wer kann mir da weiterhelfen?
Habe schon probiert:
$A \land (A \rightarrow B) .\rightarrow. A \land B$
Dann Gv:
$\forall y (A \land (A \rightarrow B)) \quad .\rightarrow. \quad A \land B$
mit Quantorenverteilung
$\forall y A \land \forall y(A \rightarrow B) \quad .\rightarrow. \quad A \land B$
Dann Ph
$\forall y A \land \forall y(A \rightarrow B) \quad .\rightarrow. \quad \exists (A \land B)$
Knapp daneben ...komme nicht weiter
Mit freundlichen Grüßen
cx
|
 Profil
|
carlox
Aktiv 
Dabei seit: 22.02.2007
Mitteilungen: 1504
| Beitrag No.1, vom Themenstarter, eingetragen 2023-01-21
|
Die Formel müsste wahr sein.
Zumindest, wenn man sie online prüft mit:
https://logic.tamu.edu/cgi/equivalency.pl
Dort gebe ich die 2 Formeln ein und das Tool sagt, dass diese äquivalent sind:
(Bitte E in der Formel durch $ ersetzen)
EyAy&@y(Ay→By)→Ey(Ay&By)
F->F
mfg
cx
|
Profil
|
nzimme10
Senior
Dabei seit: 01.11.2020
Mitteilungen: 2050
Wohnort: Köln
 | Beitrag No.2, eingetragen 2023-01-21
|
Ja, die Aussage ist richtig.
\sourceon Lean
import tactic
open classical
variable (X : Type)
variable (A : X → Prop)
variable (B : X → Prop)
theorem T : (∀(x : X), A(x) → B(x)) → (∃(y : X), A(y)) → ∃(z : X), A(z) ∧ B(z) :=
begin
intros h1 h2,
cases h2 with x hx,
use x,
split,
{
exact hx,
},
{
apply h1,
exact hx,
},
end
--Term-mode Beweis: λ h ⟨x,hx⟩, ⟨x,hx,h x hx⟩
\sourceoff
LG Nico
|
Profil
|
carlox
Aktiv
Dabei seit: 22.02.2007
Mitteilungen: 1504
| Beitrag No.3, vom Themenstarter, eingetragen 2023-01-21
|
\quoteon(2023-01-21 22:13 - nzimme10 in Beitrag No. 2)
Ja, die Aussage ist richtig.
\quoteoff
Danke für deine Mühe.
Hättest du dich nicht gemeldet, dann würde ich noch einige Zeit darüber brüten, denn ich wäre davon ausgegangen, dass der Fehler bei mir liegt.
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?
