| Article ID | Journal | Published Year | Pages | File Type |
|---|---|---|---|---|
| 4661858 | Annals of Pure and Applied Logic | 2013 | 6 Pages |
Abstract
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.
Related Topics
Physical Sciences and Engineering
Mathematics
Logic
