The proof-complexity tag has no wiki summary.

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

**15**

votes

**3**answers

793 views

### Finite versions of Godel' s incompleteness

Assume you have some notion of proof complexity: for instance, at the basic level, the length of a proof, or the number of symbols used, take your pick (there are more involved measures, but for sake ...

**3**

votes

**1**answer

574 views

### Proof system with same complexity as “informal mathematics”?

The Completeness Theorem in first-order logic states that any mathematical validity is derivable from axioms. Hence, any informal mathematical proof (which is rigorous) can be translated into a formal ...

**3**

votes

**2**answers

519 views

### Measure of progress towards a proof

Can one define some measure of progress towards a proof of a statement? I'm not sure if it's even possible for general first order logic statements so let's restrict ourselves to propositional ...

**3**

votes

**1**answer

470 views

### Proof systems and their hierarchy

Why ZFC is placed in top of the proof system hierarchy? How it can p-simulate other systems?

**3**

votes

**1**answer

102 views

### Results where complexity bounds implies finite number of test cases

We have all been there, when a formula works for the first 30 parameters,
but it is not sufficient for a proof. My question is where one can actually just check a finite number of cases, to conclude ...

**2**

votes

**0**answers

196 views

### Oracle separating FIP for bounded-depth Frege from FIP for Frege (and hardness conditions on DDH)

Is there an oracle such that in the relativized world, bd-Frege (bounded depth Frege propositional proof system) has FIP (feasible interpolation property) but Frege does not have FIP?
Such an ...