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:
“seizing the swift logic of a woman,
Curse God and die.”
—Edwin Arlington Robinson (1869–1935)