From jkominek@miranda.org Mon Aug 23 14:40:10 2004 Received: with ECARTIS (v1.0.0; list lojban-beginners); Mon, 23 Aug 2004 14:40:10 -0700 (PDT) Received: from miranda.org ([209.58.150.153] ident=qmailr) by chain.digitalkingdom.org with smtp (Exim 4.34) id 1BzMXy-0003NX-AK for lojban-beginners@chain.digitalkingdom.org; Mon, 23 Aug 2004 14:40:10 -0700 Received: (qmail 30472 invoked by uid 534); 23 Aug 2004 21:40:10 -0000 From: jkominek@miranda.org Date: Mon, 23 Aug 2004 15:40:10 -0600 To: lojban-beginners@chain.digitalkingdom.org Subject: [lojban-beginners] Re: logical proofs? Message-ID: <20040823214010.GF14716@miranda.org> References: <1093232310.412966b640996@www.gulik.co.nz> <20040823041958.GD3257@chain.digitalkingdom.org> <20040823031849.A32026@fresco.Math.McGill.CA> <20040823153053.GI3257@chain.digitalkingdom.org> <1093296583.412a61c7e09ce@www.gulik.co.nz> Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline In-Reply-To: <1093296583.412a61c7e09ce@www.gulik.co.nz> Accept-Language: jbo, en User-Agent: Mutt/1.5.6i X-archive-position: 728 X-Approved-By: jkominek@miranda.org X-ecartis-version: Ecartis v1.0.0 Sender: lojban-beginners-bounce@chain.digitalkingdom.org Errors-to: lojban-beginners-bounce@chain.digitalkingdom.org X-original-sender: jkominek@miranda.org Precedence: bulk Reply-to: lojban-beginners@chain.digitalkingdom.org X-list: lojban-beginners On Tue, Aug 24, 2004 at 09:29:43AM +1200, mikevdg@gulik.co.nz wrote: > What I'm interested in is whether it is possible that this could be > mechanically derived, for example by somebody using a proof > assistant such as COQ, but using lojban? I.e are all the steps in > the proof mechanical enough to convince a computer that (e.g.) prime > numbers are infinite? I'll have to admit that I didn't even try reading the proof, but, one could certainly restrain themselves to some sort of ritualized subset of Lojban which was analagous to the syntax used by MetaMath (http://metamath.org). At that point, the proofs could be mechanically verified, manipulated, etc, just as the MetaMath ones are. Short of that, mechanically understanding proofs is probably a bit too inherently difficult. -- Jay Kominek UNIX is all about covering up the fact that you can't type.