0
$\begingroup$

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?

$\endgroup$
5
  • 3
    $\begingroup$ Perhaps: what is a metalanguage of ZFC? $\endgroup$
    – Trebor
    Jun 14, 2023 at 7:05
  • $\begingroup$ Probably - if you could elaborate, your thoughts would be most welcome. Thank you! $\endgroup$ Jun 14, 2023 at 7:26
  • 1
    $\begingroup$ The axioms of ZFC are per se sentences in a first order theory. The "grammar" of a first order theory is (if I understand your meaning) determined by the signature of the theory, i.e. its predicates, function symbols (including constants), etc. The other grammatical elements (variables, logical operators, quantifiers, equality) are considered common to all first order theories. From there your "desire to understand" something about defining recursive functions (or complexity classes?) needs clarification. Perhaps formulating a concrete problem would help. $\endgroup$
    – hardmath
    Jun 16, 2023 at 12:53
  • $\begingroup$ @hardmath could you post that as an answer so I can discuss and engage with it more, or maybe we can form a chatroom here on the site? But yeah, let me dwell on what I’m trying to get at regarding recursion. It’s a thought that’s been on the tip of my tongue, it’s still slowly getting formulated. Thx $\endgroup$ Jun 17, 2023 at 12:55
  • $\begingroup$ Here are my thoughts on recursion for anyone that’d be interested. cs.stackexchange.com/questions/160748/… Thank you $\endgroup$ Jun 18, 2023 at 15:34

2 Answers 2

5
$\begingroup$

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.

$\endgroup$
5
  • $\begingroup$ Wow, ok, that’s exactly what I’m trying to learn. en.m.wikipedia.org/wiki/Fixed-point_combinator Would love to learn more and discuss with you further. $\endgroup$ Jun 16, 2023 at 12:47
  • $\begingroup$ @hmltn I'm no expert on fixpoints or combinators in general. Nor computability. :) $\endgroup$ Jun 18, 2023 at 10:25
  • $\begingroup$ @hmltn as a side note, I guess the right SO site to ask about fixpoints and computability is the Theoretical CS one. $\endgroup$ Jun 18, 2023 at 10:26
  • $\begingroup$ I’m trying to get more people to chat with so if you want you can join me in a stack exchange chat room (I can make one) or on my discord, thx discord.gg/SvZB43wB $\endgroup$ Jun 18, 2023 at 11:08
  • $\begingroup$ Discussing some set theory here chat.stackexchange.com/rooms/146728/… $\endgroup$ Jun 18, 2023 at 11:09
4
$\begingroup$

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.

$\endgroup$
5
  • $\begingroup$ Thank you, the first linked document is excellent for my level. Will read. If you would care to add in a step by step guide into your answer though, it would be much appreciated, especially regarding formal languages - can all 3 foundational approaches be written as transformation rules on an alphabet, as in compiler theory, and the Chomsky hierarchy? It would be nice to see a very clear, simple distinction between the characteristics of formal systems based on nothing more than their initial transformation rules on an initial alphabet (if that is possible?). Thank you!! (And I could accept.) $\endgroup$ Jun 14, 2023 at 7:25
  • $\begingroup$ My newbie train of thought is something like this. I wonder if there is a simpler but broader idea of the Church-Turing thesis where you require certain ideas in a meta-language to be able to express those ideas in a sub-language. If you define a system which constructs sets cumulatively, it implies a meta-language that already has a concept of “set”, and “constructing a set”. If you want to interpret sets you generate as functions, to actually apply them, it implied a meta-language (or, context of understanding), which already had an “opinion” about what functions are, how to represent and $\endgroup$ Jun 14, 2023 at 7:37
  • $\begingroup$ apply them. Recursion (I think) can be simplified. The concept of “growth” could be removed from the idea. Recursion is when a language can interact with its metalanguage, sort of (I think). As transformation grammars, I think it could be elementary - type-0 elements are symbols. Type-1 elements are arbitrary compositions (of any kind - interpretable as this or that operation, but it doesn’t matter what) of type-0 elements. Type-2 are compositions of type-1. Type(1, 0) are any compositions (pairings, combinations) of type 1 and type 0 elements (corresponding to cardinal number 2). We can study $\endgroup$ Jun 14, 2023 at 7:41
  • $\begingroup$ each type in more detail. But it gives us a very simple way to compare and order, the relationship between formal systems. Is this in line with a particular standard approach? Thanks very much for your guidance. - Julius. $\endgroup$ Jun 14, 2023 at 7:42
  • $\begingroup$ This is what I tried to express in my downvoted post about hypercomputation: proofassistants.stackexchange.com/questions/2232/… - on a profoundly philosophical level, there is a simple yet ignored, fundamental problem with axiomatic systems - the problem of infinite regress (meta-languages on meta-languages). Higher category theory offers a legitimate different paradigm - systems imply rules, not the other way around, as in this approach that I must read: girard.perso.math.cnrs.fr/0.pdf. $\endgroup$ Jun 14, 2023 at 7:49

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.