I am unsure which StackExchange site is the most appropriate for this question, but I believe this site is the most appropriate.
My current project involves rigorously proving all the mathematical concepts I have learned. I began this project by reading the first chapter of the book "Foundations of Mathematics" by Mohammad Safdari. In this chapter, the author says about the importance of "meta-language" by stating that "we cannot create our theory without a meta-language".
Basically, English is the meta-language used by that author.
I'd like to use not only English as a meta-language but also type theory in order to make certain concepts more precise.
I know nothing about type theory. I learned about it when I discovered that Lean uses a version of Dependent Type Theory called the Calculus of Inductive Constructions as its foundation. Because of this, I believe that I can use type theory as meta-language in order to make some concepts more precise. However, I am uncertain how to implement this approach.
For this reason, I request the following help: how can I make the following axioms more precise using type theory (preferably using dependent type theory)?
I am asking this because I believe that by seeing an answer, I will know exactly what I should look for.
A1: We define the notion of "formula" inductively
- $\perp$, $x=y$ and $x\in y$ are formulas for any variables $x$ and $y$.
- If $\phi$ and $\psi$ are formulas and $x$ is a variable, then $\neg (\phi )$, $\forall x(\phi )$ and $(\phi )\vee (\psi )$ are also formulas.
A2: We define the notion of "list of formulas" inductively:
- " " is list of formulas (known as empty list)
- If $\Delta$ is a list of formulas and $\phi$ is a formula, then $\Delta,\phi$ is a list of formulas.
A3: Let $\Gamma, \Delta,\Lambda _0,\Lambda _1,\Lambda _2$ be five lists of formulas and $\phi,\psi$ be two formulas. We assume that
- $\psi \vdash \psi $
- If $\Gamma \vdash \psi $, then $\Gamma ,\Delta \vdash \psi $
- If $\Gamma,\Delta,\Delta \vdash \psi $, then $\Gamma ,\Delta \vdash \psi $
- If $\Lambda_0,\Gamma,\Lambda _1,\Delta ,\Lambda _2\vdash \psi$, then $\Lambda_0,\Delta,\Lambda _1,\Gamma ,\Lambda _2\vdash \psi$
- If $\Gamma \vdash \phi$ e $\Delta,\phi \vdash \psi $, then $\Gamma ,\Delta \vdash \psi $
- If $\Gamma,\Delta \vdash \psi $ e $\Delta$ is empty, then $\Gamma\vdash \psi $
I think the above axioms can be thought as judgements in type theory, correct?
A4: Let $\Gamma$ be a list of formulas and $\phi,\psi ,\tau $ be three formulas. We assume that
- $\phi \vdash \phi \vee \psi $ and $\psi \vdash \phi \vee \psi $
- If $\Gamma ,\phi \vdash \tau $ and $\Gamma,\psi \vdash \tau $, then $\Gamma,\phi \vee \psi \vdash \tau $
- If $\Gamma, \phi \vdash \perp $, then $\Gamma \vdash \neg \phi $
- $\phi ,\neg \phi \vdash \perp $
- If $\Gamma ,\neg \phi \vdash \perp $, then $\Gamma \vdash\phi $
A5: Primitive notion: free variables. Let $\phi,\psi$ two formulas and $x,y,z$ three distinct variables. We assume that
- $\perp$ do not have any free variables
- $x=x$ and $x\in x$ have $x$ as the only free variable
- $x=y$ and $x\in y$ have $x$ and $y$ as the only free variables
- $x$ is free in $\phi$ if, and only if, $x$ is free in $\neg\phi$
- $x$ is free in $(\phi )\vee (\psi )$ if, and only if, $x$ is free in $\phi$ or $x$ is free in $\psi$
- $y$ is free in $\forall x(\phi )$ if, and only if, $y$ is free in $\phi$
- $x$ is not free in $\forall x(\phi )$
Another thing I'd like to formalize with type theory:
Given two variables $x,y$, there's a variable $\{x,y\}$ such that $\forall w(w\in \{x,y\}\leftrightarrow w=x\vee w=y)$.
This is somewhat the axiom of paring.
Thank you for your attention!