# Questions tagged [formal-proofs]

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

527 questions
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 = {∅,{∅}} ...
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 ...
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 ...
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,... 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 ... 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: ... 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 ... 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 ... 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∃... 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 ... 1answer 69 views ### Show that the proof rule is not sound and proof question I'm asked to show that the proof rule $$\dfrac{\varphi \to \psi}{\lnot \varphi \to \lnot \psi}$$ is not sound. To show this would I just make the truth tables for the ... 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 ... 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 ... 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? 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"? 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 ... 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 ... 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 ... 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 \\ [\... 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 ... 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 ... 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) 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 ... 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) \... 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 ... 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... 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 ... 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 ... 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 ... 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 ... 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 ... 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 ... 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 ... 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 ... 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 ... 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 ... 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 ... 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: \... 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 ... 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 ... 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'... 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. 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 ... 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'... 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 ... 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 ... 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 ... 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 ... 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 (...
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 ...