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

Groups > comp.lang.prolog > #15118

"considered consequence". Ha Ha, why this formulation? (Was: The Clown World of Joseph Vidal Rosset)

Show all headers | View raw

"considered consequence". Ha Ha, why this
formulation? I voluntarily used the Curry-
Howard theorem, when I developed my Prolog

code. I didn't invent anything. And its not
a smart system. Please never use the word
"smart" in software engineering, thats not

professional. In particular the Implication
Introduction rule has been documented around
the world a 100x times: Just have a look:

Intuitionistic implicational natural deduction

G, A |- B
------------ (->I)
G |- A -> B

Lambda calculus type assignment rules

G, x:A |- t:B
----------------------- (->I)
G |- (λx:A.t) : A -> B

https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence#Intuitionistic_natural_deduction_and_typed_lambda_calculus

Also refering to the above is probably more
useful, than referning to the paper. Since
it gives a summary of propositional

MINIMAL LOGIC in Curry-Howard simple types.

Mild Shock schrieb:
> Hi,
> 
> Instead presenting a clown world like here:
> 
> - The smart system for printing labels and reference
> lines in Fitch proofs has been invented by B., a Prolog
> expert who usually dislikes seeing his name quoted.
> https://www.vidal-rosset.net/2025-11-17-swi-tinker-for-swi-prolog-provers.html 
> 
> 
> You could simply state that the Fitch renderer
> is derived from Curry-Howard isomorphism proof
> terms. This is pretty much folk knowledge in logic
> 
> circles, and wasnt invented by me. I was only
> the messenger for things that every Logician should
> know, already at least for 60 years, the original
> 
> THE FORMULAE-AS-TYPES NOTION OF CONSTRUCTION
> W. A. Howard - University of Chicago
> https://www.cs.cmu.edu/~crary/819-f09/Howard80.pdf
> 
> Curry-Howard paper already circulated in 1969.
> That was around the same time when Automath
> ("automating mathematics") was devised by Nicolaas
> 
> Govert de Bruijn, for expressing complete mathematical
> theories in such a way that an included automated
> proof checker can verify their correctness.
> 
> 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