Switch to: References

Add citations

You must login to add citations.
  1. Intuitionistic completeness of first-order logic.Robert Constable & Mark Bickford - 2014 - Annals of Pure and Applied Logic 165 (1):164-198.
    We constructively prove completeness for intuitionistic first-order logic, iFOL, showing that a formula is provable in iFOL if and only if it is uniformly valid in intuitionistic evidence semantics as defined in intuitionistic type theory extended with an intersection operator.Our completeness proof provides an effective procedure that converts any uniform evidence into a formal iFOL proof. Uniform evidence can involve arbitrary concepts from type theory such as ordinals, topological structures, algebras and so forth. We have implemented that procedure in the (...)
    Download  
     
    Export citation  
     
    Bookmark  
  • Delimited control operators prove Double-negation Shift.Danko Ilik - 2012 - Annals of Pure and Applied Logic 163 (11):1549-1559.
    We propose an extension of minimal intuitionistic predicate logic, based on delimited control operators, that can derive the predicate-logic version of the double-negation shift schema, while preserving the disjunction and existence properties.
    Download  
     
    Export citation  
     
    Bookmark   2 citations