[FOM] Avron's questions about intuitionistic

[A.P. Hazen]

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