🚀 go-pugleaf

In article <TORKEL.93Jan12232944@bast.sics.se> torkel@sics.se (Torkel Franzen) writes:
>In article <1993Jan12.201545.27599@CSD-NewsHost.Stanford.EDU> pratt@Sunburn.
>Stanford.EDU (Vaughan R. Pratt) writes:
>
>   >Australian and American courts interrogate witnesses in a language that
>   >presumes intuitionistic logic, in that they draw a distinction between
>   >straight answers and hedged and insist on the former.
>
>  The distinction between hedging and straight answers has nothing in
>particular to do with intuitionistic logic,

I don't see what I can add to my previous posts that would make it
easier for you to see this connection, sorry.

>Furthermore, natural language is not a formal system,

Neither is the trajectory of a planet or the behavior of a wisp of
cigarette smoke.  This hasn't prevented optimists from attempting to
describe seemingly complex natural phenomena in terms of mathematically
tractable formal systems.  I can see where a committed pessimist would
have grave doubts.

>This applies equally, of course, to classical propositional
>logic. Formal logic doesn't tell us a great deal about what reasoning,
>interrogation, justification, etc in natural language is like.

This is like someone with a one-speed bicycle announcing that no
bicycles can climb steep hills.  While you sit around grumbling that
natural language simply *can't* be modelled formally, other people are
looking for models that balance realism and mathematical tractability.

>  More interesting is the other point you raised, concerning the
>possibility of interpreting classical in intuitionistic theories via
>e.g. a Godel translation, where you emphasized that the effect of this
>is to introduce distinctions where there are none in classical logic.
>But clearly this in itself tells us nothing about the usefulness or
>interest of the intuitionistic versions of the theories. We can go on
>to introduce a large number of logical distinctions, still with
>Godel-type translations of classical theorems.  Such distinctions have
>no intrinsic value. Looking at the distinctions introduced by
>intuitionistic logic, they are in part natural in the sense that they
>have a connection with or correspond to distinctions that we make in
>mathematics and that we have found useful, such as the distinction
>between direct and indirect proofs of existential statements. But
>intuitionistic logic involves very much more than such natural
>distinctions. For example, the logical distinction between ~~ExP(x)
>and ExP(x), with P a decidable number-theoretic predicate, corresponds
>to nothing in ordinary mathematical experience.

Let P(x) be the predicate "x is the least Mersenne prime with at least
a million binary digits."  This predicate is not only decidable but can
be decided by a finite state automaton in the time taken to read the
the input.  Yet a constructivist of the appropriate stripe will today
allow ~~ExP(x) while questioning ExP(x).  It is reasonable to expect
him to agree to ExP(x) in less than five years time, at the current
rate of production of Mersenne primes (up to some 200,000 bits today I
think).  I'd say this distinction was not only well within mathematical
experience but one that is very familiar to every amateur number
theorist.

>For another example,
>the splitting up of the concept of an infinite set of natural numbers
>into "infinite", "not not infinite", "not bounded" introduces
>considerable complications, and we don't even know whether it is possible to
>teach and learn mathematics without "conflating" these concepts. We need
>to think about such matters as well in considering distinctions.

If "infinite" means "not finite" then isn't "not not infinite" a
synonym for "infinite"?  But in these murkier waters involving hidden
quantifiers I concede that I am a much less capable swimmer than many
others, for all I know yourself included.
-- 
Vaughan Pratt			There's safety in large condition numbers.