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
36 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
64 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
46 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
77 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
66 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 ...
2
votes
1answer
212 views

Stuck on Formal Proofs

I'm trying to figure out this formal proof. This is what I have so far but I'm stuck in trying to reach the goal. I'm not sure if what I did is correct so far since I'm still trying to learn this on ...
2
votes
1answer
694 views

What is a judgment?

I have a hard time trying to understand the concept of a judgment in natural deduction. One distinguishes between propositions and judgments. As I understand it, propositions are just well-formed ...
2
votes
1answer
411 views

Spivak Calculus 3rd. Edition Chapter 1 Problem 12 (v) and (vi) 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
98 views

How to give a formal proof for $ \exists \space x\space \forall \space y(P(x) \rightarrow P(y))$ in fitch

To practice for my exams, my teacher gave us several exercises to practice but didn't supply us any answers. Now after looking at this problem for 2 nights I have no idea left on how to solve it. If ...
2
votes
1answer
372 views

$A⇒(B \lor C)$ and $[(A \Rightarrow B) \lor (A \Rightarrow C)]$

[(A⇒ B∨C)] ⇒ [A⇒(¬B⇒C)] ⇒[(A⇒¬B)⇒(A⇒C)] ⇒ [¬(A⇒¬B)∨(A⇒C)]⇒[(A∧B)∨(A⇒C)] [(A⇒B)∨(A⇒C)] is equivalent to A⇒(B∨C). Can I prove [(A∧B)∨(A⇒C)] ⇒ [A⇒(B V C)]? or is there problem in the proof above ...
2
votes
1answer
85 views

Another topology question

This is a two part question. The first part, part (i), I present with the solution I reached. The second part, part (ii) is where I need help. (i) Let $B$ be a basis for a topology $T$ on a non-empty ...
2
votes
1answer
2k views

Modulo Congruence Prime Proofs

Let p be an element of {2,3,4...}. Sppose that for all x,y (integers) if xy ≡ 0 mod p, then x ≡ 0 mod p or y ≡ 0 mod p. Show p is prime. I did some work on this problem but I have gotten stuck. (p|...
2
votes
1answer
107 views

$p \to (q\vee\neg r), \neg q, r ⊢ \neg p$ - Natural deduction- elimination with $\neg$ operator

I have the following proposition: $$p \to (q\vee\neg r), \neg q, r ⊢ \neg p$$ The only part I have trouble with is the : $$p \to (q\vee\neg r)$$ Clearly the first step is to eliminate $q$ or $\neg ...
2
votes
1answer
260 views

proving $ (A \rightarrow B \vee C )\rightarrow((A\rightarrow B) \vee (A\rightarrow C))$

I'm looking for a way to prow $ (A \rightarrow B \vee C )\rightarrow((A\rightarrow B) \vee (A\rightarrow C))$ from the following axioms and rules $$\vdash A \rightarrow A$$ $$\vdash A \wedge B \...
2
votes
1answer
78 views

Define $f : Z/3Z → Z/3Z$ by $f ([a]) = [2a + 1]$

Just finished proving this is well-defined, how do I prove it's surjective and injective? I know that injective means that if $x1 \neq x2$, then $f(x_1) \neq f(x2)$, i.e. each value in the domain is ...
2
votes
1answer
195 views

Problem with proving formally tautology using given rules

Using the rules below prove that the following assumeptions leads to the following conclusion by tautology. $A\vee B \vee C, A\to C, B\to C \Rightarrow C$ What I did: $A\vee B \vee C$ ...
2
votes
1answer
75 views

Show that the proof rule is not sound and proof question

I'm asked to show that the proof rule \begin{equation} \dfrac{\varphi \to \psi}{\lnot \varphi \to \lnot \psi} \end{equation} is not sound. To show this would I just make the truth tables for the ...
2
votes
2answers
78 views

Natural deduction: predicate logic proof (Prenex form)

I'm pretty familiar with proofs in propositional logic, but not so much with predicate logic. I'm trying to prove the following (which can be used during construction of prenex normal form). If $x$ ...
2
votes
0answers
92 views

Reference request: the space of formalisms for proving function totality

I'd like to develop an intuition about the space of axiomatic systems (formalisms) that can be used to prove totality of Turing machines. To this end, I'm interested in the set of "totality proof ...
2
votes
1answer
156 views

Fitch-style Deductive Proof

I am having trouble with the following question: Give natural deduction proofs of the following formulas (from no assumptions): $p \to p$. Here is what I have so far: $$\begin{array}{|l}\hline~~\...
2
votes
2answers
76 views

Some questions about the properties of equality

Given the reflexive property of equality and the axiom of substitution, we can prove the property of symmetry. I came across the following proof: $\alpha=\beta$ (hypothesis) $\alpha=\alpha$ (axiom of ...
2
votes
0answers
46 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 ...
2
votes
0answers
67 views

Elementary Hoare logic proof

I would like to prove that the following Hoare triple is correct by giving a full Hoare logic proof. (Assuming all variables are real.) How can I do so? $$\{c = 0\} ~ a := −c; ~ b := a + c; ~ c := a ~...
2
votes
0answers
132 views

Are there any recent advances in formalizing the undecidability of $\mathit{CH}$?

I'm cross-posting this from Mathoverflow. Since I'm asking for recent developments, it seems best to have answers in both sites. The website Formalizing 100 Theorems by Freek Wiedijk contains a list ...
2
votes
1answer
55 views

Are $A, B, C \vdash D$ and $A, B\vdash C \rightarrow D$ interchangeable?

For an assignment we have to make a proof in the Hilbert system. And my proof hinges on the following operation being allowed: $A, B, C \vdash D\tag 1$ Becomming: $A, B\vdash C \rightarrow D\tag 2$ ...
2
votes
1answer
409 views

Gambler's ruin: verifying Markov property

Gambler's ruin: the gambler starts with $\$i$, where $ 1<i<N$. He wins $\$1$ with probability $p$ and loses $\$1$ with probability $1-p$. When he reaches $0$ (ruin) or $N$ (win), he stops ...
2
votes
1answer
135 views

Is “forall elimination twice with the same fresh variable” allowed?

I am looking to prove that $\forall x \forall y \; P(x,y) \vdash \forall x \; P(x,x)$ and I wonder if this is allowed:...
2
votes
0answers
39 views

Formal Proof Problem [closed]

I'm doing this formal proof problem with 10 steps, given these three premises; 1) (G V H) ⊃ I 2) (J V K) ⊃ ~I 3) K / ∴ ~H 4 - 10 is unknown. I tried using material implication and DeMorgan's ...
2
votes
0answers
216 views

Hilbert style proof for $\Box A \vee \Box B \rightarrow \Box(A\vee B)$ in K.

I have to find a formal Hilbert style proof for $\Box A \vee \Box B \rightarrow \Box(A\vee B)$ on modal logic, K. I can use all classical propositional tautologies, Modus Ponens and Distribution axiom....
2
votes
2answers
2k views

Proof of a theorem in Hilbert's system

I have been trying to prove that the propositional formula $ \big( \alpha \rightarrow \lnot \beta \big) \rightarrow \big((\alpha \rightarrow \beta) \rightarrow \lnot \alpha \big)$ is a theorem in ...
2
votes
2answers
303 views

Proof about Clavius's Law

Clavius's Law claimed: $(\neg A \rightarrow A) \rightarrow A$ What it is the proof about it in Deductive System $L$? Deductive System $L$ is: L1: $A \rightarrow (B \rightarrow A)$ L2:...
1
vote
2answers
141 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) \...
1
vote
2answers
113 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
882 views

prove that the $\sqrt{n}$ is unbounded

I wanted to check if my answer to proving that the $\sqrt{n}$ is unbounded works. If the $\sqrt{n}$ is bounded then there exists a $K$ s.t. $|\sqrt{n}|< K$, for all n. therefore $|\sqrt{n}| <...
1
vote
2answers
101 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 ...
1
vote
3answers
57 views

Prove that $0.5x^2 -3x ≥ -4.5$ for all real numbers x.

I'm not familiar at all with inequality proofs. How do I approach this problem?
1
vote
2answers
114 views

Prove $(P\to (Q \to R)) \to (Q \to (P \to R))$ (derivation)…

The problem is as stated in the title. With this problem and I am restricted to modus tollens (MT), modus ponens (MP), repetition (R), and double negation (DN). I'm just getting used to logic ...
1
vote
2answers
51 views

How to prove A → N from A and (A ∨ B) → N in FOL

I have the following premises: A and (A ∨ B) → N How can I prove A → N from this in a formal proof using FOL?
1
vote
2answers
39 views

Does the Statement $\lim_{f(x)\to a}k(x)$ Make Sense

In a formal mathematics context does the statement $$\lim_{f(x)\to a}k(x)$$ where $f(x)\neq c$, where $c$ is a constant, make sense? For example does $$\lim_{x^2\to 0}x$$ make any sense in a formal ...
1
vote
1answer
93 views

Trying to understand the difference between metatheory and theory and circularity

First off I just want to say that I understand that a model is not the same as the thing it models. I've already read several answers on this topic so I am looking for a new answer to hopefully ...
1
vote
1answer
49 views

What is the name of the rule that allows us to infer the truth of an equation from the truth of another equation?

I am wondering if there is a particular named rule or principle in mathematics/formal logic (that can be listed as justification in a formal proof) that allows one to conclude the truth of an equation ...
1
vote
4answers
3k views

Propositional Logic Proof of DeMorgan's Law

This problem was recently posed to me that I prove it. $\vdash (A \land B ) \iff \neg(\neg A \lor \neg B) $ We are only allowed to use derivation rules. It is obviously just the statement of ...
1
vote
2answers
248 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 (...
1
vote
3answers
151 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, ...
1
vote
2answers
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 ...
1
vote
2answers
72 views

What's Wrong in this Proof Logic?

Trying to show that the empty set $ \emptyset \subseteq A $, for any set $ A $. Let $ x \in \emptyset $, then by definition, $ x \in \emptyset \iff (x \neq x) $. $ x \in \emptyset \implies (x \neq ...
1
vote
1answer
94 views

Deductive Logic : If A -> B it can be deduced neg(A) -> neg(B)

I am having a hard time proving the following $$ (a \to b) \vdash (\lnot a \to \lnot b) $$ I followed the book advice and first proved that $ (a \to b) \vdash (\lnot \lnot a \to \lnot \lnot b) $ ...