Questions tagged [formal-proofs]

For questions about proofs within a formal system, such as natural deduction or Hilbert system.

741 questions
Filter by
Sorted by
Tagged with
60 views

Are any well known conjectures proved to be provable or falsifiable and yet not proved or falsified?

Are there any well known conjectures that are proved to be provable or falsifiable and yet not proved or falsified? Let me give an example. Consider the statement: "There is a natural number $x$ ...
45 views

datebase of formal mathematics

I am learning Logic and set theory, in the process I have made some formal proofs, but this is tedious with the traditional tools. Now, I am wondering if there exists some software or something like a ...
28 views

54 views

How do I prove Separation Schema within ZFC?

I am assuming consistency of ZFC throughout this post. Here are what I believe is correct, but please correct me if I am wrong: Every formal proof within ZFC uses finite fragment of ZFC. Separation ...
54 views

Should you avoid using the same variable name after existential elimination?

Existential Elimination (also called Existential Instantiation) says: $$\exists x[P(x)] \vdash P(c) \text{ For some c}$$ I was wondering whether it's bad form to use the same variable $x$ to ...
32 views

A simpler axiom for "induction" in untyped lambda calculus

I'm working on a weird proof system involving reductions in the lambda calculus. I'm thinking of including the following axiom: ...
59 views

Clarification regarding substitution in sequent calculus

Wikipedia's Sequent Calculus article states: $A[t/x]$ denotes the formula that is obtained by substituting the term $t$ for every free occurrence of the variable $x$ in formula $A$ with the ...
48 views

134 views

What is the exact, formal statement of Gödel's first incompleteness theorem?

I am looking for the explicit formal statement of Gödel's first incompleteness theorem in a formal language (which I assume is the language of first-order Peano arithmetic), permitting only the ...
28 views

Need help proving theorem for limits of multivariable functions (parabola approach)

Suppose I have a function $f:R^2 \to R$, where $R$ are the reals. I want to prove that $$\lim_{(x,y) \to (0,0)} f(x,y) = L \implies \lim_{x \to 0} f(x,mx^2) = L$$ by using a $(\varepsilon, \delta)$ ...
55 views

Prove Power Rule for Limits: $\lim_{x \to a} f(x)^{g(x)} = \left(\lim_{x \to a} f(x)\right)^{\lim_{x\to a} g(x)}$ [duplicate]

Suppose $\lim_{x \to a} f(x) = L$ $\lim_{x \to a} g(x) = M$ I would like to prove $$\lim_{x \to a} f(x)^{g(x)} = \left(\lim_{x \to a} f(x)\right)^{\lim_{x\to a} g(x)}=L^M$$ I thought this had ...
If a and b are positive integers satisfying $(a^{([2n-1]^2)}) \vert b^{([2n]^2)}$ and $b^{([2n]^2)} \vert (a^{([2n+1]^2)})$ prove a = b.
Recently encountered this question: If a and b are positive integers satisfying $(a^{([2n-1]^2)})\ \vert \ b^{([2n]^2)}$ and $b^{([2n]^2)} \ \vert \ (a^{([2n+1]^2)})$ prove $a = b$. My calculations ...