# 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
2answers
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 ...
2answers
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 ...
1answer
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, ...
1answer
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 ...
3answers
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 ...
0answers
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... ...
1answer
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$.
0answers
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 ...
2answers
49 views

1answer
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 ...
1answer
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$. ...
0answers
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? ...
1answer
77 views

### Iterating proof step

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 ...
1answer
719 views

### Proof that minimum of sum of absolute differences is greater or equal of max value minus min value

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} = \...