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
3answers
156 views

How to prove $n\leq x \rightarrow x = n \vee Sn \leq x$ using Robinson Arithmetic

Given the definition $n \leq x \Leftrightarrow \exists y \ni y+n=x$, how can one prove $n\leq x \rightarrow x = n \vee Sn \leq x$ in Robinson Arithmetic? I think this should be a proof by induction, ...
1
vote
2answers
59 views

How to express induction when we just have finitely many instances, but still proceed inductively over them

Let $Q$ be some finite set with $n = |Q|$. Then suppose I want to show that for every nonempty subset $P \subseteq Q$ some property $A$ holds. One natural way to approach this is using induction, and ...
1
vote
2answers
72 views

What's Wrong in this Proof Logic?

Trying to show that the empty set $ \emptyset \subseteq A $, for any set $ A $. Let $ x \in \emptyset $, then by definition, $ x \in \emptyset \iff (x \neq x) $. $ x \in \emptyset \implies (x \neq ...
1
vote
1answer
94 views

Deductive Logic : If A -> B it can be deduced neg(A) -> neg(B)

I am having a hard time proving the following $$ (a \to b) \vdash (\lnot a \to \lnot b) $$ I followed the book advice and first proved that $ (a \to b) \vdash (\lnot \lnot a \to \lnot \lnot b) $ ...
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?
1
vote
2answers
62 views

Show that $ \forall{x}\exists{y}{(P(x) \to Q(y))} \vdash \exists{y}\forall{x}{(P(x) \to Q(y))} $

I need to show that $$ \forall{x}\exists{y}{(P(x) \to Q(y))} \vdash \exists{y}\forall{x}{(P(x) \to Q(y))} $$ using the natural deduction rules outlined in Logic in Computer Science: Modelling and ...
1
vote
1answer
34 views

$\vdash\phi \land \diamond\psi \to \diamond(\psi\land\diamond\phi)$ in KB

I've been trying to prove $\vdash\phi \land \diamond\psi \to \diamond(\psi\land\diamond \phi)$ in natural deduction where it's allowed to use $\phi\to \square \diamond \phi$ and/or $\diamond\square\...
1
vote
2answers
94 views

Proving $\exists ! x (t = x)$ constructively without double negation axiom

I am wondering how one would go about this. I am using Hilbert style proof system as described in Kleene's "Introduction to Metamathematics" or "Mathematical logic". I am pretty sure that if you can ...
1
vote
2answers
113 views

How is Post's tautology theorem used in this proof?

Could someone please explain to me how does the proof of I.4.3 reference I.4.1? In I.4.3, you are given hypotheses about A and B being theorems. However, I.4.1 talks about tautologies (as inputs) not ...
1
vote
1answer
46 views

$\Sigma ; \lnot \alpha \vdash k $. Prove that $\Sigma \vdash \alpha$

$k$ is a contradiction such that it belongs to a set of well-formed formulas. $\Sigma ; \lnot \alpha \vdash k $. Prove that $\Sigma \vdash \alpha$ where $\alpha$ is a well-formed formula. After ...
1
vote
1answer
68 views

How to formalize my intution of this theorem on continuous functions?

Theorem : If a function $f$ is continuous on a closed and bounded interval $[a, b]$ then $f$ must be uniformly continuous in $[a, b]$ My Idea : I get the intuition that for a continuous function on a ...
1
vote
1answer
96 views

How to prove $\lnot (\alpha \rightarrow \lnot \beta) \vdash \lnot (\beta \rightarrow \lnot \alpha)$ in HPC

I have the three axioms $$\alpha \rightarrow (\beta \rightarrow \alpha)$$ $$\Big(\alpha \rightarrow (\beta \rightarrow\gamma)\Big)\rightarrow \Big((\alpha \rightarrow\beta)\rightarrow(\alpha\...
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
107 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
97 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
106 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
53 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
3answers
829 views

Precise proof of equivalence of two definitions of limit of a function

Consider two (equivalent) definitions of a (real) limit of a function $f:\mathbb{R}\rightarrow\mathbb{R}$. The epsilon-delta one: $$ \lim_{x\to x_0} f(x)=l \iff \forall \varepsilon>0\exists \delta&...
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
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
354 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
3answers
835 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
1answer
117 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
21k 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
64 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
84 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
1answer
64 views

Formal Proof - premises and conclusions

So I'm learning about formal proof and understand the beginning steps. However, after I'm given an argument and conclusion, I then don't understand how to do the actual formal proving. For example: ...
1
vote
3answers
104 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
133 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
211 views

Prove reflexivity using Fitch software

I am trying to learn how to use the Fitch software from Barwise and Etchemendy to develop proofs. I am trying to prove that $R$ is reflexive from the following premises. If $R$ is symmetric, ...
1
vote
1answer
106 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
2answers
82 views

How to prove two expressions are equivalent using formal proofs?

I have this argument I'm trying to prove: ¬(A ∨ B) _ ¬A ∧ ¬B We have two expressions which are equivalent to eachother. I know they are because they have the ...
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
425 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
751 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
2answers
139 views

Solving theorem proof with only primitive rules of logic!

I am having trouble solving the theorem proof of (P-> ~Q)->(Q->~P). I can only use primitive rules and I understand I have to use arrow introduction to introduce my antecedent, but after that I am a ...
1
vote
2answers
103 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
178 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
277 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
52 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
201 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
151 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
116 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}} $ ...