Kolekcja formuł wraz z zaprzeczeniem.

[Ropoocha]

Wykaż, że jesli \(\displaystyle{ \Sigma \not\models \varphi }\), to kolekcja formuł \(\displaystyle{ \Sigma \cup \left \{ \neg \varphi \right \} }\) jest spełnialna.

Zrobiłem to w ten sposób: \(\displaystyle{ \Sigma = \left \{ \varphi_{1}, \varphi_{2}, ..., \varphi_{n} \right \} }\), więc poprzez rozpisanie wynikania zdań mamy:
\(\displaystyle{ \neg \left ( \left ( \varphi_{1}\wedge \varphi_{2}\wedge ...\wedge \varphi_{n} \right ) \rightarrow \varphi \right ) \equiv \neg \left ( \neg\varphi_{1}\vee \neg\varphi_{2}\vee ...\vee \neg\varphi_{n} \vee \varphi \right) \equiv \left ( \varphi_{1}\wedge \varphi_{2}\wedge ...\wedge \varphi_{n}\wedge \varphi \right ) (*)}\).

A \(\displaystyle{ \Sigma \cup \left \{ \neg \varphi \right \} = \left \{ \varphi_{1}, \varphi_{2}, ..., \varphi_{n}, \neg\varphi \right \} }\), stąd po rozpisaniu:
\(\displaystyle{ \left ( \left ( \varphi_{1}\wedge \varphi_{2}\wedge ...\wedge \varphi_{n}\wedge \neg\varphi \right ) \rightarrow \varphi \right ) \equiv \left ( \neg\varphi_{1}\vee \neg\varphi_{2}\vee ...\vee \neg\varphi_{n} \vee \varphi\vee \varphi \right) \equiv \left ( \neg\varphi_{1}\vee \neg\varphi_{2}\vee ...\vee \neg\varphi_{n} \vee \varphi \right) \equiv \neg \left ( \varphi_{1}\wedge \varphi_{2}\wedge ...\wedge \varphi_{n}\wedge \varphi \right ) (**)}\).

Widać stąd, że \(\displaystyle{ (**) }\) jest zaprzeczeniem \(\displaystyle{ (*) }\), co pokazuje, że kolekcja formuł \(\displaystyle{ \Sigma \cup \left \{ \neg \varphi \right \} }\) jest spełnialna.

Jednak nie wiem, czy to poprawny sposób, więc proszę o sprawdzenie tego i jakieś podpowiedzi co do poprawnego rozwiązania.

[Jan Kraszewski]

A na jakiej podstawie zakładasz, że zbiór \(\displaystyle{ \Sigma}\) jest skończony?

JK

[Ropoocha]

Mój błąd, zapomniałem napisać, tak jest zdefiniowane \(\displaystyle{ \Sigma }\) w zadaniu.

[Jan Kraszewski]

Jak definiujesz spełnialność?

JK

[Ropoocha]

Jeśli dobrze pamiętam, to taki warunek musi zostać spełniony:
\(\displaystyle{ \left ( \forall_{\pi} \right ) \left ( \forall_{\varphi\in \Sigma} \right ) \left (\text{eval}(\pi,\varphi)\equiv\textbf{1} \right ) }\), gdzie \(\displaystyle{ \pi }\) to waluacja.

[Jan Kraszewski]

Jeśli dobrze pamiętam, to taki warunek musi zostać spełniony:
\(\displaystyle{ \left ( \forall_{\pi} \right ) \left ( \forall_{\varphi\in \Sigma} \right ) \left (\text{eval}(\pi,\varphi)\equiv\textbf{1} \right ) }\), gdzie \(\displaystyle{ \pi }\) to waluacja.

No chyba nie. Warunek, który napisałeś mówi, że \(\displaystyle{ \Sigma}\) jest zbiorem tautologii. Pomyliłeś kwantyfikator.

JK

[Ropoocha]

Racja, chodziło o: \(\displaystyle{ \left ( \exists_{\pi} \right ) \left ( \forall_{\varphi\in \Sigma} \right ) \left (\text{eval}(\pi,\varphi)\equiv\mathbf{1} \right ) }\).

[Jan Kraszewski]

No i według mnie w dowodzie powinieneś odwołać się do tej definicji.

JK

[Ropoocha]

Rozumiem, tak zrobię, jednak mam problem ze zrozumieniem zapisu \(\displaystyle{ \Sigma \not\models \varphi }\). Czy to oznacza, że z zadaną kolekcją formuł \(\displaystyle{ \Sigma }\) zdanie \(\displaystyle{ \varphi }\) jest zawsze sprzeczne, czy tylko nie jest tautologią, a może być spełnialne.

[Jan Kraszewski]

Rozumiem, tak zrobię, jednak mam problem ze zrozumieniem zapisu \(\displaystyle{ \Sigma \not\models \varphi }\).

To oznacza, że nieprawdą jest, iż \(\displaystyle{ \Sigma \models \varphi }\). Natomiast \(\displaystyle{ \Sigma \models \varphi }\) oznacza, że każda waluacja wartościująca wszystkie elementy \(\displaystyle{ \Sigma}\) na prawdę wartościuje także \(\displaystyle{ \varphi }\) na prawdę. Łącząc to założenie oznacza, że istnieje waluacja, która wartościuje wszystkie elementy \(\displaystyle{ \Sigma}\) na prawdę, ale \(\displaystyle{ \varphi }\) wartościuje na fałsz.. A to już prawie teza...

JK

[Ropoocha]

Teza: \(\displaystyle{ \Sigma \not\models \varphi \rightarrow \left ( \exists_{\pi} \right ) \left (\forall_{\psi\in \Sigma\cup \left \{ \neg\varphi \right \}} \right )\left ( \text{eval}(\pi, \psi)\equiv \mathbf{1} \right ) }\)

Dowód: Zakładamy, że \(\displaystyle{ \Sigma \not\models \varphi }\). Czyli \(\displaystyle{ \text{eval}(\pi, \varphi_{1})\equiv \text{eval}(\pi, \varphi_{2})\equiv ...\equiv \text{eval}(\pi, \varphi_{n})\equiv \mathbf{1} }\) oraz \(\displaystyle{ \text{eval}(\pi, \varphi)\equiv \mathbf{0} }\).
Skoro tak jest, to \(\displaystyle{ \neg\text{eval}(\pi, \varphi)\equiv \mathbf{1} }\), czyli \(\displaystyle{ \text{eval}(\pi, \neg\varphi)\equiv \mathbf{1} }\).
Stąd mamy, że \(\displaystyle{ \text{eval}(\pi, \varphi_{1})\equiv \text{eval}(\pi, \varphi_{2})\equiv ...\equiv \text{eval}(\pi, \varphi_{n})\equiv \text{eval}(\pi, \neg\varphi)\equiv \mathbf{1} }\).
Jeśli teraz stworzymy kolekcję formuł postaci \(\displaystyle{ \Sigma\cup \left \{ \neg\varphi \right \} }\), to wtedy mamy że:
\(\displaystyle{ \left ( \exists_{\pi} \right ) \left (\forall_{\psi\in \Sigma\cup \left \{ \neg\varphi \right \}} \right )\left ( \text{eval}(\pi, \psi)\equiv \mathbf{1} \right ) }\), co trzeba było udowodnić. \(\displaystyle{ \blacksquare }\)

[Jan Kraszewski]

Dowód: Zakładamy, że \(\displaystyle{ \Sigma \not\models \varphi }\). Czyli \(\displaystyle{ \text{eval}(\pi, \varphi_{1})\equiv \text{eval}(\pi, \varphi_{2})\equiv ...\equiv \text{eval}(\pi, \varphi_{n})\equiv \mathbf{1} }\) oraz \(\displaystyle{ \text{eval}(\pi, \varphi)\equiv \mathbf{0} }\).

Wypadałoby trochę to rozbudować - używasz oznaczeń, których wcześniej nie wprowadziłeś. Powinno być:

Wtedy istnieje waluacja \(\displaystyle{ \pi}\) taka, że \(\displaystyle{ \text{eval}(\pi, \varphi_{1})\equiv \text{eval}(\pi, \varphi_{2})\equiv ...\equiv \text{eval}(\pi, \varphi_{n})\equiv \mathbf{1} }\) oraz \(\displaystyle{ \text{eval}(\pi, \varphi)\equiv \mathbf{0} }\).

Skoro tak jest, to \(\displaystyle{ \neg\text{eval}(\pi, \varphi)\equiv \mathbf{1} }\), czyli \(\displaystyle{ \text{eval}(\pi, \neg\varphi)\equiv \mathbf{1} }\).
Stąd mamy, że \(\displaystyle{ \text{eval}(\pi, \varphi_{1})\equiv \text{eval}(\pi, \varphi_{2})\equiv ...\equiv \text{eval}(\pi, \varphi_{n})\equiv \text{eval}(\pi, \neg\varphi)\equiv \mathbf{1} }\).
Jeśli teraz stworzymy kolekcję formuł postaci \(\displaystyle{ \Sigma\cup \left \{ \neg\varphi \right \} }\), to wtedy mamy że:
\(\displaystyle{ \left ( \exists_{\pi} \right ) \left (\forall_{\psi\in \Sigma\cup \left \{ \neg\varphi \right \}} \right )\left ( \text{eval}(\pi, \psi)\equiv \mathbf{1} \right ) }\), co trzeba było udowodnić. \(\displaystyle{ \blacksquare }\)

To w zasadzie może być.

JK