Mini-project I

Problem 1

Exercise a

That a propositional formula is satisfiable means it has at least one solution, i.e. at least one combination of involved truth variables leads to a true statement.

That a propositional formula is a tautology means it is always true, i.e. all combinations of involved truth variables lead to a true statement.

That a propositional formula is a contradiction means it is never true, i.e. no combinations of involved truth variables lead to a true statement.

Exercise b

1.2.11 b

\(p \to (p \lor q)\) is a tautology iff its negation is not satisfiable.

The proposition is therefore negated, and then – since only tableau rules for negation and conjunction are permitted here – rewritten using Material nonimplication and De Morgan’s 2nd law, in that order:

\[\begin{gather*} \lnot (p \to (p \lor q)) \\ \Updownarrow \\ p \land \lnot (p \lor q)) \\ \Updownarrow \\ p \land \lnot p \land \lnot q \end{gather*}\]

This negated and rewritten proposition is then tested for satisfiability using tableau method:

The above tableau is complete, and its only branch is closed as it contains both formulas \(p\) and \(\lnot p\). This proves that the proposition negated is a contradiction, hence the proposition itself is a tautology.

1.2.11 c

\(\lnot p \to (p \to q)\) is a tautology iff its negation is not satisfiable.

The proposition is therefore negated, and then – since only tableau rules for negation and conjunction are permitted here – rewritten using Material implication (twice):

\[\begin{gather*} \lnot (\lnot p \to (p \to q)) \\ \Updownarrow \\ \lnot p \land \lnot (p \to q) \\ \Updownarrow \\ \lnot p \land p \land \lnot q \end{gather*}\]

This negated and rewritten proposition is then tested for satisfiability using tableau method:

Being logically equivalent to previous 1.2.11 b, the above tableau is complete, and its only branch is closed as it contains both formulas \(p\) and \(\lnot p\). This proves that the proposition negated is a contradiction, hence the proposition itself is a tautology.

Exercise c

\(((P \to Q) \to P) \to P\) (Peirce’s law) is a tautology iff its negation has no solution:

The proposition is therefore negated, and then – since only tableau rules for negation and conjunction are permitted here – rewritten using Material implication (thrice):

\[\begin{gather*} \lnot (((P \to Q) \to P) \to P) \\ \Updownarrow \\ \lnot ((\lnot (P \land Q) \to P) \to P) \\ \Updownarrow \\ \lnot (\lnot (\lnot (P \land Q) \land P) \to P) \\ \Updownarrow \\ \lnot \lnot (\lnot (\lnot (P \land Q) \land P) \land P) \end{gather*}\]

This negated and rewritten proposition is then tested for satisfiability using tableau method:

The above tableau is complete with one branch open, proving that the proposition negated is not a contradiction, hence the proposition itself is not a tautology.

Exercise d

Yes.

I cannot prove that completing a tableau is always possible for proposition logic, but cannot intuitively imagine a counter-example either. I trust Graham Priest, when in the presented chapter about review[ing] classical propositional logic he writes that [i]n the present case, the branches of a completed tableau are always finite, where I assume that by the present case he is referring to propositional logic.

This assumption, that propositional logic but not higher-order logic can be deterministically resolved in finite computing time, aligns with feedback I recievd from professors at the beginning of my bachelor when I excitedly shared that my field of interest was Semantic Web: They tried (as I recall) to explain to me, that the scientific interest in Semantic Web has faded in recent times due to higher order logic having been proven not reliably computable.

Problem 2

Exercise a

For the tableau to be satisfiable, either of its two branches must be satisfiable. Left branch requires \(q\) to be both true and false and right branch that \(p\) is both true and false, neither of which is possible to satisfy, hence the tableau as a whole is unsatisfiable.

Problem 3

Exercise a

Given that an inhabitant of the country speaks either always true or always false, each person represents a logical truth value.

Let \(P(x)\) be x is a politican and \(S(x, y)\) be x says y, where \(P(x) \equiv \lnot x\) and \(S(x, y) \equiv (x \land y) \lor (\lnot x \land \lnot y)\).

The conversation can now be expressed in propositional logic as \(S(b,S(a,\lnot P(a))) \land S(c,P(a))\).

The above ignores temporal aspects of the conversation, notably the explicitly mentioned fact that \(c\) spoke after \(b\), because \(b\) spoke about a fact unknown to \(c\), so knowledge of \(b\) speaking truth or not cannot affect the later statement.

More generally it might be part of the riddle whether both strangers and inhabitants has to take a lot of care when interacting, or if inhabitants can tell each other apart. Again this has no consequence for the concrete conversation, however, since the two statements are independent of each other.

Exercise b

\(S(b,S(a,\lnot P(a))) \land S(c,P(a))\) is first rewritten using \(P(x)\) equivalence (twice), double negation elimination, and \(S(x, y)\) equivalence (thrice):

\[\begin{gather*} S(b,S(a,\lnot P(a))) \land S(c,P(a)) \\ \Updownarrow \\ S(b,S(a,\lnot \lnot a)) \land S(c,P(a)) \\ \Updownarrow \\ S(b,S(a,\lnot \lnot a)) \land S(c,\lnot a) \\ \Updownarrow \\ S(b,S(a,a)) \land S(c,\lnot a) \\ \Updownarrow \\ S(b,(a \land a) \lor (\lnot a \land \lnot a)) \land S(c,\lnot a) \\ \Updownarrow \\ ((b \land ((a \land a) \lor (\lnot a \land \lnot a))) \lor (\lnot b \land \lnot ((a \land a) \lor (\lnot a \land \lnot a))) ) \land S(c,\lnot a) \\ \Updownarrow \\ ( (b \land ((a \land a) \lor (\lnot a \land \lnot a))) \lor (\lnot b \land \lnot ((a \land a) \lor (\lnot a \land \lnot a))) ) \land (c \land \lnot a) \lor (\lnot c \land \lnot \lnot a) \end{gather*}\]

The proposition is tested for satisfiability using tableau method, involving also the teo disjunction rules in Priest’s section 1.4.4 (in addition to the three rules listed in this mini project):

The above tableau is complete with 3 of its 6 branches open, proving that the proposition is satisfiable. The open branches show the possible solutions t the riddle: {\(\lnot a, b, c\)}, {\(a, b, \lnot c\)} and {\(a, \lnot b, \lnot c\)}, i.e. Albert is either a politician or a citizen, Billy is a citizen when Albert is a citizen, and Camilla is the opposite of Albert.

(Billy being conditional to Albert is surprising, and may indicate an error somewhere in the tableau: it was expected that Albert was simply either/or)

Exercise c

Not understood.