Re: The future of Spark . Spark 2014 : a wreckage

[Georg Bauhaus <rm.dash-bauhaus@futureapps.de>]

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?