# Questions tagged [formal-proofs]

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

531 questions
Filter by
Sorted by
Tagged with
43 views

### Prove By Induction $U_n=2^n+1.$

Given that $U_1=3,U_2=5,$ and $U_{n+2}-3U_{n+1}+2U_n=0.$ Show that $U_n=2^n+1.$ I'm stuck at showing that if $P(n+1)$ is true if $P(n)$ is true.
106 views

### Prove 𝑃′⋀(𝑃⋁𝑄)→𝑄 - How?

I'm going a course in computer science math, and I came across an exercise that is the following: Use the rules of equivalence and/or inference to prove: $\lnot P \land (P \lor Q)\rightarrow Q$...
96 views

### Implication Introduction in reverse way

In Gentzen system, there is an inference rule such that one can deduce $\Gamma \to \Delta, \mathfrak{A} \supset \mathfrak{B}$ from $\Gamma, \mathfrak{A} \to \Delta, \mathfrak{B}$. Can we, in ...
104 views

### How do I find the contradition in this indirect proof?

I'm utterly stuck with no where to go. The assignment is to complete the indirect proof. I'm stuck on the following step, and have no clue how to proceed. Where do I go? Also, pardon the poor ...
50 views

When reading the following problem, do you assume that each premise is true? So since number 2 states ¬ B am I to assume that ¬ B is true? Which would mean B is false? A ∨ C → D Premise ¬ B ...
63 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 ...
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 ...
339 views

### Meaning of $\dashv\vdash$

I was looking at ProofWiki's articles 'Definition:Equidistance' and 'Definition:Between (Geometry)'and came across the symbol '$\dashv\vdash$.' What does it mean?
56 views

### Suppose $(s_n)$ is a sequence such that $\lim_{n \to \infty} s_n = 7$ and $s_n < 7$ for all $n\in \Bbb N$.

Suppose $(s_n)$ is a sequence such that $\lim_{n\to \infty} s_n = 7$ and $s_n<7$ for all $n\in \Bbb N$. Let $S=\{s_n\mid n\in\Bbb N\}$, i.e., let $S$ be the set of all values that appear in the ...
116 views

96 views

### Trouble understanding proof to $\vdash ((\neg(\phi\rightarrow \psi))\rightarrow\phi)$?

I am having trouble understanding the natural deduction proof of $\vdash ((\neg(\phi\rightarrow \psi))\rightarrow\phi)$ (question 2.6.2 (b)) in Hodges and Chiswell's Mathemaical Logic. The natural ...
107 views

### (P → Q) v (Q → R), Fitch-style proof

I'm trying to construct a Fitch-style proof for $(P \to Q) \lor (Q \to R)$ using reductio ad absurdum and the introduction and elimination rules for conjunction, disjunction, and implication. I'm not ...
88 views

### How much of first order statements can we derive purely from the definitions in arithmetic?

I didn't know how to formulate a more clear title for this question: Take arithmetic to be the structure $\mathcal N= (\mathbb N, \sigma, +,•, 0,1)$ with its standard interpretation. When I use the ...
224 views

1k views

### help with some Hilbert style proofs in a propositional logic axiom system.

I'm very new to classical propositional logic, and my lecturer is using a system with the following axioms: A1. X→(Y→X) A2. (X→(Y→Z))→((X→Y)→(X→Z)) A3. (¬Y→¬X)→(X→Y) Use uniform substitution and ...
44 views

### What does the following statement in first order logic translate to in english?

∃x∃y (yRf(x) ---> xRx) I have to prove that this is a tautology formally, but I don't even understand what it means.. Are R and f arbitrary relations / functions, or are we free to choose them? Is f ...
395 views

### Can we prove if ⊢ (α → β) and ⊢ (¬α → β) then ⊢ β in L0?

The system L0 is defined as follows: Axioms: A1 (α → (β → α)) A2 ((α → (β → γ)) → ((α → β) → (α → γ))) A3 ((¬β → ¬α) → (α → β)) The only rule of inference is Modus Ponens: MP From α and (α → β) ...
722 views

### Are these conditional statements true?

This chapter is brewing in me a dislike for my Math book, sort of. It seems the reasoning applied to solve a particular problem is different from that used to solve another one. I've come with my ...
1k views

### Formal proof in Fitch - How to prove contradiction in a biconditional?

I am asked to derive the conclusion $\bot$ from the premise: $P\leftrightarrow \neg P$ This is in the logic system of Fitch, the rules that I am allowed to use can be found here. I may not use ...
1k views

### Given ∃y.∀x.p(x,y), use the Fitch system to prove ∀x.∃y.p(x,y).

I have a problem to solve this question. I thought I should eliminate the existential first but it seems not work..Not sure how to use the existential condition to prove the later one. Here's the ...
98 views

### Deduction of $(\exists x Px \rightarrow \forall y Qy)\rightarrow \forall z(Pz \rightarrow Qz)$

Deduction of $(\exists x Px \rightarrow \forall y Qy)\rightarrow \forall z(Pz \rightarrow Qz)$ My try: There exists a deduction as follows. The Deduction and Generalization Theorems together imply ...
176 views

### Deduction of $\vdash \forall x \phi \rightarrow \exists x \phi$

I can show that $\forall x \phi \vdash \exists x \phi$ through a direct deduction as follows, using axioms as defined in Enderton $(\forall x) \phi$ by hypothesis. $(\forall x) \phi \rightarrow \phi$...
265 views

I want to prove double negation introduction in sequent calculus using the most basic rule set. That is what I want to prove: from the sequent $$\Gamma \rightarrow\Phi,$$ the sequent $$\Gamma \... 1answer 51 views ### Is this an onto function? Is f(m,n) = m^2 - 4 an onto function for a function that goes from Z x Z -> Z (Where Z means the set of all integers). I think it is an onto function, but I am not sure how to go about proving it. ... 1answer 1k views ### Prove ⊢(a→b)→(¬b→¬a) in HPC proof system As stated in the title, I am asked to give a proof that: ⊢(a→b)→(¬b→¬a) Using a system with the Modus Ponens rule, and the following axioms: A1: a→(b→a) A2: (a→(b→c))→((a→b)→(a→c)) A3: (¬b→¬a)→(a→b)... 2answers 194 views ### Examples of non-trivial proofs in deductive systems I want to get a better grasp of what a rigorous formal proof is. So I was hoping to find proofs of interesting results using natural deduction or Hilbert system or similar. The "interesting result" ... 2answers 150 views ### Product of negative numbers [duplicate] Why is a negative number multiplied by a negative number a positive number? I'm trying to know what does multiplying by a negative number mean. If you think of multiplication as a "groups of" (3 \... 1answer 38 views ### How to prove the group S_4 of permutations (or bijections) has no elements of order 12? I know there are no elements of S_4 with order 12 from a list of the elements of S_4 but how can I prove it without listing all the elements with their orders? 1answer 107 views ### A method of proof by contradiction for independence? Is there a way to proof to prove this for independence using the method of contradiction ? Let A_1, A_2, and A_3 be events, and let B_i represent either A_i or its complement A^c _i. Then ... 1answer 50 views ### For all real a, b, order the averages. I'm taking a proofs class and the textbook says to do this problem: For all real  a, b > 0 , show  \dfrac{2ab}{a + b} \leq \sqrt{ab} \leq \dfrac{a + b}{2} \leq \sqrt{\dfrac{a^2 + b^2}{2}}  ... 2answers 405 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 ... 2answers 126 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 ... 2answers 289 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. 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. ... 1answer 305 views ### Orthogonal Vectors and Projections Given that u and v are orthogonal unit vectors in R^3, prove that for all x, where x is a vector in R3 as well, that: perp_{u×v}(x)=proj_u(x)+proj_v(x) So far, I've tried using the definition of ... 3answers 818 views ### Prove ( \lnot C \implies \lnot B) \implies (B \implies C) without the Deduction Theorem The issue is Exercise 1.47 (d) in Elliot Mendelson's "Mathematical Logic". The exercise is to prove (\lnot C\implies\lnot B)\implies(B\implies C) by using the three axioms (A1,A2,A3) without using ... 2answers 136 views ### Hilbert's style proof (FO logic) I am stuck with this question to check whether the following formulas are valid and if they are valid, then derive them using Hilbert's axiom schema and Modes Ponens for First Order Logic. \begin{... 1answer 85 views ### Proofs of Sets and Subsets I have these proof problems that I need some help on, any direction would be great. Thanks Let A, B, and C be subsets of some universal set U (a) Prove the following: IF A \cap B \subseteq C, ... 1answer 245 views ### Formal Proofs: \vdash Py \land \exists x Qx \rightarrow \exists x (Py \land Qx) First order logic, Hilbert's System. For those familiar with Enderton's Introduction to Mathematical Logic, I am allowed the same axioms. For those unfamiliar, I can use these axioms: ... 1answer 878 views ### Stuck on First-Order Logic I'm taking a first-order logic class and I keep finding myself stuck on proofs that ask for disjunction elimination and then supply additional premises with conjunctions. How can I eliminate negations ... 1answer 189 views ### Consistent Set of Sentences is Consistent in Expanded Language Suppose that we have a set \Phi of sentences over a first-order language \mathcal{L} and that \Phi is consistent. Suppose we have another first-order language \mathcal{L}' such that \mathcal{... 1answer 775 views ### Fitch-Style Proof Help I'm having some trouble solving a Fitch Proof, Here's how far I've gotten. Any Help is appreciated. Thank You 1answer 52 views ### Proof logical statement with interference rules Proof following statement with interference rules ( without truth table) that$$ (\neg C \wedge B \wedge (A \rightarrow C) \wedge (B \rightarrow D ) )\implies (\neg A \wedge D )  Attempt to proof ...
I was given a task to construct a Hilbert-style proof for the following: $A → B ⊢ C ∨ A → C ∨ B$ I figured I could use the axiom $A→B≡A∨B≡B$, but this leads me nowhere since I don't think I can use ...
Let $\mathcal{L}$ be any language of predicate logic, $\Sigma_0$ a consistent theory in $\mathcal{L}$. Let P be the set of all consistent theories $\Sigma \supseteq \Sigma_0$ in $\mathcal{L}$. With ...