According to the methods characterized by the last examples one can apply the first-order calculus in particular to the axiomatic treatment of theories · · · .
Once logical formalism is established one can expect that a sys- tematic, so-to-say computational treatment of logical formulas is possible, which would somewhat correspond to the theory of equa- tions in algebra.
e met a well-developed algebra of logic in the propositional calculus. The most important problems solved there were the universal validity and satisfiability of a logical expression. Both problems are called the decision problem · · · .
The two problems are dual to each other. If an expression is not universally valid then its negation is satisfiable, and conversely.
The decision problem for first-order logic now presents itself · · · . One can · · · restrict oneself to the case where the propositional variables do not appear · · · .
The decision problem is solved if one knows a process which, given a logical expression, permits the determination of its validity resp. satisfiability.
The solution of the decision problem is of fundamental impor- tance for the theory of all subjects whose theorems are capable of being logically derived from finitely many axioms · · · .
e want to make it clear that for the solution of the decision prob- lem a process would be given by which nonderivability can, in princi- ple, be determined, even though the difficulties of the process would make practical use illusory · · · .
· · · the decision problem be designated as the main problem of mathematical logic.
· · · in first-order logic the discovery of a general decision proce- dure is still a difficult unsolved problem · · · .