Login

Recent searches

No recent searches

Search options

Not available on me.dm.
me.dm is one of the many independent Mastodon servers you can use to participate in the fediverse.
Ideas and information to deepen your understanding of the world. Run by the folks at Medium.

Administered by:

Server stats:

1.3K
active users

me.dm: AboutProfiles directoryPrivacy policy

Mastodon: AboutGet the appKeyboard shortcutsView source codev4.3.9

#logic

15 posts15 participants1 post today
Continued thread
Public
RanaldClouston

I've followed these odd reductions back to the original source, 'Ideas and Results in Proof Theory' by Prawitz (1971); see attached image. These rules are introduced alongside the more usual ones, but not really discussed later as far as I can tell, except implicitly in a section when he notes that not everyone would accept rules beyond beta reduction as capturing the notion of 'the same proof'. He asserts uniqueness of normalisation, which these rules clearly break. Despite this being a quite heavily cited paper (~1000 cites), no one seems to have explicitly noted there is anything odd here until a paper by Dyckhoff in 2014, as best as I can tell! #logic #proofTheory

A section of a page from a logic paper, introducing the notion of 'immediate simplifications', where natural deduction proofs can be simplified in certain cases of use of the disjunction elimination, existential elimination, and bottom elimination rules.
ExploreLive feeds
About