# Type Theory as a Meta-Language for Logic

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

1. $$\perp$$, $$x=y$$ and $$x\in y$$ are formulas for any variables $$x$$ and $$y$$.
2. 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:

1. " " is list of formulas (known as empty list)
2. 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

1. $$\psi \vdash \psi$$
2. If $$\Gamma \vdash \psi$$, then $$\Gamma ,\Delta \vdash \psi$$
3. If $$\Gamma,\Delta,\Delta \vdash \psi$$, then $$\Gamma ,\Delta \vdash \psi$$
4. If $$\Lambda_0,\Gamma,\Lambda _1,\Delta ,\Lambda _2\vdash \psi$$, then $$\Lambda_0,\Delta,\Lambda _1,\Gamma ,\Lambda _2\vdash \psi$$
5. If $$\Gamma \vdash \phi$$ e $$\Delta,\phi \vdash \psi$$, then $$\Gamma ,\Delta \vdash \psi$$
6. 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

1. $$\phi \vdash \phi \vee \psi$$ and $$\psi \vdash \phi \vee \psi$$
2. If $$\Gamma ,\phi \vdash \tau$$ and $$\Gamma,\psi \vdash \tau$$, then $$\Gamma,\phi \vee \psi \vdash \tau$$
3. If $$\Gamma, \phi \vdash \perp$$, then $$\Gamma \vdash \neg \phi$$
4. $$\phi ,\neg \phi \vdash \perp$$
5. 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

1. $$\perp$$ do not have any free variables
2. $$x=x$$ and $$x\in x$$ have $$x$$ as the only free variable
3. $$x=y$$ and $$x\in y$$ have $$x$$ and $$y$$ as the only free variables
4. $$x$$ is free in $$\phi$$ if, and only if, $$x$$ is free in $$\neg\phi$$
5. $$x$$ is free in $$(\phi )\vee (\psi )$$ if, and only if, $$x$$ is free in $$\phi$$ or $$x$$ is free in $$\psi$$
6. $$y$$ is free in $$\forall x(\phi )$$ if, and only if, $$y$$ is free in $$\phi$$
7. $$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.

Note that there are many ways you can build a logical foundation based on type theory, so don't think of "the type theory". They commonly are built upon the simply typed $$\lambda$$-calculus as a language for constructing basic types and maps between them, but there are major differences when it comes to how propositions get incorporated: In the proposition-as-types paradigm ("Curry-Howard isomorphism", though I think the name "isomorphism" is misleading here -- it's more a principle) you, as the name says, model propositions as types, and proofs as terms of that type. The beauty, here, is that you don't need a new kind of judgement, but that the typing judgement suffices. On the flipside, you typically need more complex -- dependent -- type theory for this approach. The other main approach are LCF-style proof systems (e.g. HOL-Light, HOL4, Isabelle/HOL): In those, you have a dedicated type of propositions and dedicated judgements for provability and inference rules, at the benefit of a simpler -- typically non-dependent -- underlying type theory.