KnowledgeBase » 
SEMINAR
» ID = 681
Intuitionistic Ancestral Logic
Details
- Thurs. July 12
- In Upson 5126
- From Noon - 1PM
Summary
I will (informally) present a work in progress with Robert Constable on intuisionistic Ancestral Logic (iAL). We define iAL as an extension of iFOL, and illustrate its expressive power by relating it to omega logic with equality. A constructive proof for its consistency is given by showing that all provable formulas are realizable. The computational capabilities of iAL derive from the realizer for the computational induction principle over the transitive closure of a binary relation. I will show some examples of non-provable theorems of classical AL which turn out to be provable in iAL thanks to the realizers.
