[FOM] Some informative questions about intuitionistic logic and mathematics, Arnon Avron aa at tau.ac.il

[Todd Wilson]

Rene Vestergaard wrote:
> Is it known whether intuitionistic "Ax(Fx v ~Fx)" is equivalent to some 
> classical formula?

Although perhaps not what you were looking for, a general method for 
finding classical equivalents to intuitionistic formulas is to use 
Kripke semantics, which is complete for intuitionistic predicate 
calculus (IQC).  Thus, a statement P in IQC is intuitionistically valid 
iff it is (classically) forced in all Kripke models, a notion that is 
expressible in classical predicate calculus in the language of P 
extended by some additional relations.

In more detail, we add a unary relation K, a binary relation <=, a 
binary relation D, an (n+1)-ary relation R^ for every n-ary relation R 
of the original language, and formulas

[1]   "<= partially orders K",
[2]   (Ak)(Ak')(Ax) k <= k' /\ D(k,x) -> D(k',x), and
[3]   (Ak)(Ak')(Ax1)...(Axn) k <= k' /\ D(k,x1) /\ ... /\ D(k,xn) /\
          R^(k,x1,...,xn) -> R^(k',x1,...,xn).

Here < K, <= > is the Kripke frame, D(k,x) means that x exists at stage 
k, and R^(k,x1,...,xn) means that R(x1,...,xn) holds at stage k. 
Equation [2] means that existence is persistent, and the equations in 
[3], one for each relation symbol R of the original language, state that 
the truth of atomic formulas is persistent.  We can then define a 
forcing relation ||- between elements of K and formulas of the original 
language by recursion on the structure of the formula, as follows:

    k ||- R(x1,...,xn)  is  R^(k,x1,...,xn)
    k ||- P /\ Q        is  (k ||- P) /\ (k ||- Q)
    k ||- P \/ Q        is  (k ||- P) \/ (k ||- Q)
    k ||- P -> Q        is  (Ak') k <= k' /\ (k' ||- P) -> (k' ||- Q)
    k ||- (Ax)P[x]      is  (Ak')(Ax) k <= k' /\ D(k',x) -> (k' ||- P[x])
    k ||- (Ex)P[x]      is  (Ex) D(k,x) /\ (k ||- P[x])

The intuitionistic formula phi then translates to

    [1] /\ [2] /\ [3] /\ (k) k ||- phi,

which is "unfolded" using the recursive definition of ||-.  The result 
is that the original formula is intuitionistically valid iff the 
translated formula is classically valid.

--
Todd Wilson                               A smile is not an individual
Computer Science Department               product; it is a co-product.
California State University, Fresno                 -- Thich Nhat Hanh