Switch to: Citations

Add references

You must login to add references.
  1. Two applications of Boolean models.Thierry Coquand - 1998 - Archive for Mathematical Logic 37 (3):143-147.
    Semantical arguments, based on the completeness theorem for first-order logic, give elegant proofs of purely syntactical results. For instance, for proving a conservativity theorem between two theories, one shows instead that any model of one theory can be extended to a model of the other theory. This method of proof, because of its use of the completeness theorem, is a priori not valid constructively. We show here how to give similar arguments, valid constructively, by using Boolean models. These models are (...)
    Download  
     
    Export citation  
     
    Bookmark   5 citations  
  • Saturated models of universal theories.Jeremy Avigad - 2002 - Annals of Pure and Applied Logic 118 (3):219-234.
    A notion called Herbrand saturation is shown to provide the model-theoretic analogue of a proof-theoretic method, Herbrand analysis, yielding uniform model-theoretic proofs of a number of important conservation theorems. A constructive, algebraic variation of the method is described, providing yet a third approach, which is finitary but retains the semantic flavor of the model-theoretic version.
    Download  
     
    Export citation  
     
    Bookmark   20 citations  
  • (1 other version)The correspondence between cut-elimination and normalization.J. Zucker - 1974 - Annals of Mathematical Logic 7 (1):1-112.
    Download  
     
    Export citation  
     
    Bookmark   27 citations  
  • Constructive Sheaf Semantics.Erik Palmgren - 1997 - Mathematical Logic Quarterly 43 (3):321-327.
    Sheaf semantics is developed within a constructive and predicative framework, Martin‐Löf's type theory. We prove strong completeness of many sorted, first order intuitionistic logic with respect to this semantics, by using sites of provably functional relations.
    Download  
     
    Export citation  
     
    Bookmark   12 citations  
  • Ein Ausgezeichnetes Modell Für Die Intuitionistische Typenlogik.Wilfried Buchholz - 1975 - Archive for Mathematical Logic 17 (1-2):55-60.
    Download  
     
    Export citation  
     
    Bookmark   3 citations