# Questions tagged [formal-proofs]

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

531 questions
Filter by
Sorted by
Tagged with
215 views

### Modus ponens proof in system L(¬,→,∙)

I'm trying to prove $\neg\neg\bullet\varphi$ in system $L(\neg, \to, \bullet)$, where $\bullet$ is constant truth, i.e. $\bullet \varphi \approx (\varphi \to \varphi)$ Using modus ponens with ...
20k views

### Proving sequence convergence

I'm pretty confused...I understand bits and pieces but not how it all comes together...I would appreciate some help, either a written out example (you can make up one) and/or comments on how to fix my ...
129 views

### Proof that for any $16$ digit number there is at least one sequence of $1$ or more digits which its product is a perfect square

I came across this problem where one is asked to proof that, for any $16$ digit number there is at least a sequence of $1$ or more digits which its product is a perfect square. For example, in the ...
158 views

### Deduce $\forall x P(x) \vdash \exists xP(x)$

Well it's a little awkward but how can I show this in a natural deduction proof? $\forall x P(x) \vdash \exists xP(x)$ I think one has too proof that with a proof by contradiction rule but since I ...
401 views

### Deducing $(\lnot B) \to A$ from $\lnot A \to B$ using Hilbert deductive system

As the title says, I've been trying to prove this: $(\lnot A \to B) \vdash (\lnot B) \to A)$ but unfortunately keep winding up with crazy long steps and then I have no idea where to go. The only ...
210 views

I need a proof for (¬((p→q) → ¬(q→r))) → (p→r) (which is equivalent to (p→q)→((q→r)→(p→r))) using the three axioms and MP: Axiom 1: $A \to (B \to A)$. Axiom 2: $(A \to (B \to C)) \to ((A \to B) \to ... 1answer 176 views ### Suppose$A$is an invertible matrix. Prove that$det(A^{-2}) = 1/(det(A))^2$Suppose$A$is an invertible matrix. Prove that$det(A^{-2}) = 1/(det(A))^2$I want to just say $$det(A^{-2}) = 1/(det(A))^2$$ $$\Rightarrow (det(A^2))^{-1} = 1/(det(A))^2$$ $$\Rightarrow 1/det(A^... 2answers 4k views ### prove that if a square matrix A is invertible then AA^T is invertible. prove that if a square matrix A is invertible then AA^T is invertible. and also prove the opposite, that if AA^T is invertible, then A is invertible. i wrote that det(A) = det(A^T) and ... 3answers 1k views ### Show that if A is any square matrix such that A^n = 0 for some positive intiger n, then A is not invertible. (answer check) Show that if A is any square matrix such that A^n = 0 for some positive integer n, then A is not invertible. I'm not sure if my proof is good enough, or enough "work" as my teacher put it ... 3answers 495 views ### natural deduction proof Need help with the steps for natural deduction: P1. (A \rightarrow B) \rightarrow (C \rightarrow A) P2. A \wedge (C \leftrightarrow B) P3. (A \lor C) \to (A \to B) \therefore ... 1answer 878 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 ... 1answer 240 views ### How to show \vdash (\neg\neg p \rightarrow p). Given these axioms: where \phi, \psi, \theta are formulas$$ 1.:(\psi \rightarrow (\theta \rightarrow \psi)) 2.: ((\neg \psi \rightarrow \neg \theta) \rightarrow (\theta \rightarrow \psi))$$... 4answers 219 views ### How to prove C from A \leftrightarrow (B \leftrightarrow C) and A \leftrightarrow B? How does one prove C from the premises: A \leftrightarrow (B \leftrightarrow C) and A \leftrightarrow B ? I've tried to prove C by contradiction, using a sub-proof which presumes \neg ... 1answer 192 views ### Natural deduction proof - I don't' understand the question I am supposed to give a natural deduction proof of$$(P_1∨P_2), \neg P_1 ⊢ P_2$$My assumption is (P_1∨P_2) and I am going to derive P_2 from \neg P_1 or I am wrong? EDIT: Or I am going to ... 2answers 3k views ### How to prove that P \rightarrow Q is equivalent with \neg P \lor Q ? In my book about Logic, which is called 'Language, Proof and Logic', by the way, there is explained that the conditional P \rightarrow Q is equivalent with \neg P \lor Q. There is another ... 1answer 1k views ### How to prove math theorems in formal logic or at least in the style of natural deduction? I have become rather interested lately in proofs in mathematics, and I discovered at first to my surprise that they are written in paragraph form using natural language. Although this seemed out of ... 2answers 1k views ### Subproof in Fitch style system When using a Fitch style system for proving various theorems, why are we allowed to assume anything we want in the assumption of a subproof in order to derive some desired result? It seems like there ... 5answers 894 views ### Injective function proof involving floor function Let f : \Bbb{Z} \to \Bbb{Z} and g : \Bbb{Z} \to \Bbb{Z} be functions defined by f(x)=3x+1 and g(x)=\lfloor\frac{x}{2}\rfloor. Is g(f(x)) one-to-one? So, g(f(x)) = \lfloor\frac{3x+1}{2}\... 1answer 115 views ### Why is the assumption needed in this conditional introduction? In the first derivation detailed here, why must we include a subderivation with P as an assumption? We can derive Q (4) from S \land Q (2) without the help of P (3); and then since we have ... 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{... 1answer 274 views ### Can universal instantiation be used more than once? I'm trying to follow a proof in a logic text and it seems like the author used universal instantiation twice to reach the needed result. I was under the impression that you could only use UI one time ... 1answer 103 views ### proving{\neg(\forall x)\alpha \rightarrow \alpha}\models$$(\forall x)\alpha$

prove {$\neg(\forall x)\alpha \rightarrow \alpha$}$\vdash\space(\forall x)\alpha$ Im not sure what is the convention, so to be clear I am talking about proving the formula from the seven axiom ...
64 views

### Is there a proof of this statement about deductions?

Is there a proof of the following statement: you cannot prove with natural deduction theorems that are unprovable in a Hilbert-style proof system? The logic in discussion is either propositional logic ...
775 views

### Fitch-Style Proof Help

I'm having some trouble solving a Fitch Proof, Here's how far I've gotten. Any Help is appreciated. Thank You
652 views

### Fitch style proof of $(\neg B \to \neg A) \leftrightarrow (A \to B)$

I have been stuck on this proof for a while. Here's where I'm at: Goal $(\neg B \to \neg A) \leftrightarrow (A \to B)$ l 1. $A \to B$ ll 2. $\neg B$ lll 3. $A$ lll 4. $B$ Elim 1,3 ...
1k views

### Fitch-Style Proof [closed]

Hi I'm having trouble solving a Fitch Style Proof and I was hoping someone would be able to help me. Premises: $A \land (B \lor C)$ $B \to D$ $C \to E$ Goal: $\neg E \to D$ Thank You
I'm trying to prove the following tautologies: \begin{align} & ⊢ (A \to (B \to A)) \\ & ⊢ ((A \to B) \to A) \to A \end{align} For the first one, what I did was: $A$ assumption $B$ ...