chris martens on Nostr: for natural deduction, it’s beta reduction (local soundness) and eta expansion ...
for natural deduction, it’s beta reduction (local soundness) and eta expansion (local completeness)
chris martens
npub1yp…sun2n
2024-10-03 21:23:40 UTC
in reply to nevent1q…sghk
Author Public Key
npub1yp3qerlleys6mvvc4488qfnnwy732sa3ck0meq7yuefzy6nzm7jqxsun2nSeen on
wss://relay.momostr.pinkPublished at
2024-10-03 21:23:40 UTCEvent JSON
{
"id": "ad3124d76892354071a692cf499e355361f9e5702a133888c7f51a2ca62f4cf3",
"pubkey": "20620c8fffc921adb198ad4e702673713d1543b1c59fbc83c4e652226a62dfa4",
"created_at": 1727990620,
"kind": 1,
"tags": [
[
"p",
"7b18490a7c6d49144740dd7024285904ea5bb5b8b941af497cd7ca6fe00d2940"
],
[
"e",
"9a54dd0f9f16ceb44873945b93be09844bb19698333aff1b4d7cdda2d7ee88e4",
"",
"reply",
"edffe5ec2d874030990490c20bceecca2d1ee369034513a3db82dffb0f0ff043"
],
[
"p",
"8a8316532b57248ac82db7d866a32a07d9f14900eafa3f7c3b4f4662c09f79a9"
],
[
"p",
"20620c8fffc921adb198ad4e702673713d1543b1c59fbc83c4e652226a62dfa4"
],
[
"e",
"4cb7f39c81ec254f1fad73618c4c5e0e2d949e85d4fb343118a653d1e6726b63",
"",
"root",
"20620c8fffc921adb198ad4e702673713d1543b1c59fbc83c4e652226a62dfa4"
],
[
"proxy",
"https://hci.social/@chrisamaphone/113245593315191026",
"web"
],
[
"p",
"edffe5ec2d874030990490c20bceecca2d1ee369034513a3db82dffb0f0ff043"
],
[
"proxy",
"https://hci.social/users/chrisamaphone/statuses/113245593315191026",
"activitypub"
],
[
"L",
"pink.momostr"
],
[
"l",
"pink.momostr.activitypub:https://hci.social/users/chrisamaphone/statuses/113245593315191026",
"pink.momostr"
],
[
"-"
]
],
"content": "for natural deduction, it’s beta reduction (local soundness) and eta expansion (local completeness)",
"sig": "1621f732097bc8c689855b39c5a332071a4079405140b261c1c30170e7a6df00d9dce920ede5130ffdeaaf592fc35bebd7ee20f5a78382af5867d98b4aeede7d"
}