Say a proof for the consistency of a formal system (proved within the formal system) is known. There are two possible cases: 1. the formal system is consistent and it can be and ha …

Consider the first order theory of fields, whose language contains constant symbol $0$ for additive identity, constant symbol $1$ for multiplicative identity, function symbol $A(x, …

Consider the following optimization problem. Let $n, m \in \mathbb N$ and $0 < p_1 \leq \ldots \leq p_n ~ (p_i \in \mathbb R)$ be constant. The feasible region is described by a …

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 mea …

In Gentzen's sequent calculus, a formal proof is described by a tree, with each node representing the sequent obtained from the child(ren) by applying a given inference rule. If n …

I just received my first assignment for a mathematical proofs course I am taking this year. We just began the course, and we have so far only covered examples of proofs (how to pro …

Less tongue in cheek, is it known what the relative consistency is for theorems proved with an automatic theorem prover? Of course this depends somewhat on what assumptions one mak …

Hello everyone. I am not a mathematician but recently I was thinking about one of Kimberling's questions he posted here: http://faculty.evansville.edu/ck6/integer/index.html , i.e …

I understand how to find a limit. I understand the concept of the epsilon delta definition of a limit. Can you walk me through what we're doing in this worked example? It is fro …

Technically, it is possible to prove anything in Coq proof assistant [1] (on at least Linux) due to a programming feature (or bug). This seems tractable when validating large proof …

Suppose we have a sequence $a_n$ given by some combinatorial formula, e.g. involving a sum of n terms (like ${n \choose k}^{10}3^{-k}$ etc.). Sometimes it is plausible that there …

I really need an example of some non-trivial proof (not related directly to set theory) that uses only logical symbols (no "words"). Thanks.