Timeline for What restriction(s) of Goedel's primitive recursive functionals is (are) necessary and sufficient to prove the consistency of $PRA$
Current License: CC BY-SA 3.0
5 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jan 29, 2016 at 14:39 | comment | added | Ulrik Buchholtz | Yes, I would also conjecture that (though I don't see at the moment how to prove it). And no, in Tait's “Intensional Interpretations of Functionals of Finite Type I”, several variants of T are defined either with propositional or predicate logic (and with extensions to accommodate bar recursion), with $\mathrm{T}_0'$ being close to Gödel's. He then considers directing the equations in order to study normalization, but this is not defining of the systems. | |
| Jan 29, 2016 at 13:16 | comment | added | Thomas Benjamin | Also, in Tait's 1967 paper, I understand that he defined System $T$ as a set of rewrite rules. Is this correct? | |
| Jan 29, 2016 at 13:12 | comment | added | Thomas Benjamin | Do you think that for every term $t$ of $T$-hat strong normalization is provable in $PRA$? | |
| Jan 29, 2016 at 12:23 | vote | accept | Thomas Benjamin | ||
| Jan 29, 2016 at 4:23 | history | answered | Ulrik Buchholtz | CC BY-SA 3.0 |