# Tagged Questions

303 views

### Is there any current development of a first order formalization of metamathematics?

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 ...
594 views

### Meta$^{n{-}th}$ mathematics [duplicate]

Metamathematics has a reasonably clear connotation, enough to have a Wikipedia page, with Gödel, Tarski, and Turing playing leading roles; Kleene's book (Introduction to Metamathematics (Amazon ...
308 views

### Godel 's Ladder: Undecidable PI_N sentences for N =2, 3, …

After Godel's groundbreaking results, a plethora of $\Pi_1^0$ undecidable arithmetical sentences have been found by many authors. But what about $\Pi_n^0$ for $n=2,3,.....$ ? There are, to my ...
450 views

### Arguments against Reductio ad Absurdum [closed]

Could Reductio ad Absurdum not be consireded a valid proof method? Are there any compelling arguments against it, or at it's favor? I feel like I am assuming some metamathematical hypothesis about my ...
503 views

### Applicability of Deduction theorem to Primitive recursive arithmetic [closed]

Hello. I already asked the question here. The main point is that I tried to prove in Primitive recursive arithmetic (PRA) the totality of the Ackerman function, and I found, that the single thing ...
798 views

### Formal proof of Con(ZFC) => Con(ZFC + not CH) in ZFC

Is it possible to prove $Con(ZFC) \rightarrow Con(ZFC + \neg CH)$ purely within ZFC? To prove this (using forcing) one seems to need a countable transitive model of ZFC. The texts I am reading avoid ...
1k views

### An undergraduate's guide to the foundational theorems of logic [closed]

How would you explain one of these theorems in the foundations of mathematics to a fellow colleague outside the field of logic (or rather to an undergraduate mathematics student) handwaving over the ...
2k views

### A meta-mathematical question related to Hilbert tenth problem

I am reading Bjorn Poonen's very nice survey on Hilbert's Tenth problem (http://www-math.mit.edu/~poonen/papers/uniform.pdf), and while I believe I understand the mathematics well, I have widespread ...
416 views

### Does ZF prove that a finite subtheory axiomatizes it over transitive proper class models?

If $\text{ZF}$ is consistent, then it is not finitely axiomatizable. For if $\Gamma$ is a finite axiomatization, then $\text{ZF}$ proves by reflection that $\Gamma$ has a set model, and hence (since ...
883 views

### Are there examples of nonconstructive metaproofs?

This came up in a question on the xkcd forums. Is it possible to have a nonconstructive metaproof, i.e. a proof that there exists a proof in some formal system which does not construct said proof? Are ...
488 views

### Feferman's extensional and intensional applications of the method of arithmetization

At the very beginning of Feferman's Arithmetization of metamathematics in a general setting it can be read: The method of arithmetization, as developed by Gödel[10], exploits the possibility of ...
3k views

### Proofs of Gödel's theorem

I am interested in different contexts in which Gödel's incompleteness theorems arise. Besides traditional Gödelian proof via arithmetization and formalization of liar paradox it may also be obtained ...
460 views

### Should consistency be considered as a concept in the metatheory?

Consider the statement: "ZFC is consistent". Normally this is considered at first sight as a statement in the metatheory. But if we follow Kunen's (informally) description of what the metatheory is ...
1k views

### Consistency strength needed for applied mathematics

Given that we can never proof the consistency of a theory for the foundations of mathematics in a weaker system, one could seriously doubt whether any of the commonly used foundational frameworks (ZFC ...
877 views

496 views

### What assumptions and methodology do metaproofs of logic theorems use and employ?

In logic modules, theorems like Soundness and completeness of first order logic are proved. Later, Godel's incompleteness theorem is proved. May I ask what are assumed at the metalevel to prove such ...
2k views

### Are there any good nonconstructive “existential metatheorems”?

Are there any good examples of theorems in reasonably expressive theories (like Peano arithmetic) for which it is substantially easier to prove (in a metatheory) that a proof exists than it is ...