1
$\begingroup$

I hope that this post isn't off topic, but I already asked math.stackexchange about first order formalizations of first order logic. There are provability logics and extensions in modal logic's that seem to attempt to address this question, and model theory implies answering questions about metamathematics. But I'm looking for an explicitly first order theory that can be used to prove things about metamathematics.

Basically, I'm wondering if there are first order formalizations of metamathematics. I'm interested in making proofs in first order logic about proof systems, such as the completeness and incompleteness theorems for first order theories in a fashion that is analogous to making a computer language compiler that can compile itself.

I understand that this probably should be possible, seeing it's generally agreed that you can represent most of mathematics in set theory, and represent set theory in first order logic, and I don't see any reason why encoding definitions about formal statements, provability, satisfiability, and other notions related to metamathematics would be unworkable.

There are formalizations of arithmetic both in the language of first order logic directly and in the language of set theory. Are there formalizations of metamathematical systems that I can use to make first order proofs about first order proofs similar to first order theories about arithmetic and set theory?

Improve this question
$\endgroup$
5
  • 4
    $\begingroup$ I'm confused: in light of Goedel coding, how isn't first-order arithmetic already a "logic of proofs" (and other things besides)? My understanding was that weaker systems, like modal logics of proofs, are fragments of first-order arithmetic, although I could be wrong (theories axiomatizing notions of truth are really really strong, but these aren't quite theories of provability). $\endgroup$
    – Noah Schweber
    Commented Aug 7, 2014 at 22:35
  • 1
    $\begingroup$ The definition of a Gödel numbering is done in the metatheory, along with other definitions for making informal proofs. I'm looking for formal first order definitions, including of Gödel numberings. Arithmetic is embedded in set theory, but without the appropriate definitions its hard to ask questions about arithmetic in raw set theory, and without the appropriate definitions in arithmetic, its hard to ask questions about Gödel numbering of formula in arithmetic. $\endgroup$
    – dezakin
    Commented Aug 7, 2014 at 22:50
  • 4
    $\begingroup$ You can do nearly 100% of it in PRA and 97% in much less... See the article by Craig Smorynski in the Handbook of Mathematical Logic for a detailed exposition. $\endgroup$
    – François G. Dorais
    Commented Aug 7, 2014 at 23:02
  • $\begingroup$ Thanks, I'll check it. I was mostly motivated in asking questions about satisfiability, decidability, and provability about questions inside an automated theorem proving system, so I need to be able to formalize all definitions if I want to ask a question about a particular well formed formula like "Is this a decidable statement?" or "Is this a satisfiable statement?" or "Do statements that have this form fall in the set of decidable statements?" $\endgroup$
    – dezakin
    Commented Aug 7, 2014 at 23:22
  • 2
    $\begingroup$ You might also find this interesting - r6.ca/Goedel/goedel1.html $\endgroup$
    – François G. Dorais
    Commented Aug 7, 2014 at 23:47

1 Answer 1

Reset to default
-2
$\begingroup$

Possibly, what I am currently doing can be considered as research in this direction, and I will share about it below.

First, what is metamathematics? I would treat this as a theory in a language which can serve as a metalanguage of the languages used in mathematics. In my article I introduced a language called metalingua intended to serve as one metalanguage common to different languages. Since then, I developed further this language, so that it now has only one symbol of a binary operation. I talk below about this language and its set theoretic interpretation, but first will talk about my understanding of what is meaning (sense) in a natural language which is richer than any artificial language used by mathematicians.

I call meaning of a word the set of all things denoted by it ("referents of the word"). So, a noun denotes objects, a verb denotes actions, an adjective denotes qualities of objects, an adverb denoted qualities of actions, etc. Thus, "meaning of a word" is a set. I treat punctuation signs as operators, i.e. notations of operations, over expressions, and due to my treatment of "meaning" as a set, the punctuation signs denote operations over sets. A text in a natural language is a sequence of words and punctuation signs and, therefore, it denotes a set, which can be calculated proceeding from the meanings of words which are sets.

With this treatment, the next question which appears naturally, is whether there is a small number of operations over sets through which all other operations over sets can be expressed? The answer turned out to be simple - such a binary operation was introduced by Tarski and Givant and is called "adjunction". Currently I am working on axioms of the algebra with this operation and constants to play the role of quantifiers. You might want to look into my questions - this this. and this

We can also discuss about this in more detail if you drop a message to my email indicated in my profile.

Improve this answer
$\endgroup$
1
  • $\begingroup$ This is for the moderator: can you please add the tag "set theory"? This can bring the question and my answer to attention of set theorists who could criticize my answer or add something useful. $\endgroup$
    – Ioachim Drugus
    Commented Aug 15, 2014 at 7:52

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .