[FOM] Avron's questions about intuitionistic
A.P. Hazen
a.hazen at philosophy.unimelb.edu.au
Fri Nov 4 22:37:09 EST 2005
Arnon Avron writes:
>I have several qustions to intuitionists (the first two - also
>to nonintuitionists who might know the answers).
>
>1) Is there a definable (in the same way implication is definable
>in classical logic in terms of disjunction and negation) unary
>connective @ of intuitionistic logic such that for every A, B we have
>that A and @@A intuitionistically follow from each other,
>and B intuitionistically follows from the set {A, at A}?
-------No. If such a connective were definable, it would express a
"truth function" in every matrix for intuitionistic logic. Thus, to
show indefinability, it suffices to exhibit a Heyting Algebra over
which no such operation can be defined. Consider the three-element
chain, <T,U,F>. (This is the algebra of propositions in the
two-world Kripke model: T = true in both worlds, U = true only at the
second world, F = true in neither world.) By Avron's condition
(ii) B intuitionistically follows from the set {A, at A}
@A intuitionistically implies ~A (the usual intuitionistic negation
of A). Thus @(x) must be less than (or equal to) ~(x) for each
value, so @(T)=@(U)=F. @(F), however must be T: by Avron's
(ia) A intuitionistically implies @@A
@@(T) has to be T, but @(T) is F. But now
(ib) @@A intuitionistically implies A
yields a contradiction: @(U) is F, so @@(U) = T, which does not imply U.
>
>2) Can one define in intuitionistic logic counterparts of the
>classical connectives so that the resulting translation
>preserves the consequence relation of classical logic? (Obviously,a
>negative answer to question 1 entails a negative one to question 2).
-----There are the "negative translations," discovered by Glivenko,
Gödel and Gentzen. Those that preserve the classical consequence
relation, however, do not provide "generally applicable" analogues of
the classical connectives: defined connectives which, applied to
arbitrary formulas, "act classical". In particular, there is a
negative translation, t, for which the translation of classical
negation is simply intuitionistic negation (t[~A] = ~[t[A]]) and
which allows t[A] to be inferred from t[~~A], but on it t[S] is
always built up from "pseudo-atoms" of the form ~~p.
>3) In several postings it was emphasized that LEM applies
>in intuitionistic logic to "decidable" relations. Is there
>an intuitionist definition of "decidable" according to which
>this claim conveys more than a trivial claim of the form "A implies A"?
----The claim is tautologous if we DEFINE "F is decidable" as
"Ax(Fx v ~Fx)" is (intuitionistically) true.
On the other hand, very weak intuitionistic systems of arithmetic can
represent recursive functions. So in general, if a predicate is
decidable by means of an algorithm, and you can prove that the
algorithm works -- i.e. that
Ax((Fx <=> f(x)=1)&(~Fx <=> fx = 0))
-- in a reasonable intuitionistic system, then you can also prove
Ax(Fx v ~Fx)
in the same system. So, if you think of decidability in terms of
algorithms, it can be informative to say that excluded middle holds
for decidable predicates.
>
>4) Some postings mentioned also "undecidable" relations (or predicates).
>What is the definition of "undecidable" here? is a relation P
>intuitionistically undecidable if there is procedure that produces
>a proof of absurdity from a procedure that given any x either provides
>a proof of P(x) or a procedure that carries any proof of P(x) to
>a proof of absurdity?
>
>5) Does an intutionistically-undecidable predicate intutionistically-exist?
-------It is provable in intuitionistic analysis that it is not the
case that every real number is either equal to or distinct from 0:
~Ax(Fx v ~Fx)
is provable, where F means "is equal to 0" and the variable ranges
over real numbers.
-----
Allen Hazen
Philosophy Department
University of Melbourne
More information about the FOM
mailing list