COMP2620/6262 (Logic) Tutorial

Week 12
Semester 1, 2026

Tutorial Test
In each tutorial, apart from week 2, there is a short test on skills practised in the previous tutorial. Your
top 8 test attempts, out of the 10 available, will collectively count for 50% of your final mark.
This week’s test is on CTL model checking. Your tutor will hand out paper describing the
algorithm for CTL model checking. Your tutor will also hand out question paper with a CTL formula,
and a transition system on it. You should write your university ID and name on the question paper, and
answer the question on that paper by writing every subformula of the target formula inside or beside
every state at which it holds. Omitting any subformulas, or any states, will cost you marks. You will
have twelve minutes to do this.
You are not permitted to have any other resource on the table during this test, including any electronic
device. If you finish your test before time elapses you may put your hand up and your tutor will collect
your sheet. Once you have done this, you may get a device out and start work silently on this week’s
questions. If you are still working when time elapses you must stop writing immediately and let your
tutor collect your paper.

This Week’s Exercises

This week’s tutorial contains questions from all parts of the course. Concentrate your tutorial time on
whichever part of the course you would most like to work on with a tutor in the room. There is an
appendix in Canvas that you are likely to find useful; this will also be given to you in the exam.

1. Prove or disprove the following propositional logic sequents using truth tables.

ˆ p∨q →p∧r ⊢p→r

ˆ p ∧ q, q ∨ r ⊢ p → q → r
Conceptual question: None of the propositions in the questions above are (on their own)
valid, but all are (again, on their own) satisfiable. Give examples of (a) a valid proposition,
and (b) an unsatisfiable proposition.

2. Prove the following sequents using natural deduction. In the below P is a unary predicate, R is
a binary predicate, f is a unary function, and c is a constant.

ˆ q → ¬p ⊢ ¬(p ∧ q)
ˆ p ∨ q, p → r, q → s ⊢ r ∨ s
ˆ ⊢ (p → q) ∨ (q → r)
ˆ ∀x R(x, F x), ∃x(x = F x) ⊢ ∃x Rxx
ˆ ∀x(P x ∨ Rxx), ∀x∀y(Rxy → P x ∨ P y) ⊢ ∀x P x
ˆ ∃x ¬P x → ∀y P (F y) ⊢ P (F c)

Conceptual question: Give an example of a sequent that is not provable, but would be provable
if we ignored the side condition on the ∀I rule.
3. Using truth table semantics:

1
 ˆ Prove that the following rule is sound. Be careful to explicitly state your assumptions.
Γ ⊢ φ ∧ ψ Γ′ , φ, ψ ⊢ σ
Γ, Γ′ ⊢ σ
ˆ The ‘main lemma’ in the lecture proof of completeness states that, given any proposition φ,
(a) if φ is 1 in the k’th row of its truth table, then πk ⊢ φ can be proved by natural deduction;
(b) If φ is 0 in the k’th row of its truth table, then πk ⊢ ¬φ can be proved by natural
deduction.
where πk is a big conjunction of all propositional variables, or their negation, according the
1s and 0s of the k’th row of the truth table.
Prove the (b) case only of this lemma for a proposition of form φ ∨ ψ. Be careful to explicitly
state your assumptions.

Conceptual question: After the ‘main lemma’ is proved, what role do the πk propositions play
in the completeness proof for propositional logic? Answer using a brief English description, not by
rewriting the proof.
4. Model the following situations using the logic indicated. Be careful to define using English what
symbols you are introducing, e.g. the meaning of your propositional variables.

ˆ (With propositional logic): The Logic department of Australian International University

(AIU) offers three degrees: a Bachelor, a Masters, and a PhD. To receive any of these degrees
you must enrol in them. One needs to have received the Bachelor degree to enrol in the
Master’s programme, whereas for enrolment in the PhD programme, successful completion of
either the Bachelor or the Masters is enough.
ˆ (With first order logic): Anyone that learns Logic is sure to teach it to someone else. But no
one learns Logic unless they teach it to themselves. Teaching Logic to someone who doesn’t
learn it is obviously a waste of both people’s time. Therefore, in order to avoid wasting
anyone’s time, one must teach Logic only to those who are also teaching themselves.
ˆ (With Logic4Fun; precise syntax that would check successfully is not essential so long as we
can tell what is meant): In a certain country there are five holidays. Each celebrates one of
five ‘elements’: fire, water, wood, metal, and earth. Each season (spring, summer, autumn,
and winter) has at least one holiday. Encode the clues regarding the relationship between
elements and seasons.
– The earth celebration does not have a season all to itself.
– When do we think about the wood element? In autumn, of course!
– The earth holiday happens in the season immediately after the metal holiday, and water
comes similarly after earth.
– Around the time winter turns to spring, metal has its day. But before, or after, the
change?
ˆ (With LTL): You are planning a degustation menu (a meal with a large number of little meals,
or ‘courses’, delivered one after the other). Your customers have given you some rules which
you will need to follow:
– There must be at least three courses.
– The first course should be savoury (not sweet) and the final course should be sweet.
– It is okay if some courses are not vegan, but don’t have two courses like that in a row.
– There must be at least one sweet vegan course, and at least one savoury vegan course.
ˆ (With CTL*): You are designing a machine with two buttons, red and white, and two lights
of these colours. Both buttons are pressable, but it is not possible to press them both at the
same moment. If either button is pressed, the light of the corresponding colour must shine 1
second later. The red light will eventually turn itself off, but the white light, once on, must
shine forever. Therefore it is possible for both buttons to shine together.

Conceptual question: Logic4Fun allows one to name multiple sorts. How could we express this
concept in first order logic? You do not need to consider the various attributes Logic4Fun allows
one to define for sorts, such as cardinality and enumeration.

2
5. Using first order logic semantics:

ˆ Let t be a term, x be a variable, and d be an element of the universe of discourse. Prove that
if x does not occur in t, then tM,e = tM,e[x7→d] .
y induction on t. The base case is a variable y not equal to x. Then tM,e = e(y) = e[x 7→
d](y) = tM,e[x7→d] .
For the step case, let t have form f (t1 , . . . , tn ) for some n ≥ 0. Assume for induction
M,e[x7→d]
that tM,e
i = ti for all 1 ≤ i ≤ n. Then f (t1 , . . . , tn )M,e = f M (tM,e 1 , . . . , tM,e
n ) =
M,e[x7 → d] M,e[x7 → d]
f M (t1 , . . . , tn ) by the induction assumption. This is f (t1 , . . . , tn )M,e[x7→d] .
ˆ Prove that the following rule is sound, for any term t. Be careful to explicitly state your
assumptions.

Γ ⊢ φ
x∈
/ F V (Γ) :
Γ ⊢ φ[t/x]
You will need the substitution lemma: ⊨M,e φ[t/x] if and only if ⊨M,e[x7→tM,e ] φ

Conceptual question: Suppose we altered the definition of first order logic semantics to allow
the universe of discourse to potentially be the empty set. Which natural deduction rule would
become invalid?
6. Prove or disprove the following sequent using tableaux. If the sequent is not valid, extract a model
that acts as a counterexample.

ˆ p ∧ q → r ⊢ ¬r → ¬p ∨ q
ˆ ∃x∀y Rxy ⊢ ∀x∃y Ryx (in this question and the next, R is a binary predicate).
ˆ ∀x∃y Rxy ⊢ ∃x Rxx
ˆ G(p ∨ q) ⊢ p U q
ˆ F p, ¬p ⊢ F Xp
ˆ GF p, GF ¬p ⊢ ⊥

Conceptual question: In which scenario would neither the Loop, nor the Simple Repetition rule,
guarantee termination of an LTL tableau?
7. For each of the following pairs of temporal logic formulas, one of the pair implies the other,
but the implication in the other direction does not work. Identify which direction is which, give a
proof via semantics that one implication works, and give a counterexample model showing that
the other implication fails.

ˆ (LTL) Gp ∧ F q and Gp U q
ˆ (CTL) AXp → EXq and AX(p → q)
ˆ (CTL*) A[E[α]] and E[A[α]] - for the counterexample you will need to suggest a path propo-
sition α.

8. Apply model checking to the following formulas and models. When you do so, label every state
with every applicable subformula. If the formula uses symbols not in the subset we learned model
checking for (EX, EG, EU for CTL; X, U for LTL; and variables, ⊥, ¬, ∧, ∨ for both) then you
must first modify the formula using equivalences so that is as required for the algorithm.

ˆ EG EF p and

p
s0 s1

s2 s3

3
ˆ E[EXp U EG EXq] and

s1 s2
p q
s0

q p
s3 s4

ˆ Gp and

s0 s1 s2
p p

For this and the next question, display the results of the third step as a separate picture from
the result of the second step (unless the third step produces no change).
ˆ p U Xq and
s1
q
s0 s3
p q

s2

Conceptual question: Two algorithms were presented for model checking EGp. Give a rea-
son why the version involving Strongly Connected Components might be considered superior.