Questions tagged [formal-proofs]

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

Filter by
Sorted by
Tagged with
1
vote
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 ...
1
vote
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 ...
1
vote
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, ...
2
votes
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 ...
0
votes
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 ...
1
vote
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... ...
0
votes
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$.
1
vote
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 ...
0
votes
2answers
49 views

Prove $(A\cup C=B\cup C)\implies(A\mathbin{\Delta} B\subseteq C)$ [duplicate]

My full problem is: Suppose $A$, $B$, and $C$ are sets. Prove: $A\mathbin{\Delta}B \subseteq C\text{ iff }A\cup C=B\cup C$. I've proved my case one, which is that $(A\mathbin{\Delta} B\subseteq C)\...
0
votes
1answer
20 views

Multiplication in $\mathbb{N}$ from two simple laws

From Barry Mazur's Imagining Numbers: (particularly the square root of minus fifteen), p. 97: Suppose that you have some unknown operation that allows, as its "input," any two positive whole ...
0
votes
3answers
3k views

If $x_n:=\sqrt{n}$, show that $(x_n)$ satisfies $\lim|x_{n+1}-x_n|=0$, but that it is not a Cauchy sequence.

If $x_n:=\sqrt{n}$, show that $(x_n)$ satisfies $\lim|x_{n+1}-x_n|=0$, but that it is not a Cauchy sequence. We see that $$|x_{n+1}-x_n|=|\sqrt{n+1}-\sqrt{n}|=|(\sqrt{n+1}-\sqrt{n})\cdot\frac{\sqrt{n+...
1
vote
2answers
129 views

Propositional Logic - Formal Proofs using natural deduction

I have a question I have come across in an old exam paper which I am trying to work through. It states that a formal proof must be given using the rules of natural deduction Now generally what I do ...
-1
votes
1answer
555 views

Prove f(indexed intersection Ai) is a subset of indexed intersection Ai.

Here is what I'm working on: I started with: I'd love to see how to finish the proof. Thank you for your time.
2
votes
2answers
98 views

How to give a formal proof for $ \exists \space x\space \forall \space y(P(x) \rightarrow P(y))$ in fitch

To practice for my exams, my teacher gave us several exercises to practice but didn't supply us any answers. Now after looking at this problem for 2 nights I have no idea left on how to solve it. If ...
0
votes
1answer
97 views

Order of Parentheses is Irrelevant: Metatheorem?

Here was shown by induction that the order of parentheses is irrelevant when associativity is verified. Question: Would this be a metatheorem about the formal language (say, of ZF) where the ...
1
vote
2answers
97 views

Derivation of ∀x (A(x) → B(x)) → (∀x A(x) → ∀x B(x)) in Hilbert style system

While it's quite easy to give a derivation of $$\forall x ~ \bigg(A(x) \implies B(x)\bigg) \implies \bigg(\forall x~ A(x) \implies \forall x~ B(x)\bigg)$$ in a system that contains the rule of ...
0
votes
1answer
95 views

Why aren't definitions well formed formulas?

Why aren't definitions well formed formulas? For instance, the definition of an additive inverse is: "Let $x \in \Bbb Z$. Then the additive inverse of $x$ is $y \in \Bbb Z$ such that $x+y=0$". Why ...
2
votes
2answers
303 views

Proof about Clavius's Law

Clavius's Law claimed: $(\neg A \rightarrow A) \rightarrow A$ What it is the proof about it in Deductive System $L$? Deductive System $L$ is: L1: $A \rightarrow (B \rightarrow A)$ L2:...
1
vote
1answer
1k views

Prove that if $\lim(x_n) = x$ and if $x > 0$, then there exists a natural number $M$ such that $x_n > 0$ for all $n\ge M$.

Prove that if $\lim(x_n) = x$ and if $x > 0$, then there exists a natural number $M$ such that $x_n > 0$ for all $n\geq M$. I'm not quite sure what to do with this one. By definition I know ...
1
vote
3answers
2k views

Do odd numbers have only odd divisors?

Is it true, that odd numbers have only odd divisors? If yes, what would a formal proof look like?
0
votes
1answer
170 views

How to give a formal proof for this particular case

When making exercises for my Introduction to Logic course, I came across the following question which I can't seem to solve. The question is: Give a formal proof for ¬(A ∧ (¬A ∨ B)) ∨ B. Do not ...
0
votes
1answer
34 views

Flipping Signs Using Arithmetic Axioms

This may be a dumb question, but I'm in a computer science class called Applied Logic, where we have to develop formal proofs, and I'm very inexperienced with them. So my question is: Is there a way ...
2
votes
1answer
124 views

Tricky predicate logic problem

I'm having a hard time proving that this is a valid argument $Premise 1: (Ǝx)Kx→(\forall x)(Lx→Mx)$ $Premise 2: Kc • Lc$ $Conclusion: Mc$ I am getting confused with all the existential/universal ...
1
vote
1answer
629 views

Proving that $P(X=Y) = 0$ for any two continuous random variables

I have the following question to prepare for a lecture at Uni but I've been stuck on this for a long time: Question: Let $Z$ and $V$ be independent with distribution $U[0,1]$. Show that $P(...
0
votes
1answer
460 views

Why does the 1st player in this subset take-away game always have a winning strategy?

This is a HW problem of mine that I cannot, for the life of me, figure out. There is a take-away game where there are a number of elements A, and the person that wins is that last person to remove a ...
4
votes
3answers
212 views

Is the following a correct logical proof?

A → (F ∧ P) ~A → (S ∧ R) ~R ∴ P     assume ~P         assume A         F ∧ P (1, ...
0
votes
2answers
114 views

Show that $A \lor B ⊢ B \lor A$

Prove the following derivability claim using only our primitive rules: $A \lor B ⊢ B \lor A$ I know this can be attributed to the commutative property, but I'm not exactly sure how to prove this ...
-1
votes
1answer
42 views

prove [(¬M∧R)∧Q |- Q∨T [closed]

prove [(¬M∧R→Q |- Q∨T really confused :(
0
votes
1answer
120 views

Solve the following proof : M |- M ∨ {[(Z∨S) ∧ (¬] → (C↔D)}

Solve the following proof : M |- M ∨ {[(Z∨SC↔D)} I try to proof above question with the following (F⋀Z)⋀ → (C↔D) 1 (F⋀Z)→C 2 F⋀Z 1⋀E 3 F 2⋀E really confused :( this examples
1
vote
0answers
38 views

Logical systems and formal proof

Is there any good book dealing with various formal systems and a book for formal proofs. Or atleast some good notes. This page on wikipedia also says: 'This article needs attention from an expert in ...
0
votes
1answer
187 views

Proof of deduction theorem without induction

Can we prove deduction theorem without using inductive argument. Using MP and following axiom schema: 1) A⇒(B⇒ A) 2) [A⇒(B⇒C)]⇒[(A⇒B)⇒(A⇒C)]
5
votes
1answer
308 views

Formal proof of $(A\lor B)∨C \leftrightarrow A\lor(B\lor C)$

$A\lor B$ by definition $\neg A\implies B$ Deduction rules: $A\implies (B\implies A)$ $(A\implies (B\implies C))\implies ((A\implies B)\implies(A\implies C))$ $(\neg B\implies \neg A)\implies(A\...
2
votes
1answer
373 views

$A⇒(B \lor C)$ and $[(A \Rightarrow B) \lor (A \Rightarrow C)]$

[(A⇒ B∨C)] ⇒ [A⇒(¬B⇒C)] ⇒[(A⇒¬B)⇒(A⇒C)] ⇒ [¬(A⇒¬B)∨(A⇒C)]⇒[(A∧B)∨(A⇒C)] [(A⇒B)∨(A⇒C)] is equivalent to A⇒(B∨C). Can I prove [(A∧B)∨(A⇒C)] ⇒ [A⇒(B V C)]? or is there problem in the proof above ...
1
vote
2answers
307 views

How to show that $[(p \rightarrow q) \rightarrow r] \Rightarrow [p \rightarrow (q \rightarrow r)]$

To show that $[(p \rightarrow q) \rightarrow r] \Rightarrow [p \rightarrow (q \rightarrow r)]$ without using a truth table. That is, using logical laws.
1
vote
3answers
5k views

How to prove a logical implication?

Question: Using the Laws of Logic and Rules of Inference, prove that $$(\neg(\neg p \lor q) \lor r) \Rightarrow (\neg p \lor (\neg q \lor r)).$$ I just don't know how to apply the Rules of ...
-3
votes
1answer
79 views

Is this mathematical statement? [closed]

$\{\text{integers $n$ such that $n$ is even}\}$ It can be true/false so does that mean it's proposition/mathematical statement?
3
votes
3answers
625 views

Prove that there are no positive integers $a$ and $b$, such that $b^4 + b + 1 = a^4$

So I've been trying to solve this problem for a couple of days now. What I've come up with is this: By way of contradiction, assume that there are positive integers a and b such that $b^4 + b + 1 = a^...
2
votes
1answer
109 views

Strange sum of random variables

So guys, I'm having this hard proof to solve in probability. I don't really know how to tackle it! Hope that someone can help. Let $\{Z_i\}_{i\in\mathbb{Z}}$ be i.i.d. random variables with zero mean ...
2
votes
2answers
99 views

Prove using Hilbert calculus $\forall x(Px\rightarrow x\equiv a)\vdash Pb\rightarrow Pa$, formal proof.

Prove: $\forall x(Px\rightarrow x\equiv a)\vdash Pb\rightarrow Pa$ Using Hilbert Calculus Format of solution: Step (my understanding) Solution: (1) $\forall x(Px\rightarrow x\equiv a)\vdash Pb\...
1
vote
1answer
72 views

Context-free language or not

It is language: $L = \left\lbrace a^ib^jc^kd^l \mid i+k < j+l+3 \right\rbrace$ Is it context-free or not? I have two versions: 1)Pumping lemma(refute): get a word $uvxyz = aabcd$ if $i=2$ we get ...
0
votes
3answers
137 views

Prove that the set of sentences $\{A \land (B \lor C), (\lnot C \lor H) \land (H \rightarrow \lnot H), \lnot B\}$ is inconsistent

Prove that the set of sentences $\left\{A \land (B \lor C), (¬C \lor H) \land (H \to \lnot H), \lnot B\right\}$ is inconsistent. I'm confused because it doesn't look like any of the forms I've ...
3
votes
3answers
154 views

A Natural-Deduction proof of $ \{ \neg N,\neg N \to L,D \leftrightarrow \neg N \} \vdash (L \lor A) \land D $.

I would like to prove $\{ \neg N,\neg N \to L,D \leftrightarrow \neg N \} \vdash (L \lor A) \land D $. My work until now is as follows: $$ \begin{array}{l|ll} 1 & \neg N ...
1
vote
2answers
516 views

Prove that the following argument is valid

I'm asked to show that the following argument is valid: P1) $[E \lor (L \lor M)] \land (E \leftrightarrow F)$ P2) $L \rightarrow D$ P3) $D \rightarrow \neg L$ C) $E \lor M$ Here is my work (so ...
2
votes
2answers
465 views

Natural deduction proof: {A → B, B → (C & D), ¬C v ¬D} ⊢ ¬A

Prove using natural deduction: $ {A → B, B → (C \land D), ¬C \vee ¬D} ⊢ ¬A$ Our work (so far): $1- A → B$ $2- B → (C \land D)$ $3- ¬¬A$ $4- A$ $5- B$ (from 1,4) $→E$ $6- B$ $7- C \land D$ (...
1
vote
1answer
49 views

How to prove this inference in sequent calculus?

I'm using the event-B prover to proove some proof obligations. I have a relation representing a $table: table \in 1‥n \to \mathbb{N}$. I know that in a sorted table the following property is true: $\...
2
votes
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 ...
1
vote
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$. ...
4
votes
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? ...
1
vote
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 ...
1
vote
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} = \...