# Questions tagged [formal-proofs]

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

543 questions
Filter by
Sorted by
Tagged with
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, ...
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 ...
72 views

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

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 ...
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 ...
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?
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 ...
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 ...
117 views

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: ...
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 ...
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 ...
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 ...
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, ...
106 views

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?
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 ...
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}}$ ...