Dialectica Interpretation of Intuitionistic Logic
The interpretation has two components: a formula translation and a proof translation. The formula translation describes how each formula of Heyting arithmetic is mapped to a quantifier-free formula of the system T, where and are tuples of fresh variables (not appearing free in ). Intuitively, is interpreted as . The proof translation shows how a proof of has enough information to witness the interpretation of, i.e. the proof of can be converted into a closed term and a proof of in the system T.
Read more about this topic: Dialectica Interpretation
Famous quotes containing the word logic:
“We want in every man a long logic; we cannot pardon the absence of it, but it must not be spoken. Logic is the procession or proportionate unfolding of the intuition; but its virtue is as silent method; the moment it would appear as propositions and have a separate value, it is worthless.”
—Ralph Waldo Emerson (1803–1882)