This is also an interesting article, mentioning a new
trend such as "Multiparadigm languages":

Where Programming, Ops, AI, and the Cloud are Headed in 2021
https://www.oreilly.com/radar/where-programming-ops-ai-and-the-cloud-are-headed-in-2021/

We just observed that Python 3.10 introduced a new
pattern matching construct. Now there is a proposal
for Java JDK 17 followup for some pattern matching
like switch statement. I guess there is an unspoken law:

"Every programming language over the long
run will evolve into some Prolog variant"

Well this is too harsh, maybe this pattern matching only
mimicks Haskell single sided unification and not Prolog
unification. But what if people get fed up
with single sided unification?

LoL

Mostowski Collapse schrieb am Sonntag, 28. November 2021 um 16:22:27 UTC+1:
> This shows me that functional programming is on the decline:
>
> Google Trends: Logic vs Functional Programming - From 2004 to 2021
> https://trends.google.de/trends/explore?date=all&q=logic%20programming,functional%20programming
>
> I wonder whether this will have an impact on proof assistants.
> Some of them have clearly a functional programming inclining.

Maybe the assumption that programming language further
evolve is wrong, they could also devolve to assembler again?

Awaken In 2505, Humans Devolve
https://www.youtube.com/watch?v=mnLxc954ipo

At least this would truely help to have full control of
the performance and memory allocation of your code.

LMAO!

Mostowski Collapse schrieb am Sonntag, 28. November 2021 um 16:29:16 UTC+1:
> This is also an interesting article, mentioning a new
> trend such as "Multiparadigm languages":
>
> Where Programming, Ops, AI, and the Cloud are Headed in 2021
> https://www.oreilly.com/radar/where-programming-ops-ai-and-the-cloud-are-headed-in-2021/
>
> We just observed that Python 3.10 introduced a new
> pattern matching construct. Now there is a proposal
> for Java JDK 17 followup for some pattern matching
> like switch statement. I guess there is an unspoken law:
>
> "Every programming language over the long
> run will evolve into some Prolog variant"
>
> Well this is too harsh, maybe this pattern matching only
> mimicks Haskell single sided unification and not Prolog
> unification. But what if people get fed up
> with single sided unification?
>
> LoL
> Mostowski Collapse schrieb am Sonntag, 28. November 2021 um 16:22:27 UTC+1:
> > This shows me that functional programming is on the decline:
> >
> > Google Trends: Logic vs Functional Programming - From 2004 to 2021
> > https://trends.google.de/trends/explore?date=all&q=logic%20programming,functional%20programming
> >
> > I wonder whether this will have an impact on proof assistants.
> > Some of them have clearly a functional programming inclining.

There was a proposal:
https://area51.stackexchange.com/proposals/29144/beginner-theoretical-computer-science
But it now says:
This proposal has been deleted

Now if you want to join cstheory.stackexchange.com it
says Anybody can ask a question Anybody can answer
The best answers are voted up and rise to the top

But if you do that, they slap their policy into your face:
It allows only questions that "can be discussed between
two professors or between two graduate students working
on Ph.D.'s, but not usually between a professor and a
typical undergraduate student".
https://meta.stackexchange.com/questions/79351/should-research-level-only-sites-be-allowed

I am not lying when I say even Andrej Bauer did
that. But how do you want to launch a proof assistants
site, I assume for everybody? if you cannot divert
cs theory questions to another stackexchange?

proof assistants are full of cs theory stuff.

Mostowski Collapse schrieb am Sonntag, 28. November 2021 um 20:31:11 UTC+1:
> Maybe the assumption that programming language further
> evolve is wrong, they could also devolve to assembler again?
>
> Awaken In 2505, Humans Devolve
> https://www.youtube.com/watch?v=mnLxc954ipo
>
> At least this would truely help to have full control of
> the performance and memory allocation of your code.
>
> LMAO!
> Mostowski Collapse schrieb am Sonntag, 28. November 2021 um 16:29:16 UTC+1:
> > This is also an interesting article, mentioning a new
> > trend such as "Multiparadigm languages":
> >
> > Where Programming, Ops, AI, and the Cloud are Headed in 2021
> > https://www.oreilly.com/radar/where-programming-ops-ai-and-the-cloud-are-headed-in-2021/
> >
> > We just observed that Python 3.10 introduced a new
> > pattern matching construct. Now there is a proposal
> > for Java JDK 17 followup for some pattern matching
> > like switch statement. I guess there is an unspoken law:
> >
> > "Every programming language over the long
> > run will evolve into some Prolog variant"
> >
> > Well this is too harsh, maybe this pattern matching only
> > mimicks Haskell single sided unification and not Prolog
> > unification. But what if people get fed up
> > with single sided unification?
> >
> > LoL
> > Mostowski Collapse schrieb am Sonntag, 28. November 2021 um 16:22:27 UTC+1:
> > > This shows me that functional programming is on the decline:
> > >
> > > Google Trends: Logic vs Functional Programming - From 2004 to 2021
> > > https://trends.google.de/trends/explore?date=all&q=logic%20programming,functional%20programming
> > >
> > > I wonder whether this will have an impact on proof assistants.
> > > Some of them have clearly a functional programming inclining.

Anyway, these bitrot exchanges are mushrooming,
what about this one, would it be helpful?

https://cs.stackexchange.com/

Mostowski Collapse schrieb am Montag, 29. November 2021 um 00:20:32 UTC+1:
> There was a proposal:
> https://area51.stackexchange.com/proposals/29144/beginner-theoretical-computer-science
> But it now says:
> This proposal has been deleted
>
> Now if you want to join cstheory.stackexchange.com it
> says Anybody can ask a question Anybody can answer
> The best answers are voted up and rise to the top
>
> But if you do that, they slap their policy into your face:
> It allows only questions that "can be discussed between
> two professors or between two graduate students working
> on Ph.D.'s, but not usually between a professor and a
> typical undergraduate student".
> https://meta.stackexchange.com/questions/79351/should-research-level-only-sites-be-allowed
>
> I am not lying when I say even Andrej Bauer did
> that. But how do you want to launch a proof assistants
> site, I assume for everybody? if you cannot divert
> cs theory questions to another stackexchange?
>
> proof assistants are full of cs theory stuff.
> Mostowski Collapse schrieb am Sonntag, 28. November 2021 um 20:31:11 UTC+1:
> > Maybe the assumption that programming language further
> > evolve is wrong, they could also devolve to assembler again?
> >
> > Awaken In 2505, Humans Devolve
> > https://www.youtube.com/watch?v=mnLxc954ipo
> >
> > At least this would truely help to have full control of
> > the performance and memory allocation of your code.
> >
> > LMAO!
> > Mostowski Collapse schrieb am Sonntag, 28. November 2021 um 16:29:16 UTC+1:
> > > This is also an interesting article, mentioning a new
> > > trend such as "Multiparadigm languages":
> > >
> > > Where Programming, Ops, AI, and the Cloud are Headed in 2021
> > > https://www.oreilly.com/radar/where-programming-ops-ai-and-the-cloud-are-headed-in-2021/
> > >
> > > We just observed that Python 3.10 introduced a new
> > > pattern matching construct. Now there is a proposal
> > > for Java JDK 17 followup for some pattern matching
> > > like switch statement. I guess there is an unspoken law:
> > >
> > > "Every programming language over the long
> > > run will evolve into some Prolog variant"
> > >
> > > Well this is too harsh, maybe this pattern matching only
> > > mimicks Haskell single sided unification and not Prolog
> > > unification. But what if people get fed up
> > > with single sided unification?
> > >
> > > LoL
> > > Mostowski Collapse schrieb am Sonntag, 28. November 2021 um 16:22:27 UTC+1:
> > > > This shows me that functional programming is on the decline:
> > > >
> > > > Google Trends: Logic vs Functional Programming - From 2004 to 2021
> > > > https://trends.google.de/trends/explore?date=all&q=logic%20programming,functional%20programming
> > > >
> > > > I wonder whether this will have an impact on proof assistants.
> > > > Some of them have clearly a functional programming inclining.

The devolution could be also a form of evolution. I recently saw
a book about ARM assembly which had a garbage collection
section. In 2018 ARM started supporting pointer tagging.

See also:

ARM Memory Tagging Extension
Kosty Serbryany - 2019
https://www.usenix.org/system/files/login/articles/login_summer19_03_serebryany.pdf

C–: a portable assembly language that supports garbage collection
Simon Peyton Jones - 1999
https://www.cs.tufts.edu/~nr/pubs/c–gc.pdf

Basically what was once conceived as a Java Chip seems to
happen right now. You can also view it as LISP on a Chip I guess,
remove the object oriented obsession, and focus on safety.

Mostowski Collapse schrieb am Sonntag, 28. November 2021 um 20:31:11 UTC+1:
> Maybe the assumption that programming language further
> evolve is wrong, they could also devolve to assembler again?
>
> Awaken In 2505, Humans Devolve
> https://www.youtube.com/watch?v=mnLxc954ipo
>
> At least this would truely help to have full control of
> the performance and memory allocation of your code.
>
> LMAO!
> Mostowski Collapse schrieb am Sonntag, 28. November 2021 um 16:29:16 UTC+1:
> > This is also an interesting article, mentioning a new
> > trend such as "Multiparadigm languages":
> >
> > Where Programming, Ops, AI, and the Cloud are Headed in 2021
> > https://www.oreilly.com/radar/where-programming-ops-ai-and-the-cloud-are-headed-in-2021/
> >
> > We just observed that Python 3.10 introduced a new
> > pattern matching construct. Now there is a proposal
> > for Java JDK 17 followup for some pattern matching
> > like switch statement. I guess there is an unspoken law:
> >
> > "Every programming language over the long
> > run will evolve into some Prolog variant"
> >
> > Well this is too harsh, maybe this pattern matching only
> > mimicks Haskell single sided unification and not Prolog
> > unification. But what if people get fed up
> > with single sided unification?
> >
> > LoL
> > Mostowski Collapse schrieb am Sonntag, 28. November 2021 um 16:22:27 UTC+1:
> > > This shows me that functional programming is on the decline:
> > >
> > > Google Trends: Logic vs Functional Programming - From 2004 to 2021
> > > https://trends.google.de/trends/explore?date=all&q=logic%20programming,functional%20programming
> > >
> > > I wonder whether this will have an impact on proof assistants.
> > > Some of them have clearly a functional programming inclining.

What about this riddle, doing it in Prolog, s(CASP) or LK?
(LK as per the Phil Zucker page might not do it,
would need a FOL or so extension I guess)

An impossible asylum - Avigad et al. 2021
“In 1982, Raymond Smullyan published an article, “The Asylum of
Doctor Tarr and Professor Fether,” that consists of a series of
puzzles. These were later reprinted in the anthology, “The Lady
or The Tiger? and Other Logic Puzzles.” The last puzzle, which
describes the asylum alluded to in the title, was designed to be
especially difficult. With the help of automated reasoning, we
show that the puzzle’s hypotheses are, in fact, inconsistent,
which is to say, no such asylum can possibly exist.”
https://arxiv.org/abs/2112.02142

No Son of BirdBrain III yet in sight?
I tried https://www.umsu.de/trees/ on this here, to find a model of:

E * x = x. % left identity
x’ * x = E. % left inverse
(x * y) * z = x * (y * z). % associativity
A * B != B * A. % A and B do not commute

But its horribly choking.

Interesting call:

"For example, have a look at the Coq standard libarary or
the user contributions, these are formalizations of
mathematics in type theory. And this stuff is written mostly
by computer scientists. If mathematicians moved onto
the proof-assistant bandwagon, there would be much more."
https://mathoverflow.net/a/133599

Maybe they would join the bandwagon if there were
less typos? Whats a "libarary"? Is it library? Or libarray?

LoL

Small bug in the LK code:

There is a nice theorem prover for propositional logic with LK implemented in Prolog here:
https://www.philipzucker.com/javascript-automated-proving/

Its not complete for FOL matrices, try this:

prove0(((p(X) => p(t) | p(s)) & (p(X) => p(s))), Proof).
Failed To Prove.

Now remove the cut in the axiom rule:

prove0(((p(X) => p(t) | p(s)) & (p(X) => p(s))), Proof).
X = s

Mostowski Collapse schrieb am Dienstag, 28. Dezember 2021 um 19:26:21 UTC+1:
> Interesting call:
>
> "For example, have a look at the Coq standard libarary or
> the user contributions, these are formalizations of
> mathematics in type theory. And this stuff is written mostly
> by computer scientists. If mathematicians moved onto
> the proof-assistant bandwagon, there would be much more."
> https://mathoverflow.net/a/133599
>
> Maybe they would join the bandwagon if there were
> less typos? Whats a "libarary"? Is it library? Or libarray?
>
> LoL

To handle FOL matrices, unify_with_occurs_check/2 might
also come into play. Whats a short example and short
explanation about things that can go wrong?

Mostowski Collapse schrieb:
> Small bug in the LK code:
>
> There is a nice theorem prover for propositional logic with LK implemented in Prolog here:
> https://www.philipzucker.com/javascript-automated-proving/
>
> Its not complete for FOL matrices, try this:
>
> prove0(((p(X) => p(t) | p(s)) & (p(X) => p(s))), Proof).
> Failed To Prove.
>
> Now remove the cut in the axiom rule:
>
> prove0(((p(X) => p(t) | p(s)) & (p(X) => p(s))), Proof).
> X = s
>
> Mostowski Collapse schrieb am Dienstag, 28. Dezember 2021 um 19:26:21 UTC+1:
>> Interesting call:
>>
>> "For example, have a look at the Coq standard libarary or
>> the user contributions, these are formalizations of
>> mathematics in type theory. And this stuff is written mostly
>> by computer scientists. If mathematicians moved onto
>> the proof-assistant bandwagon, there would be much more."
>> https://mathoverflow.net/a/133599
>>
>> Maybe they would join the bandwagon if there were
>> less typos? Whats a "libarary"? Is it library? Or libarray?
>>
>> LoL

Oh, this is very nice!

∃x∃y(Pyy → Pxf(x)) is invalid.
https://www.umsu.de/trees/#~7x~7y%28Pyy~5Pxf%28x%29%29

Countermodel:
Domain: { 0, 1 }
f: { (0,1), (1,0) }
P: { (0,0), (1,1) }

Mostowski Collapse schrieb am Donnerstag, 30. Dezember 2021 um 09:56:23 UTC+1:
> To handle FOL matrices, unify_with_occurs_check/2 might
> also come into play. Whats a short example and short
> explanation about things that can go wrong?
>
> Mostowski Collapse schrieb:
> > Small bug in the LK code:
> >
> > There is a nice theorem prover for propositional logic with LK implemented in Prolog here:
> > https://www.philipzucker.com/javascript-automated-proving/
> >
> > Its not complete for FOL matrices, try this:
> >
> > prove0(((p(X) => p(t) | p(s)) & (p(X) => p(s))), Proof).
> > Failed To Prove.
> >
> > Now remove the cut in the axiom rule:
> >
> > prove0(((p(X) => p(t) | p(s)) & (p(X) => p(s))), Proof).
> > X = s
> >
> > Mostowski Collapse schrieb am Dienstag, 28. Dezember 2021 um 19:26:21 UTC+1:
> >> Interesting call:
> >>
> >> "For example, have a look at the Coq standard libarary or
> >> the user contributions, these are formalizations of
> >> mathematics in type theory. And this stuff is written mostly
> >> by computer scientists. If mathematicians moved onto
> >> the proof-assistant bandwagon, there would be much more."
> >> https://mathoverflow.net/a/133599
> >>
> >> Maybe they would join the bandwagon if there were
> >> less typos? Whats a "libarary"? Is it library? Or libarray?
> >>
> >> LoL

On Thursday, 30 December 2021 at 10:06:49 UTC+1, burs...@gmail.com wrote:

> Oh, this is very nice!

There is nothing nice about a fucking retard and piece of spamming
shit polluting all public ponds, you shameless retarded piece of shit.

But all I'd still want to know is who's the criminal nazi cunts who pay your bills...

*Plonk*

Julio

LoL, are you feeling tense Culio?

Julio Di Egidio <julio@diegidio.name> schrieb am Donnerstag, 30. Dezember 2021 um 11:48:09 UTC+1:
> On Thursday, 30 December 2021 at 10:06:49 UTC+1, burs...@gmail.com wrote:
>
> > Oh, this is very nice!
> There is nothing nice about a fucking retard and piece of spamming
> shit polluting all public ponds, you shameless retarded piece of shit.
>
> But all I'd still want to know is who's the criminal nazi cunts who pay your bills...
>
> *Plonk*
>
> Julio

Lean TAP can be fun. Spent the whole day to
render MathJax. Then was annoyed by MathJax,
how do you put this thingy into an email?

So here is barber paradox in list form with Unicode:

1. s(a,a) ⊢ s(a,a) (ax)
2. s(a,a) ⊢ ∃zs(z,z) (R∃)
3. ⊢ ¬s(a,a), ∃zs(z,z) (R¬)
4. s(a,a) ⊢ s(a,a) (ax)
5. s(a,a) ⊢ ∃zs(z,z) (R∃)
6. ¬s(a,a) ⇒ s(a,a) ⊢ ∃zs(z,z) (L⇒, 3)
7. ∀y(¬s(y,y) ⇒ s(a,y)) ⊢ ∃zs(z,z) (L∀)
8. ∃x∀y(¬s(y,y) ⇒ s(x,y)) ⊢ ∃zs(z,z) (L∃)
9. ⊢ ∃x∀y(¬s(y,y) ⇒ s(x,y)) ⇒ ∃zs(z,z) (R⇒)

http://www.xlog.ch/izytab/doclet/en/docs/18_live/40_bin2021/paste07/package.html

So how was it done? First one needs to reduce proof noise:

Dogelog Player removes proof noise
https://twitter.com/dogelogch/status/1477236879795830785

Dogelog Player removes proof noise
https://www.facebook.com/groups/dogelog

Mostowski Collapse schrieb am Freitag, 31. Dezember 2021 um 01:11:37 UTC+1:
> Lean TAP can be fun. Spent the whole day to
> render MathJax. Then was annoyed by MathJax,
> how do you put this thingy into an email?
>
> So here is barber paradox in list form with Unicode:
>
> 1. s(a,a) ⊢ s(a,a) (ax)
> 2. s(a,a) ⊢ ∃zs(z,z) (R∃)
> 3. ⊢ ¬s(a,a), ∃zs(z,z) (R¬)
> 4. s(a,a) ⊢ s(a,a) (ax)
> 5. s(a,a) ⊢ ∃zs(z,z) (R∃)
> 6. ¬s(a,a) ⇒ s(a,a) ⊢ ∃zs(z,z) (L⇒, 3)
> 7. ∀y(¬s(y,y) ⇒ s(a,y)) ⊢ ∃zs(z,z) (L∀)
> 8. ∃x∀y(¬s(y,y) ⇒ s(x,y)) ⊢ ∃zs(z,z) (L∃)
> 9. ⊢ ∃x∀y(¬s(y,y) ⇒ s(x,y)) ⇒ ∃zs(z,z) (R⇒)
>
> http://www.xlog.ch/izytab/doclet/en/docs/18_live/40_bin2021/paste07/package.html

Oki Doki, full first order logic can be also rendered now:

Leibniz’s Dream in Dogelog Player
https://twitter.com/dogelogch/status/1477779371628933121

Leibniz’s Dream in Dogelog Player
https://www.facebook.com/groups/dogelog

Mostowski Collapse schrieb am Samstag, 1. Januar 2022 um 12:30:25 UTC+1:
> So how was it done? First one needs to reduce proof noise:
>
> Dogelog Player removes proof noise
> https://twitter.com/dogelogch/status/1477236879795830785
>
> Dogelog Player removes proof noise
> https://www.facebook.com/groups/dogelog
> Mostowski Collapse schrieb am Freitag, 31. Dezember 2021 um 01:11:37 UTC+1:
> > Lean TAP can be fun. Spent the whole day to
> > render MathJax. Then was annoyed by MathJax,
> > how do you put this thingy into an email?
> >
> > So here is barber paradox in list form with Unicode:
> >
> > 1. s(a,a) ⊢ s(a,a) (ax)
> > 2. s(a,a) ⊢ ∃zs(z,z) (R∃)
> > 3. ⊢ ¬s(a,a), ∃zs(z,z) (R¬)
> > 4. s(a,a) ⊢ s(a,a) (ax)
> > 5. s(a,a) ⊢ ∃zs(z,z) (R∃)
> > 6. ¬s(a,a) ⇒ s(a,a) ⊢ ∃zs(z,z) (L⇒, 3)
> > 7. ∀y(¬s(y,y) ⇒ s(a,y)) ⊢ ∃zs(z,z) (L∀)
> > 8. ∃x∀y(¬s(y,y) ⇒ s(x,y)) ⊢ ∃zs(z,z) (L∃)
> > 9. ⊢ ∃x∀y(¬s(y,y) ⇒ s(x,y)) ⇒ ∃zs(z,z) (R⇒)
> >
> > http://www.xlog.ch/izytab/doclet/en/docs/18_live/40_bin2021/paste07/package.html

I am afraid, I didn't post the full Barber Paradox. I only posted
what was found in Jens Ottens ex_barber.pl. Now a regret not
providing (<=>)/2 in my leanseq_v5.pl fork. The two sided barber
paradox cannot so concisely be formulate without (<=>)/2.

What would be fun is not only XOR-SAT but also XOR-FOL.
The Jens Otten provers can solve FOL problems among which
we also find FOL problems in prenex normal form Q1x1…QnxnM

where Q1,…,Qn are the alternating quantifier blocks and M is
the FOL matrix. Quantifiers are handled in Jens Otten provers:

Qj=∀: is handled by a Skolem function.
Qj=∃: is handled by fresh variable and contraction.

Besides that all the 3 provers he presents, leanseq_v5.pl,
leantap_pure.pl and leancop_pure.pl do the same with the
FOL matrix M, they put it into conjunctive normal form (CNF),
and try to solve it via unification. Lets take the Barber Paradox

and see how the CNF looks like. The Barber Paradox with (<=>)/2:

¬∃x∀y(¬s(y,y) <=> s(x,y))

The Barber Paradox in prenex with CNF:

∀x∃y((¬s(y,y) | s(x,y)) & (s(y,y) | ¬s(x,y))

When the above is solved unification wise the same thing
happens twice for both conjuncts. But since the XOR-SAT
rewriting prototype has simp(A=A, 1) does this mean we could
solve XOR-FOL differently and for example have a FOL matrix

format where we solve P<=>Q by directly trying to unify P and Q?

Mostowski Collapse schrieb am Montag, 3. Januar 2022 um 00:29:00 UTC+1:
> Oki Doki, full first order logic can be also rendered now:
>
> Leibniz’s Dream in Dogelog Player
> https://twitter.com/dogelogch/status/1477779371628933121
>
> Leibniz’s Dream in Dogelog Player
> https://www.facebook.com/groups/dogelog
> Mostowski Collapse schrieb am Samstag, 1. Januar 2022 um 12:30:25 UTC+1:
> > So how was it done? First one needs to reduce proof noise:
> >
> > Dogelog Player removes proof noise
> > https://twitter.com/dogelogch/status/1477236879795830785
> >
> > Dogelog Player removes proof noise
> > https://www.facebook.com/groups/dogelog
> > Mostowski Collapse schrieb am Freitag, 31. Dezember 2021 um 01:11:37 UTC+1:
> > > Lean TAP can be fun. Spent the whole day to
> > > render MathJax. Then was annoyed by MathJax,
> > > how do you put this thingy into an email?
> > >
> > > So here is barber paradox in list form with Unicode:
> > >
> > > 1. s(a,a) ⊢ s(a,a) (ax)
> > > 2. s(a,a) ⊢ ∃zs(z,z) (R∃)
> > > 3. ⊢ ¬s(a,a), ∃zs(z,z) (R¬)
> > > 4. s(a,a) ⊢ s(a,a) (ax)
> > > 5. s(a,a) ⊢ ∃zs(z,z) (R∃)
> > > 6. ¬s(a,a) ⇒ s(a,a) ⊢ ∃zs(z,z) (L⇒, 3)
> > > 7. ∀y(¬s(y,y) ⇒ s(a,y)) ⊢ ∃zs(z,z) (L∀)
> > > 8. ∃x∀y(¬s(y,y) ⇒ s(x,y)) ⊢ ∃zs(z,z) (L∃)
> > > 9. ⊢ ∃x∀y(¬s(y,y) ⇒ s(x,y)) ⇒ ∃zs(z,z) (R⇒)
> > >
> > > http://www.xlog.ch/izytab/doclet/en/docs/18_live/40_bin2021/paste07/package.html

Nice! Now the example runs also from within Python. Even
on ordinary CMD on Windows 10. Just use for example this
font *NSimSum*, select it in the console properties.

See also:

Unicode Proof Listing in Dogelog Player
https://twitter.com/dogelogch/status/1478315286491287553

Unicode Proof Listing in Dogelog Player
https://www.facebook.com/groups/dogelog

But I have to simplify the Python Dogelog Player console.
Now the Python Dogelog Player console is a tutorial example,
but dogelog.py should do it by default.

Please be patient.

Mostowski Collapse schrieb am Dienstag, 4. Januar 2022 um 11:49:53 UTC+1:
> I am afraid, I didn't post the full Barber Paradox. I only posted
> what was found in Jens Ottens ex_barber.pl. Now a regret not
> providing (<=>)/2 in my leanseq_v5.pl fork. The two sided barber
> paradox cannot so concisely be formulate without (<=>)/2.
>
> What would be fun is not only XOR-SAT but also XOR-FOL.
> The Jens Otten provers can solve FOL problems among which
> we also find FOL problems in prenex normal form Q1x1…QnxnM
>
> where Q1,…,Qn are the alternating quantifier blocks and M is
> the FOL matrix. Quantifiers are handled in Jens Otten provers:
>
> Qj=∀: is handled by a Skolem function.
> Qj=∃: is handled by fresh variable and contraction.
>
> Besides that all the 3 provers he presents, leanseq_v5.pl,
> leantap_pure.pl and leancop_pure.pl do the same with the
> FOL matrix M, they put it into conjunctive normal form (CNF),
> and try to solve it via unification. Lets take the Barber Paradox
>
> and see how the CNF looks like. The Barber Paradox with (<=>)/2:
>
> ¬∃x∀y(¬s(y,y) <=> s(x,y))
>
> The Barber Paradox in prenex with CNF:
>
> ∀x∃y((¬s(y,y) | s(x,y)) & (s(y,y) | ¬s(x,y))
>
> When the above is solved unification wise the same thing
> happens twice for both conjuncts. But since the XOR-SAT
> rewriting prototype has simp(A=A, 1) does this mean we could
> solve XOR-FOL differently and for example have a FOL matrix
>
> format where we solve P<=>Q by directly trying to unify P and Q?
> Mostowski Collapse schrieb am Montag, 3. Januar 2022 um 00:29:00 UTC+1:
> > Oki Doki, full first order logic can be also rendered now:
> >
> > Leibniz’s Dream in Dogelog Player
> > https://twitter.com/dogelogch/status/1477779371628933121
> >
> > Leibniz’s Dream in Dogelog Player
> > https://www.facebook.com/groups/dogelog
> > Mostowski Collapse schrieb am Samstag, 1. Januar 2022 um 12:30:25 UTC+1:
> > > So how was it done? First one needs to reduce proof noise:
> > >
> > > Dogelog Player removes proof noise
> > > https://twitter.com/dogelogch/status/1477236879795830785
> > >
> > > Dogelog Player removes proof noise
> > > https://www.facebook.com/groups/dogelog
> > > Mostowski Collapse schrieb am Freitag, 31. Dezember 2021 um 01:11:37 UTC+1:
> > > > Lean TAP can be fun. Spent the whole day to
> > > > render MathJax. Then was annoyed by MathJax,
> > > > how do you put this thingy into an email?
> > > >
> > > > So here is barber paradox in list form with Unicode:
> > > >
> > > > 1. s(a,a) ⊢ s(a,a) (ax)
> > > > 2. s(a,a) ⊢ ∃zs(z,z) (R∃)
> > > > 3. ⊢ ¬s(a,a), ∃zs(z,z) (R¬)
> > > > 4. s(a,a) ⊢ s(a,a) (ax)
> > > > 5. s(a,a) ⊢ ∃zs(z,z) (R∃)
> > > > 6. ¬s(a,a) ⇒ s(a,a) ⊢ ∃zs(z,z) (L⇒, 3)
> > > > 7. ∀y(¬s(y,y) ⇒ s(a,y)) ⊢ ∃zs(z,z) (L∀)
> > > > 8. ∃x∀y(¬s(y,y) ⇒ s(x,y)) ⊢ ∃zs(z,z) (L∃)
> > > > 9. ⊢ ∃x∀y(¬s(y,y) ⇒ s(x,y)) ⇒ ∃zs(z,z) (R⇒)
> > > >
> > > > http://www.xlog.ch/izytab/doclet/en/docs/18_live/40_bin2021/paste07/package.html

Holy cow, the monke army is in full bloom, now
#Python trending on Twitter!!! So “Digital Twin”
is the new name for software agent?

https://towardsdatascience.com/digital-twin-with-python-a-hands-on-example-2a3036124b61

Mostowski Collapse schrieb am Dienstag, 4. Januar 2022 um 12:28:22 UTC+1:
> Nice! Now the example runs also from within Python. Even
> on ordinary CMD on Windows 10. Just use for example this
> font *NSimSum*, select it in the console properties.
>
> See also:
>
> Unicode Proof Listing in Dogelog Player
> https://twitter.com/dogelogch/status/1478315286491287553
>
> Unicode Proof Listing in Dogelog Player
> https://www.facebook.com/groups/dogelog
>
> But I have to simplify the Python Dogelog Player console.
> Now the Python Dogelog Player console is a tutorial example,
> but dogelog.py should do it by default.
>
> Please be patient.
> Mostowski Collapse schrieb am Dienstag, 4. Januar 2022 um 11:49:53 UTC+1:
> > I am afraid, I didn't post the full Barber Paradox. I only posted
> > what was found in Jens Ottens ex_barber.pl. Now a regret not
> > providing (<=>)/2 in my leanseq_v5.pl fork. The two sided barber
> > paradox cannot so concisely be formulate without (<=>)/2.
> >
> > What would be fun is not only XOR-SAT but also XOR-FOL.
> > The Jens Otten provers can solve FOL problems among which
> > we also find FOL problems in prenex normal form Q1x1…QnxnM
> >
> > where Q1,…,Qn are the alternating quantifier blocks and M is
> > the FOL matrix. Quantifiers are handled in Jens Otten provers:
> >
> > Qj=∀: is handled by a Skolem function.
> > Qj=∃: is handled by fresh variable and contraction.
> >
> > Besides that all the 3 provers he presents, leanseq_v5.pl,
> > leantap_pure.pl and leancop_pure.pl do the same with the
> > FOL matrix M, they put it into conjunctive normal form (CNF),
> > and try to solve it via unification. Lets take the Barber Paradox
> >
> > and see how the CNF looks like. The Barber Paradox with (<=>)/2:
> >
> > ¬∃x∀y(¬s(y,y) <=> s(x,y))
> >
> > The Barber Paradox in prenex with CNF:
> >
> > ∀x∃y((¬s(y,y) | s(x,y)) & (s(y,y) | ¬s(x,y))
> >
> > When the above is solved unification wise the same thing
> > happens twice for both conjuncts. But since the XOR-SAT
> > rewriting prototype has simp(A=A, 1) does this mean we could
> > solve XOR-FOL differently and for example have a FOL matrix
> >
> > format where we solve P<=>Q by directly trying to unify P and Q?
> > Mostowski Collapse schrieb am Montag, 3. Januar 2022 um 00:29:00 UTC+1:
> > > Oki Doki, full first order logic can be also rendered now:
> > >
> > > Leibniz’s Dream in Dogelog Player
> > > https://twitter.com/dogelogch/status/1477779371628933121
> > >
> > > Leibniz’s Dream in Dogelog Player
> > > https://www.facebook.com/groups/dogelog
> > > Mostowski Collapse schrieb am Samstag, 1. Januar 2022 um 12:30:25 UTC+1:
> > > > So how was it done? First one needs to reduce proof noise:
> > > >
> > > > Dogelog Player removes proof noise
> > > > https://twitter.com/dogelogch/status/1477236879795830785
> > > >
> > > > Dogelog Player removes proof noise
> > > > https://www.facebook.com/groups/dogelog
> > > > Mostowski Collapse schrieb am Freitag, 31. Dezember 2021 um 01:11:37 UTC+1:
> > > > > Lean TAP can be fun. Spent the whole day to
> > > > > render MathJax. Then was annoyed by MathJax,
> > > > > how do you put this thingy into an email?
> > > > >
> > > > > So here is barber paradox in list form with Unicode:
> > > > >
> > > > > 1. s(a,a) ⊢ s(a,a) (ax)
> > > > > 2. s(a,a) ⊢ ∃zs(z,z) (R∃)
> > > > > 3. ⊢ ¬s(a,a), ∃zs(z,z) (R¬)
> > > > > 4. s(a,a) ⊢ s(a,a) (ax)
> > > > > 5. s(a,a) ⊢ ∃zs(z,z) (R∃)
> > > > > 6. ¬s(a,a) ⇒ s(a,a) ⊢ ∃zs(z,z) (L⇒, 3)
> > > > > 7. ∀y(¬s(y,y) ⇒ s(a,y)) ⊢ ∃zs(z,z) (L∀)
> > > > > 8. ∃x∀y(¬s(y,y) ⇒ s(x,y)) ⊢ ∃zs(z,z) (L∃)
> > > > > 9. ⊢ ∃x∀y(¬s(y,y) ⇒ s(x,y)) ⇒ ∃zs(z,z) (R⇒)
> > > > >
> > > > > http://www.xlog.ch/izytab/doclet/en/docs/18_live/40_bin2021/paste07/package.html

Now having more fun with Jens Ottens Lean Prover. This
is a nice little example, where 1 contraction doesn’t work,
but 2 contractions work:

?- prove0(?[X='x']:![Y='y']:(p(X) | ~p(Y)), 1), !.
fail.
?- prove0(?[X='x']:![Y='y']:(p(X) | ~p(Y)), 2), !.
true.

See also:

Maslovs Method in Dogelog Player
https://twitter.com/dogelogch/status/1479792480908414979

Maslovs Method in Dogelog Player
https://www.facebook.com/groups/dogelog

The problem with the French logician is, that he does not
get through the thicket of classical logic into the Maslovs method.
He only shows a translation for intuitionstic logic in the following form:

(∃xA)* := ∃x !A
https://girard.perso.math.cnrs.fr/Synsem.pdf

Given his other definitions for other connectives and quantifiers
it might work. In his “Table 2: Classical connectives : definition in
terms of linear logic” he then repeats this translation.

I think his translation works since he has exponentation
elsewhere outside of the quantifier. But the Maslov method shows
that the outside exponentation in classical connectives is

superflous, and that we can put the exponentiation in front
of a certain quantifier.

Mostowski Collapse schrieb am Samstag, 8. Januar 2022 um 14:06:42 UTC+1:
> Now having more fun with Jens Ottens Lean Prover. This
> is a nice little example, where 1 contraction doesn’t work,
> but 2 contractions work:
>
> ?- prove0(?[X='x']:![Y='y']:(p(X) | ~p(Y)), 1), !.
> fail.
> ?- prove0(?[X='x']:![Y='y']:(p(X) | ~p(Y)), 2), !.
> true.
>
> See also:
>
> Maslovs Method in Dogelog Player
> https://twitter.com/dogelogch/status/1479792480908414979
>
> Maslovs Method in Dogelog Player
> https://www.facebook.com/groups/dogelog

One more iteration of our prover:

Proof systems that are based on the Howard-Curry isomorphism
and that extract proof terms in the lambda calculus are familiar
to node dropping. Lambda calculus expressions have a notion
of variable occurence.

/* Eta Reduction */
λx(Mx) ~~> M for x ∉ M

Variable occurence can then be used similarly to has_usage/2
to shorten proof terms in the form of lambda expressions. A
prominent reduction rule is seen in the above that goes by
the name eta reduction.

Our provers do extract terms where we store integer sequent
indexes of used formulas. For the newest variant we generalized
the terms to alfa, beta, gamma and delta, but we currently do
not use a generic binder format.

See also:

Node Dropping for Maslovs Method
https://twitter.com/dogelogch/status/1480091985222451201

Node Dropping for Maslovs Method
https://www.facebook.com/groups/dogelog

Mostowski Collapse schrieb am Samstag, 8. Januar 2022 um 16:57:45 UTC+1:
> The problem with the French logician is, that he does not
> get through the thicket of classical logic into the Maslovs method.
> He only shows a translation for intuitionstic logic in the following form:
>
> (∃xA)* := ∃x !A
> https://girard.perso.math.cnrs.fr/Synsem.pdf
>
> Given his other definitions for other connectives and quantifiers
> it might work. In his “Table 2: Classical connectives : definition in
> terms of linear logic” he then repeats this translation.
>
> I think his translation works since he has exponentation
> elsewhere outside of the quantifier. But the Maslov method shows
> that the outside exponentation in classical connectives is
>
> superflous, and that we can put the exponentiation in front
> of a certain quantifier.
> Mostowski Collapse schrieb am Samstag, 8. Januar 2022 um 14:06:42 UTC+1:
> > Now having more fun with Jens Ottens Lean Prover. This
> > is a nice little example, where 1 contraction doesn’t work,
> > but 2 contractions work:
> >
> > ?- prove0(?[X='x']:![Y='y']:(p(X) | ~p(Y)), 1), !.
> > fail.
> > ?- prove0(?[X='x']:![Y='y']:(p(X) | ~p(Y)), 2), !.
> > true.
> >
> > See also:
> >
> > Maslovs Method in Dogelog Player
> > https://twitter.com/dogelogch/status/1479792480908414979
> >
> > Maslovs Method in Dogelog Player
> > https://www.facebook.com/groups/dogelog

Somehow being less obsessed with Curry-Howard isomorphism
pays off. Everything is Prolog terms, and maybe some of its
arguments are integers. So what? Proofs are anyway finitistic.

I wonder what happens if I would do some meta logic and
strip myself from lambda calculus translations, going without
logical frameworks or higher-order abstract syntax.

Making also ideas of λ-Prolog obsolete. Hm..

Mostowski Collapse schrieb am Sonntag, 9. Januar 2022 um 09:30:13 UTC+1:
> One more iteration of our prover:
>
> Proof systems that are based on the Howard-Curry isomorphism
> and that extract proof terms in the lambda calculus are familiar
> to node dropping. Lambda calculus expressions have a notion
> of variable occurence.
>
> /* Eta Reduction */
> λx(Mx) ~~> M for x ∉ M
>
> Variable occurence can then be used similarly to has_usage/2
> to shorten proof terms in the form of lambda expressions. A
> prominent reduction rule is seen in the above that goes by
> the name eta reduction.
>
> Our provers do extract terms where we store integer sequent
> indexes of used formulas. For the newest variant we generalized
> the terms to alfa, beta, gamma and delta, but we currently do
> not use a generic binder format.
>
> See also:
>
> Node Dropping for Maslovs Method
> https://twitter.com/dogelogch/status/1480091985222451201
>
> Node Dropping for Maslovs Method
> https://www.facebook.com/groups/dogelog
> Mostowski Collapse schrieb am Samstag, 8. Januar 2022 um 16:57:45 UTC+1:
> > The problem with the French logician is, that he does not
> > get through the thicket of classical logic into the Maslovs method.
> > He only shows a translation for intuitionstic logic in the following form:
> >
> > (∃xA)* := ∃x !A
> > https://girard.perso.math.cnrs.fr/Synsem.pdf
> >
> > Given his other definitions for other connectives and quantifiers
> > it might work. In his “Table 2: Classical connectives : definition in
> > terms of linear logic” he then repeats this translation.
> >
> > I think his translation works since he has exponentation
> > elsewhere outside of the quantifier. But the Maslov method shows
> > that the outside exponentation in classical connectives is
> >
> > superflous, and that we can put the exponentiation in front
> > of a certain quantifier.
> > Mostowski Collapse schrieb am Samstag, 8. Januar 2022 um 14:06:42 UTC+1:
> > > Now having more fun with Jens Ottens Lean Prover. This
> > > is a nice little example, where 1 contraction doesn’t work,
> > > but 2 contractions work:
> > >
> > > ?- prove0(?[X='x']:![Y='y']:(p(X) | ~p(Y)), 1), !.
> > > fail.
> > > ?- prove0(?[X='x']:![Y='y']:(p(X) | ~p(Y)), 2), !.
> > > true.
> > >
> > > See also:
> > >
> > > Maslovs Method in Dogelog Player
> > > https://twitter.com/dogelogch/status/1479792480908414979
> > >
> > > Maslovs Method in Dogelog Player
> > > https://www.facebook.com/groups/dogelog

Some papers show calculi with two substitution rules
where the equation appears as ~(s=t) and flipped
as ~(t=s). Strange in our take we dont need this,

only flipped polarity of atomic formulas, this
is provable with a=b in it:

1. a = b ∧ p(a) ⇒ p(b)
2. p(b) (T⇒2 1)
3. ¬(a = b ∧ p(a)) (T⇒1 1)
4. ¬p(a) (F∧2 3)
5. ¬a = b (F∧1 3)
6. ¬p(b) (F= 5, 4)
✓ (ax 6, 2)

And now with flipped b=a, it works as well:

1. b = a ∧ p(a) ⇒ p(b)
2. p(b) (T⇒2 1)
3. ¬(b = a ∧ p(a)) (T⇒1 1)
4. ¬p(a) (F∧2 3)
5. ¬b = a (F∧1 3)
6. p(a) (F= 5, 2)
✓ (ax 4, 6)

See also:

First-Order Equality for Maslovs Method
https://twitter.com/dogelogch/status/1482885333486379015

First-Order Equality for Maslovs Method
https://www.facebook.com/groups/dogelog

I did the barber paradox always wrong!
The biconditional makes it so much easier.

1. ¬∃y ∀x (s(x, y) ⇔ ¬s(x, x))
2. ¬∀x (s(x, a) ⇔ ¬s(x, x)) (F∃ 1)
3. ¬(s(a, a) ⇔ ¬s(a, a)) (F∀ 2)
4. ¬(s(a, a) ∧ ¬s(a, a)) (F⇔1 3)
5. ¬¬s(a, a) (F∧2 4)
6. ¬s(a, a) (F∧1 4)
7. s(a, a) (F¬ 5)
✓ (ax 6, 7)
4. s(a, a) ∨ ¬s(a, a) (F⇔2 3)
5. ¬s(a, a) (T∨2 4)
6. s(a, a) (T∨1 4)
✓ (ax 5, 6)

See also:

Biconditional Support for Maslovs Method
https://twitter.com/dogelogch/status/1483455561031106563

Biconditional Support for Maslovs Method
https://www.facebook.com/groups/dogelog