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
1
vote
3answers
824 views

Prove $( \lnot C \implies \lnot B) \implies (B \implies C)$ without the Deduction Theorem

The issue is Exercise 1.47 (d) in Elliot Mendelson's "Mathematical Logic". The exercise is to prove $(\lnot C\implies\lnot B)\implies(B\implies C)$ by using the three axioms $(A1,A2,A3)$ without using ...
1
vote
2answers
137 views

Hilbert's style proof (FO logic)

I am stuck with this question to check whether the following formulas are valid and if they are valid, then derive them using Hilbert's axiom schema and Modes Ponens for First Order Logic. \begin{...
1
vote
1answer
85 views

Proofs of Sets and Subsets

I have these proof problems that I need some help on, any direction would be great. Thanks Let A, B, and C be subsets of some universal set U (a) Prove the following: IF $A \cap B$ $\subseteq$ C, ...
1
vote
1answer
246 views

Formal Proofs: $\vdash Py \land \exists x Qx \rightarrow \exists x (Py \land Qx)$

First order logic, Hilbert's System. For those familiar with Enderton's Introduction to Mathematical Logic, I am allowed the same axioms. For those unfamiliar, I can use these axioms: ...
1
vote
1answer
191 views

Modus ponens proof

I'm trying to prove that $\neg\bullet\varphi$ in system $L(\neg, \to, \bullet)$, $\bullet \varphi \approx (\varphi \to \varphi)$ Axiomas are the followind: A1) $\neg\neg\bullet\bullet\varphi$ A2) ...
1
vote
1answer
882 views

Stuck on First-Order Logic

I'm taking a first-order logic class and I keep finding myself stuck on proofs that ask for disjunction elimination and then supply additional premises with conjunctions. How can I eliminate negations ...
1
vote
1answer
189 views

Consistent Set of Sentences is Consistent in Expanded Language

Suppose that we have a set $\Phi$ of sentences over a first-order language $\mathcal{L}$ and that $\Phi$ is consistent. Suppose we have another first-order language $\mathcal{L}'$ such that $\mathcal{...
1
vote
2answers
61 views

Deduction of $\forall x(\neg p(x)\rightarrow q(x)), \forall z(p(z)\rightarrow r(z))\vdash \forall z(\neg r(z) \rightarrow\exists yq(y))$

I trying to study for my final exam and I can't figure out how to solve this: $\forall x(\neg p(x)\rightarrow q(x)), \forall z(p(z)\rightarrow r(z))\vdash \forall z(\neg r(z) \rightarrow\exists yq(y))...
1
vote
2answers
55 views

Prove distribution of or over implies knowing the implication is always true

I was given a task to construct a Hilbert-style proof for the following: $A → B ⊢ C ∨ A → C ∨ B$ I figured I could use the axiom $A→B≡A∨B≡B$, but this leads me nowhere since I don't think I can use ...
1
vote
1answer
28 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 ...
1
vote
1answer
93 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 ...
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
vote
2answers
69 views

Complement function: how to prove surjective?

Given some set A and a complement function C(K) = A - K from the power set of A onto the power set of A, how can I formally prove that it is surjective? I think I get it, but can't get it on paper. (...
1
vote
1answer
241 views

Inductive proof using Fitch software

I am trying to prove the integer square root theorem $\forall x: \mathbb{N}, \exists y : \mathbb{N}((y^2 \leq x) \land (x < (y+1)^2))$ for $\lfloor \sqrt{x} \rfloor$. In words: for any natural ...
1
vote
1answer
76 views

Fitch Style Proof

¬(A↔B) conclusion ¬A↔B I'm having trouble with the second part of this proof. I think I managed the first part: 1 |¬(A↔B)$\,$ $\,$ A prem. 2 ||B $\,$ $\,$ A →intro 3 |||A $\,$ $\,$ ...
1
vote
2answers
148 views

Inference Proof for Biconditional

I'm asked to prove $(p\rightarrow (q \vee r)) \leftrightarrow ((p \wedge \neg q)\rightarrow r)$ using inference rules and I'm not quite sure how to do it. This is what I have so far. $1 [(p \wedge \...
1
vote
1answer
305 views

Proving either or statements (in group theory)

Suppose we need to prove statement of the form either $P$ or $Q$. Is it sufficient to prove $P$ whenever not $Q$. Or do we need to show $Q$ whenever not $P$ holds as well? I was trying to prove this: ...
1
vote
2answers
38 views

Limit of $f(x) = x \bmod k$

I'm trying to prove that a function $f(x)$ tends to infinity when $x$ rises. Clearly, I used limit to do so. The problem is, $f(x) = x\ mod\ k$, in which mod is the division's residue of $x$ by $k$. ...
1
vote
2answers
1k views

Subsequences of a convergent sequence converge to the same limit as the original sequence

Here is my proof: Proof. Let $(a_j) \to L$ be the original sequence and $({a}_{n_{j}})$ be a subsequence of $(a_j)$. We have to then show that $ ({a}_{n_{j}}) \to L$. Since $(a_j) \to L$, we have ...
1
vote
1answer
419 views

Lindenbaum's Lemma in Propositional Logic

I've recently learnt Lindenbaum's Lemma in propositional logic: Suppose $\Gamma$ is a consistent set of $L$-formulas. Then there exists a consistent set $\Gamma'$ of $L$-formulas containing $\Gamma$, ...
1
vote
2answers
312 views

How to prove ~~P from P in the Hilbert Axiomatic System?

Can someone provide me with hints for, or a rough sketch of, a proof of ~~P from P in the Hilbert system? I had very little trouble proving the reverse, that P is provable from ~~P, but seem to be ...
1
vote
2answers
94 views

Prove P from B ∨ P when we have proven ¬B

I have the following proof so far: In step 9 I'm not sure how to prove P from the steps I have before. I thought that I could use ∨ Elim but I don't think I can now.
1
vote
2answers
173 views

Is simplification from 'or' ($\lor$) valid?

The question in my text is : Identify the error or errors in this argument that supposedly shows that if $\forall x (P (x ) \lor Q(x ))$ is true then $\forall x P(x) \lor \forall x Q(x)$ is true. \...
1
vote
1answer
105 views

Proving that this statement is a theorem of our proof system

So I need to produce a proof tree of the below statement using the introduction and elimination rules. $$ \begin{array}{c} x \in a &q \\ \hline \exists x \colon a \bullet q \\ \hline ((\exists ...
1
vote
1answer
49 views

Let $Y = \{y_n\}$ be defined inductively by $y_1=1$ , $y_{n+1} = \frac 14\left(2y_n +3\right)$. Show that $\lim_{n\to \infty}y_n=\frac 32$

Let $Y = \{y_n\}$ be defined inductively by $y_1=1$ , $y_{n+1} = \frac 14\left(2y_n +3\right)$. Show that $$\lim_{n\to \infty}y_n=\frac 32$$ This is a problem from Bartle's Introduction to Real ...
1
vote
1answer
53 views

Attempt to prove the $∀d∀x∀y (d | x ∧ d | y ∧ x ≤ y → d | y- x)$ property of the “divides” relation for non-negative integers

I am attempting to prove the $∀d∀x∀y (d | x ∧ d | y ∧ x ≤ y → d | y- x)$ property of the “divides” relation for non-negative integers, but am having a little difficulty and am hoping someone can help. ...
1
vote
1answer
107 views

peano arithmetic - PA sentences

In using the non-logical axiom sentences of PA, I was trying a practice problem to get the hang of using the PA sentences: $((S0 * S0) = S0)$ And so my approach was the following: $\forall x_1((x_1 ...
1
vote
1answer
35 views

Proof of the equation of a surface

In Ian N. Sneddon's Elements of Partial Differential Equations, there is the following text: If the rectangular Cartesian co-ordinates of any point $P(x,y,z)$ in space satisfies the relation $$f(x,...
1
vote
3answers
490 views

(¬A ∨ B) is equivalent to B?

Is there any proof that states (¬A ∨ B) is equivalent to B? There was an example in my text book that had a step I didn't understand. It stated (¬A ∨ B) ∧ A → B is equivalent to B ∧ A → B. I don't see ...
1
vote
3answers
2k views

Formal Proof for not (p or not q) implies not p and q

I've been trying to give a formal proof for $$ \lnot \left(p \lor \lnot q\right) \rightarrow \left(\lnot p \land q \right) $$ in deductive system N (natural deduction system) and got stuck. I've ...
1
vote
2answers
737 views

Order the following propositions from the strongest to the weakest: A, B, A → B?

So I was recently given a number of questions in class but this one in particular, despite scouring my notes and the internet, has escaped me. "Given formal statements P and Q, P is said to be ...
1
vote
1answer
476 views

Formal deductions on Hilbert system

I have proved {(α→β),(β →γ)} ⊢ (α→γ) } using formal deductions using Modus Ponens and the three axiom of H2 : A1: A -> (B-> A) A2: (A-> (B->C)) -> ((A-> B) -> ( A -> C)) A3: (( ¬ A) -> ( ¬B)) -> ( ...
1
vote
4answers
76 views

Prove: $\forall n\in\mathbb{N}(3|n^2\Rightarrow 3|n)$

guys. I just started to learn infinitesimal mathematics 1 (I think it's analagous to calculus A - the professor said that it's the most theoretical course on calculus offered in the university (The ...
1
vote
1answer
236 views

Correct notation for presenting solutions to equations

Let's say I have a cubic equation $(x-a)(x+b)(x-c) = 0$, and I want to represent the solutions to this equation, what is the formal/conventional way that one would arrive and state the solution to the ...
1
vote
2answers
83 views

Trying to check whether a formal proof is correct

Am having a little difficulty trying to formally prove a formula. I'm new to this so just trying to have a go and see where I get to. The formula I have is copied in below; ...
1
vote
2answers
119 views

Formal proof for $q \land \neg q \vdash r \land \neg r$

Having some issue with some logic. The question is to formally prove; $$q \land \neg q \vdash r \land \neg r$$ I've never done this before so would appreciate some help with it. No idea really where ...
1
vote
1answer
264 views

Recursive definitions in formal logic

A binary tree $T$ is either A single vertex, or A graph formed by taking two binary trees, adding a vertex, and adding an edge directed from the new vertex to the root of each binary tree. Suppose ...
1
vote
1answer
865 views

Di-graphs handshaking lemma proof

I am starting to learn about graph theory and in the study of the graph theory proofs, I have inevitably come across the handshake lemma for undirected graphs which is a quite straight forward proof, ...
1
vote
2answers
97 views

Derivation of ∀x (A(x) → B(x)) → (∀x A(x) → ∀x B(x)) in Hilbert style system

While it's quite easy to give a derivation of $$\forall x ~ \bigg(A(x) \implies B(x)\bigg) \implies \bigg(\forall x~ A(x) \implies \forall x~ B(x)\bigg)$$ in a system that contains the rule of ...
1
vote
1answer
629 views

Proving that $P(X=Y) = 0$ for any two continuous random variables

I have the following question to prepare for a lecture at Uni but I've been stuck on this for a long time: Question: Let $Z$ and $V$ be independent with distribution $U[0,1]$. Show that $P(...
1
vote
3answers
5k views

How to prove a logical implication?

Question: Using the Laws of Logic and Rules of Inference, prove that $$(\neg(\neg p \lor q) \lor r) \Rightarrow (\neg p \lor (\neg q \lor r)).$$ I just don't know how to apply the Rules of ...
1
vote
1answer
72 views

Context-free language or not

It is language: $L = \left\lbrace a^ib^jc^kd^l \mid i+k < j+l+3 \right\rbrace$ Is it context-free or not? I have two versions: 1)Pumping lemma(refute): get a word $uvxyz = aabcd$ if $i=2$ we get ...
1
vote
2answers
516 views

Prove that the following argument is valid

I'm asked to show that the following argument is valid: P1) $[E \lor (L \lor M)] \land (E \leftrightarrow F)$ P2) $L \rightarrow D$ P3) $D \rightarrow \neg L$ C) $E \lor M$ Here is my work (so ...
1
vote
1answer
77 views

Iterating proof step

Many books proves theorems by performing one proof step and using this step as a scheme they say by repeating this step $l$ times we prove that... I wonder whether there is some formal meta-theorem ...
1
vote
3answers
288 views

If $ A \in B $ and $ B \subseteq C $ then $ A \in C $. vs. If $ A \in B $ and $ B \subseteq C $ then $ A \subseteq C $.

I am trying to decipher the difference between the following two statements: If $ A \in B $ and $ B \subseteq C $ then $ A \in C $. vs. If $ A \in B $ and $ B \subseteq C $ then $ A \subseteq ...
1
vote
1answer
891 views

Modus tollens - Negations on the implication

This is likely a basic question however based on my textbook definition of Modus tollens it looks like this: $$\neg q$$ $$\frac{(p \implies q)}{\neg p}$$ I however have something that looks like ...
1
vote
1answer
434 views

Linearly Independent Set Proof

If S = {${v_1,...,v_n}$} is a set of vectors in $R^n$ such that no $v_i$ is a scalar multiple of $v_j$ with $i≠j$, then {${v_1,...,v_n}$} is linearly independent. So far, I've used the ...
1
vote
1answer
592 views

Predicate natural deduction: Prove (∀x R(x,x)) => ∀x∃y R(x,y)

Prove that if the relation R is reflexive, it is also serial: $ \forall x \space R(x,x) \vdash \forall x \exists y \space R(x,y)$ I've tried this so far but can't think of anything further: $1. \...
1
vote
1answer
173 views

Formal Proofs: $\vdash \exists x (Py \land Qx) \rightarrow Py \land \exists x Qx$

I wish to show $\vdash \exists x (Py \land Qx) \rightarrow Py \land \exists x Qx$ using the Hilbert System in First-Order Logic with the following axioms: Tautologies $\forall x \alpha \...
1
vote
2answers
133 views

Help with semi-formal logic

How do I write semi-formally 'there are only 2 objects in the universe'? My hypothesis is: ∃x∃y(x≠y) Any ideas?