Exercise 7

\[% Shared mathematical notation for CSC438. % % Keep this file limited to commands supported by both LaTeX and MathJax. % Quarto loads it through filters/shared-macros.lua; TeX preambles can use % \input{../macros} when compiled from a first-level project directory. \renewcommand{\subset}{\subseteq} \renewcommand{\iff}{\leftrightarrow} \newcommand{\N}{\mathbb{N}} \newcommand{\proves}{\vdash} \newcommand{\cA}{\mathcal{A}} \newcommand{\cF}{\mathcal{F}} \newcommand{\cL}{\mathcal{L}} \newcommand{\cP}{\mathcal{P}} \newcommand{\cM}{\mathcal{M}} \newcommand{\Var}{\mathrm{Var}} \newcommand{\FV}{\mathrm{FV}} \newcommand{\Z}{\mathbb{Z}} \newcommand{\TR}{\mathbf{TR}} \newcommand{\D}{\mathbf{D}} \newcommand{\R}{\mathbb{R}} \newcommand{\seq}{\Rightarrow} \newcommand{\RA}{\Longrightarrow} \newcommand{\LRA}{\Longleftrightarrow} \newcommand{\OI}{\{0,1\}} \renewcommand{\SS}{\Sigma^*} \newcommand{\powerset}{\mathcal{P}} \newcommand{\blank}{\sqcup} \newcommand{\angles}[1]{\left\langle #1\right\rangle} \newcommand{\enc}[1]{\left\ulcorner #1\right\urcorner} \newcommand{\Lang}{\mathcal{L}} \newcommand{\Th}{\operatorname{Th}} \newcommand{\Thm}{\operatorname{Thm}} \newcommand{\Prov}{\operatorname{Prov}} \newcommand{\Con}{\operatorname{Con}} \newcommand{\ATM}{A_{\mathrm{TM}}} \newcommand{\HALTTM}{\operatorname{HALT}_{\mathrm{TM}}} \newcommand{\HALTe}{\operatorname{HALT}_{\epsilon}} \newcommand{\AExp}{A_E} \newcommand{\AMult}{A_M} \newcommand{\green}[1]{\textcolor{green}{#1}} \newcommand{\red}[1]{\textcolor{red}{#1}} \newcommand{\st}[1]{\sout{#1}} \]

1 parser and is_formula

Revisit is_formula and parser from exercise 4, and convince yourself you could implement similar functions for first order logic (given a particular language with all the constants, functions, relations and their arities).

2 Exercises from Cook’s Notes

2.1

Do exercises 2-10 and 15 from here.

Note the differences in notation.

• \(\supset\) is \(\to\) (implication in the object language).
• \(\LRA\) is \(\equiv\) (logical equivalance).
• They use “vocabulary” where we use “language”.