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
0
votes
1answer
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 ...
1
vote
1answer
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 ...
3
votes
1answer
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 ...
2
votes
2answers
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 ...
4
votes
2answers
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 ...
0
votes
1answer
210 views

How to prove (¬((p→q) → ¬(q→r))) → (p→r) using Lukasiewicz's axioms and MP?

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 ...
1
vote
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^...
1
vote
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 ...
1
vote
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 ...
2
votes
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 ...
1
vote
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 ...
2
votes
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))$$ ...
3
votes
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 ...
2
votes
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 ...
4
votes
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 ...
4
votes
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 ...
2
votes
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 ...
0
votes
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}\...
4
votes
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 ...
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
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 ...
0
votes
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 ...
1
vote
1answer
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 ...
1
vote
1answer
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
2
votes
2answers
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 ...
3
votes
3answers
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
5
votes
3answers
2k views

Natural Deduction Tautology

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$ ...
2
votes
4answers
159 views

Hilbert System with propositional logic $p \rightarrow q,\neg q \vdash \neg p$

This is my set of axiom $A \rightarrow (B\rightarrow A)$ $(A\rightarrow(B\rightarrow C))\rightarrow ((A\rightarrow B) \rightarrow (A \rightarrow C))$ $(\neg A \rightarrow B)\rightarrow ((\neg A \...
4
votes
4answers
190 views

Find propositional formulas $\phi$ and $\psi$ such that $(\phi \rightarrow (\psi \rightarrow (¬\psi)))$ is a theorem of L.

Find propositional formulas $\phi$ and $\psi$ such that $(\phi \rightarrow (\psi \rightarrow (¬\psi)))$ is a theorem of L. So every axiom is a theorem of L so I thought there would be some way to ...
4
votes
5answers
6k views

Prove that $\vdash p \lor \lnot p$ is true using natural deduction

I'm trying to prove that $p \lor \lnot p$ is true using natural deduction. I want to do this without using any premises. As it's done in a second using a truth table and because it is so intuitive, I ...
4
votes
3answers
2k views

Proof of transitivity in Hilbert Style

We can use the following axioms: $$\begin{align} &A\to(B\to A)&\tag{A1}\\ &[A\to(B\to C)]\to[(A\to B)\to(A\to C)]&\tag{A2}\\ &(\lnot A\to\lnot B)\to(B\to A)&\tag{A3} \end{align}...