# P

∧ ∀x∀y P x ∧ S q x, y

Py

∀x P x

one can put the universal quantifier (P) in front of the formula.

x

y ≡ x, y

∀F F x

⇐

Fy

The solution of this general decision problem (for the extended logic) would not only permit us to answer questions about the provability of simple geometric theorems, but it would also, at least in principle, make possible the decision about the provability, resp. nonprovabil- ity, of an arbitrary mathematical statement.

But as soon as one makes the foundations of theories, especially of mathematical theories, as the object of investigation · · · the extended calculus is indispensable.

# F

¬∃x F x

# F

∃x F x ∧ ∀y F y

≡ x, y

.

# ∀F ∀G

F∧

G

# SC F, G ∧

F ∧ SC F, G

G

SC F, G F

G

It is also of particular interest that the number theoretic axioms become logically provable theorems.

,