Richard Zach on Nostr: Bill’s work up until 1980 concentrated on proof theory, specifically ...
Bill’s work up until 1980 concentrated on proof theory, specifically cut-elimination, functional interpretations, the ε-substitution method, type theory and lambda calculus. In Tait (1966), he proved the consistency of second order logic, settling the Takeuti conjecture positively. (Prawitz and Takahashi independently settled Takeuti’s conjecture for the full simple theory of types a year later.)
Published at
2024-03-24 22:44:10Event JSON
{
"id": "6ecf6274707acd9389e5abc6077a41a5356746ddf62877e48c98f56d1c71a378",
"pubkey": "580ba9c3849e80d58cbcd2c76728f33468f41c54396d73656137b224781f45d2",
"created_at": 1711320250,
"kind": 1,
"tags": [
[
"e",
"d9904d3b027c74b9296f7ab54a107d4896701bbe2ab71b993a20a7b2a9e02b85",
"wss://relay.mostr.pub",
"reply"
],
[
"proxy",
"https://mathstodon.xyz/users/rrrichardzach/statuses/112153083961174798",
"activitypub"
]
],
"content": "Bill’s work up until 1980 concentrated on proof theory, specifically cut-elimination, functional interpretations, the ε-substitution method, type theory and lambda calculus. In Tait (1966), he proved the consistency of second order logic, settling the Takeuti conjecture positively. (Prawitz and Takahashi independently settled Takeuti’s conjecture for the full simple theory of types a year later.)",
"sig": "d26a371ca59304804e60070228a1550a6a67fbb7a488b25d142f7791492c09b13b1d9dc000f69360224f325ccd24fde113056606550c126fc949916b279e6232"
}
