# Tagged Questions

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

267 views

### Proof of completeness and soundness of a proof system

As stated here, https://en.wikipedia.org/wiki/List_of_rules_of_inference, "a set of rules can be used to infer any valid conclusion if it is complete, while never inferring an invalid conclusion, if ...
74 views

### Decidability of certain first-order statements

Is it possible to construct an algorithm that can formally prove any statement in some countable first-order theory except for exactly those which aren't provable in the theory? Why or why not? Edit: ...
33 views

239 views

### Why is $n^2+4$ never divisible by $3$? [duplicate]

Can somebody please explain why $n^2+4$ is never divisible by $3$? I know there is an example with $n^2+1$, however a $4$ can be broken down to $3+1$, and factor out a three, which would be divisible ...
144 views

### role of definitions in proofs

Definitions are needed to define objects and such, however I am confused as to where definitions come from. I feel that they cannot be something that we arbitrarily define because simply saying ...
440 views

### When are two proofs “the same”?

Often, we find different proofs for certain theorems that, on the surface, seem to be very different but actually use the same fundamental ideas. For example, the topological proof of the infinitude ...
166 views

### How can I start to learn proof theory?

I'm studying computer science and I realized that I have problems in working with mathematical proofs. They are for example part of my class Formal Systems and Automata. I'm really interested in ...
71 views

### A provability puzzle

This is a problem I came up with on my own, and it has me stumped, so I am going to pose it as a kind of puzzle. Let $F$ be a formal proof system, recursively axiomatizable, with an acceptable Gö...
106 views

### What does it mean by Proving false

With respect to the recent finding of a bug in a Coq theorem prover in which false was proved, I'm asking this question. As a hobbyist studying maths, I'm ...
34 views

### Is the full strength of first-order logic needed for dealing with equational theories?

More specifically, if we have an equational theory $T$ (a set of equations understood as being implicitly universally quantified), are the (equational) consequences of $T$ that can be proved with ...
83 views

57 views

### Inference rule for Non-Empty Domains

I am currently experimenting with logic frameworks. I am basically using something along dependent types as in "Proof-assistants using Dependent Type Systems" by Henk Barendregt and Herman Geuvers. ...
87 views

### Is there any unreachable result?

I hope that this question is reasonable and make sense because I am not sure. Every theorem's proof is consisting of finite logical steps. Can a proof of the theorem require infinitely many ...
80 views

### Is the following derivation of Gödel's Paradox generalizable to an intuitionistic one using provability?

I will follow Goedel's original proof of Goedel's paradox located on pg. 264 of Hao Wang's A Logical Journey: From Gödel to Philosophy. With this in sight, and to also avoid confusion, I will also ...
72 views

### Can PA prove very fast growing functions to be total?

The Goodstein-sequence is a total function, but PA cannot prove this. Is this true for any other function with growth rate at least $f_{\epsilon_0}$ or are there functions growing at least as fast ...
85 views

### Proof in sequent calculus without cut

I met an exercise in Gaisi Takeuti, Proof Theory [Exercise 2.7, page 14]. How to construct a cut-free proof of$\ \forall xA(x)\rightarrow B\vdash \exists x(A(x)\rightarrow B)$, where A(a) and B are ...