Groups | Search | Server Info | Keyboard shortcuts | Login | Register [http] [https] [nntp] [nntps]
Groups > sci.physics > #887905
| From | Mild Shock <janburse@fastmail.fm> |
|---|---|
| Newsgroups | sci.physics |
| Subject | Re: An Ode to Dan Christensen: The Curry's Paradox in Fitch Style |
| Date | 2024-06-05 08:57 +0200 |
| Message-ID | <v3p27v$17co2$3@solani.org> (permalink) |
| References | <v3p1ir$17ca8$1@solani.org> |
Dan Christensen was my long term sparring partner on sci.logic, but he somehow disappeared. He had a proof tool, that implemented some sort of free logic, and was heavily defending his tool, and calling other tools that implemented the more traditional non-free first order logic nonsense. The last he posted on sci.logic was a solution to the Russell paradox, where he got into multivalued logic. But in a very stubborn way, and he didn't accept again, that each resolution of the Russell paradox, provokes a new kind of Russell paradox. This was actually quite interesting Mild Shock schrieb: > We present a little tour de force in implementing > a Prolog technology theorem prover for intuitionistic > propositional and first order logic. The main idea > was already demonstrated by John Slaney in > his MINLOG System. > > Instead of transforming a proof from NJ to LJ as in > cut elimination, we transform a proof back from LJ > to NJ. What helps us doing this transformation is > extracting and rendering proof terms from > the Curry-Howard isomorphism. > > Drawing upon Jens Ottens ileanSeP and leanSeq we > deviced propositional and first order proof search > for LJ. We can render Fitch Style proofs of Curry's > Paradox and the propositionally resembling Barber > Paradox, whereby our logic assumes at least one > Barber. Both are intuitionistically valid. > > See also: > > The Curry's Paradox in Fitch Style > https://twitter.com/dogelogch/status/1798242629152637208 > > The Curry's Paradox in Fitch Style > https://www.facebook.com/groups/dogelog
Back to sci.physics | Previous | Next — Previous in thread | Next in thread | Find similar
An Ode to Dan Christensen: The Curry's Paradox in Fitch Style Mild Shock <janburse@fastmail.fm> - 2024-06-05 08:45 +0200
Re: An Ode to Dan Christensen: The Curry's Paradox in Fitch Style Mild Shock <janburse@fastmail.fm> - 2024-06-05 08:57 +0200
Re: An Ode to Dan Christensen: The Curry's Paradox in Fitch Style Mild Shock <janburse@fastmail.fm> - 2024-06-06 23:29 +0200
csiph-web