nprofile1qy2hwumn8ghj7un9d3shjtnyd968gmewwp6kyqpqjd874v63430gng67kpw5m597f34dr9vr0yhkp8dkmnma8208raysj9xuzd (nprofile…xuzd) I'm TAing a proof theory course that uses the book "Structural Proof Theory" and sharing a lot of these feelings at the moment... How can a book published 16 years ago already be so outdated‽
It also does this weird thing where the weight of a formula is defined as its symbol count except that ⊥ counts for 0, so when doing induction on the weight of a formula you have to special case nonsense like ⊥ → ⊥... Way to invent complexity where there is none.
Naïm Camille Favier
npub1av…z5z7z
2026-02-09 13:08:08 UTC
in reply to nevent1q…t593
Author Public Key
npub1avwd5p4zn7ndkvjf9qtrsddacax0cvmujryu2qnlxcm6nmlnquwqxz5z7zSeen on
wss://relay.mostr.pubPublished at
2026-02-09 13:08:08 UTCEvent JSON
{
"id": "a97b0b67da00f7b6238cf8d3fcec65ee66542d768cb3781e2570efe20f63b3b1",
"pubkey": "eb1cda06a29fa6db324928163835bdc74cfc337c90c9c5027f3637a9eff3071c",
"created_at": 1770642488,
"kind": 1,
"tags": [
[
"p",
"934feab351ac5e89a35eb05d4dd0be4c6ad19583792f609db6dcf7d3a9e71f49",
"wss://relay.ditto.pub"
],
[
"p",
"ba51d3bb7fc92891016b5873c0b4f7c6a0550c964ec565ece24b6fc2dcf93301",
"wss://relay.ditto.pub"
],
[
"e",
"32b545deec9902e55e3bfe25b8772a097e0e93d5145aa3ed0ca3856e0170b4ec",
"wss://relay.ditto.pub",
"reply"
],
[
"proxy",
"https://types.pl/users/ncf/statuses/116040826105874781",
"activitypub"
],
[
"client",
"Mostr",
"31990:6be38f8c63df7dbf84db7ec4a6e6fbbd8d19dca3b980efad18585c46f04b26f9:mostr",
"wss://relay.ditto.pub"
]
],
"content": "nostr:nprofile1qy2hwumn8ghj7un9d3shjtnyd968gmewwp6kyqpqjd874v63430gng67kpw5m597f34dr9vr0yhkp8dkmnma8208raysj9xuzd I'm TAing a proof theory course that uses the book \"Structural Proof Theory\" and sharing a lot of these feelings at the moment... How can a book published 16 years ago already be so outdated‽\n\nIt also does this weird thing where the weight of a formula is defined as its symbol count except that ⊥ counts for 0, so when doing induction on the weight of a formula you have to special case nonsense like ⊥ → ⊥... Way to invent complexity where there is none.",
"sig": "2f2e9b34b56da72edb499c13c2ec3fd22a208ccdfe9e0488598a08be25066c9a8a59ab6e42a5305f03953490ba795938b53fede86ffcff6de479b0c100b18a52"
}