hello and mathspad

[rustompmody]

Hello folks! Good to be here!

My immediate question -- hopefully not too off-topic, guessing that Roland Backhouse is part of the culture of this group:

I tried to compile mathspad. It kind of compiled (lots of warnings).  However it does not seem to run.

My understanding of mathspad is that -- at least in 1990 -- it was an attempt at using the computer to make
calculational math and reasoning more easy.

So what do folks in the Eindhoven tradition use today, which is similar to mathspad of the 1990s?

[Matthew Heaney]

Will Mathematica work for you?

> --
> --
> You received this message because you are subscribed the mathmeth.com
> mailing list.
> To unsubscribe from this group, send email to
> Calculational-Math...@googlegroups.com
> For more options, visit this group at
> http://groups.google.com/group/Calculational-Mathematics?hl=en
> ---
> You received this message because you are subscribed to the Google Groups
> "Calculational Mathematics" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to calculational-math...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.

[rustompmody]

On Tuesday, August 26, 2014 2:08:02 PM UTC+5:30, Matthew Heaney wrote:

Will Mathematica work for you?

Thats an interesting suggestion. I will have to look into it further
However I wonder...

Mathematica is calculational for numbers and algebra. I am looking for calculational over the boolean domain.

Can mathematica do (or be taught) things like associativity of ≡ ?

At a more philosophical level, the way logic is demonstrated in Dijkstra&Scholten, there is a certain characteristic
pun between meta and object level (which can be unnerving to traditional logicians!) viz when we write

[A ≡ true] (which may be shortened to [A] )

• We (ie the human) may be making a meta-math statement that we know A is true
• We may be taking an object language formula which we further explore to see where it leads us

The first is traditionally written '⊢ A' or '⊨ A'

I would be surprised if a system could handle this pun without being consciously engineered for that purpose

Rusi

PS Hope the unicode chars come through!

[Jeremy Weissmann]

I still need to remind myself every few years why it makes sense to write  [A]  when stating a "result" or "theorem", as opposed to  [A == true] .  (Usually when I'm explaining the calculational style to someone else.)  It can be a tricky pun indeed!

I think Dijkstra helpfully wrote somewhere something along the lines of: we don't say " 'p is prime' is true " , we just say  "p is prime" .

Welcome aboard, Rusi!

+j

--

[Diethard Michaelis]

As for problems with the MathSpad general-purpose structure editor "that
is particularly useful for writing articles that contain substantial
amounts of mathematical calculations" I'd contact Roland Backhouse
directly ... http://www.cs.nott.ac.uk/~rcb/mathspad/

As for Mathematica and the associativity of Boolean equivalence. If the
Mathematica programming language can handle Boolean Algebra then it has
to "know" about ...

As for [A] and [A == true]. There is no pun whatever. Both are Boolean
expressions. Especially "true" is a Boolean constant just as "0" is a
numeric constant. It could have been named "top" or "white" of "L" as
well. The naming does not imply a meaning or interpretation! It might
equally be interpreted as <on> or <high voltage> or even <falsehood>.
Neither of the two expressions states that it is a mathematical theorem.
Such fact must always be stated in words (or special symbols not being
part of the algebra). The everywhere operator [] is part of the Boolean
algebra as presented in the Dijkstra-Scholten book. It replaces explicit
universal quantification over the statespace by point-free notation. And
it evaluates to Boolean constant "true" exactly when its argument equals
Boolean constant "true" otherwise to Boolean constant "false". Further
Boolean constant "true" is the neutral element of the Boolean
(equivalence) operator "==" , i.e. "== true" is as redundant as "+ 0" is
redundant in number theory, or as
if (a == true)
return true;
else
return false;
is in a beginner's C++ program when a is of type bool.
All of [A], [A == true], [A] == true, [A == true] == true,
[[A]], [[A == true]], [[A] == [true]], [[A == true] == [true]], ...
have the same Boolean value. But [A] is the most simple expression
amongst them.

Otherwise carefully read the preface of the Dijkstra-Scholten book where
you will find "The most important recommendation is to remember all the
time that this is NOT a treatise on logic, ..." (p. vii).

All the best, Diethard.

Am 26.08.2014 um 17:10 schrieb Jeremy Weissmann:
> I still need to remind myself every few years why it makes sense to write [A] when stating a "result" or "theorem", as opposed to [A == true] . (Usually when I'm explaining the calculational style to someone else.) It can be a tricky pun indeed!
>
>
> I think Dijkstra helpfully wrote somewhere something along the lines of: we don't say " 'p is prime' is true " , we just say "p is prime" .
>
>
>
>
> Welcome aboard, Rusi!
>
>
>
>
> +j
>
> On Tue, Aug 26, 2014 at 5:24 AM, rustompmody <rusto...@gmail.com>
> wrote:
>
>> On Tuesday, August 26, 2014 2:08:02 PM UTC+5:30, Matthew Heaney wrote:
>>>
>>> Will Mathematica work for you?
>>>
>> Thats an interesting suggestion. I will have to look into it further
>> However I wonder...
>> Mathematica is calculational for numbers and algebra. I am looking for
>> calculational over the boolean domain.
>> Can mathematica do (or be taught) things like associativity of ≡ ?
>> At a more philosophical level, the way logic is demonstrated in
>> Dijkstra&Scholten, there is a certain characteristic
>> pun between meta and object level (which can be unnerving to traditional
>> logicians!) viz when we write
>> [A ≡ true] (which may be shortened to [A] )

>> - We (ie the human) may be making a meta-math statement that we *know* A
>> is true
>> - We may be taking an object language formula which we further explore

[rustompmody]

On Saturday, August 30, 2014 3:32:52 PM UTC+5:30, Diethard Michaelis wrote:

As for [A] and [A == true]. There is no pun whatever. Both are Boolean
expressions. Especially "true" is a Boolean constant just as "0" is a
numeric constant. It could have been named "top" or "white" of "L" as
well. The naming does not imply a meaning or interpretation! It might
equally be interpreted as <on> or <high voltage> or even <falsehood>.
Neither of the two expressions states that it is a mathematical theorem.
Such fact must always be stated in words (or special symbols not being
part of the algebra).

Let me take and quote an example,  pg 35 Dijkstra&Scholten:

-----------------------------
Finally we derive for the identity element of the equivalence
(9)        [true]
by calculating for some X
  [true]
= {(7) parsed as [true ≡ (X ≡ X) }
   [X ≡ X]
= {(8)}
  true
--------------------------------------

Where/what is the 'stated in words' or special symbols?

[Diethard Michaelis]

"... we derive [a theorem] for ... by calculating [a proof] ..."
Note that both [additions] of mine are obvious from the context.
It is the very same pattern as in the immediately preceding Theorem (8)
and its Proof, just the keywords "Theorem" and "Proof" have been left
implied.

Hope that helps. Diethard.