# Questions tagged [formal-proofs]

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

54 questions
Filter by
Sorted by
Tagged with
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 ...
3answers
2k views

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 ...
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 ...
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 ...
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 ...
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 ...
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.
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)) -> ( ...
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(...
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 ...
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 ...
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 ...
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 ...
1answer
84 views

2answers
405 views

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$ ...
1answer
64 views

1answer
34 views

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 ...
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 ...
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.
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 ...
1answer
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 \... 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 ... 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 ... 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 ... 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: ...
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 ...