Tautology And Contradiction Assignment

Assignment Task

Question 1

A tautology is a statement that is true for every valuation of the propositional variables it contains; a contradiction is a statement that is false for every valuation of the variables; and a contingency is a statement that is neither a tautology nor a contradiction.

Which of the following are tautologies, which are contradictions, and which are contingencies?

(a) p ➾ (pV ~p)

(b) (p➾ q) ⇔(q➾ 7p)

In each case, you should present a truth table to justify your answer.

Question 2

Using the algebra of propositional logic, rewrite the propositions of Question 1 in their simplest equivalent forms. (By simplest, we mean the form that has the fewest logical connectives.) In each case you should justify the rewriting through a chain of equivalences of the form

p=> (pV -p)

Question 3

By constructing proof trees, show that the tautologies of Question 1 (if there
are any) are theorems of the propositional calculus. In doing so, you may
make use of any theorems proved during the course.

Question 4

Assume two sets, A = {0,1,2} and B = {0,1}. Assume also a relation,
R∈ A ⟷ B, such that R= {0⟷1,1⟷0,2⟷1}.

(a) Give values for the following.

(i) #(A © B)

(ii) #(A + B)

(iii) #(A > B)

(iv) #(A +» B)

(v) #(A — B)

(vi) #(A > B)

(b) Give values for the following.

(i) The reflexive closure of R.

(ii) The symmetric closure of R.

(iii) The transitive closure of R.

Question 5

The relational composition operator is associative, which is to say that, if

R ∈ W ⟷ X, S ∈ X ⟷ Y and T ∈ Y ⟷ Z, then the statement

(R:S):T = R: (S:T)

is a theorem. To prove this, it is enough to complete the following chain of
equivalences:

w ⟶ z € (R:S) :T
=>
w ⟶ z € R :(S:T)

Complete this (short) proof by completing the chain, justifying each step
with a reference to a standard definition or an equivalence of predicate logic.

Question 6

You have been asked to think about a data model for an initial prototype of a messaging system.

The model makes use of the following basic types, free types and abbreviations:

[ User Id ]

| Messageld |

YesNo := Yes | No

Timestamp == N
The variable current represents the current time:
| current : Timestamp
The data associated with the system is represented via the following.

users : F Userld

messages : MessageId ++ (UserId x Userld x Timestamp)
received_status : MessageId + YesNo

received_time : Messageld ++ Timestamp

read_status : MessageId ++ YesNo

read_time : Messageld ++ Timestamp

This captures the following:

The system keeps track of a (finite) set of users.
The messages function maps message identifiers to triples. In position 1 of each such triple is the identifier of the user who sent the message; in position 2 is the identifier of the recipient; in position 3 is the time at which it was sent.
The functions received_status and read_status are concerned with the status of messages whether they’ve been read or received, respectively.
The functions received_time and read_time document the times at which messages are received and read, respectively.

Complete the definition by writing the following predicates.

(a) Any user identifier that appears in messages must also appear in users.

(b) Users can’t send messages to themselves.

(d) Only sent messages can be received.

(e) Only received messages can be read.

(f) All received messages (and no others) appear in received_time.

(g) All read messages (and no others) appear in read_time.

(h) Messages can be received only after they’ve been sent.

(i) Messages can be read only after they’ve been received.

Question 7

Assuming the sets and functions of the previous question, represent the following via the mathematical language of Z.

(a) The set of identifiers of messages that have been sent, but not received.

(b) The set of identifiers of messages that have been received, but not read.

(c) The identifier of the user who sent the first message. (You should feel
free to assume that there is a unique such user.)

(d) The identifier of the user who has sent the most messages. (You should
feel free to assume that there is a unique such user.)

Question 8

Consider the following free type definition:)

Status := SentButNotReceived | ReceivedButNotRead | Read

a) Assuming the above, together with the sets and functions of Questions 6 and 7, define — in terms of messages, read_status and received_status (and anything else that you deem to be of relevance) — a function, message_status € Messageld ++ Status, that maps message identifiers to their status. So, for example, given some m € Messageld as in-put, the function would return ReceivedButNotRead as output if that
message has been received, but not read.

b) Assuming the above, together with the sets and functions of Questions 6 and 7, define — in terms of messages, read_status and received_status (and anything else that you deem to be of relevance) — a function

change_status_to_read €
((MessageId ++ Status) x MessageId) +»
(Messageld ++ Status)

that has the effect of changing the status of a specific message from
ReceivedButNotRead to Read.

Question 9

Assume the existence of message_status:

| message_status : Messageld ++ Status

a) Define a recursive function, count, which takes as input a sequence,s € seq Messageld, and returns as output the number of elements that appear in s.

b) Define a recursive function, not_received, which takes as input a sequence, s € seq Messageld, and returns a subsequence of s containing all the messages of whose status is SentButNotReceived (according to message_status).

c) Define a recursive function, not_read, which takes as input a sequence, s € seq Messageld, and returns a subsequence of s containing all the messages of s whose status is ReceivedButNotRead (according tomessage_status).

d) Define a recursive function, read, which takes as input a sequence,s € seq Messageld, and returns a subsequence of s containing all the messages of s whose status is Read (according to message_status).

e) Show, via structural induction, that

Vs:seq MessageId
count (not_received (s))
+
count (not_read (s))
+
count (read (s))

count (s)

Question 10

Consider the following free type definition.

MessageList :=
nil |
join ( Messageld x UserId x UserId x Timestamp x Status x
MessageList ))

(a) Give a suitable induction principle for this free type.

(b) Define recursive functions count,, not_received,, not_read;,, and read; that take as input elements of MessageList and have behaviour that correspond to the functions of Question 9.

Vi: MessageList e
county, (not_receivedy, (1))
+
count, (not_read,, (1))
+
count, (read, (1))

count, (1)