Groups | Search | Server Info | Keyboard shortcuts | Login | Register [http] [https] [nntp] [nntps]

Groups > comp.lang.prolog > #15126

The French Square Wheele Bicycle of Logic (Re: Secret Sauce of Dana Scott and Raymond Smullyan)

Show all headers | View raw

Hi,

I always admired the French Teaching of Logic.
This silly Philosophy Professor scolded me a couple
of times with this nonsense, playing dumb and deaf,

like a complete idiot:

Me: LEM is derivable from RAA, in minimal logic.
Prof: LEM is not even derivable from RAA in intuitionistic logic.
Me: You didn’t use RAA as an inference schema!
Prof: Our discussion is about logic and not about Prolog. I apologize.
https://swi-prolog.discourse.group/t/needing-help-with-call-with-depth-limit-3/7398/78

Still his prover demonstrates LEM from RAA:

?-prove((a | ~a)).
\begin{prooftree}
\AxiomC{\scriptsize{1}}
\noLine
\UnaryInfC{$ \lnot (A \lor  \lnot A)$}
\RightLabel{\scriptsize{$ \lor\to E$}}
\UnaryInfC{$ \lnot  \lnot A$}
\AxiomC{\scriptsize{1}}
\noLine
\UnaryInfC{$ \lnot (A \lor  \lnot A)$}
\RightLabel{\scriptsize{$ \lor\to E$}}
\UnaryInfC{$ \lnot A$}
\RightLabel{\scriptsize{$ \to E $}}
\BinaryInfC{$\bot$}
\RightLabel{\scriptsize{$ IP $}  1}
\UnaryInfC{$A \lor  \lnot A$}
\end{prooftree}
https://g4-mic.vidal-rosset.net/wasm/tinker#prove((a%20%7C%20~a)).

Please note that RAA = IP, synonymous names.
Reductio Ad Absurdum and Indirect Proof.

LoL

Bye

Mild Shock schrieb:
> Hi,
> 
> How it started:
> 
> Computers Still Can't Do Beautiful Mathematics - by Gina Kolata
> -----------------------------------------------------------------
> Mathematicians often say that their craft is as much an art
> as a science.  But as more and more researchers are using
> computers to prove their theorems, some worry that the magic
> is in danger of fading away.
> 
> How its going:
> 
> Computers Do Produce Beautiful Mathematics - Dr. Larry Wos
> -----------------------------------------------------------------
> In addition to exhibiting logical reasoning of the type
> found in mathematics, reasoning programs produce results
> that are startling and elegant.  Dr. J. Lukasiewicz was well
> recognized for his contributions to areas of logic,
> 
> and yet the program OTTER recently found a proof far shorter and
> more elegant than that produced by this eminent researcher,
> and the program used the same notation and style of
> reasoning.  Mathematicians and logicians find elegance in
> shorter proofs.
> 
> In August of 1990, Dr. Dana Scott of Carnegie Mellon
> University attended a workshop at Argonne National
> Laboratory.  There he learned of OTTER and some of its uses
> and successes.  Upon returning to his university, Dr.
> Scott's curiosity prompted him to suggest (via electronic
> mail) 68 theorems for consideration by the computer.
> 
> His curiosity was almost immediately satisfied, for the sought-
> after 68 proofs were returned with the comment that all were
> obtained in a single computer run with the program--and in
> less than 16 CPU minutes on a Sun 4 workstation.  Dr. Scott
> now uses his own copy of OTTER on his Macintosh.
> 
> Dr. R. Smullyan of the University of Indiana showed
> great pleasure and surprise at learning of some of the
> successes achieved by an automated reasoning program.  As
> evidence of his interest, he posed a number of questions,
> receiving in turn the answers to all but one of them--a
> question that is still open.
> https://theory.stanford.edu/~uribe/mail/qed.messages/91.html
> 
> Bye

Back to comp.lang.prolog | Previous | Next — Previous in thread | Next in thread | Find similar | Unroll thread

Thread

Secret Sauce of Dana Scott and Raymond Smullyan Mild Shock <janburse@fastmail.fm> - 2025-01-18 01:15 +0100
  The Clown World of Joseph Vidal Rosset (Re: Philosophize not God, Philosophize the Door Knob) Mild Shock <janburse@fastmail.fm> - 2025-12-04 11:26 +0100
    The SWI-Prolog community is a circus (Was: The Clown World of Joseph Vidal Rosset) Mild Shock <janburse@fastmail.fm> - 2025-12-04 11:47 +0100
      Alectryon: Long Life Learning or Stable Diffusion? (Was: The SWI-Prolog community is a circus) Mild Shock <janburse@fastmail.fm> - 2025-12-04 13:37 +0100
      From Unrusting Blade to Unburning Icarus (Re: The SWI-Prolog community is a circus ) Mild Shock <janburse@fastmail.fm> - 2026-07-27 12:18 +0200
    "considered consequence". Ha Ha, why this formulation? (Was: The Clown World of Joseph Vidal Rosset) Mild Shock <janburse@fastmail.fm> - 2025-12-04 21:41 +0100
      Don't worry, be happy: Take your time (Re: "considered consequence". Ha Ha, why this formulation?) Mild Shock <janburse@fastmail.fm> - 2025-12-04 21:57 +0100
        Write a book about the glorious 1960s (Re: Don't worry, be happy: Take your time) Mild Shock <janburse@fastmail.fm> - 2025-12-04 22:40 +0100
  Alain Colmerauer: Prologia cirque (Re: Secret Sauce of Dana Scott and Raymond Smullyan) Mild Shock <janburse@fastmail.fm> - 2025-12-04 22:52 +0100
    Where did the "smarts" go? Drinker Paradox fails (Was: Alain Colmerauer: Prologia cirque) Mild Shock <janburse@fastmail.fm> - 2025-12-05 15:46 +0100
      BB(N): Prover should be verified [Henkin Constructive?] (Was: Where did the "smarts" go? Drinker Paradox fails) Mild Shock <janburse@fastmail.fm> - 2025-12-05 16:08 +0100
  The French Square Wheele Bicycle of Logic (Re: Secret Sauce of Dana Scott and Raymond Smullyan) Mild Shock <janburse@fastmail.fm> - 2025-12-05 19:54 +0100
    The episode told everything about the Character (Re: The French Square Wheele Bicycle of Logic) Mild Shock <janburse@fastmail.fm> - 2025-12-05 20:12 +0100

csiph-web