Defining Formulas in ∧, ∨, →, ⇒, ¬, ∀, ∃.

We consider all formulas having any computable function as function symbol, any computable predicate as predicate symbol, the constants T (true) and F (false), the propositional connectives ∧, ∨, → (material implication), ⇒ (constructive implication) ¬, and the quantifiers ∀, ∃. The intended meaning of  ∀, ∃ are quantifications over the domain N of natural numbers. Examples are:

    ((¬A∨C)∧B→F),        ∀x.((¬A∨C)∧B→F),       ∃x.((¬A∨C)∧B→F),   
     (∃x.∀y.f(x)≤f(y)→∃x.f(x)≤fg(x)∧f(x)≤fh(x)),
    ∀x.¬¬(∃y.P(x,y)∨¬∃y.P(x,y))

with f denoting some computable map, and P denoting some decidable predicate.

In this program we can type directly only atomic formulas, such as f(x)≤f(y), or P(x,y), as: "f(x)≤f(y)", or "P(x,y)". For denoting compound formulas, we have to use the operators

        Conj,     Disj,     Impl,     Neg,     Un["x",.],     Ex["x",_]
        
to introduce the connectives ∧, ∨, →, ¬, ∀, ∃. For instance, A∧B, with A, B atomic, must be written Conj["A", "B"]. Later, we will introduce a linearization operator, computing "A∧B" out of Conj["A", "B"]. Notice that the name of the bound variable must be written "x", not x. For instance, ∀x.x=x must be written Un["x","x=x"].

Created by Mathematica  (October 17, 2006)