What are the basic assumptions of type theory-based proof…
0 reactions
What are the basic assumptions of type theory-based proof assistants compared to those of traditional mathematics ?
I am trying to understand the foundational differences between proof assistants based on dependent type theory (such as Agda/Lean) and traditional mathematics as practiced in areas like real analysis.
For example, in Peano arithmetic, statements such as `0 ≠ S(n)` and the induction principle are usually presented as *axioms*. In Agda, however, defining an inductive type:
data Nat : Set where
zero : Nat
suc : Nat → Nat
automatically provides these properties through the rules of inductive types (constructor disjointness and the eliminator), which means you can write this as a *theorem*:
0-is-not-suc : ∀ {n} -> suc n ≡ 0 -> ⊥
0-is-not-suc ()
Does this mean inductive type theory is based on stronger assumptions than axiomatic mathematics, or are these just different choices of primitive rules?
More generally, what are the fundamental assumptions/rules that a type-theoretic prover starts with, and how do they compare with the foundations usually assumed in fields such as real analysis?
#technology
I am trying to understand the foundational differences between proof assistants based on dependent type theory (such as Agda/Lean) and traditional mathematics as practiced in areas like real analysis.
For example, in Peano arithmetic, statements such as `0 ≠ S(n)` and the induction principle are usually presented as *axioms*. In Agda, however, defining an inductive type:
data Nat : Set where
zero : Nat
suc : Nat → Nat
automatically provides these properties through the rules of inductive types (constructor disjointness and the eliminator), which means you can write this as a *theorem*:
0-is-not-suc : ∀ {n} -> suc n ≡ 0 -> ⊥
0-is-not-suc ()
Does this mean inductive type theory is based on stronger assumptions than axiomatic mathematics, or are these just different choices of primitive rules?
More generally, what are the fundamental assumptions/rules that a type-theoretic prover starts with, and how do they compare with the foundations usually assumed in fields such as real analysis?
#technology
| 1,000 mlx | |
| 3 | |
| 0 |