Some examples of formulas.

Here is how the previous formulas (and some more) look like. Implication is material implication here.

(1) (((¬A∨C)∧B)→F)

In[2]:=

Out[2]=

(2) ∀x.(((¬A∨C)∧B)→F)

In[3]:=

Out[3]=

(3) ∃x.(((¬A∨C)∧B)→F)

In[4]:=

Out[4]=

(4) "If the map f has a minimum point, then the unequation system f(x)≤f(g(x))∧f(x)≤f(h(x) has a solution"
(∃x.∀y.f(x)≤f(y)→∃x.(f(x)≤f(g(x))∧f(x)≤f(h(x))))

In[5]:=

Out[5]=

(5) "Excluded Middle for ∃y.P(x,y) is not false"
∀x.¬¬(∃y.P(x,y)∨¬∃y.P(x,y))

In[6]:=

Out[6]=

(6) "The map f has a minimum point"

∃x.∀y.f(x)≤f(y)

In[7]:=

Out[7]=

(7) "Excluded Middle for ∃y.∀z.P(x,y,z)"
∀x.(∃y.∀z.P(x,y,z)∨∀y.∃z.¬P(x,y,z))

In[8]:=

Out[8]=

(8) "Between any two numbers there is a third one."
∀x.∀y.(x<y→∃z.(x<z∧z<y))

In[9]:=

Out[9]=

(9) "If f:N→N is any map, there are x < y < z such that f(x)≤f(y)≤f(z)."
∃x.∃y.( (x<y∧f(x)≤f(y)) ∧ ∃z.(y<z∧f(y)≤f(z)) )

In[10]:=

Out[10]=

Created by Mathematica  (October 17, 2006)