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
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.
1
vote
4answers
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$...
1
vote
2answers
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 ...
1
vote
2answers
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 ...
1
vote
2answers
50 views

Question about reading proof notation

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 ...
1
vote
2answers
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 ...
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
1answer
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?
1
vote
2answers
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 ...
1
vote
1answer
116 views

Proof of $p\rightarrow (\Box (\Box p \wedge p) \rightarrow (\Box p \wedge p))$

I need to prove: $$p\rightarrow (\Box (\Box p \wedge p) \rightarrow (\Box p \wedge p))$$ The system contains all propostional tautologies and the axiom scheme $\mathbf K$:$ \Box(p \rightarrow q) \...
1
vote
1answer
20k views

Proving sequence convergence

I'm pretty confused...I understand bits and pieces but not how it all comes together...I would appreciate some help, either a written out example (you can make up one) and/or comments on how to fix my ...
1
vote
1answer
30 views

Verification of proof on repeated root for a quadratic polynomial

I'm fairly new to writing proofs so I'd appreciate it if anyone could point out amy holes in this proof, and if there's any comments so I could improve my proof writing! Question: "Let $a ≠ 0$. If ...
1
vote
1answer
62 views

Having trouble figuring out when to use induction or direct proof.

I know for simple induction you generally want to use this technique when the domain of the conjecture is in the Naturals.However, direct-proof approach would sometimes work too. For example, if i ...
1
vote
4answers
81 views

Formal Deduction (logic) Question: $\lnot C, (B \to \lnot C) \to A \vdash (A \to C) \to F$

I've been stuck on this question for around two hours now. I'm trying to prove that: $\lnot C, \ (B \to \lnot C)\to A \vdash (A \to C)\to F $ I'm trying to get my second last step to be: $\lnot C,...
1
vote
3answers
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 ...
1
vote
2answers
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 ...
1
vote
1answer
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 ...
1
vote
1answer
224 views

Fitch Natural Deduction proof problem

I have been working on this proof but I feel like I am stuck in a loop in the end and cannot get one step to be logically out of the sub proof. I have the premise $P \lor \lnot P$ and need to prove $(...
1
vote
1answer
101 views

Prove distributive law in Hilbert system

Using the logical axioms of the Hilbert system $\phi\to\phi$ $\phi\to(\psi\to\phi)$ $\left( \phi \to \left( \psi \rightarrow \xi \right) \right) \to \left( \left( \phi \to \psi \right) \to \left( \...
1
vote
1answer
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 ...
1
vote
2answers
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 ...
1
vote
1answer
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 (α → β) ...
1
vote
2answers
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 ...
1
vote
1answer
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 ...
1
vote
1answer
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 ...
1
vote
2answers
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 ...
1
vote
1answer
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$...
1
vote
1answer
265 views

Sequent calculus, how to prove double negation introduction and conjunction

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 \...
1
vote
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. ...
1
vote
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)...
1
vote
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" ...
1
vote
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 \...
1
vote
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?
1
vote
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 ...
1
vote
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}} $ ...
1
vote
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 ...
1
vote
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 ...
1
vote
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.
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$. ...
1
vote
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 ...
1
vote
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 ...
1
vote
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{...
1
vote
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, ...
1
vote
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: ...
1
vote
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 ...
1
vote
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{...
1
vote
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
1
vote
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 ...
1
vote
2answers
52 views

Prove distribution of or over implies knowing the implication is always true

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

show that for every consistent theory there is a complete consistent theory

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 ...