# Questions tagged [formal-proofs]

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

537 questions
Filter by
Sorted by
Tagged with
199 views

### Can't understand this set theory proof.

I read the proof of a 'set theory' equation from a website called Meritnation. But I can't understand the proof after 30 minutes of trying and even find some mistakes in it. This is the proof(I have ...
90 views

### Determining the correctness of a formal proof

Is the following formal proof, proving $\forall A\forall B \forall C[A+C=B+C\Longrightarrow A=B]$ correct?? Proof 1) $a+c=b+c$.............................................................Hypothesis ...
2k views

### Proving that two expressions are equivalent

So, I'm working through some proof exercises, and one of the questions is about the following regular expression: (a|b)* = a*(a|b)* if they are equivalent, prove ...
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 ...
2k views

### equivalence between formal and informal proof

I'm reading Cohen's book on the independence of the continuum hypothesis, and I see that all the proofs that he gives when he's defining the basic notions of set theory (ordinals, cardinals, ...
87 views

### Prove formally that $\frac {n^2 + 2}{3n^3 - 5n}\to 0$ as $n \to \infty$.

I'm reviewing some Sequences notes from a Mathematics Analysis course I'm taking. I'm finding the beginning of the formal proof below confusing. Some clarity on the following questions would be much ...
287 views

171 views

### Should $x$ be not free in $\beta$ to prove $\vdash [ \forall x(\beta\rightarrow \alpha)\rightarrow (\exists x\beta\rightarrow \alpha)]$?

Should $x$ be not free in $\beta$ to prove $\vdash [ \forall x(\beta\rightarrow \alpha)\rightarrow (\exists x\beta\rightarrow \alpha)]$? In "Mathematical Introduction to Logic, Enderton" This is an ...
107 views

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 ...
592 views

357 views

### Status of declarative proof languages in proof assistants

I'm interested in formalising mathematics and logics in a proof assistant, both to get to know a proof assistant and to make an archive of proofs for myself (nothing too fancy, mainly first order ...
173 views

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 \... 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{... 4answers 1k views ### Motivation for natural deduction I've been learning natural deduction recently. I've seen many problems and am starting to be able to solve problems more easily. For some reason I feel the need to ask what high school math students ... 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$... 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, ... 1answer 245 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: ... 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? 1answer 78 views ### Prove a predicate formula in the constructive logic Using the constructive logic (the axiom$A\lor\lnot A$cannot be used), using quantifier axioms and Modus Ponens, and Generalization, prove the following:$\exists x(B(x) \to C(x)) \to (\forall xB(x) ...
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 ...