1
$\begingroup$

There are several axiomatizations for number theory, group theory, and other theories represented in first order logic. Further, these theories are also representable in set theory such as $\sf ZFC$ or $\sf NBG$ and it got me thinking about reasoning about formal systems in formal systems.

Can we represent the theory (or meta-theory?) of first order logic or set theory inside first order logic or set theory the way we represent number theory inside first order logic or set theory? I assume its possible, and has been done before, but how is this usually done, and is there a good reference for using such axiomatizations? I'm interested in creating a formal system that models a formal system, so I can create formal proofs about the system that makes the formal proofs.

I'm thinking of predicates and functions that are definitions that assert that sentences that belong to the set of formulas of first order logic or set theory have certain properties or some such representation, similar to how the Peano axioms are definitions of predicates and functions that assert members belonging to the natural numbers have certain properties.

$\endgroup$
3
  • 8
    $\begingroup$ You don't quite notice it, but pretty much everything you do which includes the word "model" implies that you have defined first-order logic inside set theory; and when you talk about models of set theory this means that you have internalized set theory into set theory as well. $\endgroup$
    – Asaf Karagila ♦
    Jul 29, 2014 at 21:06
  • $\begingroup$ Sorry, I don't have any academic training, so I'm often struggling with definitions. I thought "model" was usually used to find interpretations of a statement that was satisfiable; Is model theory where I should be looking? Is there a term for describing a theory within itself? It sounds like recursive axiomatization, but when I look it up that points to axiom schemata, which I don't think is quite the same thing. $\endgroup$
    – dezakin
    Jul 29, 2014 at 21:45
  • $\begingroup$ Looks like this is the area of proving metatheorems in metamathematics, specifically formal metalogic or metalanguage. Model theory gave a good start to start digging, so I might find some first order axiomatization of metalanguages describing first order theories and proof calculi. $\endgroup$
    – dezakin
    Jul 29, 2014 at 22:25

0

Reset to default

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.