From mikevdg@gulik.co.nz Sun Aug 22 20:36:57 2004
Received: with ECARTIS (v1.0.0; list lojban-beginners); Sun, 22 Aug 2004 21:03:12 -0700 (PDT)
Received: from genamics.blastula.net ([205.214.85.184])
	by chain.digitalkingdom.org with esmtp (TLS-1.0:DHE_RSA_3DES_EDE_CBC_SHA:24)
	(Exim 4.34)
	id 1Bz5dh-00048W-1I
	for lojban-beginners@lojban.org; Sun, 22 Aug 2004 20:36:57 -0700
Received: from cpanel by genamics.blastula.net with local (Exim 4.34)
	id 1Bz5fC-0007HK-9R
	for lojban-beginners@lojban.org; Mon, 23 Aug 2004 15:38:30 +1200
Received: from localhost (localhost [127.0.0.1]) 
	by www.gulik.co.nz (IMP) with HTTP 
	for <mikevdg@localhost>; Mon, 23 Aug 2004 15:38:30 +1200
Message-ID: <1093232310.412966b640996@www.gulik.co.nz>
Date: Mon, 23 Aug 2004 15:38:30 +1200
From: mikevdg@gulik.co.nz
To: lojban-beginners@lojban.org
Subject: [lojban-beginners] logical proofs?
MIME-Version: 1.0
Content-Type: text/plain; charset=ISO-8859-1
User-Agent: Internet Messaging Program (IMP) 3.2.2
X-Originating-IP: 127.0.0.1
X-MailScanner-Information: Please contact the ISP for more information
X-MailScanner: Found to be clean
X-AntiAbuse: This header was added to track abuse, please include it with any abuse report
X-AntiAbuse: Primary Hostname - genamics.blastula.net
X-AntiAbuse: Original Domain - lojban.org
X-AntiAbuse: Originator/Caller UID/GID - [32001 32001] / [47 12]
X-AntiAbuse: Sender Address Domain - gulik.co.nz
X-Source: 
X-Source-Args: 
X-Source-Dir: 
X-archive-position: 716
X-Approved-By: rlpowell@digitalkingdom.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: mikevdg@gulik.co.nz
Precedence: bulk
Reply-to: lojban-beginners@chain.digitalkingdom.org
X-list: lojban-beginners

Hi all.

I'm a programmer in Auckland, New Zealand. I have a question about lojban, and
I'm hoping that this list is the best place to ask stupid questions :-).

Is it possible to do logical proofs in lojban? When I learned logic at uni
(which, btw, is a course I only just passed...), we learned that there were
proofs by contradiction, direct proofs and some other form of proof that I've
completely forgotten about.

Anyway, the idea was that a proof is a set of nested mini-proofs. For example, a
proof by contradiction would be something like:

Assume A
    do some stuff here.
    discover "A and not A".
    aha! This mini-world can't exist!
Therefore, "not A".

...or something like that. This was a few years ago and I'm really rusty. The
proof would be a very nice looking paper filled with lots of ^, v, ->, inverted
A's and reversed E's.

The reason I'm asking is because, so far, I've seen no sign of language
constructs to create a proof other than the very basic logical connectives (and,
or, not, therefore) (disclaimer: I've only known lojban for a few days). Also,
I couldn't find "proof", "prove", "proves", "theory", "axiom", "contradiction",
"implication" or "statement" (jufra? found only when looking up "sentence") in
the jbovlaste dictionary. I'm certain there are probably other ways of talking
about these concepts in lojban.

Michael.