 Home

Codex Wiki

List of universities

University of Oxford

Course of the University of Oxford

Undergraduate course of the University of Oxford

Computer science course of the University of Oxford

Year 1 of the computer science course of the University of Oxford

Past exam of the year 1 of the computer science course of the University of Oxford

2015

Digital systems, linear algebra, introduction to formal proof

Choose an <eigenvariable> $v$ fresh for the premise. Use the <existential quantifier introduction rule> to contradict the premise under a <temporary assumption> $R(v)$:
$$
\begin{array}{rll}
1&\neg\exists x\,R(x)&\text{premise}\\
2&\vert\ R(v)&\text{assumption; }v\text{ fresh}\\
3&\vert\ \exists x\,R(x)&\exists\text{-intro }2\\
4&\vert\ \bot&\neg\text{-elim }3,1\\
5&\neg R(v)&\neg\text{-intro }2\text{--}4\\
6&\forall y\,\neg R(y)&\forall\text{-intro }5
\end{array}
$$
At line 6 the assumption $R(v)$ has been discharged and the sole remaining premise has no free $v$, satisfying the <eigenvariable condition>. Thus
$$
\boxed{\neg\exists x\,R(x)\ \vdash\ \forall y\,\neg R(y).}
$$

Solution

Past exam of the year 1 of the computer science course of the University of Oxford / 2015 / Digital systems, linear algebra, introduction to formal proof / 8 / a / ii / Solution

Past exam of the year 1 of the computer science course of the University of Oxford / 2015 / Digital systems, linear algebra, introduction to formal proof / 8 / a / ii / Solution

 Ancestors (13)

 Discussion (0) New discussion

 Articles by others on the same topic (0)

Past exam of the year 1 of the computer science course of the University of Oxford / 2015 / Digital systems, linear algebra, introduction to formal proof / 8 / a / ii / Solution

 Ancestors (13)

 Discussion (0)  Subscribe (1) New discussion

 Articles by others on the same topic (0)

 Discussion (0) New discussion