How does the finitely axiomatized formalization of predicate logic correspond to natural deduction for predicate logic?

Question

I'm really interested in using Metamath, but Metamath comes with a funky version of predicate logic. Substitution is not allowed in Metamath, so Metamath employs Tarski's system S2 which is "finitely axiomatized", i.e. a complete axiomatization of predicate logic that doesn't require substitution. Rather than give a bad explanation of the theorem, you can get a feel for it with Norm Megill's article on the subject and Tarski's original paper.

I'm so confused about how I can use this system to simulate normal predicate logic that I'm not even sure what kind of questions I should ask here. But I will try:

• It seems like there are only two predicates in this system, $=$ and $\in$. How can we use these to get any predicate we'd need?
• How can we extend the system to give us predicates with three or more arguments? How about functions?
• Are there any easy resources that a beginner could use to map the traditional natural deduction in predicate logic that they know to Tarski's S2

Thanks very much for the help everyone.

Answer 1

The key-point is that IF we restrict to only a finite number of predicate symbol (Megill uses only $\in$, in addition to equality) we may replace the "schematic" axioms by a finite list.

For example, the substitution axiom schema for equality: $x=y \to (\varphi[u/x] \to \varphi[u/y])$, can be replaced by the following two axioms:

$x = y → (x ∈ z → y ∈ z)$ and $x = y → (z ∈ x → z ∈ y)$.

They manage the two only cases of atomic formulas using $\in$: $u \in z$ and $z \in u$ [the "pattern" is more clear if we write them as: $\in (x,u)$ and $\in (u,x)$], and they are enough because the "general" case can be proved by induction.

This "procedure" cab be iterated to cover a finite number of predicate symbols, because we have to manage only a finite number of cases.

The "restriction" to atomic formulas only is necessary to implement Tarski's idea of avoiding the complex rule of substitution (more precisely: proper substitution, that take care of quantifiers).

As per Metamath's page: Appendix 1: A Note on the Axioms:

Tarski's system is exactly equivalent to the traditional textbook formalization, but (by clever use of equality axioms) it eliminates the latter's primitive notions of "proper substitution" and "free variable," replacing them with direct substitution and the notion of a variable not occurring in a formula (which we express with distinct variable constraints).

The trick is simply that in an atomic formula "simple" substitution is always allowed, due to the absence of quantifiers.