10 11 12 13 14 15 16 17 18 19 20
22 23 24 25
28 29 30 31
Assignment 1, Logic course COMP2620/COMP6262/PHIL2080
Copyright By PowCoder代写 加微信 powcoder
Semester 1, 2022
compiled last: Tuesday 22nd March, 2022, 13:26 General Comments
• The three questions in this assignment account for 15% of the final course mark.
• You have to use the turnitin plugin to hand in your solutions – one file per question. Please add
your information (name and ANU id) at the top of each PDF.
• The plugin is configured in a way that you can’t submit within the first week. This gives us time
to make improvements to the descriptions should that be required before submissions are made. • Please check the announcement forum regularly in case this PDF gets updated/improved. (Line
numbers were added to make changes more transparent in our update history.)
• There are further notes right below the plugin for the assignment. Read them carefully
as they contain important information, e.g., regarding academic misconduct and due dates.
• 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 in the forum! Be careful! Exercise 1 (Natural Deduction) (7 points)
In nutshell, you will have to provide a valid sequent X ⊢ A in propositional Logic and prove its validity both via the formal definition as well as via Natural Deduction (ND). Your sequent will however have to adhere certain restrictions (these restrictions are both of a syntactical nature, but they also refer to which ND rules are used/required to prove it). So make sure you satisfy all requirements!
List of Requirements for your Valid Sequent
You must construct your sequent on your own!
X = {A1, A2, A3}, |X| = 3, 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 ∪ {A} must depend on p, q, and r. The next point states on how many proposition symbols each formula must be based.
Each assumption in X as well as A must contain at least two different proposition symbols. (I.e., neither A1, A2, A3, nor A may consist of a single proposition symbol.)
X may not be contradictory, i.e., A1 ∧ A2 ∧ A3 must be satisfiable.
None of your assumptions may be redundant, i.e., in addition to demanding that A1,A2,A3 ⊢ A
is valid, we also demand:
• A1,A2 ⊢Aisinvalid • A1,A3 ⊢Aisinvalid • A2,A3 ⊢Aisinvalid
Your sequent must enable to perform a ND proof that allows for the following rule applications: • Disjunction elimination (at least once),
• Any rule that performs a vacuous discharge.
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
49 50 51 52 53
58 59 60 61
This is an example with an unnecessary detour. The proof still works if lines (3), (4), and (5) get eliminated as lines (2) and (5) are identical. Adding such loops (e.g., to apply some rules like here →I with a vacuous discharge) is not allowed. If lines can be removed, they have to be removed.
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.
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.
We can’t forbid or prevent tool support (from/for our course), so use what’s there!
Double-check that you did not accidentally miss a constraint that we demand!
How to find an appropriate sequent? That’s the hard part! This requires both an understanding 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).
longer one. For example, consider the following proof
α1 (1) p∧q α1(2)q
α1 (3) p→q α1(4)p α1(5)q
α1 (6) q∧p
showing p ∧ q ⊢ q ∧ p:
1∧E 2→I[] 1∧E 3,4 →E 5,4∧E
Your Exercises
Proving validity and further constraints. (3 points)
Write down a sequent that satisfies all requirements that are demanded above.
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.
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.
Exercise 2 (Semantic Tableau) (5 points)
In nutshell, you will have to provide an invalid sequent X ⊢ A in propositional Logic and prove its invalidity both via the formal definition as well as via Semantic Tableau (and then relate the two). Your sequent will however have to adhere certain restrictions. So make sure you satisfy all requirements!
List of Requirements for your Invalid Sequent
You must construct your sequent on your own!
90 91 92 93
108 109 110 111
X = {A1,A2}, |X| = 2, and P = {p,q}, where P is the set of propositional symbols used. That is, your sequent must be based on two distinct assumptions (formulae), and X ∪ {A} must depend on p and q. The next point states on how many proposition symbols each formula must be based.
Neither assumption in X nor A may exist of just a single proposition symbol (negated or not). (I.e., A1, A2, and A must be a formula that contains at least one connective different from the negation symbol.)
Though A1, A2 ⊢ A must be invalid, A ⊢ A1 ∧ A2 must be valid.
Your Exercises
1. Proving invalidity and validity. (2 points)
(a) Write down your invalid sequent A1 , A2 ⊢ A that satisfies all requirements that are demanded above.
(b) Prove that your sequent is invalid 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 invalidity. As for Exercise 1, briefly explain why your table(s) prove invalidity.
(c) Also prove, again with truth tables and a short explanation, the validity of A ⊢ A1 ∧ A2.
2. Proving invalidity via Semantic Tableau. (3 points)
Prove invalidity of your sequent A1,A2 ⊢ A via Semantic Tableau. Use the notation from the lecture. Make sure to include all required annotations, e.g., indicate whether a branch is contradictory (and if so, why) or whether it’s open. Also indicate for each line where it comes from.
Extract an interpretation from your tableau that proves invalidity and explain (in at most a few sentences) how it relates to the first part of this exercise.
Exercise 3 (Question about Natural Deduction) (3 points)
Assume you are given a sequent X ⊢ A in Propositional Logic and you are able to derive, using Natural Deduction, both some formula B from X as well as its negation ¬B. Assume that the rule RAA is not available to you, otherwise all Natural Deduction rules we taught can be used.
• Can you infer any property (satisfiable, unsatisfiable, tautology) of the formula A1 ∧ · · · ∧ An, provided X = {A1,…,An}?
• Can you say anything about the validity of the sequent? Does its validity depend on which formula A represents?
• In which way does the fact that we don’t have RAA available influence your response?
Answer these questions as precisely as possible. If it supports your arguments, refer to the respective
Natural Deduction rules as required. Provide your explanation in at most 200 words.
Academic Misconduct / Collaboration (and More)
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 mark, so every collaboration is strictly forbidden. Please read our rules on Academic Integrity, Academic Misconduct, and Deadlines and Late Submissions on our Wattle page.
程序代写 CS代考 加微信: powcoder QQ: 1823890830 Email: powcoder@163.com