xuebaunion@vip.163.com

3551 Trousdale Rkwy, University Park, Los Angeles, CA

留学生论文指导和课程辅导

无忧GPA：https://www.essaygpa.com

工作时间：全年无休-早上8点到凌晨3点

微信客服：xiaoxionga100

微信客服：ITCS521

COMP6262/PHIL2080-comp2620/6262 logic代写-Assignment 1

时间：2023-04-10

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).

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).