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
2
votes
2answers
99 views

Prove using Hilbert calculus $\forall x(Px\rightarrow x\equiv a)\vdash Pb\rightarrow Pa$, formal proof.

Prove: $\forall x(Px\rightarrow x\equiv a)\vdash Pb\rightarrow Pa$ Using Hilbert Calculus Format of solution: Step (my understanding) Solution: (1) $\forall x(Px\rightarrow x\equiv a)\vdash Pb\...
2
votes
1answer
794 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 ...
2
votes
1answer
109 views

Strange sum of random variables

So guys, I'm having this hard proof to solve in probability. I don't really know how to tackle it! Hope that someone can help. Let $\{Z_i\}_{i\in\mathbb{Z}}$ be i.i.d. random variables with zero mean ...
2
votes
4answers
160 views

Hilbert System with propositional logic $p \rightarrow q,\neg q \vdash \neg p$

This is my set of axiom $A \rightarrow (B\rightarrow A)$ $(A\rightarrow(B\rightarrow C))\rightarrow ((A\rightarrow B) \rightarrow (A \rightarrow C))$ $(\neg A \rightarrow B)\rightarrow ((\neg A \...
2
votes
2answers
115 views

In proof writing, is it mathematically sound to prove uniqueness before proving existence?

As stated in the title, I'd like to find out is whether or not it is always mathematically sound to prove the uniqueness of something before proving the existence of said something. I am still ...
2
votes
1answer
88 views

Predicate Logic Natural Deduction: $∃x P(x) ⊢P(x)$

I am really puzzled right now. To solve the issue, I need to prove this formular: $$ \exists x P(x) \vdash P(x) $$ with the natural deduction rules for propositional and predicate logic. I am ...
2
votes
1answer
106 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 ...
2
votes
1answer
240 views

How to show $\vdash (\neg\neg p \rightarrow p)$.

Given these axioms: where $\phi, \psi, \theta$ are formulas $$ 1.:(\psi \rightarrow (\theta \rightarrow \psi))$$ $$ 2.: ((\neg \psi \rightarrow \neg \theta) \rightarrow (\theta \rightarrow \psi))$$ ...
2
votes
2answers
653 views

Fitch style proof of $(\neg B \to \neg A) \leftrightarrow (A \to B)$

I have been stuck on this proof for a while. Here's where I'm at: Goal $(\neg B \to \neg A) \leftrightarrow (A \to B)$ l 1. $A \to B$ ll 2. $\neg B$ lll 3. $A$ lll 4. $B$ Elim 1,3 ...
2
votes
1answer
37 views

Proving the theorem $\forall a\in\mathbb{N},\forall m\in\mathbb{N},(m<a\Rightarrow m\leq a-1)$

I want to solve this proof by the method of Contradiction. Though without using the well ordering principle. I don't have any idea how to start. I have found other ways to prove this theorem but only ...
2
votes
2answers
52 views

Proof by contradiction - Getting my head around it

Hey there Math community! I have a general question on contradiction and it's getting difficult to get my head around it. Notes: I have some background in math and I have read several proofs by ...
2
votes
4answers
107 views

Proof of $(P\to Q) \vee (Q\to P)$ with natural deduction

I need to prove the following statement in natural deduction: $$(P\rightarrow Q) \lor (Q\rightarrow P)$$ I tried assuming not (target statement) and assuming the left hand side, but I don't know ...
2
votes
2answers
385 views

Proving that the norm of a Matrix is bigger or equal to it's smallest singular value multiplied by a vector.

I need to prove the following: Let $A \in \mathbf R^{n*n}$ be a real matrix and $x \in \mathbf R^n$ a vector.show that: $$\Vert Ax \Vert_{2} \geq s_{\min}\Vert x \Vert_{2}$$ where $s_{\min}$ is the ...
2
votes
1answer
534 views

Prove commutative law of multiplication using peano axioms.

That is, prove $∀x∀y(x \cdot y=y \cdot x)$. I have tried induction but it seems not work well. It may require the rule of additive cancellation to be proved. could someone please prove it please? ...
2
votes
1answer
773 views

Natural deduction: negation of quantifiers

How can I show that $\lnot \exists x P(x) \vdash \forall x\lnot P(x)$ ? Because I want to show: $\lnot \exists x (P(x) \lor R(x)) \vdash \forall x \lnot R(x)$ My idea: maybe a proof by ...
2
votes
1answer
122 views

Tricky predicate logic problem

I'm having a hard time proving that this is a valid argument $Premise 1: (Ǝx)Kx→(\forall x)(Lx→Mx)$ $Premise 2: Kc • Lc$ $Conclusion: Mc$ I am getting confused with all the existential/universal ...
2
votes
1answer
65 views

If a wff is simply atomic (e.g. $Pxy$) are $x$ and $y$ considered free in it?

(Using First-Order Logic Hilbert System) I found the following "solution" to $\forall x \forall y Pxy \vdash \forall y \forall x Pyx$: $\forall x \forall y Pxy \vdash \forall y Pzy$ (A2, MP) $...
2
votes
1answer
80 views

Understanding $\lor~E$ in Natural Deduction?

I'm reading Frank Pfenning's Lecture Notes on Natural Deduction. It's reasonable that the following $\lor$-elimination rule is incorrect since we can have any theorem $\alpha$ given a single theorem $\...
2
votes
2answers
54 views

Is this proof in natural deduction proof system correct?

Consider a natural deduction proof system. Suppose I know that $\vdash \phi$ (the sentence $\phi$ is provable from no premises). If I'm proving something like $\vdash \psi$, can I just use that $\phi$ ...
2
votes
1answer
111 views

When should I use RAA in natural deduction proofs?

I can't understand exactly when should I use RAA (reductio ad absurdum) rule in natural deduction proofs? What situation should "trigger" me to think "Now it's time to use RAA"?
2
votes
2answers
81 views

How do we formally define “j-th smallest element”?

Let $A$ be a nonempty finite subset of $\mathbb{R}$. Firstly, let me write down how to define the term "the smallest element of $A$" formally. Suppose 'for every $x\in A$, there exists $y \in A$ ...
2
votes
2answers
64 views

Construct a deductive system where $1^n$ is provable iff n is not prime

I'd appreciate some help for the following exercise: Construct a (as simple as possible) deductive system where all sequences of the form 1n (which means 111... n-times) is provable if and only if n ...
2
votes
1answer
560 views

Proving the distributive law with natural deduction

I have to prove the following logical equivalence, also known as one of the two distributive laws: $$ P \vee (Q \wedge R) \equiv (P \vee Q) \wedge (P \vee R) $$ I have solved the first part, $P \lor ...
2
votes
2answers
125 views

Doubts about Goedel Completeness Theorem

My book (Mendelson) states this theorem the following way: (1) A logically valid formula of a first order theory is a theorem. On Wikipedia the statement is a little more general: (2) For any ...
2
votes
2answers
23 views

What is the difference in meaning between these two antecedents …?

$$ (\forall x)(Mx \to Wx) \to \quad... \tag{1} $$ $$ (\forall x)(Mx \land Wx) \to \quad... \tag{2} $$ The consequent is clear: $\, (\exists y)(Fy \land Sy)$ The statement is: If every member of ...
2
votes
2answers
143 views

How to convert … to logical symbols?

If Bluenose is guilty then no witness is lying unless he is fearful. There is a witness who is fearful. Therefore, Bluenose is not guilty. $$B\to[(\forall x)(\,(Wx\land\lnot Fx)\to(\lnot Lx)\,)] \...
2
votes
1answer
161 views

Natural deduction proof - problem with existential elimination

I have problems with the following proof: $$ \forall x \exists y (Rxy \land Py), \forall x \neg Rxx \vdash \neg \forall x \forall y (Px \implies (Py \implies x=y)) $$ The problem is with the ...
2
votes
2answers
134 views

Formally proving $p\wedge q \rightarrow p$

I want to write a full prove for $p\wedge q \rightarrow p$ without using deduction, using only ${\neg, \rightarrow}$ connectives. I use the standard axiomatic system: $\alpha\rightarrow(\beta\...
2
votes
1answer
235 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 $(...
2
votes
1answer
92 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]\...
2
votes
2answers
50 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 ...
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
3answers
135 views

A rigorous proof of ∀ m ∈ ℕ, 0 < m → 1 < 2 * m

There's a class of problems I struggle to prove by induction/recursion (I'm working in CIC). The best way I can describe this class of problems is "finite cases below m, inductive case above m". An "...
2
votes
1answer
190 views

Proving $C \vdash D \lor \neg D$ using natural deduction, and WITHOUT any additional hypotheses/assumptions?

I proved $(A \land \neg A) \vdash B$ by doing the following: \begin{array}{l l l} 1. & A \land \neg A & (\text{premise}) \\ 2. & A & (1, \text{ simplification}) \\ 3. & A \lor B &...
2
votes
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 ...
2
votes
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 ...
2
votes
2answers
53 views

What is missing on Gödel's theorem explanation in “Emperor's New Mind” from Roger Penrose?

In "Emperor's New Mind", from pages 132 to 141, Roger Penrose explains Gödel's incompleteness theorem in very simple terms. Basically he says that, in a system of ordered propositions ($P_1(w)$, $P_2(...
2
votes
1answer
382 views

Spivak Calculus 3rd. Edition Chapter 1 Problem 12 (i) and (ii) Proofs Critique

Here are my "proofs" for Spivak's Calculus Chapter 1 Problem 12. I am new to this level of rigour and I am attempting to intimate myself with more advanced topics of mathematics to prepare for next ...
2
votes
2answers
1k views

Natural deduction proof / Formal proof : Complicated conclusion with no premise

Find a formal proof for the following: $\vdash [(\neg p \land r)\rightarrow (q \lor s )]\longrightarrow[(r\rightarrow p)\lor(\neg s \rightarrow q)]$ As you can see. No premise to use. We have to use ...
2
votes
2answers
465 views

Natural deduction proof: {A → B, B → (C & D), ¬C v ¬D} ⊢ ¬A

Prove using natural deduction: $ {A → B, B → (C \land D), ¬C \vee ¬D} ⊢ ¬A$ Our work (so far): $1- A → B$ $2- B → (C \land D)$ $3- ¬¬A$ $4- A$ $5- B$ (from 1,4) $→E$ $6- B$ $7- C \land D$ (...
2
votes
1answer
123 views

Question regarding using the natural deduction system

I have the following: Premise: ((V → ¬W) ∧ (X → Y)) Premise: (¬W → Z) Premise: (V ∧ X) |- (Z ∧Y) The part I want to know is how do I go about separating ...
2
votes
2answers
165 views

Deduce $ \forall x P(x) \vdash \exists xP(x) $

Well it's a little awkward but how can I show this in a natural deduction proof? $ \forall x P(x) \vdash \exists xP(x) $ I think one has too proof that with a proof by contradiction rule but since I ...
2
votes
2answers
1k views

Subproof in Fitch style system

When using a Fitch style system for proving various theorems, why are we allowed to assume anything we want in the assumption of a subproof in order to derive some desired result? It seems like there ...
2
votes
1answer
782 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
2
votes
2answers
52 views

Showcases of formalized mathematics in a system like Coq or Lean?

I have been reading about and trying out type theory based proof assistants Lean and Coq, and I have seen a few formalized proofs of basic, isolated propositions. I am looking for examples, showcases,...
2
votes
1answer
59 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 ...
2
votes
1answer
64 views

Show $\neg(\forall x\phi)\vdash \exists x(\neg \phi)$ using an ND-derivation

I'm trying to show that $\neg(\forall x\phi)\vdash \exists x(\neg \phi)$ through a natural deduction (ND) derivation. I'm kind of stuck, because I don't see how I can find some $t$ such that we have $...
2
votes
1answer
67 views

Showing $\vdash \phi\to \square \diamond \phi$

I'm trying to prove the converse of what was shown here. Namely, I'm trying to prove B-axioms of modal logic ($\vdash \phi\to \square \diamond \phi$ or $\vdash\diamond\square\phi\to\phi$, whatever is ...
2
votes
1answer
105 views

Formalizing the deduction theorem in the metatheory

Here is the deduction theorem, in the "$\Leftrightarrow$" version (I'm considering it for first order logic): $$\Delta \cup \lbrace A \rbrace \vdash \lbrace B \rbrace \Longleftrightarrow \Delta \vdash ...
2
votes
3answers
62 views

Prove that $n^2\in \mathcal O(n^2-1)$.

Prove that $$\smash { n^2\in\mathcal{O}(n^2 -1)}$$ I don't quite understand what strategy I should use when trying to prove the following big $\mathcal{O}$ notation that doesn't include the use of ...