# Questions tagged [formal-proofs]

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

537 questions
Filter by
Sorted by
Tagged with
64 views

### Peano Arithmetic: How would this formalized statement be correct?

Using Peano Axioms I have formalized the following: x is the square of an odd prime number For some odd prime number x' , x is its square IF x is some odd prime number, THEN x is the square of x' IF ...
411 views

### Natural deduction predicate logic for equality

I have to use natural deduction on the following 2 sequents: $$t_1=t_2 \vdash (t+t_1)=(t+t_2)$$ $$(x=0)\lor ((x+x)>0)\vdash (y=(x+x))\to ((y>0)\lor (y=0+x))$$ At first I thought that the first ...
865 views

### Di-graphs handshaking lemma proof

I am starting to learn about graph theory and in the study of the graph theory proofs, I have inevitably come across the handshake lemma for undirected graphs which is a quite straight forward proof, ...
773 views

### Natural deduction: negation of quantifiers

How can I show that $\lnot \exists x P(x) \vdash \forall x\lnot P(x)$ ? Because I want to show: $\lnot \exists x (P(x) \lor R(x)) \vdash \forall x \lnot R(x)$ My idea: maybe a proof by ...
393 views

### Suppose that $a$ and $b$ are natural numbers such that $a^2 = b^3$. Prove that if $4$ divides $b$, then $8$ divides $a$.

Proposition: Suppose that $a$ and $b$ are natural numbers such that $a^2 = b^3$. Prove that if $4$ divides $b$, then $8$ divides $a$. Proposed Proof: Assume $4$ divides $b$ then $b = ?$ for some ...
553 views

### Existential and Universal Equivalence Proof

Taking ¬∀x:X.r≡∃x:X.¬r Is there a way of actually formally proving this? Not implementing it but proving how to go from a negated universal quantifier to a an existential with a negated element... ...
55 views

### Determine all theta satisfying an expression

For what values of θ does the following equation hold $$∏^{100}_{k=1} [\cos (kθ)+ i \sin (kθ)] = 1.$$ We can assume $∑^n_{i=1} i =\frac{n(n+1)}{2}$ for all natural numbers $n$.
149 views

### (Another) Proof within Hilbert system

I know there are plenty of similar posts around, but I could not find an answer to this particular question (and I've been at it for two days now, getting nowhere). The proof I'm trying to construe in ...
49 views

123 views

### Question regarding using the natural deduction system

I have the following: Premise: ((V → ¬W) ∧ (X → Y)) Premise: (¬W → Z) Premise: (V ∧ X) |- (Z ∧Y) The part I want to know is how do I go about separating ...
184 views

### Hilbert-calculus, formal proof

I have to give a formal proof in the Hilbert calculus for $(\forall x\,\,\phi)\rightarrow (\forall y\,\, \phi\frac{y}{x})$, if $x$ is free for $y$ in $\phi$ and $y$ is not free in $\phi$. ...
371 views

### Axioms of Newtonian Mechanics

Axiomatically speaking, could Newton's laws be derived (as theorems) from the conservation of momentum and energy -- along with a few suitable definitions of things like an inertia frame and force? ...
Many books proves theorems by performing one proof step and using this step as a scheme they say by repeating this step $l$ times we prove that... I wonder whether there is some formal meta-theorem ...
Let's have an vector of natural numbers $[v_1, ..., v_N]$ my goal is to show that $$\sum_{i=1}^{N-1}|v_i - v_{i+1}| \ge v_{max} - v_{min}$$ where $v_{max} = \max_{i\in1...N}(v_i)$ and \$v_{min} = \...