[TYPES] [tag] Re: Declarative vs imperative

[Sergei SOLOVIEV]

To add a bit in support to Uday's remark about "presumption of 
supremacy" of classical logic:

In fact, it is well known that classical logic can be embedded in 
intuitionistic logic
using, for example, negative interpretation (classical "exists" becomes 
\not\forall\not etc.)
 From the point of view of provability, the interpretation of a 
classical theorem is provable
intuitionistically if and only if the original theorem was provable 
classically.
So, what is bad rationally, if instead of respectable "exists" we shall 
say "it is
not true that for all x does not exist..."? It is clear, that it is a 
"bad publicity",
a less "convincing" way to say - bad for "supremacy", but it has nothing 
to do
with scientific rationality itself. (Constructive mathematics is just 
more subtle
concerning existence.)

Best regards

Sergei Soloviev

Uday S Reddy wrote:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>
> Tadeusz Litak writes:
>
>   
>>> It is time to leave behind the classical logic.  In fact, we should have
>>> done it a long time ago.
>>>       
>> (even if it wasn't intended, it does indeed sound "like a total and
>> unconditional rejection"... such things happen in the fervor of a
>> discussion :-)
>>     
>
> Having thought about why it sounds like a "total and unconditional
> rejection", I believe the difference is in the perspective of what logic is
> about.
>
> Logic consists of the principles of "reasoned discourse", as per Aristotle.
> Our reasoned discourse happens in natural language, which is a humongous
> ocean.  We may never be able to understand fully all the principles of logic
> that are there.  But it is clear that the logic that we do understand (all
> the known logics put together) represents only a miniscule proprotion of the
> vast ocean of "logic" that is employed in reasoned discourse.  So, it seems
> to me that a great deal of humility is warranted in talking about "logic" in
> general.
>
> In contrast, people that vax about classical logic seem to have the
> presumption that classical logic has it all cased.  They seem to think that
> it represents the sum total of all reasonable principles of reasoned
> discourse (even if they are willing to admit modal logics of one kind or
> another as being reasonable *extensions* of classical logic).  Hence,
> anybody that talks about alternative logics is seen to be mounting an attack
> on the classical logic, denying the supreme position of classical logic as
> the one true logic.
>
> We, the non-believers, of course deny that classical logic is supreme in any
> sense.  However, that is not an attack on classical logic itself.  It is
> just an attack on the *presumption* that classical logic is supreme.
>
> All that we can say about classical logic is that it seems to be the
> canonical logic for the present-day mathematics.  Given that mathematics is
> a very conservative discipline, with the bar of entry for new ideas set very
> high, it has an abundance of depth but not so much in breadth.  Thus, a
> canonical logic for mathematics in no way represents a canonical logic for
> all of human thought.
>
> In particular, in a young and dynamic discipline like Computer Science,
> which has none of the mathematical conservatism, we should be free to
> explore all possible logics and invent new ones.  In fact, devising logics
> is our very main business.  We should be very wary of any presumptions about
> "the canonical logic" of any kind.
>
> Cheers,
> Uday
>