What is the meta-language of ZFC?

Question

This is a good post which says that all proof assistants are founded in HOL, first order logic, or dependent types.

Does this mean that the axioms of ZFC are just expressions obtainable from the grammar of first order logic?

What is required to define first order logic, for example, in x86 assembly language?

Perhaps these resources provide the answers:

https://people.compute.dtu.dk/ahfrom/Formalized%20First-Order%20Logic.pdf

https://math.stackexchange.com/questions/2221705/how-do-you-construct-first-order-logic

https://builds.openlogicproject.org/content/first-order-logic/first-order-logic.pdf

This is leading up to a desire to understand and define recursion/complexity classes. The ability to define a recursive function depends on the concepts available in the formal grammar / axioms of the formal system. So I am wondering if recursion is best viewed as a relationship between an expression in a formal language, and that formal language itself (which may further require it respectively to be understood in terms of its metalanguage)? Like a three-way relationship?

Answer 1

Does this mean that the axioms of ZFC are just expressions obtainable from the grammar of first order logic?

As SEP tells us,

ZFC is an axiom system formulated in first-order logic with equality and with only one binary relation symbol ∈ for membership.

Note that

1. ZFC uses FOL with equality
2. ZFC uses non-logical constant ∈

Naturally, axioms of ZFC are "non-logical" or "extra-logical" in the sense they're talking about properties of a non-logical constant ∈; while "purely logical" axioms specify properties of logical connectives like ∧, ∨, ⇒ and whatever else you have in your system.

Thus while axioms of ZFC use the grammatical structure of FOL, they cannot be obtained (i.e. derived) from purely logical axioms.

What is required to define first order logic, for example, in x86 assembly language?

To define an axiomatic system (FOL in particular) in any language, you need a way to write down the formulae (i.e. syntactic trees with constants and variables aka AST), the proofs (either lists or trees of formulae depending on Hilbert or Gentzen system), and a procedure to check that a proof is indeed a proof. Also you are likely to want some kind of a proof-search procedure.

So to implement a FOL in an x86 assembly, you implement a Standard ML interpreter in x86 assembly, and then implement a LCF-style system in your SML. 😁

This is leading up to a desire to understand and define recursion/complexity classes.

Recursion is a property of a function that calls itself by name. Thus it's purely syntactical notion. You can define the same functions without direct recursion if you have, say, "built-in" fixpoint function (combinator). While Turing machines define all the functions without recursion and arguably without syntax at all. So recursion has very little to do with (computational) complexity.

Answer 2

First, in a standard logic textbook (or at least a standard set theory textbook), yes, ZFC as a foundation takes place in first order logic (FOL). Each axiom of ZFC is written in the language of FOL. So the full set of axioms for FOL+ZFC consist of both the axioms of FOL and the axioms of ZFC.

There are also natural deduction systems for implementing FOL that are rule-based instead of axiom-based. For example, you may see something like:

A |- a \/ b      A, a |- c     A, b |- c
----------------------------------------
                 A |- c

This rule states that if you can derive some a \/ b from some set of assumptions A and also derive c from A, a and A, b, then we can derive c from A. Axioms can be implemented as rules as well where there is nothing above the line, like:

-------------------------------------------------------
|- forall x, forall y, exists z, ((x in z) /\ (y in z)) 

Proof assistants based on ZFC (or say Peano arithmetic) similarly use FOL. I believe this is what metamath/set.mm, Isabelle/ZFC, and Mizar use, modulo a few variations to the set theory. They may add support for large cardinals or proper classes (as in NBG set theory). I admit I'm not very familiar with the specifics, but you could probably consult the documentation for each.

To implement a proof assistant for FOL+ZFC, technically all you need is a computer system in which you can write a FOL proof in some text format and the system checks that each step is well-formed and follows all the rules and axioms of your system. But in practice you also need support for practical concerns like constructing definitions, building a library of theorems, and providing a good user experience (say, through interaction and automation).

While Mizar is a bit ad hoc, metamath and Isabelle are principled meta-logics that can support arbitrary foundations, not just FOL+ZFC. You may want to look at the documentation for either to get a sense of how one goes about implementing FOL in those systems, but it is basically just by providing rules and axioms like I described above.

As for recursive functions, in textbook set theory, functions are not really first class citizens. They are just sets of input-output pairs. Recursive functions can be justified by theorems in FOL+ZFC showing that a recursive description of a function on a well-founded set uniquely specifies a function on that set. I don't know if Mizar, metamath/set.mm, or Isabelle/ZFC provide any tooling to make defining recursive functions easier.

Edit: The chapter Foundations by Jeremy Avigad goes into more detail about the foundations for all the proof assistants including set theory based ones. Here is a blog post by Andrej Bauer about How to implement dependent type theory I. It wouldn't be much different to implement a HOL or FOL system. The principles are similar.