Re: [TYPES] [tag] Re: Declarative vs imperative

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]


On 05/03/2013 11:22 PM, Uday S Reddy wrote:
> Marc Denecker writes:
>
>> "It is time to leave behind the classical logic.  In fact, we should
>> have  done it a long time ago."
>>
>> To me, that sounds like a total and unconditional rejection.
>
> No, what I meant is that the classical logic represents a stage in the
> development of logic.  It cannot be taken as the final answer.  In
fact, we
> cannot accept that we have a final answer until the entire natural
language
> has been formalized, which might take a very very long time indeed!  (The
> view I take, following Quine, is that logic is a regimentation of natural
> language.  We can perfectly well circumscribe various regimens for various
> purposes.)
>
> I am entirely happy with the characterization of logical connectives as
> "information composition" operators.

We then agree on this point. This view goes back to Frege and
even to  Leibniz, right?

But do we agree that the standard logical connectives of FO correctly
implement an important set of  basic information composition operators.
That is, conjunction, disjunction, negation, the quantifiers?

If that is the case  then FO's connectives
will have to be in other languages as well?  We agree that these
operators are not enough but  the  more universal languages that the
scientific community should strive for in your and my opinion,  will
have to contain FO's information composition operators (modulo syntactic
sugar) and hence be extensions of classical logic?

I'm confused about your position in this right now. On the one hand, you
do not (unconditionally) reject FO ; on the other hand, in your reaction
on my first email. you seemed to react against the fact that  I propose
FO as a base language. If you agree that FO's connectives correctly
implement a set of  basic information composition operators, then you
should agree with me on that claim. But if you think FO's connectives
are not correct or not basic, then please consider the challenge in my
previous email (or see below)


> But we can only accept it as a good,
> but vague, intuition.  We do not know what this "information" is.  Neither
> do we know what the information is about.  So, in order to claim that
> classical logic is a canonical information composition calculus, somebody
> would need to formalize those notions.

I'm sure Tarski would disagree with you. I think this would be his answer.

The notion of "information" that you claim is vague, is actually
formalized in model semantics in a very precise way, albeit slightly
implicitly.

The information content of a logic expression/theory T is formalized by
the class of its models (i.e., the structures in which T is true).
Models are formal representations of possible states of affairs,
non-models are formal representations of impossible states of affairs.
This set is characteristic for the information expressed in T.

This is obvious e.g., when we look at the notion of logical equivalence:
two expressions T, T' are equivalent iff the classes of their models are
identical.

The logical connectives and quantifiers correspond to
operators on these classes of models. Their definition is implicit
in the definition of the satisfaction relation.   E.g., the
characteristic function of a conjunction is the intersection of the
classes of models of the  conjuncts.

From this formal concept (the class of models), we can derive concepts
like formal concepts of entailment, validity, equivalence.  All this is
mathematical and precise.

This formal notion of "information" needs to be connected to the
informal notion of "information" which is the interpretation that we,
human experts, give to a logical expression.

Logic does not know and is not supposed to know  what the informal
information (in a logic sentence) is about because  this
depends on the meaning that we, human
experts, give to the uninterpreted non-logical symbols.
But once a precise intended interpretation is given,
then I would say that the informal information content of a logic
sentence is precise as well.

For example, if we interpret the nonlogical symbols Semester/1,
Course/1, Registered/3, TakesPlace/2 in the way the names suggest, then
the intuitive information content of


B	! c ! s : Semester(s) & Course(c) & ~ ? st: Registered(st,c,s)
		   => ~ TakesPlace(x,s)

is perfectly clear and is given by the equally precise informal sentence


A	if in a semester no student registered for a course, then
	this course does not take place in that semester.


If anything is vague or inprecise, then I guess it should be easy to
come up with e.g., an example of a database representing a situation
where B and A disagree or at least where it is not clear whether A or B
is true or not. This was the challenge in my previous email.

I think informal language sentence A is precise, at least in any context
where the underlying relations semester, course, are precise,
and I dont think one can find a database where A and B would disagree.

I would love to see a counterexample.


>
> Even though Vladimir has omitted the word "programming" in titling this
> subthread, the discussion has been about "declarative" and "imperative" as
> paradigms of programming.  So, I would rather not divorce myself from
> programming concerns in discussing these issues.


One can only view a logic theory as a program if one associates an
inherent  form of inference to the logic. As I argued in my first email,
this is the first step in messing up the difference between declarative
logic and programming languages.

It is the association of a unique
inherent form of inference to a logic  that blurs the distinction
between declarative theories and procedural programs



Cheers,

Marc


>
> Cheers,
> Uday
>
> PS. I will try to respond to your more detailed points a little later.
 For
> now, I just wanted to set the record straight about what you called my
> "total and unconditional rejection" of classical logic, which it wasn't.
>


-- 

   Marc Denecker (prof)
   KU Leuven   			
   Departement Computerwetenschappen    tel: ++32 (0)16/32.75.57
   Celestijnenlaan 200A Room A02.145    fax: ++32 (0)16/32.79.96
   B-3001 Heverlee, Belgium
   email: [email protected]
   http://people.cs.kuleuven.be/~marc.denecker/
 ........................................................................




-- 

   Marc Denecker (prof)
   KU Leuven   			
   Departement Computerwetenschappen    tel: ++32 (0)16/32.75.57
   Celestijnenlaan 200A Room A02.145    fax: ++32 (0)16/32.79.96
   B-3001 Heverlee, Belgium
   email: [email protected]
   http://people.cs.kuleuven.be/~marc.denecker/
 ........................................................................

Disclaimer: http://www.kuleuven.be/cwis/email_disclaimer.htm