Dear logicians,

How to prove the following theorem with natural deduction in
intuitionistic propositional logic (namely, no classical inference rules)?

`(P -> Q -> R) |- (P /\ Q -> R)`

Thanks for any help.

-Julio

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

0: P -> (Q -> R) (Premisse)
1: P /\ Q (Assumption)
2: P (/\E,1)
3: Q -> R (->E,0,2)
4: Q (/\E,1)
5: R (->E,3,4)
6: P /\ Q -> R (Discharge,1)

Julio Di Egidio schrieb:

Dear logicians,

How to prove the following theorem with natural deduction in
intuitionistic propositional logic (namely, no classical inference rules)?

  `(P -> Q -> R) |- (P /\ Q -> R)`

Thanks for any help.

-Julio

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

On 18/11/2024 23:22, Mild Shock wrote:

Julio Di Egidio schrieb:

`(P -> Q -> R) |- (P /\ Q -> R)`

0: P -> (Q -> R) (Premisse)
1: P /\ Q        (Assumption)
2: P             (/\E,1)
3: Q -> R        (->E,0,2)
4: Q             (/\E,1)
5: R             (->E,3,4)
6: P /\ Q -> R   (Discharge,1)

Wonderful, thank you.

-Julio

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

Hi,

Can λ-prolog do it? The proof is a little bit
tricky, since line 1 is used twice in
line 2 and in line 4. So its not a proof

tree, rather a proof mesh (*). What would λ-prolog
give via curry howard? If we would use something
along these lines:

https://en.wikipedia.org/wiki/%CE%9BProlog#Programming_in_%CE%BBProlog

The proof search is loosely from the book
figure 9.6 Programming in Higher-Order Logic
from Miler and Nadathur.

Bye

(*) Displayed in Fitch Style.

Julio Di Egidio schrieb:

On 18/11/2024 23:22, Mild Shock wrote:

Julio Di Egidio schrieb:

`(P -> Q -> R) |- (P /\ Q -> R)`

0: P -> (Q -> R) (Premisse)
1: P /\ Q        (Assumption)
2: P             (/\E,1)
3: Q -> R        (->E,0,2)
4: Q             (/\E,1)
5: R             (->E,3,4)
6: P /\ Q -> R   (Discharge,1)

Wonderful, thank you.

-Julio

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

Hi,

Meanwhile, you might have seen it, I have also asked on SE:

<https://proofassistants.stackexchange.com/questions/4455/negative-translation-for-linear-propositional-logic>

Sorry, but I must quite. Anything where Andrej Bauer is
a red flag. I remember he was censoring some post of mine,
don't remember exactly where it was.

You can try searching here:

https://groups.google.com/g/sci.logic/search?q=Andrej%20Bauer%20


Julio Di Egidio schrieb:

Dear logicians,

How to prove the following theorem with natural deduction in
intuitionistic propositional logic (namely, no classical inference rules)?

  `(P -> Q -> R) |- (P /\ Q -> R)`

Thanks for any help.

-Julio

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

Yeah, they impose a "level" on questions:

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.

Very problematic behaviour!

Mostowski Collapse - 29.11.2021, 00:19:03 https://groups.google.com/g/sci.logic/c/12DNbf3QI5I/m/V_Yal3wBBgAJ

Mild Shock schrieb:

Hi,

Meanwhile, you might have seen it, I have also asked on SE:

<https://proofassistants.stackexchange.com/questions/4455/negative-translation-for-linear-propositional-logic>

Sorry, but I must quite. Anything where Andrej Bauer is
a red flag. I remember he was censoring some post of mine,
don't remember exactly where it was.

You can try searching here:

https://groups.google.com/g/sci.logic/search?q=Andrej%20Bauer%20

Julio Di Egidio schrieb:

Dear logicians,

How to prove the following theorem with natural deduction in
intuitionistic propositional logic (namely, no classical inference
rules)?

   `(P -> Q -> R) |- (P /\ Q -> R)`

Thanks for any help.

-Julio

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

On 01/12/2024 11:56, Mild Shock wrote:

Hi,

Meanwhile, you might have seen it, I have also asked on SE:

<https://proofassistants.stackexchange.com/questions/4455/negative-translation-for-linear-propositional-logic>

Sorry, but I must quite. Anything where Andrej Bauer is
a red flag. I remember he was censoring some post of mine,
don't remember exactly where it was.

Don't make it personal, a third of the world population is nazi-retarded
by now: the incivilization and involution is just like the Huns, not
even grass grows anymore.

It's a fucking shame for humanity: but there just seems to be no bottom
to it, it's like those rats on the boat, killing and shitting on all intelligence and decency to begin with.

"Progress" is watch these nazi-retards play WW3, get some popcorn...


-Julio

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

Its extremly personal, because SO and other
systems establish para-governemental prisons,
and mostly the reason is a form

of agile processes, agil forms of website
development, including the many "business rules"
that are involved in SO,

thats a very dangerous form of creating such
things, since it might violate existing law
which also applies to the digital.

P.S.: In a normal IT setting you have
subject matter experts that define "business
rules", such mechanisms should be a playground

for infantile developers with a mindset of a 5 year old.

Julio Di Egidio schrieb:

On 01/12/2024 11:56, Mild Shock wrote:

Hi,

Meanwhile, you might have seen it, I have also asked on SE:
;

<https://proofassistants.stackexchange.com/questions/4455/negative-translation-for-linear-propositional-logic>


Sorry, but I must quite. Anything where Andrej Bauer is
a red flag. I remember he was censoring some post of mine,
don't remember exactly where it was.

Don't make it personal, a third of the world population is nazi-retarded
by now: the incivilization and involution is just  like the Huns, not
even grass grows anymore.

It's a fucking shame for humanity: but there just seems to be no bottom
to it, it's like those rats on the boat, killing and shitting on all intelligence and decency to begin with.

"Progress" is watch these nazi-retards play WW3, get some popcorn...

-Julio

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

One problem I generally see is, that most people
are not aware, that an employee has no rights
on the stuff he writes for his employer.

Standard Rules:
- Work for Hire Doctrine: In most jurisdictions, code
written by an employee within the scope of their employment is
considered a "work for hire," meaning the employer owns
the intellectual property (IP) unless otherwise agreed in writing.
- Employment Contracts: Most employment agreements
explicitly state that any code, inventions, or intellectual
property created as part of your job belongs to the employer.
- Use of Employer Resources: If an employee uses the
employer’s time, tools, or resources to create code, the employer
generally owns the resulting work.

Exceptions:
- Independent Work: If an employee writes code outside
working hours, without using company resources, and it’s
unrelated to their job, they may retain rights. Some
jurisdictions, like California, have laws (e.g., California Labor Code
§2870) protecting employees in such cases.
- Negotiated Agreements: If the employee has a specific
agreement (e.g., consulting or freelance arrangements),
ownership terms might differ.

So like 90% of the stackoverflow users cannot
go into an agreement individually, since they are
employed, with stackoverflow in that they would be
able to give a license to what they write.


Mild Shock schrieb:

Mild Shock schrieb:

such mechanisms should be a playground
for infantile developers with a mindset of a 5 year old.

Corr.:

such mechanisms should not be a playground
for infantile developers with a mindset of a 5 year old.

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

It could be that among the exceptions is
also certain academic work. So maybe
there are different rules for CSTHEORY,

that for SO. Which has different audience.
But especially SO is problematic, since
it adresses "developers", they start their site with:

"Every developer has a
tab open to Stack Overflow."
For over 15 years we’ve been the Q&A platform
of choice that millions of people visit every
month to ask questions, learn, and
share technical knowledge.
https://stackoverflow.com/

So what is really "muddled" is thery IP
theft. Although they offer stack overflow
for teams. But maybe there is another solution

to the dilemma, something inbetween and more
fluid. Like GitHub, where you easily switch back
and forth a repository from private to non-private.

It is probably part and parcel of their marketing
stategiy that they make it most difficult to get
control over your own IP. So as to move you into

stackoverflow for teams. Which is of course a
moronic idea that this would work. There are
quite a couple of alternatives around,

Scryer Prolog uses GitHub discussions. But GitHub
can be also extremly Nazi.

Mild Shock schrieb:

One problem I generally see is, that most people
are not aware, that an employee has no rights
on the stuff he writes for his employer.

Standard Rules:
- Work for Hire Doctrine: In most jurisdictions, code
written by an employee within the scope of their employment is
considered a "work for hire," meaning the employer owns
the intellectual property (IP) unless otherwise agreed in writing.
- Employment Contracts: Most employment agreements
explicitly state that any code, inventions, or intellectual
property created as part of your job belongs to the employer.
- Use of Employer Resources: If an employee uses the
employer’s time, tools, or resources to create code, the employer
generally owns the resulting work.

Exceptions:
- Independent Work: If an employee writes code outside
working hours, without using company resources, and it’s
unrelated to their job, they may retain rights. Some
jurisdictions, like California, have laws (e.g., California Labor Code §2870) protecting employees in such cases.
- Negotiated Agreements: If the employee has a specific
agreement (e.g., consulting or freelance arrangements),
ownership terms might differ.

So like 90% of the stackoverflow users cannot
go into an agreement individually, since they are
employed, with stackoverflow in that they would be
able to give a license to what they write.

Mild Shock schrieb:

Mild Shock schrieb:

such mechanisms should be a playground
for infantile developers with a mindset of a 5 year old.

Corr.:

such mechanisms should not be a playground
for infantile developers with a mindset of a 5 year old.

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

Mild Shock schrieb:

such mechanisms should be a playground
for infantile developers with a mindset of a 5 year old.

Corr.:

such mechanisms should not be a playground
for infantile developers with a mindset of a 5 year old.

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