I have been doing exercises in Lean theorem prover where I was introduced to type theory.
There is a variety of type theories, this question applies to those that behave similarly to Lean's dependent type theory (Lean specifically uses a version known as Calculus of Inductive Constructions, CIC).
In classical logic we inductively define a formula (well-formed formula).
- Propositional variables are formulas (such as $A$, $B$, …)
- Constants true and false ($\top$, $\bot$) are formulas.
- If A and B are formulas, then so are $\neg A$, $(A \wedge B)$, $(A \vee B)$, …
In type theory we define the constants true and false ($\top$, $\bot$) to be formulas. The keyword for this in Lean is $\tt{prop}$. As far as I know, it can be done similarly in Agda.
$\tt{true : prop}\quad$ (A)
$\tt{false : prop }\quad$ (B)
We also define any variables we want to use as formulas.
$\tt{ A : prop} \quad$ (C)
Then we define the predicates.
$\tt{\wedge : prop \to prop \to prop} \quad$ (D)
Motivation
It is possible to have a formula with formula variables $X$, $Y$ in classical logic such as:
$(X \Rightarrow Y).$ By substitution and definition of formulas, you can easily have $((W \wedge Z) \Rightarrow Y)$, if you substitute $X$ for $(W \wedge Z)$ where $(W \wedge Z)$ is also a formula. This is useful because you can have axiom schemes such as $(\phi \Rightarrow (\psi \Rightarrow \phi))$ where you can substitute the variables for any other formula.
My question
- Is this [motivation] possible in type theory foundations as described above? Can we have axiom schemes?
- If it's impossible, can type theory like Lean's only work with natural deduction and tactics instead of Hilbert-style system and pure logic (just substitution)? Or can we have such foundations as well with type theory?
- Do logical connectives in type theory not form well-formed formulas like they do in classical logic, creating problems 1 and 2?
My reasoning
By my reasoning this [motivation] is not possible because the only objects of type prop that we have are true and false, meaning we can only substitute formula variables with true and false and nothing else. When we add a new connective like conjunction with (D) that connective's compound formula (together with it's conjuncts) is not of type prop, it merely maps to type prop. Meaning we can't substitute a variable of type prop with, say, a conjunction formula.
In other words, $\tt{\wedge : prop \to prop \to prop}$ takes two props and gives you a third prop with a mechanism of a mapping. But that entire construction ($X \wedge Y$) is not a prop itself, the result ($\top$ / $\bot$) is.
Best Answer
Yes you can have things that behave like axiom schemes (of Hilbert calculi etc). The type $\forall (\phi, \psi : Prop), \phi \to (\psi \to \phi)$ expresses what you want. An element of this type is a proof of this "axiom schema". They are not axiom schemes wrt. the deduction system that Lean uses. To Lean this is just a kind of dependent function.
It is possible to do Hilbert-style reasoning or other kinds, but behind the scenes it will all be expressed in CIC.
Not as you might expect. There is a definition of well-formed formulae for the CIC, but when using $Prop$ to reason internally, no need for such a thing arises. The definitions of the CIC already ensure that every element of $Prop$ is a meaningful proposition. But there is no way to make an inductive proof over all propositions inside the CIC. Exactly as you can't do it inside your favourite classical logic. You can only do this in the meta-theory, which for Lean and the CIC can't be written inside Lean or we'd have Gödel problems.
When you add a new inductive definition like for conjunction, you create a new type constructor. This means that as long as you don't add certain axioms to the CIC (like classical logic, which Lean does by default iirc), then you can treat the types $X \land Y$ or $X \lor Y$ as being distinct from $\top, \bot$. But you won't be able to prove that they are different.