PRL Seminar July 12: Intuitionistic Ancestral Logic
Join us on Thursday July 12 at noon for a PRL Seminar from Liron Cohen.
Liron will present her current work on 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.