Type Theory as a Meta-Language for Logic

logicmeta-mathmetalogicsoft-questiontype-theory

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.

Thank you for your attention!

Best Answer

Since you have no knowledge of type theory, I suggest that -- in parallel to learning whatever math you are interested in -- you consult an introductory text on the use of type theory as a logical foundation. For example, the book "Type Theory and Formal Proof: An Introduction" by Nedervelt and Geuvers, serves this purpose. In particular, it will motivate, introduce and study the calculus of inductive constructions that, as you noticed, is at the heart of the Lean and Coq proof assistants.

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.

Related Question