# Questions tagged [proof-theory]

Proof theory is an area of logic that studies proof as formal mathematical objects. If you'd like advice on the presentation of a proof you have in draft, use proof-writing instead. If you'd like feedback on its validity, use proof-verification. If none of the above apply, you do not need a proof-* tag.

907 questions
Filter by
Sorted by
Tagged with
73 views

### Natural Deduction: An unusual(?) presentation

1. Context On page 241 of their paper Natural deduction and coherence for weakly distributive categories Blute et al give the right- and left-introduction rules of multiplicative conjunction for (...
60 views

### Proofs and Types: Girard's remarks on Theoretical Computing

In the first chapter of Girard's Proofs and Types (1989) one finds the following remarks: Theoretical Computing is not yet a science. Many basic concepts have not been clarified, and current work in ...
2k views

### Are there are any inherent mathematical reasons some proofs are difficult?

This is not a complaint about my proofs course being difficult, or how I can learn to prove things better, as all other questions of this flavour on Google seem to be. I am asking in a purely ...
1 vote
83 views

### Is consistency with the $\omega$-rule absolute to $\omega$-models?

According to Wikipedia, a theory $T$ that interprets arithmetic is consistent with the $\omega$-rule if and only if it has an $\omega$-model. That would mean that consistency with the $\omega$-rule is ...
1 vote
111 views

### Why Hilbert's 24th Problem is unsolvable?

Hilbert's famous 24th problems handles the problem of the simplest possible proof of a mathematical statement, in a nutshell. It is said that there are a few problems with this problem. First of all, ...
15 views

### Conservativity and proof-theoretical ordinals

I assume the second-order arithmetical theory $T$ in concern is consistent and r.e. The most well-known kind of proof-theoretical ordinal $\|T\|$ of $T$ is the $\Pi_1^1$-ordinal, defined as $\|T\|=\{$...
1 vote
21 views

135 views

### Why do we need ordinal representation systems?

Trying to learn about ordinal analysis and I keep seeing the concept of the natural ordinal representation system, for representing ordinals as relations on N. In particular the definition of an ...
35 views

### Is the intuitionistic absurdity rule $\bot E$ necessary to prove that a theory $\mathcal{T}$ is consistent?

In Elements of Intuitionism (p. 145), Dummett wrote: Cut-elimination is directly connected with establishing consistency, and was so intended by Gentzen. Given the equivalence of N and L, acceptance ...
1 vote
73 views

### Different textbooks, different formulations of the Deduction Theorem: sometimes the formula in the antecedent need to be closed, sometimes not. Why? [duplicate]

For clarity, let me take two examples: Shoenfield's Mathematical Logic, and Enderton's A Mathematical Introduction To Logic. Well, in those texts we have two different Deduction Theorems (we are in ...
119 views

### Open problems in Proof theory and Logic

There are numerous questions in the same form: "What are some open problems in mathematical logic". So for this we know: Shelahs "Logical Dreams" Logical Dreams Friedmans "102 ...
1 vote
93 views

80 views

### Are there any proof-size-aware logics?

I'm aware of provability logics which have a notation $\square P$ for "$P$ is provable", but I'm not aware of one which is more 'fine grained' and has a notion of proof term size (e.g. with ...
134 views

### Proof of nonexistence of purely algebraic proof of the Fundamental Theorem of Algebra.

There have been questions before on Math SE about whether there is a purely algebraic proof of the FTA. But as far as I know, nobody has proven rigorously that there is no purely algebraic proof. Has ...
1 vote