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

Todd Wilson 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

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

```