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

818 questions
Filter by
Sorted by
Tagged with
40 views

### Odd perfect number importance [closed]

If someone proved the non existence of an odd perfect number how important would it be to the mathematics field as well as their career?
64 views

### First order logic natural deduction problem

I am struggling with a particular case in the (inductive) proof of Theorem 2.8.3 (i) of Logic and Structure by Dirk Van Dalen ($c \neq x$ in the Theorem statement is a variable) The cases when we ...
24 views

### Every provably recursive function in PA is bounded by a Hardy function

The following lemma and proof are from Takeuti's Proof Theory (2nd edition, pp. 126-127), I've highlighted the problematic part in blue: How does Takeuti get this inequality? If the proof $x$ is not ...
52 views
+50

### Characterization of provably recursive functions in PA

This concerns Takeuti's Proof Theory: the book contains a lot of wonderful material, but the presentation is sometimes lacking (and so many typos!). At least that has been my experience so far, ...
71 views

### While using the method of proof by contradiction, are we “assuming” consistency?

I am aware of threads here and here which asks something similar. However, I had something very specific to ask under the same context. I have a very elementary question about the connection between ...
85 views

149 views

66 views

68 views

### Removing an Antecedent

Suppose $A \vdash B$ where $A$ is of the form $\forall x\ P(x) \rightarrow \ ...$ and where $B$ does not include the predicate $P$. My intuition is that this implies that $B$ is a tautology, as ...
86 views

### self-contained vs. non-self-contained notions of realizability

There seem to be two notions of realizability in literature, where in one case the realization of a formula is fully self-contained with respect to providing a proof object for the given formula, ...
78 views

### Proof-theoric ordinal of ETCS

What is the proof-theoric ordinal of Lawvere's elementary theory of the category of sets?
99 views

### Theorems & proof by contradiction

The following formula seems to be regarded as the essence of proof by contradiction: p → (q ∧ ~q) ⊢ ~p Or perhaps this one: ~p → (q ∧ ~q) ⊢ p If this is the case, what are the mathematical ...
42 views

49 views

### Hilbert calculi for First-Order Logic

I'm a bit confused about the Hilbert-style axiomatization of first-order logic. More precisely, I am a bit confused about completeness w.r.t. to Hilbert-calculi. A complete Hilbert-style calculus I am ...
121 views

### Takeuti's proof of the Second Incompleteness theorem

I am reading Gödel's second incompleteness theorem in Takeuti's "Proof theory" (page 85), and I don't understand how he derives the sequent  \operatorname{Con},\operatorname{Pr}(\ulcorner A_G\...
36 views

### Does the failure of the substitution law of logical equivalents entails inconsistency?

Does the failure of the substitution law of logical equivalents entails inconsistency? By "logical equivalents" I mean equivalences that are logically provable. For example: \begin{equation} \tag{1} (...
65 views

### Developing model theory in the language of PA

Is it possible to develop model theory for models of $PA$, inside $PA$ itself (augmented with consistency raising assumptions such as $Con(ZFC)$ if necessary, but still in the language of $PA$)? What ...
44 views

### Bourbaki Proof in First Consequences? Use of Not?

In Bourbaki Theory of Sets English (c) 1970 Section 3.2 C6 there is a first consequence that I have questions about. I have attached images of the text here. My question is: We are told that A, B, ...
66 views

### Problem with a proof ( sequent calculus)

I have to proof this sequent: ⊢ (p → q) → ((q → r) → ((p v q) → r))) i ve already done sth like this ...
36 views