From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00
	autolearn=unavailable autolearn_force=no version=3.4.4
Path: 
 border1.nntp.ams3.giganews.com!border1.nntp.ams2.giganews.com!border3.nntp.ams.giganews.com!border1.nntp.ams.giganews.com!nntp.giganews.com!news.mixmin.net!feeder.erje.net!eu.feeder.erje.net!eweka.nl!lightspeed.eweka.nl!193.141.40.65.MISMATCH!npeer.de.kpn-eurorings.net!npeer-ng0.de.kpn-eurorings.net!newsfeed.arcor.de!newsspool3.arcor-online.net!news.arcor.de.POSTED!not-for-mail
Date: Wed, 10 Jul 2013 10:21:29 +0200
From: Georg Bauhaus <rm.dash-bauhaus@futureapps.de>
User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.7;
 rv:17.0) Gecko/20130620 Thunderbird/17.0.7
MIME-Version: 1.0
Newsgroups: comp.lang.ada
Subject: Re: The future of Spark . Spark 2014 : a wreckage
References: <d84b2eb2-eab3-4dec-917c-0498473c1e93@googlegroups.com>
 <87hag4ahu5.fsf@mid.deneb.enyo.de>
 <1rbbala6i0jcl$.dswyfcctu6vs$.dlg@40tude.net>
 <wcc7ggztkhz.fsf@shell01.TheWorld.com>
 <grcdle1q7kkw$.m5t82cn92atl.dlg@40tude.net>
In-Reply-To: <grcdle1q7kkw$.m5t82cn92atl.dlg@40tude.net>
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 7bit
Message-ID: <51dd1988$0$6579$9b4e6d93@newsspool3.arcor-online.net>
Organization: Arcor
NNTP-Posting-Date: 10 Jul 2013 10:21:28 CEST
NNTP-Posting-Host: 21fe106f.newsspool3.arcor-online.net
X-Trace: DXC=\]2; 5mO\; G<i6K; >iZ]763McF=Q^Z^V384Fo<]lROoR18kF<OcfhCO;
 FK5>jeYMIE?PCY\c7>ejV8EJ0JIOO5>F21=]g9>2Do3<
X-Complaints-To: usenet-abuse@arcor.de
X-Original-Bytes: 2581
Xref: number.nntp.dca.giganews.com comp.lang.ada:182421
Date: 2013-07-10T10:21:28+02:00
List-Id: <comp.lang.ada>

On 10.07.13 09:49, Dmitry A. Kazakov wrote:
> On Tue, 09 Jul 2013 18:51:36 -0400, Robert A Duff wrote:

>>> ...because logical implication (not P or Q) must be
>>> denoted as P => Q.
>>
>> It must be?
>
> Yes, if logical implication is indeed meant here, of which I am not sure.
>
>> In Eiffel, it is denoted by the "implies" keyword.
>> In Ada 2012, one writes "(if P then Q)", which is shorthand for
>> "(if P then Q else True)".
>
> But this is not an implication (Boolean operation). It is a rule based on
> implication. E.g. Modus ponens:
>
> P, P=>Q
> ------------
> Q
>
> So "implies" and "if-then" are correct, while P->Q looks wrong even when
> spelled correctly as P=>Q.
>
> If there should be a symbol, I think,
>
>     P |= Q  or P |- Q
>
> would be more appropriate.

Appropriate even though semantic and syntactic entailment resp.
are not usually considered part of the language governing P and Q?

Wouldn't we rather be writing computable expressions and
feed them to mechanical testing of satisfiability? (Which
means, right now, we have just formulae, but not any language
for speaking about arguments or about consistent sets.)

What's your plan?