Logika - redukcja logiki pierwszego rzędu obejmującej materialny warunek
Przypuszczam, że $$ \forall x \forall y: P(x,y) \implies Q(x) $$ i $$ \forall x \exists y: P(x,y) $$
W takim razie mogę to stwierdzić $$ \forall x: Q(x) $$
Jeśli to prawda, jakie jest tego uzasadnienie?
Co próbowałem:
$$ \begin{align} &\forall x \forall y: P(x,y) \implies Q(x)\\ &\iff \forall x \forall y:\lnot P(x,y) \lor Q(x)\\ &\iff \forall x: (Q(x) \lor \forall y:\lnot P(x,y))\\ &\iff \forall x: (Q(x) \lor \lnot (\exists y:P(x,y))) \end{align} $$ Łącząc wynik z $\forall x \exists y: P(x,y)$, Doszedłem do tego $Q(x)$ powinno być prawdziwe dla wszystkich $x$ od $\lnot (\exists y:P(x,y))$ jest zawsze fałszywa.
$$ \begin{align} &\forall x: (Q(x) \lor \lnot (\exists y:P(x,y))) \land \forall x \exists y: P(x,y)\\ &\iff \forall x: ((Q(x) \lor \lnot (\exists y:P(x,y))) \land \exists y: P(x,y))\\ &\iff \forall x: (Q(x) \land \exists y: P(x,y))\\ &\implies \forall x: Q(x) \end{align} $$
Odpowiedzi
Wszystko się zgadza. w tym ostatnim kroku możesz faktycznie użyć dystrybucji$\forall$ nad $\land$ jeszcze raz:
$$\forall x : (Q(x) \land \exists y : P(x,y))$$
$$\Leftrightarrow$$
$$\forall x : Q(x) \land \forall x \exists y : P(x,y))$$
$$\Rightarrow$$
$$\forall x : Q(x)$$
Nie nauczyłeś się jeszcze formalnych wyprowadzeń?
Jeśli to prawda, jakie jest tego uzasadnienie?
$\def\boxit#1{\bbox[lemonchiffon,0.5ex]{#1}}$Posiadamy lokal $\boxit{\forall x~\forall y:(P(x,y)\to Q(x))}$ i $\boxit{\forall x~\exists y:P(x,y)}$. Czy powinniśmy wziąć dowolną zmienną,$\boxit a$, następnie wnioskujemy z drugiej przesłanki, że istnieje zmienna świadka, nazwij ją $\boxit b$, który spełnia $\boxit{P(a,b)}$. W przypadku tych zmiennych wnioskujemy również z pierwszej przesłanki, że$\boxit{P(a,b)\to Q(a)}$będzie zadowolony. Dlatego wnioskujemy o tym na podstawie modus ponens$\boxit{Q(a)}$jest spełniony. Od$\boxit b$ nie występuje w tej instrukcji, i $\boxit a$ jest arbitralne, dlatego też to pokazaliśmy $\boxit{\forall x:Q(x)}$ wynikają z tych przesłanek.
$$\def\fitch#1#2{~~~~{\begin{array}{|l}#1\\\hline#2\end{array}}}\fitch{~~1.~\forall x\,\forall y:(P(x,y)\to Q(x))\hspace{3.5ex}\textsf{Premise}\\~~2.~\forall x\,\exists y:P(x,y)\hspace{14ex}\textsf{Premise}}{\fitch{~~3.~\boxed a\hspace{23.5ex}\textsf{Assumption (Arbitrary)}}{~~4.~\forall y:(P(a,y)\to Q(a))\hspace{4ex}\textsf{Universal Elimination, 1}\\~~5.~\exists y:P(a,y)\hspace{14.5ex}\textsf{Universal Elimination, 2}\\\fitch{~~6.~\boxed b~P(a,b)\hspace{13.5ex}\textsf{Assumption (Witness)}}{~~7.~P(a,b)\to Q(a)\hspace{8ex}\textsf{Universal Elimination, 4}\\~~8.~Q(a)\hspace{18.5ex}\textsf{Conditional Elimination, 6, 7}}\\~~9.~Q(a)\hspace{21.5ex}\textsf{Existential Elimination 5, 6-8}}\\10.~\forall x:Q(x)\hspace{19.75ex}\textsf{Universal Introduction, 3-9}}$$