Prädikatenlogischer Beweis lösen

Beweisen Sie Folgendes mit FOL in forallx

Verwenden Sie das natürliche Deduktionssystem und die Beweisstrategien in forallx , um einen formalen Beweis für Folgendes zu liefern. Bitte stellen Sie ein Foto Ihres Beweises zur Verfügung.

∃xFx ∧ ∀yGy ∴ ∃x(Fx ∧ Gx)

Was hast du versucht? Welche Regeln denken Sie zu verwenden?
Ich bin kein Experte für das Forallx- Beweissystem, aber innerhalb des "normalen" natürlichen Abzugs ist der Beweis eine sehr einfache Übung in der Anwendung von Quantifiziererregeln.
Ich bin mir nicht sicher, ob ich vorwärts oder rückwärts arbeiten soll, um die Schlussfolgerung abzuleiten.
Sie können mit der Vereinfachung der Prämisse beginnen.
Willkommen bei der SE-Philosophie! Vielen Dank für Ihren Beitrag. Bitte nehmen Sie sich einen kurzen Moment Zeit , um an der Tour teilzunehmen oder um Hilfe zu bitten . Sie können hier Suchen durchführen oder auf der Meta-Site nach weiteren Erläuterungen suchen . Vergessen Sie nicht, wenn jemand Ihre Frage beantwortet hat, können Sie auf den Pfeil klicken, um den Beitragenden zu belohnen, und auf das Häkchen klicken, um die Ihrer Meinung nach beste Antwort auszuwählen.
Bei dieser Frage geht es darum, ob Sie die Eliminationsregeln für den Existenzquantor verstehen. Stellen Sie sich das so vor - wie würden Sie Ihre Beweisregeln verwenden, um einen bestimmten konstanten Term "c" so auszuwählen, dass "F(c)"? Wenn Sie dann dieses 'c' haben, was können Sie sonst noch damit machen, und was könnte Ihnen das sagen?

Antworten (2)

Ich bin mir nicht sicher, ob ich vorwärts oder rückwärts arbeiten soll, um die Schlussfolgerung abzuleiten.

Warum nicht beide? Sie wissen, womit Sie anfangen müssen und wohin Sie wollen.

Ihre Prämisse ist eine Konjunktion eines existenziellen und eines universellen. Schauen Sie sich die Regeln der Konjunktionsbeseitigung, der universellen Beseitigung und der existenziellen Beseitigung an. Sehen Sie, was Ihnen dieser Start gibt, mit dem Sie arbeiten können.

Ihre Schlussfolgerung ist ein Existential einer Konjunktion. Schauen Sie sich die Regeln der Konjunktionseinführung und der existentiellen Einführung an. Finden Sie, was Sie brauchen, um das endgültige Ziel zu erreichen.

Überbrücken Sie sie miteinander.

Nehmen Sie ∃xFx ∧ ∀yGy an und beweisen Sie dann ∃x(Fx ∧ Gx) basierend auf dieser Annahme.

Verwenden Sie die Konjunktionselimination, um ∃xFx aus Ihrer Annahme abzuleiten. Instanziieren Sie dann die Variable x in eine Konstante, sagen wir a.* Das Ergebnis ist Fa.

Verwenden Sie die Konjunktionselimination, um ∀yGy aus Ihrer anfänglichen Annahme abzuleiten. Daraus können Sie die Variable y in eine beliebige Konstante, z. B. a, instanziieren.** Das Ergebnis ist Ga.

Verwenden Sie die Konjunktionseinführung, um Fa und Ga zu kombinieren, wobei das Ergebnis Fa ∧ Ga ist.

Verwenden Sie die existenzielle Verallgemeinerung, wobei die Variable x jedes Vorkommen von a ersetzt. Das Ergebnis ist ∃x(Fx ∧ Gx).

*Die Konstante kann nicht bereits im Beweis verwendet werden. Das liegt daran, dass ∃ auf etwas im Definitionsbereich zutrifft, wir aber nicht genau wissen, was. ** Universalien gelten für alles in der Domäne, nicht nur für etwas. Das heißt, wir können wählen, y in die Konstante a zu instanziieren.

Prädikatenlogischer Beweis lösen
AntwortenHierDatenschutz-Bestimmungen1y, 0v