README.md

COMP4161 T3/2024 Advanced Topics in Software Verification - Assignment 1

1. λ-Calculus (16 marks)

(a) Simplify the term $(pq)(\lambda p\cdot (\lambda q\cdot (\lambda r\cdot (q(rp))))))))$ syntactically by applying the syntactic conventions and rules. Justify your answer. (2 marks)

1. First, we apply the application rule. The term is of the form $(MN)$ where $M=pq$ and $N=\lambda p\cdot (\lambda q\cdot (\lambda r\cdot (q(rp))))))))$.
   • When we apply $(MN)$ with $M=pq$ and $N=\lambda p\cdot (\lambda q\cdot (\lambda r\cdot (q(rp)))))))$, we substitute $p$ with $p$ (from $pq$) and $q$ with $q$ (from $pq$) in the body of $N$.
   • The body of $N$ is $\lambda q\cdot (\lambda r\cdot (q(rp)))))))$. Substituting $p$ and $q$ gives us $\lambda q\cdot (\lambda r\cdot (q(rp)))))))$ where $p$ and $q$ are the values from $pq$.
   • Now we have another application. The term is now $q(\lambda r\cdot (q(rp)))))))$ (because we applied the first substitution).
   • We again apply the application rule. Substitute $r$ with $r$ (whatever its value is in the context) in the body of $\lambda r\cdot (q(rp)))))))$.
   • The body becomes $(q(rp))))))$.
   • So the simplified term is $(q(rp))))))$.

(b) Restore the omitted parentheses in the term $a(\lambda ab.(bc)a(bc))(\lambda b.cb)$ (but make sure you don’t change the term structure). (2 marks)

1. The term should be $a((\lambda ab.((bc)a(bc))))(\lambda b.cb))$.
   • The innermost lambda expression $\lambda ab.(bc)a(bc)$ needs its own parentheses around the body.
   • And the whole application of $a$ to the lambda expression and then to $(\lambda b.cb)$ also needs appropriate parentheses.

(c) Find the normal form of $(\lambda f\cdot \lambda x\cdot f(fx))(\lambda g\cdot \lambda y\cdot g(g(gy)))))$. Justify your answer by showing the reduction sequence. Each step in the reduction sequence should be a single β-reduction step. Underline or otherwise indicate the redex being reduced for each step. (6 marks)

1. Let's start with the term $(\lambda f\cdot \lambda x\cdot f(fx))(\lambda g\cdot \lambda y\cdot g(g(gy)))))$.
   • The redex is $(\lambda f\cdot \lambda x\cdot f(fx))(\lambda g\cdot \lambda y\cdot g(g(gy)))))$. We substitute $f$ with $\lambda g\cdot \lambda y\cdot g(g(gy)))$ and $x$ with any value (let's say $z$ for simplicity, but it doesn't matter in this context as we are just reducing syntactically).
   • After the first β-reduction, we get $\lambda x\cdot (\lambda g\cdot \lambda y\cdot g(g(gy)))(\lambda g\cdot \lambda y\cdot g(g(gy))x)))$.
   • Now the new redex is $(\lambda g\cdot \lambda y\cdot g(g(gy)))(\lambda g\cdot \lambda y\cdot g(g(gy))x)))$. We substitute $g$ with $\lambda g\cdot \lambda y\cdot g(g(gy)))$ and $y$ with $x$.
   • After the second β-reduction, we get $\lambda y\cdot (\lambda g\cdot \lambda y\cdot g(g(gy)))(\lambda g\cdot \lambda y\cdot g(g(gy)))(\lambda g\cdot \lambda y\cdot g(g(gy))y)))$.
   • We can continue this process, but it becomes clear that the term will keep expanding and we won't reach a normal form in a finite number of steps. This is because the function $\lambda g\cdot \lambda y\cdot g(g(gy)))$ is being applied to itself repeatedly.

(d) Recall the encoding of natural numbers in lambda calculus (Church Numerals) seen in the lecture:

• $0\equiv \lambda fx,x$
• $1\equiv \lambda fx.fx$
• $2\equiv \lambda fx.f(fx)$
• $3\equiv \lambda fx.f(f(fx))...$ Define exp where exp m n beta-reduces to the Church Numeral representing $m^n$. Provide a justification of your answer. (6 marks)

1. We want to define an exp function in lambda calculus. Let's first consider what the operation should do.
   • If we have $m$ and $n$ as Church Numerals, we want to apply the function $m$ times to another function, and then apply that result $n$ times to the argument $x$.
2. We define exp as follows:
   • exp ≡ $\lambda mnfx.m(nf)x$
3. Justification:
   • Let $m=\lambda f_m{x}_m.f_m^m(x_m)$ and $n=\lambda f_n{x}_n.f_n^n(x_n)$ (where $f_m^m(x_m)$ means applying $f_m$ to $x_m$ $m$ times and similarly for $n$).
   • First, we consider the inner application $nf$.
     • Substituting $f$ with $f$ and $x$ with $f$ in the body of $n$, we get $nf=\lambda x_n.f_n^n(f)$.
   • Then we apply $m$ to $(nf)$.
     • Substituting $f$ with $(nf)$ and $x$ with $x$ in the body of $m$, we get $m(nf)=\lambda x_m.(nf{)}^m(x_m)=\lambda x_m.(\lambda x_n.f_n^n(f){)}^m(x_m)$.
     • This means applying the function $nf$ (which is applying $f_n^{n}(f)$) $m$ times to $x_m$.
   • Finally, we apply the result to $x$.
     • So exp m n f x will result in applying the function $m$ times to $nf$ and then applying that result to $x$, which is equivalent to the Church Numeral representation of $m^n$.

2. Types (20 marks)

(a) Provide the most general type for the term $\lambda abc.a(xbb)(cb)$. Show a type derivation tree to justify your answer. Each node of the tree should correspond to the application of a single typing rule, and be labeled with the typing rule used. Under which contexts is the term type correct? (5 marks)

1. Type derivation tree:
   • Start with the root node representing the whole term $\lambda abc.a(xbb)(cb)$.
   • Apply the rule for lambda abstraction. The type of $\lambda abc.a(xbb)(cb)$ is of the form ${\tau }_1\to {\tau }_2\to {\tau }_3\to {\tau }_4$ where we need to find the types ${\tau }_1,{\tau }_2,{\tau }_3,{\tau }_4$.
   • For the first application $a(xbb)$, we know that $a$ has a type ${\tau }_1$ and $xbb$ must have a type that is compatible with the argument type of $a$. Let's assume $x$ has type $\sigma$ and $b$ has type $\rho$. Then $xbb$ has type $\sigma \to \rho \to \rho$. So the type of $a$ must be $\sigma \to \rho \to \rho \to {\tau }_2$.
   • For the second application $(cb)$, $c$ has type ${\tau }_3$ and $b$ has type $\rho$. So ${\tau }_3$ must be $\rho \to {\tau }_4$.
   • Combining these, the most general type is $(\sigma \to \rho \to \rho \to {\tau }_2)\to (\rho \to {\tau }_4)\to {\tau }_1\to {\tau }_2\to {\tau }_3\to {\tau }_4$.
   • The term is type correct under the context where the types of variables are assigned as described above (i.e., $x:\sigma ,b:\rho ,a:\sigma \to \rho \to \rho \to {\tau }_2,c:\rho \to {\tau }_4$).

(b) Find a closed lambda term that has the following type:

• ${(}^{\prime }a{\Rightarrow }^{\prime }b)\Rightarrow {(}^{\prime }c{\Rightarrow }^{\prime }a){\Rightarrow }^{\prime }c{\Rightarrow }^{\prime }b$ (You don’t need to provide a type derivation, just the term). (4 marks)

1. The term $\lambda fgx.f(gx)$ has the given type.
   • Let's assume $f$ has type ${(}^{\prime }a{\Rightarrow }^{\prime }b)$, $g$ has type ${(}^{\prime }c{\Rightarrow }^{\prime }a)$, and $x$ has type ${}^{\prime }c$.
   • Then $gx$ has type ${}^{\prime }a$ (by applying the function $g$ of type ${(}^{\prime }c{\Rightarrow }^{\prime }a)$ to $x$ of type ${}^{\prime }c$).
   • Then $f(gx)$ has type ${}^{\prime }b$ (by applying the function $f$ of type ${(}^{\prime }a{\Rightarrow }^{\prime }b)$ to $gx$ of type ${}^{\prime }a$).
   • So $\lambda fgx.f(gx)$ has the type ${(}^{\prime }a{\Rightarrow }^{\prime }b)\Rightarrow {(}^{\prime }c{\Rightarrow }^{\prime }a){\Rightarrow }^{\prime }c{\Rightarrow }^{\prime }b$.

(c) Explain why $\lambda x.xx$ is not typable. (3 marks)

1. The term $\lambda x.xx$ is not typable because when we try to assign a type to it, we run into a problem.
   • Let's assume $x$ has type $\tau$. Then the term $xx$ is applying the function $x$ to itself. But for a function application to be type correct, the type of the function (the first $x$) must be of the form $\sigma \to \rho$ and the type of the argument (the second $x$) must be $\sigma$.
   • In the case of $\lambda x.xx$, we have the same variable $x$ being both the function and the argument. If we assume $x:\tau$, then for $xx$ to be type correct, $\tau$ would need to be both $\sigma \to \rho$ and $\sigma$ simultaneously, which is not possible for a single type. So the term is not typable.

(d) Find the normal form and its type of $(\lambda fx.f(xx))(\lambda yz.z)$. (3 marks)

1. First, we apply the function $(\lambda fx.f(xx))$ to $(\lambda yz.z)$.
   • The redex is $(\lambda fx.f(xx))(\lambda yz.z)$. We substitute $f$ with $\lambda yz.z$ and $x$ with any value (let's say $a$ for simplicity).
   • After the β-reduction, we get $\lambda x.(\lambda yz.z)(xx)$.
   • Now the new term is $\lambda x.z$.
   • The normal form is $\lambda x.z$.
   • The type of the original term $(\lambda fx.f(xx))$ is ${\tau }_1\to {\tau }_2\to {\tau }_3$ where ${\tau }_1$ is the type of $f$, ${\tau }_2$ is the type of $x$, and ${\tau }_3$ is the result type. If we assume $f:\sigma \to \rho ,x:\tau$, then the type of $f(xx)$ is $\rho$ (assuming $xx$ has a compatible type). So the type of $(\lambda fx.f(xx))$ is $(\sigma \to \rho )\to \tau \to \rho$.
   • The term $(\lambda yz.z)$ has type $\sigma \to \tau \to \tau$. When we apply the first term to the second term, the resulting type is $\tau \to \tau$. So the type of the normal form $\lambda x.z$ is $\tau \to \tau$.

(e) Is $(\lambda fx.f(xx))(\lambda yz.z)$ typable? Compare this situation with the Subject Reduction that you learned in the lecture. (5 marks)

1. The term $(\lambda fx.f(xx))(\lambda yz.z)$ is typable.
   • As we saw in part (d), the type of $(\lambda fx.f(xx))$ is $(\sigma \to \rho )\to \tau \to \rho$ and the type of $(\lambda yz.z)$ is $\sigma \to \tau \to \tau$. The types are compatible for application.
2. Regarding Subject Reduction:
   • Subject Reduction states that if a term $M$ has a type $\tau$ and $M$ reduces to $N$ (i.e., $M\to N$), then $N$ also has a type and the type is related to $\tau$.
   • In this case, we started with $(\lambda fx.f(xx))(\lambda yz.z)$ and reduced it to $\lambda x.z$. The original term had a certain type as we determined, and the reduced term also has a type.
   • The type of the reduced term is a consequence of the reduction and the typing rules. The fact that the term can be typed before and after reduction is consistent with the idea of Subject Reduction. If the term was not typable before reduction and became typable after reduction (or vice versa), it would violate the principle of Subject Reduction. Here, the typing is consistent throughout the reduction process, which aligns with the concept of Subject Reduction.

3. Propositional Logic (29 marks)

(a) $x\to \mathrm{\neg }\mathrm{\neg }x$ (3 marks)

1. Proof:
   • We use the rule notI (introduction of negation).
   • Assume $x$.
   • We want to show $\mathrm{\neg }\mathrm{\neg }x$.
   • Assume $\mathrm{\neg }x$ (for the purpose of notI).
   • This leads to a contradiction since we have assumed $x$ and now $\mathrm{\neg }x$.
   • By notI, we can conclude $\mathrm{\neg }\mathrm{\neg }x$.
   • So $x\to \mathrm{\neg }\mathrm{\neg }x$ holds by the rule impI (introduction of implication).

(b) $(X\to Y\to \mathrm{\neg }X)\to X\to \mathrm{\neg }Y$ (3 marks)

1. Proof:
   • Assume $(X\to Y\to \mathrm{\neg }X)$.
   • Also assume $X$.
   • We want to show $\mathrm{\neg }Y$.
   • From $(X\to Y\to \mathrm{\neg }X)$ and $X$, by impE (elimination of implication), we get $Y\to \mathrm{\neg }X$.
   • Since we have $X$ and $Y\to \mathrm{\neg }X$, and assuming $Y$ (for the purpose of notI), we get $\mathrm{\neg }X$ by impE.
   • But we already have $X$, so this is a contradiction.
   • By notI, we can conclude $\mathrm{\neg }Y$.
   • So $(X\to Y\to \mathrm{\neg }X)\to X\to \mathrm{\neg }Y$ holds by impI.

(c) $\mathrm{\neg }\mathrm{\neg }A\to A$ (4 marks)

1. Proof:
   • Assume $\mathrm{\neg }\mathrm{\neg }A$.
   • Assume $\mathrm{\neg }A$ (for the purpose of notI).
   • This leads to a contradiction since we have $\mathrm{\neg }\mathrm{\neg }A$ and now $\mathrm{\neg }A$.
   • By notI, we can conclude $A$.
   • So $\mathrm{\neg }\mathrm{\neg }A\to A$ holds by impI.

(d) $\mathrm{\neg }(A\wedge B)\to \mathrm{\neg }A\vee \mathrm{\neg }B$ (4 marks)

1. Proof:
   • Assume $\mathrm{\neg }(A\wedge B)$.
   • We want to show $\mathrm{\neg }A\vee \mathrm{\neg }B$.
   • Assume $\mathrm{\neg }(\mathrm{\neg }A\vee \mathrm{\neg }B)$ (for the purpose of notI).
   • By De Morgan's law, $\mathrm{\neg }(\mathrm{\neg }A\vee \mathrm{\neg }B)$ is equivalent to $A\wedge B$.
   • But we have assumed $\mathrm{\neg }(A\wedge B)$, so this is a contradiction.
   • By notI, we can conclude $\mathrm{\neg }A\vee \mathrm{\neg }B$.
   • So $\mathrm{\neg }(A\wedge B)\to \mathrm{\neg }A\vee \mathrm{\neg }B$ holds by impI.

(e) $\mathrm{\neg }(A\to B)\to A$ (4 marks)

1. Proof:
   • Assume $\mathrm{\neg }(A\to B)$.
   • Assume $\mathrm{\neg }A$ (for the purpose of notI).
   • Since $\mathrm{\neg }A$, then $A\to B$ holds vacuously (if the antecedent is false, the implication is true).
   • But we have assumed $\mathrm{\neg }(A\to B)$, so this is a contradiction.
   • By notI, we can conclude $A$.
   • So $\mathrm{\neg }(A\to B)\to A$ holds by impI.

(f) (continued)

1. Proof of $\mathrm{\neg }(A\vee B)\to (\mathrm{\neg }A\wedge \mathrm{\neg }B)$:
   • Assume $\mathrm{\neg }(A\vee B)$.
   • Assume $A$ (for the purpose of notI).
   • Then $A\vee B$ holds, which contradicts $\mathrm{\neg }(A\vee B)$.
   • So by notI, we can conclude $\mathrm{\neg }A$.
   • Assume $B$ (for the purpose of notI).
   • Then $A\vee B$ holds, which contradicts $\mathrm{\neg }(A\vee B)$.
   • So by notI, we can conclude $\mathrm{\neg }B$.
   • By conjI (introduction of conjunction), we have $\mathrm{\neg }A\wedge \mathrm{\neg }B$.
   • So $(\mathrm{\neg }A\wedge \mathrm{\neg }B)=(\mathrm{\neg }(A\vee B))$ holds by the two implications we proved.

(g) $(A\to B)\to ((B\to C)\to A)\to B$ (5 marks)

1. Proof:
   • Assume $A\to B$.
   • Also assume $(B\to C)\to A$.
   • We want to show $B$.
   • Assume $\mathrm{\neg }B$ (for the purpose of notI).
   • From $A\to B$ and $\mathrm{\neg }B$, by notE (elimination of negation), we can conclude $\mathrm{\neg }A$.
   • From $(B\to C)\to A$ and $\mathrm{\neg }A$, by notE, we can conclude $\mathrm{\neg }(B\to C)$.
   • By the definition of implication, $\mathrm{\neg }(B\to C)$ is equivalent to $B\wedge \mathrm{\neg }C$.
   • By conjunct1, we have $B$, which contradicts $\mathrm{\neg }B$.
   • By notI, we can conclude $B$.
   • So $(A\to B)\to ((B\to C)\to A)\to B$ holds by impI.

4. Higher-Order Logic (35 marks)

(a) $(\mathrm{\forall }x.\mathrm{\neg }Px)=(\nexists x.Px)$ (4 marks)

1. Proof:
   • We want to show $(\mathrm{\forall }x.\mathrm{\neg }Px)\to (\nexists x.Px)$ and $(\nexists x.Px)\to (\mathrm{\forall }x.\mathrm{\neg }Px)$.
2. Proof of $(\mathrm{\forall }x.\mathrm{\neg }Px)\to (\nexists x.Px)$:
   • Assume $\mathrm{\forall }x.\mathrm{\neg }Px$.
   • Assume $\mathrm{\exists }x.Px$ (for the purpose of notI).
   • By exE (elimination of existential quantifier), there exists a particular $a$ such that $Pa$.
   • But from $\mathrm{\forall }x.\mathrm{\neg }Px$, we have $\mathrm{\neg }Pa$, which is a contradiction.
   • By notI, we can conclude $\mathrm{\neg }\mathrm{\exists }x.Px$, which is equivalent to $\mathrm{\forall }x.\mathrm{\neg }Px$.
3. Proof of $(\nexists x.Px)\to (\mathrm{\forall }x.\mathrm{\neg }Px)$:
   • Assume $\mathrm{\neg }\mathrm{\exists }x.Px$.
   • We want to show $\mathrm{\forall }x.\mathrm{\neg }Px$.
   • Let $a$ be an arbitrary element.
   • Assume $Pa$ (for the purpose of notI).
   • Then $\mathrm{\exists }x.Px$, which contradicts $\mathrm{\neg }\mathrm{\exists }x.Px$.
   • By notI, we can conclude $\mathrm{\neg }Pa$.
   • Since $a$ was arbitrary, we have $\mathrm{\forall }x.\mathrm{\neg }Px$.
   • So $(\mathrm{\forall }x.\mathrm{\neg }Px)=(\nexists x.Px)$.

(b) $(\mathrm{\exists }xy.Pxy)=(\mathrm{\exists }yx.Pxy)$ (4 marks)

1. Proof:
   • We know that the order of existential quantifiers does not matter in this case.
   • Assume $\mathrm{\exists }xy.Pxy$.
   • By exE, there exist $a$ and $b$ such that $Pab$.
   • Then $\mathrm{\exists }yx.Pxy$ holds because we have found $b$ and $a$ such that $Pxy$ (with $x=a$ and $y=b$).
   • Conversely, assume $\mathrm{\exists }yx.Pxy$.
   • By exE, there exist $b$ and $a$ such that $Pab$.
   • Then $\mathrm{\exists }xy.Pxy$ holds.
   • So $(\mathrm{\exists }xy.Pxy)=(\mathrm{\exists }yx.Pxy)$.

(c) $(\mathrm{\exists }x.Px\to Q)=((\mathrm{\forall }x.Px)\to Q)$ (7 marks)

1. Proof:
   • First, we prove $(\mathrm{\exists }x.Px\to Q)\to ((\mathrm{\forall }x.Px)\to Q)$.
   • Assume $\mathrm{\exists }x.Px\to Q$.
   • Assume $\mathrm{\forall }x.Px$.
   • We want to show $Q$.
   • From $\mathrm{\forall }x.Px$, by allE (elimination of universal quantifier), we can get $Pa$ for any particular $a$.
   • Since $\mathrm{\exists }x.Px$ holds (because we have $Pa$ for some $a$), and $\mathrm{\exists }x.Px\to Q$, by impE, we can conclude $Q$.
   • So $(\mathrm{\exists }x.Px\to Q)\to ((\mathrm{\forall }x.Px)\to Q)$.
2. Now, we prove $((\mathrm{\forall }x.Px)\to Q)\to (\mathrm{\exists }x.Px\to Q)$.
   • Assume $(\mathrm{\forall }x.Px)\to Q$.
   • We want to show $\mathrm{\exists }x.Px\to Q$.
   • Assume $\mathrm{\exists }x.Px$.
   • By exE, there exists a particular $a$ such that $Pa$.
   • Now assume $\mathrm{\neg }Q$ (for the purpose of notI).
   • Since we have $Pa$ and $\mathrm{\neg }Q$, and assuming $\mathrm{\forall }x.Px$ (for the purpose of notI), we get a contradiction because $(\mathrm{\forall }x.Px)\to Q$.
   • By notI, we can conclude $Q$.
   • So $\mathrm{\exists }x.Px\to Q$.
   • Therefore, $(\mathrm{\exists }x.Px\to Q)=((\mathrm{\forall }x.Px)\to Q)$.

(d) $((\mathrm{\forall }x.Px)\to (\mathrm{\exists }x.Qx))=(\mathrm{\exists }x.Px\to Qx)$ (7 marks)

1. Proof:
   • First, we prove $((\mathrm{\forall }x.Px)\to (\mathrm{\exists }x.Qx))\to (\mathrm{\exists }x.Px\to Qx)$.
   • Assume $(\mathrm{\forall }x.Px)\to (\mathrm{\exists }x.Qx)$.
   • We want to show $\mathrm{\exists }x.Px\to Qx$.
   • Assume $\mathrm{\exists }x.Px$.
   • By exE, there exists a particular $a$ such that $Pa$.
   • Now assume $\mathrm{\neg }Qa$ (for the purpose of notI).
   • Assume $\mathrm{\forall }x.Px$.
   • From $\mathrm{\forall }x.Px\to (\mathrm{\exists }x.Qx)$ and $\mathrm{\forall }x.Px$, by impE, we get $\mathrm{\exists }x.Qx$.
   • By exE, there exists a $b$ such that $Qb$.
   • But we have assumed $\mathrm{\neg }Qa$, so this is a contradiction.
   • By notI, we can conclude $Qa$.
   • So $\mathrm{\exists }x.Px\to Qx$.
2. Now, we prove $(\mathrm{\exists }x.Px\to Qx)\to ((\mathrm{\forall }x.Px)\to (\mathrm{\exists }x.Qx))$.
   • Assume $\mathrm{\exists }x.Px\to Qx$.
   • We want to show $(\mathrm{\forall }x.Px)\to (\mathrm{\exists }x.Qx)$.
   • Assume $\mathrm{\forall }x.Px$.
   • We want to show $\mathrm{\exists }x.Qx$.
   • Assume $\mathrm{\neg }\mathrm{\exists }x.Qx$ (for the purpose of notI).
   • By notE, this is equivalent to $\mathrm{\forall }x.\mathrm{\neg }Qx$.
   • Now assume $Pa$ for a particular $a$ (since $\mathrm{\forall }x.Px$).
   • From $\mathrm{\exists }x.Px\to Qx$ and $Pa$, we should have $Qa$.
   • But we have $\mathrm{\forall }x.\mathrm{\neg }Qx$, which is a contradiction.
   • By notI, we can conclude $\mathrm{\exists }x.Qx$.
   • So $((\mathrm{\forall }x.Px)\to (\mathrm{\exists }x.Qx))=(\mathrm{\exists }x.Px\to Qx)$.

(e) $\mathrm{\forall }x.\mathrm{\neg }Rx\to R(Mx)\Rightarrow \mathrm{\forall }x.Rx\vee R(Mx)$ (6 marks)

1. Proof:
   • Assume $\mathrm{\forall }x.\mathrm{\neg }Rx\to R(Mx)$.
   • We want to show $\mathrm{\forall }x.Rx\vee R(Mx)$.
   • Let $a$ be an arbitrary element.
   • We consider two cases:
     • Case 1: Assume $\mathrm{\neg }Ra$.
       • From $\mathrm{\forall }x.\mathrm{\neg }Rx\to R(Mx)$, by allE, we have $\mathrm{\neg }Ra\to R(Ma)$.
       • Since we have assumed $\mathrm{\neg }Ra$, by impE, we get $R(Ma)$.
       • Then $Ra\vee R(Ma)$ holds by disjI2 (introduction of disjunction).
     • Case 2: Assume $Ra$.
       • Then $Ra\vee R(Ma)$ holds by disjI1 (introduction of disjunction).
   • Since $a$ was arbitrary, we have $\mathrm{\forall }x.Rx\vee R(Mx)$ by allI (introduction of universal quantifier).

(f) $\text{llbracket}\mathrm{\forall }x.\mathrm{\neg }Rx\to R(Mx);\mathrm{\exists }x.Rx\text{rrbracket}\Rightarrow \mathrm{\exists }x.Rx\wedge R(M(Mx))$ (7 marks)

1. Proof:
   • Assume $\mathrm{\forall }x.\mathrm{\neg }Rx\to R(Mx)$ and $\mathrm{\exists }x.Rx$.
   • By exE, there exists a particular $a$ such that $Ra$.
   • From $\mathrm{\forall }x.\mathrm{\neg }Rx\to R(Mx)$, by allE, we have $\mathrm{\neg }Ra\to R(Ma)$.
   • Now assume $\mathrm{\neg }R(M(Ma))$ (for the purpose of notI).
   • Since $Ra$, we have $\mathrm{\neg }\mathrm{\neg }Ra$.
   • From $\mathrm{\neg }Ra\to R(Ma)$ and $\mathrm{\neg }\mathrm{\neg }Ra$, by mp (modus ponens), we get $R(Ma)$.
   • Now assume $\mathrm{\neg }R(Ma)$ (for the purpose of notI).
   • Since $\mathrm{\neg }Ra\to R(Ma)$ and $\mathrm{\neg }R(Ma)$, we have $\mathrm{\neg }\mathrm{\neg }Ra$ by notE.
   • But we have $Ra$, which is a contradiction. So we can conclude $R(Ma)$.
   • Now assume $\mathrm{\neg }Ra$ (for the purpose of notI).
   • Since $\mathrm{\neg }Ra\to R(Ma)$ and $\mathrm{\neg }Ra$, we have $R(Ma)$.
   • Then assume $\mathrm{\neg }R(M(Ma))$ (for the purpose of notI).
   • Since $\mathrm{\neg }Ra\to R(Ma)$ and $R(Ma)$, we have $\mathrm{\neg }\mathrm{\neg }Ra$ by notE.
   • But we have $Ra$, which is a contradiction. So we can conclude $R(M(Ma))$.
   • So we have $Ra\wedge R(M(Ma))$.
   • Since $a$ was obtained from $\mathrm{\exists }x.Rx$, we have $\mathrm{\exists }x.Rx\wedge R(M(Mx))$ by exI (introduction of existential quantifier).

COMP4161 A1 Isabelle

CS Tutor | 计算机编程辅导 | Code Help | Programming Help

WeChat: cstutorcs

Email: tutorcs@163.com

QQ: 749389476

非中介, 直接联系程序员本人