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
823 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 ...
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}...
5
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 ...
3
votes
4answers
1k views

natural deduction: introduction of universal quantifier and elimination of existential quantifier explained

Currently, I am dealing with the calculus of natural deduction by Gentzen. This calculus gives us rules to manipulate so-called sequents. Definition. If $\phi_1,\dots, \phi_n,\phi$ are formulas, then ...
8
votes
4answers
410 views

Calculus of Natural Deduction That Works for Empty Structures

Currently, I am dealing with the calculus of natural deduction by Gentzen. This calculus gives us rules to manipulate so-called sequents. Definition. If $\Gamma$ is a set of formulas and $\phi$ a ...
1
vote
1answer
1k views

help with some Hilbert style proofs in a propositional logic axiom system.

I'm very new to classical propositional logic, and my lecturer is using a system with the following axioms: A1. X→(Y→X) A2. (X→(Y→Z))→((X→Y)→(X→Z)) A3. (¬Y→¬X)→(X→Y) Use uniform substitution and ...
9
votes
1answer
285 views

What is “magic” about the combination of addition and multiplication in formal arithmetic?

Goedel's incompleteness tells us that any system containing Robinson arithmetic is incomplete. OTOH, Presburger Arithmetic, which contains only the successor and addition, is complete. I'm pretty ...
5
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 ...
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$ ...
7
votes
4answers
317 views

Show that $(p \to q) \lor (q \to p)$ is a tautology

I tried to prove that $(p \to q) \lor (q \to p)$ is a tautology. I used $p$ and $¬q$ as conditions. (Premises 1 and 5) I managed to get to a solution, but I'm not sure if it's right. Can you please ...
2
votes
1answer
260 views

proving $ (A \rightarrow B \vee C )\rightarrow((A\rightarrow B) \vee (A\rightarrow C))$

I'm looking for a way to prow $ (A \rightarrow B \vee C )\rightarrow((A\rightarrow B) \vee (A\rightarrow C))$ from the following axioms and rules $$\vdash A \rightarrow A$$ $$\vdash A \wedge B \...
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 ...
4
votes
1answer
540 views

Fitch proof for $(p \implies (q \implies r)) \implies ((p \implies q) \implies (p \implies r))$ with no premises

I'm having trouble solving this problem using the Fitch system. As I understand Fitch, if the goal has the form $(φ \implies ψ)$, it is often good to assume $φ$ and prove $ψ$ and then use Implication ...
3
votes
1answer
561 views

Fitch System For logic proofs

Does anyone know the Fitch program/ system used for logical proofs ? I am stuck with using fitch to construct a proof of¬(¬A∨¬B) from the premises A and B ... This is how it looks like in ...
2
votes
2answers
2k views

Proof of a theorem in Hilbert's system

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 ...
2
votes
2answers
1k views

Natural deduction proof / Formal proof : Complicated conclusion with no premise

Find a formal proof for the following: $\vdash [(\neg p \land r)\rightarrow (q \lor s )]\longrightarrow[(r\rightarrow p)\lor(\neg s \rightarrow q)]$ As you can see. No premise to use. We have to use ...
3
votes
2answers
220 views

How to prove this sequent using natural deduction?

How do I prove $$S\rightarrow \exists xP(x) \vdash \exists x(S\rightarrow P(x))$$ using natural deduction? Just an alignment of which axioms or rules that one could use would be much appreciated.
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)) -> ( ...
0
votes
1answer
58 views

Stuck on formal proofs. Not sure how to continue

I'm stuck on what how to continue. I know I'm missing a few steps but this is what I have so far. Thank you in advance! ¬Cube(b) → Small(b) Small(c) → (Small(d) ∨ Small(e)) Small(d) → ¬Small(c) Cube(...
30
votes
2answers
2k views

When writing proofs, is logical notation a crutch?

I'm near the end of Velleman's How to Prove It, self-studying and learning a lot about proofs. This book teaches you how to express ideas rigorously in logic notation, prove the theorem logically, and ...
4
votes
3answers
3k views

Use Fitch system to proof ((p ⇒ q) ⇒ p) ⇒ p without any premise. ONLY FOR FITCH SYSTEM.

I know here has few similar questions, but I cannot figure out with those answer. Since for Fitch system, I can only use And Intro, And Elim, Or Inro, Or Elim, Neg Intro, Neg Elim, Impl Intro, Impl ...
3
votes
1answer
83 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 ...
2
votes
1answer
372 views

$A⇒(B \lor C)$ and $[(A \Rightarrow B) \lor (A \Rightarrow C)]$

[(A⇒ B∨C)] ⇒ [A⇒(¬B⇒C)] ⇒[(A⇒¬B)⇒(A⇒C)] ⇒ [¬(A⇒¬B)∨(A⇒C)]⇒[(A∧B)∨(A⇒C)] [(A⇒B)∨(A⇒C)] is equivalent to A⇒(B∨C). Can I prove [(A∧B)∨(A⇒C)] ⇒ [A⇒(B V C)]? or is there problem in the proof above ...
3
votes
1answer
84 views

Is there a proof of $\lnot \forall x, P(x) \iff \exists x, \lnot P(x)$

I am interested in how one would formally prove: $\lnot \forall x, P(x) \iff \exists x, \lnot P(x)$ I realize that it's basically saying that: $\lnot(P(x_0) \land P(x_1) \land ... \land P(x_n)) \...
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
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
1k views

Prove ⊢(a→b)→(¬b→¬a) in HPC proof system

As stated in the title, I am asked to give a proof that: ⊢(a→b)→(¬b→¬a) Using a system with the Modus Ponens rule, and the following axioms: A1: a→(b→a) A2: (a→(b→c))→((a→b)→(a→c)) A3: (¬b→¬a)→(a→b)...
0
votes
1answer
216 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 ...
0
votes
1answer
50 views

Can the Negation of a Conditional Implying the First Atomic Proposition Get Proven in Around 50 Steps?

The following uses Polish notation with the following definition for meaningful expressions. All lower case letters are meaningful expressions. If $\alpha$ is a meaningful expression, then so is N$\...
6
votes
2answers
405 views

Propositional Logic Help: $(\neg p \wedge (p \vee q)) \rightarrow q $ is a tautology

I need to prove that $(\neg p \wedge (p \vee q)) \rightarrow q $ is a tautology using Laws of Logic (not truth tables). This is what I tried: $\equiv (( \neg p \wedge p) \vee (\neg p \wedge q)) \...
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
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))$$ ...
2
votes
1answer
133 views

Formally prove that these two premises are contradictory

Clever(a) ∧ ¬Happy(a) ∀x (Clever(x) → Happy(x)) So far I have something like this [EDIT] Thanks to Bram28 I got the correct proof.
2
votes
2answers
134 views

Formally proving $p\wedge q \rightarrow p$

I want to write a full prove for $p\wedge q \rightarrow p$ without using deduction, using only ${\neg, \rightarrow}$ connectives. I use the standard axiomatic system: $\alpha\rightarrow(\beta\...
2
votes
2answers
81 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$ ...
2
votes
1answer
64 views

Show $\neg(\forall x\phi)\vdash \exists x(\neg \phi)$ using an ND-derivation

I'm trying to show that $\neg(\forall x\phi)\vdash \exists x(\neg \phi)$ through a natural deduction (ND) derivation. I'm kind of stuck, because I don't see how I can find some $t$ such that we have $...
2
votes
2answers
653 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 ...
2
votes
4answers
160 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 \...
1
vote
1answer
34 views

$\vdash\phi \land \diamond\psi \to \diamond(\psi\land\diamond\phi)$ in KB

I've been trying to prove $\vdash\phi \land \diamond\psi \to \diamond(\psi\land\diamond \phi)$ in natural deduction where it's allowed to use $\phi\to \square \diamond \phi$ and/or $\diamond\square\...
1
vote
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 (...
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
2answers
123 views

(P → Q) v (Q → R), Fitch-style proof

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 ...
1
vote
2answers
304 views

How to show that $[(p \rightarrow q) \rightarrow r] \Rightarrow [p \rightarrow (q \rightarrow r)]$

To show that $[(p \rightarrow q) \rightarrow r] \Rightarrow [p \rightarrow (q \rightarrow r)]$ without using a truth table. That is, using logical laws.
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
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
1answer
236 views

Hilbert system (with inference rule of modus ponens), show $\vdash \exists x (Px \rightarrow \forall x Px)$

We're in first-order logic, using the Hilbert system (with inference rule of modus ponens), and the problem is to show $\vdash \exists x (Px \rightarrow \forall x Px)$. We just learned about this ...
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
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
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: ...
0
votes
4answers
316 views

In formal verification, what is the formal specification, what formally means there?

I have been reading a lot about formal verification of software and apparantly you need to formalize the behaviour of the program to create an equivalent model of it (if I get it right). But nowhere ...