[FOM] Some informative questions about intuitionistic logic and mathematics, Arnon Avron aa at tau.ac.il
twilson at csufresno.edu
Wed Nov 9 01:36:33 EST 2005
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
 "<= partially orders K",
 (Ak)(Ak')(Ax) k <= k' /\ D(k,x) -> D(k',x), and
 (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  means that existence is persistent, and the equations in
, 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
 /\  /\  /\ (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
More information about the FOM