Stack Exchange Network

Stack Exchange network consists of 175 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.

Visit Stack Exchange

Questions tagged [formal-proofs]

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

2
votes
1answer
91 views

Variations in the Statement of Strong Induction: Equivalent or Different?

I often see two variations in how the principle of strong induction is stated: First Variation: $\Big(B\!\subseteq\!\mathbb{N}\wedge1\!\in\!B\wedge\big(\forall x[x\!\leq\!k\rightarrow x\!\in\!B]\...
3
votes
2answers
70 views

How would I show that X is equivalent to ((¬X ↔ X ) ∨ X )?

I use the https://en.wikipedia.org/wiki/Fitch_notation, or fitch notation, for logical deduction systems. I don't know how to derive a contradiction in the other half of the biconditional where $X \...
2
votes
2answers
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 ...
-4
votes
1answer
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 ...
0
votes
2answers
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 ...
1
vote
1answer
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: ...
0
votes
1answer
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$...
1
vote
2answers
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$. ...
1
vote
2answers
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 ...
5
votes
2answers
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: ...
2
votes
1answer
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 ...
3
votes
2answers
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 ...
2
votes
1answer
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 ...
0
votes
0answers
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$ ...
0
votes
1answer
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 ...
0
votes
1answer
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 ...
0
votes
1answer
55 views
0
votes
2answers
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) ...
1
vote
2answers
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 ...
0
votes
2answers
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 ...
1
vote
2answers
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 ...
0
votes
3answers
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'...
0
votes
1answer
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 ...
0
votes
2answers
64 views

Proving a seemingly simple inequality is proving difficult [duplicate]

After what feels like an embarrassing hour of scribbling I can't seem to find a direct solution to the following problem $Show \space that: a^2 + b^2 + c^2 \geq ab+bc+ca \space \space \forall [a,b,c]...
1
vote
2answers
234 views

Prove $\mathrm{ext}\,(A)=\mathrm{int}\,(X\setminus A)$

For a subset $A$ of topological space $X$, the exterior of $A$ is the set $\mathrm{ext}\,(A)=X\setminus\mathrm{cl}(A)$. What I have so far: $\text{ext}\,(A) = X\setminus \text{cl}(A) = X\setminus (...
4
votes
1answer
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, ...
0
votes
1answer
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, ...
1
vote
1answer
99 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
395 views

Lindenbaum's Lemma in Propositional Logic

I've recently learnt Lindenbaum's Lemma in propositional logic: Suppose $\Gamma$ is a consistent set of $L$-formulas. Then there exists a consistent set $\Gamma'$ of $L$-formulas containing $\Gamma$, ...
0
votes
1answer
90 views

Remembering Proofs in Geometry [closed]

I'm taking a College Geometry class and the teacher wants us to be able to recite roughly 13 proofs on the exam. How should I try to remember those proofs? If anyone has any suggestions that would be ...
-1
votes
1answer
311 views

logic proof with Fitch System [closed]

I am stuck with using Fitch system to construct a proof of ¬(P → Q) ↔ (P ∧ ¬Q) with no premises. This is what I have done
1
vote
2answers
139 views

Prove $(\neg B \to \neg A) \to (A \to B)$ from axioms

How can I prove that $$(\neg B \to \neg A) \to (A \to B),$$ if it is told that $A \to (B \to A),$ $(A \to (B \to C)) \to ((A \to B) \to (A \to C)),$ $(\neg B \to \neg A) \to ((\neg B \to \neg A) \...
0
votes
1answer
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 ...
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 ...
0
votes
0answers
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 ...
2
votes
1answer
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.
2
votes
1answer
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 ...
1
vote
1answer
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 ...
0
votes
3answers
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^...
-1
votes
2answers
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 ...
1
vote
2answers
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))$ ...
1
vote
2answers
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 ...
1
vote
0answers
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 ...
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 ...
9
votes
1answer
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 ...
3
votes
2answers
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.
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$...
0
votes
1answer
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
2
votes
0answers
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 ...