# Questions tagged [formal-proofs]

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

524 questions
91 views

48 views

### Can the natural deduction system prove $P \iff ¬P$ to show that it's a contradiction?

I use the Fitch notation for the natural deduction system. More information on https://en.wikipedia.org/wiki/Fitch_notation. In attempting to derive "$P \iff ¬P$" without any previous assumptions, I ...
608 views

### Countability of Fibonacci series [closed]

Fibonacci series is an infinite sequence of integers, starting with $1$ and $2$ and defined recursively after that, for the $n$th term in the array, as $F(n) = F(n-1) + F(n-2)$. How is the ...
2k views

### Prove a floor function is onto/surjective

I have function u(x) = $\lfloor x \rfloor$ mapped from R to Z which I need to prove is onto. I know that standard way of proving a function is onto requires that for every Y in the co-domain there ...
289 views

### Proving either or statements (in group theory)

Suppose we need to prove statement of the form either $P$ or $Q$. Is it sufficient to prove $P$ whenever not $Q$. Or do we need to show $Q$ whenever not $P$ holds as well? I was trying to prove this: ...
38 views

### Need help with formalising proofs in Calculus. Convergent and Divergent series:

Let $\sum_{n=1}^\infty a_n$ be a positive convergent series and let $\sum_{n=1}^\infty b_n$ be a positive divergent series. Prove that there exists an infinite number of n's such that $b_n\gt a_n$...
38 views

### Limit of $f(x) = x \bmod k$

I'm trying to prove that a function $f(x)$ tends to infinity when $x$ rises. Clearly, I used limit to do so. The problem is, $f(x) = x\ mod\ k$, in which mod is the division's residue of $x$ by $k$. ...
47 views

### What is a gross-looking formal axiomatic proof for a relatively simple proposition?

I'm looking for long and hard to follow derivations or symbolic proofs to motivate how tedious it is to actually reason within a formal system. I'm hoping there is an image of the proof, with few if ...
111 views

### Natural Deduction with identity: two distinct elements proof

Here's an argument that's quite clearly valid, but which I'm having trouble proving in Natural Deduction: $\exists x~\exists y~\lnot x=y \vdash\forall x~\exists y~\lnot x=y$ The informal reasoning: ...
755 views

### How to proof ¬P∨Q entails P→Q by Natural deduction

I can easily proof that $P \to Q$ entails $\lnot P \lor Q$ by Natural deduction, but I cannot find a way to proof $\lnot P \lor Q$ entails $P \to Q$. Could you show me the way by using Natural ...
82 views

### Propositional Logic: Prove $(p \land \lnot q) \to \lnot p \vdash p \to q$.

I'm having a lot of trouble trying to solve this. Any help would be greatly appreciated, I just can't seem to go any further! "Give syntactic proofs for the following sequent using only propositional ...
105 views

### What logic can express induction on natural numbers?

The induction theorem: $P(0) \land \forall n \in \mathbb{N}\{ P(n) \Rightarrow P(n+1)\} \Rightarrow \forall n \in \mathbb{N} \{P(n)\}$ My understanding is that nature numbers are constructed from ...
59 views

### Hilbert system equivalence

Show that it’s provable in the Hilbert system that identity behaves as an equivalence relation, i.e., show that for any terms $t_1, t_2$, and $t_3$ the following hold. (a) $\vdash_H t_1 \approx t_1$ ...
407 views

### Natural Deduction proof question

Questions on Natural deduction proof: 1.(A→A) → (B→B) 2.(B→C) → (A→A) / conclusion: (B→B) I was able to solve it using indirect proof but I want to try to prove it using the rules of inference and ...
47 views

### Meaning of “Polynomial in $x^2$”

I provide both the official question and answer below. At the end, I present my doubts which are to be clarified. QUESTION: Let $P(x)$ be a polynomial with integer coefficients. Prove that there ...
55 views

### If C'$_{ji}$ is a cofactor of C$^T$, how can I explain why C'$_{ji}$=C$_{ij}$ [closed]

I am stuck with this proof. Can anybody help me out?
2k views

### How can you prove that: A-(A∩B)=A-B ? [duplicate]

I know this might be stupid for most of the people here. I am starting with set theory and I cannot prove this:A-(A∩B)=A-B I start by assuming: 1) x∈A & ¬ (x∈A & x∈B) ...
1k views

### Subsequences of a convergent sequence converge to the same limit as the original sequence

Here is my proof: Proof. Let $(a_j) \to L$ be the original sequence and $({a}_{n_{j}})$ be a subsequence of $(a_j)$. We have to then show that $({a}_{n_{j}}) \to L$. Since $(a_j) \to L$, we have ...
33 views

### Sequence from $\Bbb N$ to $\Bbb Q$ between $0$ and $1$ which converges to $l$ (between $0$ and $1$)

$a_n$ is a sequence which maps the natural numbers onto the rational numbers between 0 and 1. I have to show that when $l \in [0,1]$ that there exists a subsequence $b_n$ which converges to $l$ I ...
100 views

### Difference between rigorous proof and intutive understanding

As the title suggests I am confused between what arguments will qualify a explanation as a proof and when does the intuition betrays us. Here is the question that made me think about this: On a ...
555 views

...
2k views

### Propositional Logic Proof of DeMorgan's Law

This problem was recently posed to me, and I prove it. $\vdash (A \land B ) \iff \neg(\neg A \lor \neg B)$ We are only allowed to use derivation rules, its obviously just the statement of DeMorgan'...
148 views

### Obtaining a formal proof (derivation) in modal logic

Assume we have the following statement: $$\mathsf{K} + \mathsf{A4} + \mathsf{AB} \models \mathsf{A5},$$ where $\mathsf{A4}$ is the transitivity axiom, and $\mathsf{AB}$ is the symmetry axiom. One ...
64 views

664 views

### Why, precisely, do mathematicians think the Collatz conjecture is true? [closed]

I noticed Wikipedia says that most mathematicians who have looked into the problem think the conjecture is true because experimental evidence and heuristic arguments support it (seen on Wikipedia, ...
199 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, ...
99 views

74 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 ...
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 ...
507 views

### Prove double negation introduction WITHOUT elimination, in a propositional logic axiom system.

I'm looking for a proof in classical propositional logic of "double negation introduction" (Q⊢¬¬Q) without using double negation elimination (¬¬Q⊢Q). I'm using the Hilbert system with the following ...
133 views

### Formally prove that these two premises are contradictory

Clever(a) ∧ ¬Happy(a) ∀x (Clever(x) → Happy(x)) So far I have something like this [EDIT] Thanks to Bram28 I got the correct proof.
535 views

### Fitch System For logic proofs

Does anyone know the Fitch program/ system used for logical proofs ? I am stuck with using fitch to construct a proof of¬(¬A∨¬B) from the premises A and B ... This is how it looks like in ...
241 views

### Question on proving validity in predicate logic

Using the proof rules of predicate logic prove the validity of the following sequent: $$\forall X \exists Y(P(X)\lor Q(Y))\vdash \exists Y \forall X(P(X)\lor Q(Y))$$ I have been trying to prove ...
61 views

### Prove, for N as a whole number, n^2 is even if n is even.

For the proof, "prove for n as a whole number, n^2 is even if and only if n is even", if we were to prove it via contradiction, would the negative of the statement which we need to contradict be: "n^...
83 views

### Prove that $3^n > 3n$ for integer $n\geq2$

How would we prove, by contradiction that $3^n > 3n$ for integer $n\geq2$. I'm having trouble on where I should start in tackling this question. I know that we should first state the negative of ...
111 views

### Rules of Inference : Showing that we can conclude $\exists xP(x) \lor \exists xQ(x)$ from $\exists x( P(x) \lor Q(x))$

From my discrete mathematics class, we are given an exercise, where one of the question is we have to prove that we can conclude $\exists xP(x) \lor \exists xQ(x)$ from $\exists x( P(x) \lor Q(x))$ ...
304 views

### How to prove ~~P from P in the Hilbert Axiomatic System?

Can someone provide me with hints for, or a rough sketch of, a proof of ~~P from P in the Hilbert system? I had very little trouble proving the reverse, that P is provable from ~~P, but seem to be ...
50 views

### Distinction between “implicit” and “explicit” formal proofs

Can anyone comment on the distinction between two different methods of formal proof? Since I'm pretty shaky on the methods and terminology of Proof Theory I a refer to them below as the "implicit" 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 ...
267 views

### What is “magic” about the combination of addition and multiplication in formal arithmetic?

Goedel's incompleteness tells us that any system containing Robinson arithmetic is incomplete. OTOH, Presburger Arithmetic, which contains only the successor and addition, is complete. I'm pretty ...
219 views

### How to prove this sequent using natural deduction?

How do I prove $$S\rightarrow \exists xP(x) \vdash \exists x(S\rightarrow P(x))$$ using natural deduction? Just an alignment of which axioms or rules that one could use would be much appreciated.
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$...
48 views

### Is this an axiom or does it have to be proved?

a and b are positive integers and x is greater than 1. In Rudin principles of real analysis it is not given as an axiom but proving is seems difficult to me
44 views

### Strength of Asymmetric Tautology/Reverse Unit Propagation in proofs

Given a set of disjunctions in propositional logic, they can be said to entail another disjunction D if the negation of D, when added as a set of unit clauses to the original set, yields an ...