Mini-project II
Question 1
The truth table for the negation of Exercise 1.2.14 from Rosen’s book, i.e. the formula \(\lnot((\lnot p \land (p \to q)) \to \lnot q)\), is shown below.
| \(p\) | \(q\) | \(\lnot p\) | \(p\to q\) | \(\lnot p \land (p \to q)\) | \(\lnot q\) | \((\lnot p \land (p \to q)) \to \lnot q\) | \(\lnot((\lnot p \land (p \to q)) \to \lnot q)\) |
|---|---|---|---|---|---|---|---|
| T | T | F | T | F | F | T | F |
| T | F | F | F | F | T | T | F |
| F | T | T | T | T | F | F | T |
| F | F | T | T | T | T | T | F |
The table shows that \(\lnot((\lnot p \land (p \to q)) \to \lnot q)\) is satisfiable. Specifically, The two leftmost columns and the rightmost column show that the formula is satisfied when \(p\) is true and \(q\) is false.
This can be expressed as the function \(\upsilon\) with domain {\(p,q,\lnot,\land,\to\)}, codomain {\(0,1\)} and the following mapping:
\(\upsilon(\lnot x)\) = 1 if \(\upsilon(x)\) = 0, and 0 otherwise.
\(\upsilon(x \land y)\) = 1 if \(\upsilon(x)\) = 1 and \(\upsilon(y)\) = 1, and 0 otherwise.
\(\upsilon(x \to y)\) = 0 if \(\upsilon(x)\) = 1 and \(\upsilon(y)\) = 0, and 1 otherwise.
Question 2
The function \(\upsilon(x \lor y)\) can be expressed in set-theoretic notation as
\(\{ B_1, \ldots, B \cup \{ \phi\lor\psi \}, \ldots, B_i \} \leadsto \{ \{ B_1, \ldots, B \cup \{ \phi \}, \ldots, B_i \}, \{ B_1, \ldots, B \cup \{ \psi \}, \ldots, B_i \} \}\)
The above expression contains two errors (as pointed out in feedback):
Error #1: The syntax confused branches and formulas.
Error #2: Derived formulas should be negated.
Corrected expression:
\(\{ B_1, \ldots, B \cup \{ \phi\lor\psi \}, \ldots, B_i \} \leadsto \{ B_1, \ldots, B \cup \{ \lnot\phi \}, B \cup \{ \lnot\psi \}, \ldots, B_i \}\)
and the function \(\upsilon(x \to y)\) can be expressed as
\(\{ B_1, \ldots, B \cup \{ \phi\to\psi \}, \ldots, B_i \} \leadsto \{ \{ B_1, \ldots, B \cup \{ \lnot\phi \}, \ldots, B_i \}, \{ B_1, \ldots, B \cup \{ \psi \}, \ldots, B_i \} \}\)
The above expression contains one error (as pointed out in feedback):
Error #1: The syntax confused branches and formulas.
Corrected expression:
\(\{ B_1, \ldots, B \cup \{ \phi\to\psi \}, \ldots, B_i \} \leadsto \{ B_1, \ldots, B \cup \{ \lnot\phi \}, B \cup \{ \psi \}, \ldots, B_i \}\)
Question 3
Obtaining a complete tableau by applying tableau rules can be described in pseudecode like this:
Each round of the while-loop beginning at line 2 either drops a branch, applies rules to a branch, or ends the function. Every rule reduces the length of involved formulas, which means it is certain to eventually stop with either a set of irreducible branches or the empty set of branches.
Question 4
\[\begin{align*} && \{ \lnot p \land p \land \lnot q \} &\leadsto \{ \lnot p, p \land \lnot q \} && \\ && &\leadsto \{ \lnot p, p, \lnot q \} && \end{align*}\]
Question 5
TODO