1. Forum
  2. Usenet
  3. SCI.PHYSICS

  • An Ode to Dan Christensen: The Curry's Paradox in Fitch Style

    From Mild Shock@21:1/5 to All on Wed Jun 5 08:45:47 2024
    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

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Mild Shock@21:1/5 to Mild Shock on Wed Jun 5 08:57:03 2024
    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

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Mild Shock@21:1/5 to Mild Shock on Thu Jun 6 23:29:14 2024
    Hi,

    I can't say how grateful I am to Dan Christensen,
    and his tool DC Proof, that had join and split.

    Its fast! All Arend Heyting axioms
    verified online in a blink:

    :- show((p=>p&p)).
    :- show((p&q=>q&p)).
    :- show(((p=>q)=>(p&r=>q&r))).
    :- show(((p=>q)&(q=>r)=>(p=>r))).
    :- show((p=>(q=>p))).
    :- show((p&(p=>q)=>q)).

    Example 44: RAA Cartesian https://www.xlog.ch/runtab/doclet/docs/06_demo/wilson/example44/package.html

    The examples are from here: https://archive.org/details/intuitionismintr1966heyt/page/100/mode/2up

    Bye

    Mild Shock schrieb:
    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


    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)