# Tagged Questions

**1**

vote

**1**answer

296 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 ...

**2**

votes

**2**answers

574 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 ...

**3**

votes

**1**answer

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

**1**

vote

**0**answers

448 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 ...

**1**

vote

**3**answers

502 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 ...

**6**

votes

**5**answers

797 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 ...

**1**

vote

**2**answers

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

**6**

votes

**5**answers

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

**4**

votes

**1**answer

415 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 ...

**13**

votes

**3**answers

880 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 ...

**3**

votes

**1**answer

486 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 ...

**18**

votes

**8**answers

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

**3**

votes

**1**answer

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

**12**

votes

**5**answers

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

**4**

votes

**5**answers

869 views

### “Let $x \in A$”, beginning a proof of “$\forall x \in A$ …”, if A were empty [closed]

I work at a four-year teaching school, where we pride ourselves on teaching pure math, proof, and a rather obsessive carefulness of work. Recently I have been criticized for saying that "Let $x \in ...

**10**

votes

**3**answers

634 views

### Complete Extensions of First Order Logic (or Language)

Lindstrom's theorem states that any extension of FOL more expressible than FOL fails to have either compactness or Lowenheim-Skolem. When I first read Lindstrom's theorem my first reaction was: "Does ...

**5**

votes

**2**answers

594 views

### Are computable models sufficient?

What I mean is this. By downward Lowenheim-Skolem theorem, first-order formula Q is a always true iff it is true in every countable structure. But is there some first-order formula Q which is true in ...

**9**

votes

**10**answers

3k views

### The best text to study both incompleteness theorems

Hi!
What text on both incompleteness theorems you would recommend for beginner?
Specifically, I'm looking for the text with the following properties:
1) The proofs should be finitistic, in Godel's ...

**11**

votes

**3**answers

1k views

### Are there natural examples of mathematical statements which follow from consistency statements?

Motivation
One of the methods for strictly extending a theory $T$ (which is axiomatizable and consistent, and includes enough arithmetic) is adding the sentence expressing the consistency of $T$ ( ...

**19**

votes

**6**answers

2k views

### Complete mathematics

Hello, I would like to ask you if there is a mathematical theory, that is complete (in the sense of Goedel's theorem) but practically applicable. I know about Robinson arithmetic that is very limited ...

**6**

votes

**1**answer

832 views

### Using the multiverse approach to decide the law of the exluded middle?

Recently, in response to deciding the Continuum Hypothesis $CH$, Hamkins and Gitman have proposed consider a multiverse of set-theoretic universes, some in which $CH$ is true, some in which $\neg CH$ ...

**8**

votes

**3**answers

974 views

### Is there a formal notion of what we do when we 'Let X be …'?

This is likely an elementary question to logicians or theoretical computer scientists, but I'm less than adequately informed on either topic and don't know where to find the answer. Please excuse the ...

**0**

votes

**4**answers

282 views

### Deficiency of necessary conditions

Motivation
Consider the situation: You know that
every $x$ that has property $P$ must have property $Q$. $Q$ is a
rather strong condition but not strong
enough to fulfill $P$. What is ...

**10**

votes

**3**answers

3k views

### Bourbaki's epsilon-calculus notation

Bourbaki used a very very strange notation for the epsilon-calculus consisting of $\tau$s and $\blacksquare$. In fact, that box should not be filled in, but for some reason, I can't produce a \Box.
...

**6**

votes

**3**answers

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

**18**

votes

**11**answers

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

**51**

votes

**28**answers

6k views

### Can infinity shorten proofs a lot?

I've just been asked for a good example of a situation in maths where using infinity can greatly shorten an argument. The person who wants the example wants it as part of a presentation to the general ...

**6**

votes

**2**answers

768 views

### “Requires axiom of choice” vs. “explicitly constructible”

I think I'm a bit confused about the relationship between some concepts in mathematical logic, namely constructions that require the axiom of choice and "explicit" results.
For example, let's take ...