Timeline for What assumptions and methodology do metaproofs of logic theorems use and employ?
Current License: CC BY-SA 2.5
5 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jan 13, 2010 at 17:30 | comment | added | Neel Krishnaswami | In normalization by evaluation, you (basically) start with a logic with cut. Then, you give the universal/syntactic model of the logic (concretely the Kripke model of contexts ordered by inclusion), and the composition of (constructive) soundness and completeness is the NBE algorithm! Here's some Agda code illustrating this idea: cs.nott.ac.uk/~dwm/nbe/html/NBE.html | |
| Jan 13, 2010 at 14:43 | comment | added | Charles Stewart | I don't see where you are going. Maybe light is cast if I point out that PRA is enough to show the equivalence of SN for System F and consistency of second-order arithmetic? Here, one can claim the object theory is constructive, but the metatheory is not strong enough to show that proofs in System F have normal forms. Where is there any metatheoretic reliance on the constructive content of the object theory? PRA is as agnostic about the constructive content of System F as it is about the consistency of Z2. | |
| Jan 13, 2010 at 13:39 | comment | added | Neel Krishnaswami | One example of a place where constructivity is necessary: normalization-by-evaluation relies on the constructive content of a pair of soundness and completeness theorems. | |
| Jan 13, 2010 at 13:13 | history | edited | Charles Stewart | CC BY-SA 2.5 |
sp
|
| Jan 13, 2010 at 13:04 | history | answered | Charles Stewart | CC BY-SA 2.5 |