simply a test of whether I can or cannot export an LyX file to html

This is just a “proof of concept” check to see how well (and not so well) I can export from LyX to html to post on my blog.

Proof Schemes

Proof schemes are deduction or transformation apparatuses. Once defined, they can be used to efficiently describe both well-formed formulas and proofs within a formal system.

Let $U$ be the universe of discourse and $F_0\subseteq U$, called the foundation of the proof scheme. When applied to well-formed formulas (wffs), the foundation will be the set of atomic wffs. When applied to formal systems, the foundation will be the set of axioms of that formal system.

A transformation rule $R$ is an $n$-ary function in $\left[H\to U\right]$ where $H\subseteq U^n$. By $\left[H\to U\right]$, we mean the set of all functions whose domain is $H$ and range is $U$. Let $R$ be the set of transformation rules for the proof scheme.

A proof is a finite sequence $langle{x}_1,\mathrm{...},x_{n}rangle$ of elements of $U$ such that for all $k\in \left\{1,\mathrm{...},n\right\}$ we have either $x_k\in F_0$ or there is an $R\in R$ and a subsequence $langle{y}_1,\mathrm{...},y_{k-1}rangle\subseteq langle{x}_1,\mathrm{...},x_{n}rangle$ such that $x_k=R\left(y_1,\mathrm{...},y_{k-1}\right)$. If $langle{x}_1,\mathrm{...},x_{n}rangle$ is a proof then it is called a proof of $x_n$. $x$ is called provable if there is a proof $langle{x}_1,\mathrm{...},x_{n}rangle$ in which $x=x_n$. This is written $⊢x$ or $\varnothing ⊢x$.

A proof scheme can be specified by an ordered triple $\left(F_0,U,R\right)$ where $U$ is any set with $F_0\subseteq U$ and $R$ is a set of transformation rules. If $P=\left(F_0,U,R\right)$ is a proof scheme then we will let $T\left(P\right)=\left\{x\in U:⊢x\right\}$. Intuitively, $T\left(P\right)$ is the set of all tautologies of the proof scheme $P$.

Formal Systems

A formal system is a deduction apparatus in which one defines wffs over an alphabet and proves theorems from a set of axioms using some inference rules. More formally, a formal system $F$ is a 4-tuple $\left(A,G,T,I\right)$ where $A$ is a finite set (considered to be symbols), $S\left(A\right)$ is the set of all finite strings (also called utterances), $G\subseteq S\left(A\right)$ is the set of wffs (also called statements), $T\subseteq G$ is the set of axioms, and $I$ is the set of inference rules. $I$ is called an inference rule if there exists an $n\ge 1$ and there is an $H\subseteq G^n$ such that $I\in \left[H\to G\right]$.

Sometimes one defines $G$ by specifying a set of atomic wffs $G_0$ and a set of transformation rules $R$ that enable us to “build” new wffs from old wffs. We then can say that $G=T\left(G_0,S\left(A\right),R\right)$, considering the proof scheme $\left(G_0,S\left(A\right),R\right)$. When specifying a formal system this way, a formal system can be said to be a 5-tuple $\left(A,G_0,R,T,I\right)$ where $G_0\subseteq S\left(A\right)$ is a set of atomic wffs and $R$ is the set of formation rules (which are viewed as transformation rules) for wffs, $T\subseteq G$ is a set of axioms, and $I$ is a set of inference rules.

A proof in a formal system is a finite sequence $langle{x}_1,\mathrm{...},x_{n}rangle$ of elements of $G$ such that for all $k\in \left\{1,\mathrm{...},n\right\}$ we have either $x_k\in T$ (i.e., $x_k$ is an axiom) or there is an $I\in I$ and a subsequence $langle{y}_1,\mathrm{...},y_{k-1}rangle\subseteq langle{x}_1,\mathrm{...},x_{n}rangle$ such that $x_k=I\left(y_1,\mathrm{...},y_{k-1}\right)$. If $langle{x}_1,\mathrm{...},x_{n}rangle$ is a proof then it is called a proof of $x_n$. $x$ is called provable if there is a proof $langle{x}_1,\mathrm{...},x_{n}rangle$ in which $x=x_n$. This is written $⊢x$ or $\varnothing ⊢x$. If $M\subseteq G$ and there is a finite sequence $langle{x}_1,\mathrm{...},x_{n}rangle$ of elements of $G$ such that for all $k\in \left\{1,\mathrm{...},n\right\}$ we have either $x_k\in M\cup T$ or there is an $I\in I$ and a subsequence $langle{y}_1,\mathrm{...},y_{k-1}rangle\subseteq langle{x}_1,\mathrm{...},x_{n}rangle$ such that $x_k=I\left(y_1,\mathrm{...},y_{k-1}\right)$, then we say $M⊢x_n$.