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

Groups > comp.lang.prolog > #15123

BB(N): Prover should be verified [Henkin Constructive?] (Was: Where did the "smarts" go? Drinker Paradox fails)

Show all headers | View raw

Hi,

Well the problem might be only the rendering.
Ultimately a prover itself should be verified.
The Isabelle/HOL people did that for SAT solvers:

A Verified SAT Solver Framework
Jasmin Christian Blanchette et. al. 2018
https://matryoshka-project.github.io/pubs/sat_article.pdf

What would be a funny project, to refrain from
using infinite actual sets. Do a Gödel completeness
proof with infinite potential sets, applying

a kind of Scott's trick, maybe it would make the
proof even amenable to be carried out in the prover
itself, that is verified, requireing only a little

theory, like for example Kőnig's lemma. Henkin
model proofs are not really constructive. The involve
a choice among A v ~A. The problem is when constructing

a model, adding a literal A or ~A could lead in both
cases to a consistent new theory. It would be easier
when one of the literatals A or ~A would lead to

an inconsistency, giving a kind of choice certificate.
But the choice is kind of uncertified, in the
forcing for Henkin models. Not sure whether it can

be made a little bit more constructive. It also
relates to the busy beaver discussion, the recent
result that BB(748) is independent of ZFC.

Bye

Mild Shock schrieb:
> Hi,
> 
> Somebody attributed to me:
> 
> "The smart system to print via Prolog labels
> and reference lines in Fitch proofs"
> 
> But you find the Fitch labeling already here:
> 
> Rewriting for Fitch Style Natural Deductions
> Herman Geuvers, Rob-Nederpelt - 2004
> https://www.researchgate.net/publication/221220647
> 
> Bye
> 
> P.S.: I had a lot of smart posted on SWI-Prolog
> discourse, an other post had a few tricks to
> nicely render proofs involving quantifiers.
> 
> Still I was scolded and laughed at. At one
> moment the silly Philosophy Professor asked
> whether I am even human. What is the result
> 
> of this ignorance. A prover that doesn't work.
> I first thought I would do some fuzzy testing.
> But then I hand picked a manuel example from
> 
> FOL and not from propositional logic:
> 
> ?- prove(?[X]:(d(X) => ![Y]:d(Y))).
> https://en.wikipedia.org/wiki/Drinker_paradox
> 
> It doesn't produce something useful, although
> it says it has found a proof:
> 
> Continue despite warnings? (y/n): |: y.
> ------------------------------------------
> G4 PROOF FOR: ?[_4012-_4014]:(d(_4012-_4014)=>![_3560]:d(_3560))
> ------------------------------------------
> MODE: Theorem
> 
> === CLASSICAL PATTERN DETECTED ===
>      -> Skipping constructive logic
> === TRYING CLASSICAL LOGIC ===
> % 210 inferences, 0.000 CPU in 0.000 seconds (?% CPU, Infinite Lips)
>     Classical proof found
> G4+IP proofs in classical logic
> 
> - Sequent Calculus -
> 
> \begin{prooftree}
> \AxiomC{}
> \RightLabel{\scriptsize{$Ax.$}}
> \UnaryInfC{$
> false.
> 
> Was the thingy even tested before it went online?
> https://swi-prolog.discourse.group/t/swi-tinker-for-g4-mic-f-o-l-automated-prover/9410 
> 
> 
> Mild Shock schrieb:
>> Hi,
>>
>> Watch Alain Colmerauer juggle with 3 balls.
>> Thats the secret souce. Prolog is a circus.
>>
>> Prologia cirque
>> Alain Colmerauer explique avec humour comment il
>> a dû jongler avec la recherche, l'enseignement et
>> l'entreprise ...cette vidéo a été filmée en VHS en
>> 1994 à l'occasion de l'anniversaire de la création
>> de Prologia à Luminy, Marseille
>> https://www.youtube.com/watch?v=VyTgeUIb-OE
>>
>> But it is usually not circus of clowns. It was many
>> times a circus of artists, that can juggle with Philosophy,
>> Mathematical Logic and Computer Science,
>>
>> The contrary to morons like Boris the Loris,
>> Nazi Retard Julio, and many others, like EricGT,
>> Triska, Neumerkel, etc.. that forgot the roots of
>>
>> Prolog, turning it into an ISO nonsense, or
>> Ciao with their "cause" of Prolog. Basically loosing
>> the Compass of Prolog.
>>
>> Bye
>>
>> Contact XLOG schrieb:
>>  > Hi,
>>  >
>>  > Philosophy is a mandatory and highly important
>>  > subject in the French education system, studied
>>  > in the final year of high school (Terminale) and
>>  > as part of the Baccalauréat exams.
>>  >
>>  > France has strong philosophy education but weak
>>  > interdisciplinary bridges, especially compared
>>  > to places like the US, UK, or Germany where
>>  > “logic” spans departments.
>>  >
>>  > - Philosophers may focus on conceptual foundations,
>>  > argumentation, epistemology.
>>  > - Mathematicians/logicians focus on formal systems,
>>  > proof theory, model theory.
>>  > - Computer scientists focus on algorithms, computation,
>>  > complexity, type theory.
>>  >
>>  > But see the positive side. You could write
>>  > a book about the glorious 1960s, that saw
>>  > the Curry-Howard theorem comming.
>>  >
>>  > - The 1960s counterculture (“hippies”) were
>>  > drawn to new ways of thinking: systems, feedback loops,
>>  > interconnectedness — all ideas central to cybernetics.
>>  >
>>  > - Netherlands-based logicians were quietly
>>  > inventing AUTOMATH and type theory. probably
>>  > visiting a coffee shop from time to time.
>>  >
>>  > 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