Questions tagged [formal-proofs]

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

1
vote
1answer
58 views

Proof of Natural Numbers using n+1 = n ∪ {n}

In set theory natural numbers are defined by 0 = ∅ and natural number n+1 = n ∪ {n} I need to prove that for every n ∈ N , n = {k ∈ N | k < n}. I know that natural numbers 1 = {∅} 2 = {∅,{∅}} ...
2
votes
4answers
104 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 ...
0
votes
4answers
64 views

Proving Symmetric Difference of A and B

Let A and B be sets. Define the symmetric difference of A and B as A∆B= (A ∪ B) − (A ∩ B). (a) Prove that A∆B = (A − B) ∪ (B − A) I tried to start this but am getting really lost. if someone could ...
1
vote
4answers
79 views

Formal Deduction (logic) Question: $\lnot C, (B \to \lnot C) \to A \vdash (A \to C) \to F$

I've been stuck on this question for around two hours now. I'm trying to prove that: $\lnot C, \ (B \to \lnot C)\to A \vdash (A \to C)\to F $ I'm trying to get my second last step to be: $\lnot C,...
1
vote
2answers
87 views

Proving $\exists ! x (t = x)$ constructively without double negation axiom

I am wondering how one would go about this. I am using Hilbert style proof system as described in Kleene's "Introduction to Metamathematics" or "Mathematical logic". I am pretty sure that if you can ...
0
votes
0answers
43 views

Formal Proof - premises and conclusions

So I'm learning about formal proof and understand the beginning steps. However, after it gives an argument and conclusion. I then don' t understand how to do the actual formal proofing. For example: ...
0
votes
1answer
25 views

Formal proof method for predicate logics

I am looking for the official name for a proof method, The method consists of proving the INconsistency of a theory. This was done using trees. We call it classic-elimination method but I don't know ...
3
votes
3answers
109 views

How to prove the following formula using an indirect proof

I need to prove that the premise $A \to (B \vee C)$ leads to the conclusion $(A \to B) \vee (A \to C)$. Here's what I have so far. From here I'm stuck (and I'm not even sure if this is correct). My ...
3
votes
1answer
39 views

How can I prove the following with natural deduction rules? ¬∀x∃yP(x,y) ⊢ ∃x∀y¬P(x,y)

I have been stuck with this problem for a long time, I tried reductio ad absurdum and I got the hypothesys [¬∃x∀y¬P(x,y)], then I try to eliminate the negation of the premise, but I have to prove ∀x∃...
3
votes
2answers
94 views

How to use natural deduction to show $\neg (P \land Q) \vdash \neg P \lor \neg Q$?

How to use natural deduction to show $\lnot (P \land Q) \vdash \lnot P \lor \lnot Q$? I think I need to first assume $\neg(\neg P \lor \neg Q)$ and then find a contradiction but I cannot see how to do ...
2
votes
1answer
69 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 ...
3
votes
1answer
82 views

Proof using natural deduction (Tautology)

I've been asked to prove the following tautology via natural deduction: $\forall x \, (\lnot Px \lor Qx) \rightarrow (\forall y \, Py \rightarrow \forall z \,Qz)$ I normally use tree proofs, but I ...
2
votes
2answers
110 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
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
1answer
92 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
1answer
85 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 ...
1
vote
3answers
96 views

Trouble understanding proof to $\vdash ((\neg(\phi\rightarrow \psi))\rightarrow\phi)$?

I am having trouble understanding the natural deduction proof of $\vdash ((\neg(\phi\rightarrow \psi))\rightarrow\phi)$ (question 2.6.2 (b)) in Hodges and Chiswell's Mathemaical Logic. The natural ...
0
votes
0answers
33 views

Proving a logical implication using modus ponens and metatheorems [duplicate]

Using the law of inference the axiomatic system and metatheorems prove that $${(\neg A > B),(A > C),(B > D)} \vdash (\neg C > D)$$ Where > is 'implies' and ~ negation. I know how to use ...
1
vote
1answer
55 views

Induction with two variables in PA

This probably has been asked before, but apologies, I don't know how to locate it. I want to prove $\forall x,y: P(x, y)$. My premises are: $$P(0, 0) \wedge \\ [\forall x: P(x, 0)] \wedge \\ [\...
2
votes
2answers
74 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$ ...
1
vote
1answer
86 views

show that for every consistent theory there is a complete consistent theory

Let $\mathcal{L}$ be any language of predicate logic, $\Sigma_0$ a consistent theory in $\mathcal{L}$. Let P be the set of all consistent theories $\Sigma \supseteq \Sigma_0$ in $\mathcal{L}$. With ...
-2
votes
2answers
45 views

Let f : R → R be a function, such that $|f(x)−f(y)|≥5|x−y| \:\forall \:x, y\in \mathbb{R}$. Show that $f$ is injective. [closed]

Intro to Math Proofs course Know basic concepts of Injection functions (one-to-one)
1
vote
0answers
67 views

Predicate Logic Hilbert Proof

In the Hilbert proof system for predicate logic, prove that the formula: $\exists x~\big(B(x)\to C(x)\big)\to\big(\forall x~B(x)\to\exists x~C(x)\big)$ I'm awful with Hilbert Proofs and have no idea ...
3
votes
0answers
90 views

Formal proof of $\exists x (\exists y P(y) \rightarrow P(x))$ and $(\forall x \exists y R(x,y))\rightarrow (\forall y \exists x R(y,x))$

within the following axiomatic system I've beeb trying to proof the formulas (1) $\forall x \exists y R(x,y) \rightarrow \forall y \exists x R(y,x) \\$ and (2) $\\ \exists x (\exists y P(y) \...
2
votes
2answers
73 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$ ...
3
votes
1answer
77 views

Find a natural deduction proof to show ∃x∃y (S(x,y) ∨ S(y,x)) ⊢ ∃x∃y S(x,y) by predicate logic.

I'm trying to prove $\exists x \exists y (S(x,y) \lor S(y,x)) \vdash \exists x \exists y S(x,y)$ in natural deduction, and I have already applied existential elimination to get $S(x_0,y_0)$, with $x_0$...
1
vote
2answers
109 views

How is Post's tautology theorem used in this proof?

Could someone please explain to me how does the proof of I.4.3 reference I.4.1? In I.4.3, you are given hypotheses about A and B being theorems. However, I.4.1 talks about tautologies (as inputs) not ...
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 ...
1
vote
0answers
30 views

Definition of the spectrum in first order logic

I want to understand the definition of the spectrum and therefore I want to know, what it means that a model has n elements or that a model is of size n. What is said to be an element? Are these only ...
0
votes
2answers
37 views

Induction: Using P(n) vs P(n+1) is bad style?

I'm in a proofs class and we were discussing induction. One of the most common ways we (the students) had seen induction was to represent "Statement P hold for $n$" by $P(n)$. Thus, we take the ...
3
votes
1answer
82 views

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

I'd appreciate some help or at least a hint for the following exercise: Construct a (as simple as possible) deductive system where all sequences of the form $1^n$ (which means 111... $n$-times) is ...
0
votes
5answers
131 views

Starting with a false statement, how can one prove anything is true? [duplicate]

So I've been learning a bit of logic for class and heard that if you begin with a false statement, you can then prove anything to be true, however I don't entirely understand what this means or how to ...
0
votes
2answers
21 views

Is it possible to show that there is some multiple of 4 that when added to a multiple of 16, will give you perfect square?

Like given some multiple of 16, (in the integers), is it possible to show that there is some multiple of 4 that would make it a perfect square? For example, 32, you can add 4 to make it a perfect ...
0
votes
1answer
115 views

Prove by induction that the union of countable sets is countable

Say you have a set A_i for i in the natural numbers N, and that is a countable set. Then for all natural numbers n, the union of those sets is countable. I must prove this by induction, and I do ...
0
votes
4answers
51 views

Formal proof of implication

I am currently stuck on this particular task. I need to formally prove that (∃a ∀b (b<a)) → (∀a ∃b (a<b)) Now, what I have so far is that I need to prove ...
1
vote
1answer
46 views

$\Sigma ; \lnot \alpha \vdash k $. Prove that $\Sigma \vdash \alpha$

$k$ is a contradiction such that it belongs to a set of well-formed formulas. $\Sigma ; \lnot \alpha \vdash k $. Prove that $\Sigma \vdash \alpha$ where $\alpha$ is a well-formed formula. After ...
0
votes
1answer
88 views

Axiom Problems (Intro to Computer Logic)

"Show that—or prove that—$ \Gamma \vdash A $" means "write a $ \Gamma $-proof that establishes $ A $". The proof can be Equational or Hilbert-style. Show that $ A \equiv C \vdash A \rightarrow (B ...
0
votes
1answer
64 views

Need help for a proof ( sequent calculus )

I have to prove the following: $$\vdash((A \to B) \land (B \to A)) \to (A \leftrightarrow B)$$ But I'm totally stuck here after using introduction of implication and introduction of equivalence: \...
0
votes
1answer
41 views

Can a sequent be valid if the conclusion contains atoms that are not in the premise?

Is it possible to prove the validity of the following sequent: $p \vdash (p \to q) \to q$ Here, our premise is that $p$ is True. The conclusion references a new atom, $q$. I would argue that this ...
0
votes
1answer
57 views

Weakest theory equi-consistent to ZFC

I've recently read that ZF is equi-consistent to ZFC. From what I understand, to establish this we transform a formal proof of a contradiction in ZFC into a formal proof of a contradiction in ZF. We ...
1
vote
3answers
35 views

Prove that a sequence which converges at L, still converges at L when a fixed positive integer is added to the variable.

Here is the problem I am attempting to solve/prove: Let $(a_n)$ n∈N be a sequence that converges to L and let p be a fixed positive integer. Prove that the sequence $(a_{n+p})$ n∈N converges to L. I'...
-1
votes
3answers
35 views

How can I prove this in a systematic manner? [closed]

I have to prove the following claim. For all $n \in \mathbb{N}, 2$ divides $3n^{3} + 13n^{2} + 18n + 8.$ I want to have a systematic proof or even just a hint, to start.
0
votes
1answer
71 views

Prove $\forall n \in \mathbb N, \forall k\in \mathbb Z, \forall \ell \in \mathbb Z, \neg (n = 5k+3 \land n = 5\ell +1)$, Intended meaning?

I am understanding this question to prove $5k+3 \neq 5l+1$ for all values of l and k as long as the result is a natural number. Since it's for all, it can easily be disproved by finding any example ...
8
votes
1answer
134 views

Semantic proofs to syntactic proofs

Given a first-order logic theory $T$ and and a formula $F$, suppose I have semantically proved that $T\vdash F$. That is, I have proved that any model $M$ of $T$ satisfies $F$ and I conclude by Gödel'...
0
votes
2answers
127 views

Let $a,b,c,d$ be real numbers such that $a<b < c<d$. Express the set $[a,b] \cup [c,d]$ as the difference of two sets [duplicate]

I am not sure how I would express these sets as a difference. My original attempt was to show that it is the set $[a,d]$ and take away the universal set. I would appreciate any help. Thank you in ...
1
vote
1answer
67 views

How to formalize my intution of this theorem on continuous functions?

Theorem : If a function $f$ is continuous on a closed and bounded interval $[a, b]$ then $f$ must be uniformly continuous in $[a, b]$ My Idea : I get the intuition that for a continuous function on a ...
1
vote
1answer
110 views

Book Recommendation

To start out with, I'm a junior in high school who is intrigued by the rigor of higher mathematics and is currently attempting to self study Volume 1 of Apostol's Calculus. I haven't had any previous ...
0
votes
0answers
28 views

Good list of theorems tobprove

HI I am a highschooler currently taking calc BC and I am looking for some fun theorems I could try to prove. I have proved a lot of trigonometric identities and the fundemental theorem of calculus and ...
1
vote
0answers
56 views

Prove $\Sigma \vdash \lnot(\phi \rightarrow \psi)$ iff $\Sigma \vdash \phi$ and $\Sigma \vdash \lnot \psi.$

$\Sigma$ is a set of sentences, the set $ L$ consists of all axioms of the forms: A1) $ \ \phi \rightarrow (\psi \rightarrow \phi)$ A2) $\ (\phi \rightarrow (\psi \rightarrow \theta)) \rightarrow (...
1
vote
2answers
103 views

(P → Q) v (Q → R), Fitch-style proof

I'm trying to construct a Fitch-style proof for $(P \to Q) \lor (Q \to R)$ using reductio ad absurdum and the introduction and elimination rules for conjunction, disjunction, and implication. I'm not ...