Assignment 1, Logic Course
COMP2620/COMP6262/PHIL2080
General Comments
• Due date is 16 April, 23:59pm (Canberra time).
• The two questions in this assignment account for 15% of the final course mark.
• You have to use the turnitin plugin onWattle to hand in your solutions. Please add your information
(name and ANU id) at the top of your PDF.
• Do not copy our questions into your answers! Just provide their numbers and your answers.
• All text must be written with a computer (word, LATEX etc.), you are not allowed to write by
hand and insert a photograph. Such photographs are fine for truth tables, Semantic Tableaux, and
Natural Deduction proofs, but not for text.
• Do not reveal potential solutions when asking questions on the forum! Be careful!
Question 1 (Natural Deduction) (8 points)
In nutshell, you will have to provide a valid sequent X ⊢ C in propositional Logic and prove its validity
both via the formal definition as well as via Natural Deduction (ND). Your sequent will however need to
adhere to certain restrictions. These restrictions will make sure that almost every sub-question in this
Assignment is doable. So please carefully make sure you satisfy all requirements! The first few questions
are there to check that these requirements are satisfied (and that you understand what they mean, of
course).
List of Requirements for your Valid Sequent
You must construct your sequent on your own!
1. X = {A1, A2, A3}, |X| = 3 (meaning that there are exactly three different elements), and P =
{p, q, r} (where P is the set of propositional symbols used). That is, your sequent must be based
on three distinct assumptions (formulae), and X ∪ {C} must all depend on p, q, and r. The next
point states on how many proposition symbols each formula must be based.
2. Each assumption in X as well as C must contain at least two different proposition symbols. (I.e.,
neither A1, A2, A3, nor C may consist of only a single proposition symbol.)
3. X may not be contradictory, i.e., A1 ∧A2 ∧A3 must be satisfiable.
4. None of your assumptions may be redundant, i.e., in addition to demanding that A1, A2, A3 ⊢ C
is valid, we also demand:
• A1, A2 ⊢ C is invalid
• A1, A3 ⊢ C is invalid
• A2, A3 ⊢ C is invalid
5. Your sequent must enable to perform a ND proof that allows for the following rule applications:
• Disjunction elimination (at least once),
• Negation elimination, as well as negation introduction. We want to see both of these rules
used at least once, so you are welcome to use RAA, but only if you also use ¬E and ¬I
somewhere.
1
Note that your proof is not allowed to contain redundant lines. I.e., if a certain number of lines
can be removed from your proof without violating its correctness, you have to do so. Note that
this does not mean that your proof has to be optimal: you can still submit a proof with, say, 15
lines, even though one with 10 lines might exist! But that 10-liner may not be a subproof of the
longer one. For example, consider the following proof showing p ∧ q ⊢ q ∧ p:
α1 (1) p ∧ q A
α1 (2) q 1 ∧E
α1 (3) p→ q 2 →I[]
α1 (4) p 1 ∧E
α1 (5) q 3,4 →E
α1 (6) q ∧ p 5,4 ∧E
This is an example with an unnecessary detour. The proof still works if lines (3) and (5) get
eliminated. Adding such loops is not allowed (even if it allows you to use one of the required rules).
If lines can be removed, they have to be removed.
Finally, your sequent must not be too close to any of the homework/tutorial/practice questions/etc.
provided by us. Specifically, any two of A1, A2, A3, C may not be the same as in any practice
question. This mostly just means that you may not alter any practice questions in order to fit the
requirements, so again, come up with your own sequents!
Your Exercises
1. Proving validity and further constraints. (4 points)
(a) Write down a sequent that satisfies all the requirements that are demanded above.
(b) Prove that your sequent is valid using the formal definition of validity, i.e., via truth tables.
Explain in a few sentences why and how your truth table(s) do actually prove validity. You
don’t have to write much just for the sake of it – a few sentences are fine. But we need to be
convinced that you actually understand why your table(s) prove validity. If we are in doubt
you lose marks. Just the table might score zero.
(c) Explain in at most a few sentences why/how your table(s) show(s) that X is not contradictory
and why none of the assumptions are redundant. Be specific here.
Note that you can score fully for this part even if your sequent only satisfies all criteria 1 to 4, but
not all from 5.
2. Proving validity via Natural Deduction. (4 points)
For the sequent you presented in the first part of this exercise (satisfying constraints 1. to 4.),
present your proof that also satisfies all restrictions listed in constraint number 5. Use the notation
from the course.
Hints
• You are more than welcome to use the proof checker on wattle, but all work must be your own.
This means no AI usage or anything of the like (be careful here, AI is often wrong in very subtle
ways, and we will mark strictly on these points).
• Double-check that you did not accidentally miss a constraint that we demand!
• How do you find an appropriate sequent? That’s the hard part! This requires both an understand-
ing of the semantics of formulae and sequents, as well as how the ND proof steps/rule work (e.g.
think about which formulae are required at which part of the sequent for a certain rule application).
Question 2 (Semantic Tableau) (7 points)
We would now like you to come up with an invalid sequent in Propositional Logic and prove its invalidity
via Semantic Tableaux. Given what you have shown in the previous exercise, creating this sequent is
easy to do!
2
Your Exercises
1. Proving invalidity. (4 points)
(a) Prove invalidity of the sequent A1, A2 ⊢ C via Semantic Tableau (with Ai and C the same as
in Exercise 1.
2. Extracting an interpretation. (3 points)
(a) Extract an interpretation from your second tableau (of A1, A2 ⊢ C) that proves invalidity and
explain why this interpretation proves invalidity.
Academic Misconduct / Collaboration / Extension
Again, note that any form of collaboration is strictly forbidden for this assignment and any other!
Assignments (and the exam) contribute towards the final course marks, so any collaboration is strictly
forbidden. The deadline is strict and no extension is allowed (unless supported by a verifiable evidence).