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
112 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
87 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
652 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
36 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
51 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
105 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
383 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
521 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
757 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
121 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
78 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
52 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
97 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
76 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
520 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
123 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
141 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
151 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
130 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
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]\...
2
votes
2answers
49 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
1answer
550 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 ...
2
votes
3answers
134 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
188 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
2answers
923 views

Given ∃x.¬p(x), use the Fitch System to prove ¬∀x.p(x).

What I am thinking was I need two formulas, AX.p(X) => something AX.p(X) => ~ something I guess something maybe is the p(x) and the other is ~p(x) since we was given EX.~p(x)..But actually it can't ...
2
votes
2answers
52 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
377 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
452 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
192 views

Natural deduction proof - I don't' understand the question

I am supposed to give a natural deduction proof of $$(P_1∨P_2), \neg P_1 ⊢ P_2$$ My assumption is $(P_1∨P_2)$ and I am going to derive $P_2$ from $\neg P_1$ or I am wrong? EDIT: Or I am going to ...
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
2answers
42 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
61 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
64 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
102 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 ...
2
votes
2answers
35 views

Natural deduction - formal proof troubles

I'm pretty new to the topic of natural deduction using the Fitch method. I found a very helpful site (http://proofs.openlogicproject.org/) in which you can construct your proofs, but I'm having a lot ...
2
votes
4answers
63 views

Natural deduction proof of $(A \to \lnot B \lor C), ((\lnot D \land A) \to B), (\lnot E \to A) \vdash D \lor (C \lor E)$

I'm struggling to proof this both if I use or introduction rule $\lor_{I_1}$ (to work on $D$) or or introduction rule $\lor_{I_2}$ (to work on $C \lor E$). Could you help me?
2
votes
2answers
44 views

Need help with tautology proof without truth tables.

I am trying to prove $$[(p\to q)~\&~(q\to r)]\to (p\to r) $$ is a tautology using only logical laws. I have gotten part-way there but I got stuck and am not sure how to proceed. Please state ...
2
votes
1answer
70 views

Natural deduction in first-order logic

I've sat for more than an hour now and I don't understand how I'm supposed to solve the task below. $\{\forall x(P(x) \land Q(x)), \exists x\neg P(x)\} \vdash \exists x \neg Q(x) $ So I'm a bit ...
2
votes
1answer
65 views

Most adequate logic system to formally prove Euler's identity (and what would the proof look like)?

If we were given the task of proving Euler's identity using a formal logic system, which logic system out there would be the most convenient for such a task? And more or less what would the proof look ...
2
votes
1answer
102 views

Proof of $\forall x \forall y(x+x \neq y+y+1)$ in Peano arithmetic

How to prove $\forall x \forall y(x+x \neq y+y+1)$ using the axioms of Peano arithmetic?
2
votes
1answer
92 views

Proving $∀x (x ≠ 0 → gcd(x, 0) = x)$ formally attempt

I have proved $a≤gcd(a,0)$ in my attempt to prove $∀x (x ≠ 0 → gcd(x, 0) = x)$ but I am having trouble proving $gcd(a,0)≤a$ see below: I have access to the normal rules of natural deduction and the ...
2
votes
1answer
59 views

Proof by Induction Help: Prove that there are unique integers $a\geq 0$ and $k>0$ such that $n=(3^a)\cdot k$ and $k$ is not divisible by $3$.

Suppose $n$ is a positive integer. Using induction, prove that there are unique integers $a\geq 0$ and $k>0$ such that $n=(3^a)\cdot k$ and $k$ is not divisible by $3$. Note: I have already proven ...