# * Intuitionistic Ancestral Logic *

## by Liron Cohen

2012

**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.