% -----------------------acknowledge for overleaf and designer of this template-----------------------
\documentclass[12pt]{exam}
\usepackage{amsthm}
\usepackage{libertine}
\usepackage[utf8]{inputenc}
\usepackage[margin=1in]{geometry}
\usepackage{amsmath,amssymb}
\usepackage{ascmac}
\usepackage{multicol}
\usepackage[shortlabels]{enumitem}
\usepackage{siunitx}
\usepackage{cancel}
\usepackage{graphicx}
\usepackage{pgfplots}
\usepackage{listings}
\usepackage[all]{xy}

% automata
%\usepackage{tikz}
%\usetikzlibrary{automata, positioning, arrows}


\pgfplotsset{width=10cm,compat=1.9}
\usepgfplotslibrary{external}
\tikzexternalize

\newcommand{\class}{\Large Logic and Foundations I, Autumn 2023 } % This is the name of the course
\newcommand{\examnum}{Homework No.6} % This is the index of the homework https://www.overleaf.com/project/650b9566039710695765623c
\newcommand{\examdate}{Due: 2023.11.07 }% This is the due date
\newcommand{\examname}{Name:    }
% Your name here





\begin{document}
\pagestyle{plain}
\thispagestyle{empty}

\noindent
\begin{tabular*}{\textwidth}{l @{\extracolsep{\fill}} r @{\extracolsep{8pt}} l}
\textbf{\class} & & \textit{~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~}\\
&&\\
\textbf{\examnum} & &\textit{~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~}\\
\textbf{\examdate} &&\\
\textbf{\examname} &&\\
\end{tabular*}\\
\rule[2ex]{\textwidth}{2pt}
% ---

\noindent \textbf{Problem 1 (difficult)}\\

Let $\Sigma$ be a theory in a language $\mathcal{L}$ including
an $n$-ary relation symbol $R$ and some others.
Then, $R$ is said to be \textbf{explicitly definable} in $\Sigma$,
if there exists a formula $\varphi(x_0, \dots, x_{n-1})$
in $\mathcal{L} - \{ R \}$ such that
$$\Sigma \vdash \forall x_0, \dots, x_{n-1} (R(x_0, \dots, x_{n-1}) \leftrightarrow
\varphi(x_0, \dots, x_{n-1})).$$

Now, we construct $\Sigma'$ from $\Sigma$ by replacing
all occurrences of $R$ by a new symbol $R'$.
Then, $R$ is said to be \textbf{implicitly definable} in $\Sigma$,
if the following hold
$$\Sigma\cup \Sigma' \vdash \forall x_0, \dots, x_{n-1} (R(x_0, \dots, x_{n-1}) \leftrightarrow
R'(x_0, \dots, x_{n-1})).$$

Show that $R$ is explicitly definable in $\Sigma$ iff
$R$ is implicitly definable in $\Sigma$.
\bigskip

\noindent\underline{\textsf{Solution:}}


\newpage

\end{document}




