It should be noted that the operators we have been displaying as the logical operators are actually defined as type-valued functions. See
We shall focus on a few aspects of constructive mathematical language: effective notations, computational content, and existential proof witnesses.
Effective Notation
The core of computational type theory is a semantic method for notating values and types that is intended to be adequate for constructivist mathematical expression. See
A paradigm for constructively adequate notation is notating natural numbers. From a(n adequate) notation for a number, one can effectively determine whether it denotes zero, and if it does not, then one can effectively derive a notation for its predecessor. Similarly, from a notation for an ordered pair one must be able to derive a notation for each component.
Unless otherwise stipulated, we'll use the word "notation" to refer to an effective notation in this sense.
Notations for functions inherit criteria for effectiveness from their output types, and can exploit effectiveness of notations for their arguments. A notation for a (one-place) function is, at least in part, a way of building a notation for its result for any argument from a notation for that argument. So, from notations for a natural-number-valued function and for an argument, one can build a notation for the function's value and ascertain whether it denotes zero, et cetera.
Computational Content and Constructive Choice
Constructivists maintain that constructively understanding what a proposition means requires a conception of "computational content" of possible proofs of that proposition. Further, if one understands a proof then one can come up with its computational content. In particular, the computational content of a proof of an implication Q"
Similarly, the computational content of a proof that x:A. Q(x)"
A
Constructive type theory claims that the computational content of all the possible proofs of a proposition constitutes a type, and that giving a complete explanation of the meaning of a proposition requires explaining what that corresponding type of computational content is. Thus, the type of computational content for proofs of Q"
B"
Existential Proof Witnesses
From a (constructive) proof of an existential proposition x:A. P(x)"
Consequently, for example, since Q
(
x:
. (x = 0
P) & (x
0
Q))
Q"
Use
modus ponens on the above theorem to get a proof of x:
. (x = 0
P) & (x
0
Q)"
P) & (r
0
Q)"
P"
0
Q"
This example leads to the famous intuitionist rejection of the "law of the excluded middle", A:Prop. A
A
Thus, constructively, one may not always perform a case split on whether a proposition is true. One may do so for a proposition
P"
P
Thm* Dec(P) [there is a coercion from(
b:
. P
b)
to Prop ]
It should be noted that we do not mean by "proof" here a particular formalization of proof, such as Nuprl
About:
![]() | ![]() | ![]() | ![]() | ![]() | ![]() | ![]() | ![]() | ![]() |
![]() | ![]() | ![]() | ![]() | ![]() | ![]() |