nLab computational consistency

Idea

Computational consistency of a formal system says that

If the sequent $\vdash e \colon (x_1 = x_2)$ is derivable (claiming a witness of the proposition of equality of two terms) then the terms $x_1$ and $x_2$ have the same value by computation.

(Miquel, p.38)

Related concepts

• proof

References

• Alexandre Miquel, The experimental effectiveness of mathematical proof (pdf)