skip to main content

About Goodmanʼs Theorem

Coquand, Thierry

Annals of pure and applied logic, 2013-04, Vol.164 (4), p.437-442 [Periódico revisado por pares]

Elsevier B.V

Texto completo disponível

Citações Citado por
  • Título:
    About Goodmanʼs Theorem
  • Autor: Coquand, Thierry
  • Assuntos: Computer and Information Science ; Data- och informationsvetenskap ; Forcing and realizability ; Formal topology ; Goodman's Theorem ; Goodmanʼs Theorem
  • É parte de: Annals of pure and applied logic, 2013-04, Vol.164 (4), p.437-442
  • Descrição: We present a proof of Goodmanʼs Theorem, which is a variation of the proof of Renaldel de Lavalette (1990) [9]. This proof uses in an essential way possibly divergent computations for proving a result which mentions systems involving only terminating computations. Our proof is carried out in a constructive metalanguage. This involves implicitly a covering relation over arbitrary posets in formal topology, which occurs in forcing in set theory in a classical framework, but can also be defined constructively.
  • Editor: Elsevier B.V
  • Idioma: Inglês

Buscando em bases de dados remotas. Favor aguardar.