Path: ...!news.mixmin.net!weretis.net!feeder8.news.weretis.net!reader5.news.weretis.net!news.solani.org!.POSTED!not-for-mail
From: Mild Shock <janburse@fastmail.fm>
Newsgroups: sci.logic
Subject: Re: How to prove this theorem with intuitionistic natural deduction?
Date: Mon, 18 Nov 2024 23:22:11 +0100
Message-ID: <vhgemi$ca9e$1@solani.org>
References: <vhgdq0$19evr$1@dont-email.me>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Mon, 18 Nov 2024 22:22:10 -0000 (UTC)
Injection-Info: solani.org;
	logging-data="403758"; mail-complaints-to="abuse@news.solani.org"
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:91.0) Gecko/20100101
 Firefox/91.0 SeaMonkey/2.53.19
Cancel-Lock: sha1:l+iApJgYDrjkutLF7JvPdIeWeKs=
In-Reply-To: <vhgdq0$19evr$1@dont-email.me>
X-User-ID: eJwNyMkNwEAIBLCWWHGXAwP0X0Lys6xsz+BiaqKnR9flyc43lPKCwjttem2QkPtdHlvoRzq7xwChCJ3xT35ojxZd
Bytes: 1487
Lines: 20


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