Sprawdzanie czy formuła jest tautologią

[tomeek]

Mam podaną formułę:
\(\displaystyle{ [(\exists y \sim F(y)\Rightarrow \forall x \exists y G(x,y))\wedge \exists x \forall y \sim G(x,y)] \Rightarrow \forall x F(x)}\)
Muszę sprawdzić, czy jest ona tautologią. Z praw De Morgana:
\(\displaystyle{ [(\sim \forall y F(y)\Rightarrow \forall x \exists y G(x,y))\wedge \sim \forall x \exists y G(x,y)] \Rightarrow \forall x F(x)}\)
Próbuję doprowadzić ją do sprzeczności:
\(\displaystyle{ \forall x F(x) = 0}\)
Aby implikacja była prawdziwa to poprzednik implikacji musi być równy 1, z czego wynika:
\(\displaystyle{ \forall x \exists y G(x,y) = 0}\)
Aby poprzedni implikacji był prawdziwy to:
\(\displaystyle{ \sim \forall y F(y)=0}\)
Z czego uzyskuję:
\(\displaystyle{ \forall y F(y)=1}\)
Tutaj mam pytanie. Zgodnie ze wcześniejszymi założeniami \(\displaystyle{ \forall x F(x) = 0}\), więc \(\displaystyle{ \forall y F(y)=1}\) jest z tym sprzeczne i wynika z tego, iż formuła jest tautologią, czy w związku z tym, iż przy kwantyfikatorze znajduje się inna zmienna związana nie ma sprzeczności i formuła nie jest tautologią?

[Jan Kraszewski]

Zgodnie ze wcześniejszymi założeniami \(\displaystyle{ \forall x F(x) = 0}\), więc \(\displaystyle{ \forall y F(y)=1}\) jest z tym sprzeczne i wynika z tego, iż formuła jest tautologią,

Tak.

nie ma sprzeczności i formuła nie jest tautologią?

Brak sprzeczności w rozumowaniu nie wprost nie jest dowodem na cokolwiek.

Nawiasem mówiąc, w tym momencie

\(\displaystyle{ [(\sim \forall y F(y)\Rightarrow \forall x \exists y G(x,y))\wedge \sim \forall x \exists y G(x,y)] \Rightarrow \forall x F(x)}\)

wystarczy podstawić \(\displaystyle{ p:=\forall y F(y)}\) i \(\displaystyle{ q:=\forall x \exists y G(x,y)}\) i masz prawo rachunku zdań

\(\displaystyle{ \left( (\neg p \Rightarrow q)\land \neg q\right) \Rightarrow p.}\)

JK